如何从 Some 的相等性证明相等性

Question

我想在 Coq 中证明两个 nat 数相等：

a, b : nat
Heq : Some a = Some b
============================
a = b

Answer 1

当你遇到这样的等式时，通常，最快的方法是使用 inversion 策略，它或多或少会利用构造函数的单射性。

Lemma foo :
  forall (a b : nat),
    Some a = Some b ->
    a = b.
Proof.
  intros a b e. inversion e. reflexivity.
Qed.

然而，Some 的情况非常特殊，您可能希望以不同的方式编写它（特别是如果您希望能够阅读生成的证明）。您可以使用默认值为 option 编写一些 get 函数：

Definition get_opt_default {A : Type} (x : A) (o : option A) :=
  match o with
  | Some a => a
  | None => x
  end.

所以get_opt_default x (Some a) = a。现在在相等 Some a = Some b 上使用 f_equal (get_opt_default a) 你得到

get_opt_default a (Some a) = get_opt_default a (Some b)

简化为

a = b

Lemma Some_inj :
  forall A (a b : A),
    Some a = Some b ->
    a = b.
Proof.
  intros a b e.
  apply (f_equal (get_opt_default a)) in e.
  cbn in e.
  exact e.
Qed.

这是一般情况下可以做到的事情。基本上，你为你的值编写一个提取器作为一个函数，并将它应用于相等的两边。通过计算它会产生预期的结果。

Answer 2

congruence战术的威力足以单独解决这个目标。更一般地说，在某些情况下，您希望从以相同构造函数开头的项的等式 H : x = y 开始，将 a = b 作为附加假设导出。在这种情况下，您可以调用

injection H.

提取该假设隐含的等式。

Answer 3

我认为写下基本引理是有启发性的：

Definition some_inj A (x y : A) (h_eq : Some x = Some y) : x = y :=
  match h_eq with
  | eq_refl _ => eq_refl
  end.

实际上，这似乎令人惊讶；事实上，Coq 正在精心设计匹配以帮助用户，而现实是有点丑陋，正如术语所见证的那样：

Print some_inj.

Definition some_inj A (x y : A) (h_eq : Some x = Some y) : x = y :=
  match h_eq in (_ = option_y)
        return match option_y with
               | Some y => x = y
               | None => IDProp
               end
  with
  | eq_refl => eq_refl
  end.

所以确实 return 类型的匹配做了很多工作来告诉 Coq 构造函数是单射的。

如何从 Some 的相等性证明相等性

How to prove equality from equality of Some

coq

coq-tactic