如何证明某些人的平等

Question

我想证明Coq中两个自然数相等：

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

Answer 1

congruence策略足以自行解决此目标。更一般而言，在某些情况下，您希望从以相同构造函数开始的词语的相等性a = b开始推导H : x = y作为附加假设。在这种情况下，您可以致电

injection H.

提取该假设所隐含的等式。

Answer 2

[通常，当拥有这样的相等性时，最快的方法是使用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。现在在等式f_equal (get_opt_default a)上使用Some a = Some b你得到

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.

这通常可以完成。基本上，您将值编写为函数的提取器，并将其应用于等式的两侧。通过计算，它将产生预期的结果。