模式匹配案例中的统一

Posted 2023-05-08

【中文标题】模式匹配案例中的统一

【英文标题】：Unification in pattern matching case

【发布时间】：2020-09-19 11:35:31

【问题描述】：

我正在尝试编写一个类型为 forall n, option (n = 1) 的函数。

我选择option 作为reflect 的替代方案，避免给出否定情况的证明。所以Some扮​​演角色ReflectT并持有证明，而None不持有否定证明。

Definition is_1 n: bool:=
  match n with
    1 => true |
    _ => false
  end.

Lemma is_1_complete : forall n, is_1 n = true -> n = 1.
intros.
destruct n. simpl in H. discriminate.
destruct n. reflexivity.
simpl in H. discriminate.
Qed.

Lemma a_nat_is_1_or_not: forall n, option (n = 1).
intros.
cut (is_1 n = true -> n = 1).
- 
intros.
destruct n. exact None.
destruct n. simpl in H. exact (Some (H (eq_refl))).
exact None.
-
exact (is_1_complete n).
Qed.

我已经完成了战术。 a_nat_is_1_or_not 就是证明。而且我认为我可以直接写定义，所以我尝试了。

Definition a_nat_is_1_or_not' n: option (n = 1) :=
  match is_1 n with
     true => Some (is_1_complete n eq_refl)
     | false => None
  end.

但 Coq 说

Error:
In environment
n : nat
The term "eq_refl" has type "is_1 n = is_1 n"
while it is expected to have type "is_1 n = true" (cannot unify "is_1 n" and
"true").

在true自身模式匹配的情况下，is_1 n似乎无法统一到true。

所以我尝试了一个更简单的例子。

Definition every_true_is_I x: x = I :=
  match x with
     I => eq_refl
  end.

有效。

a_nat_is_1_or_not' 和 every_truer_is_I 有什么区别？ 我错过了什么吗？我可以做些什么来编写forall n, is_1 n = true -> n = 1. 的有效定义？

【问题讨论】：

正如@Guillaume 所说，您的问题是您正在丢失信息，或者您可以使用 Ltac 解决，您只需要使用做同样事情的记住策略。定义 a_nat_is_1_or_not' n ：选项 (n = 1)。记住（is_1n）。破坏 b.精确（一些（@is_1_complete n (eq_sym Heqb)））。确切无。已定义。

如果不需要负数，可以考虑使用sigma类型。

【参考方案1】：

不同之处在于，在a_nat_is_1_or_not' 中，您依赖于类型为is_1 n = true -> _ 的外部术语。如果你想让a_nat_is_1_or_not' 看起来像every_true_is_I，你必须确保所有出现的is_1 n 都被模式匹配所覆盖：

Definition a_nat_is_1_or_not' n: option (n = 1) :=
  match is_1 n as b return ((b = true -> _) -> _) with
  | true => fun H => Some (H eq_refl)
  | false => fun _ => None
  end (is_1_complete n).

注意is_1_complete 是如何在模式匹配之外被实例化的，以便处理它的出现is_1 n（重命名为b）。

还有另一种方法可以做到这一点，也许更惯用一些。无需概括整个上下文，您只需保留足够的信息来填补所有漏洞：

Definition a_nat_is_1_or_not' n: option (n = 1) :=
  match is_1 n as b return (is_1 n = b -> _) with
  | true => fun H => Some (is_1_complete n H)
  | false => fun _ => None
  end eq_refl.

但想法是一样的。通过在模式匹配之外实例化eq_refl，您在匹配is_1 n 时不会丢失任何信息。