Coq中的Leibniz属性

Question

我对自然数的平等有这样的定义：

Fixpoint equal_nat (n m : nat) : bool := 
  match n, m with
    | O, O => true
    | O, S _ => false
    | S _, O => false
    | S n1, S n2 => equal_nat n1 n2
  end.

(这几乎是标准定义)

我试图证明以下观点：

Proposition equal_nat_correct :
  forall a b : nat, a = b <-> equal_nat a b = true.

我可以做前半部分的证明，但另一个不能.你能给我个提示吗？以下是我迄今所做的工作：

Proof.
  intros.
  split.

  (* => *)
  destruct a.
  destruct b.
  reflexivity.
  discriminate.
  intros. destruct H. simpl.
  induction a. reflexivity.
  simpl. assumption.

  (* <= *)
  (* ? *)
Qed.

谢谢。

编辑:

以下是完整的证明(也许不是最优的)：

Proposition equal_nat_correct :
  forall a b : nat, a = b <-> equal_nat a b = true.
Proof.
  split.

  (* => *)
  revert b.
  induction a as [ | a hi]; intros [ | b ]; simpl in *; intuition.
  discriminate.
  discriminate.

  (* <= *)
  revert b.
  induction a.
  intros.
  induction b.
  reflexivity.
  discriminate.
  intros [ | b]; simpl in *; intuition.
  discriminate.  
Qed.

Answer 1

这两个部分的想法都是通过induction进行的，但是在执行之前，您必须小心上下文中的内容。在您的特定情况下，您不应该立即引入b。以下是我在上半场的表现：

intros.
split.
revert b. (* puts b back into the goal, so that it is generalized correctly by induction *)
induction a as [ | a hi ]. (* this just gives explicit names to the term newly created by induction *)
  intro [ | b ]. (* this is equalivalent to intro b. destruct b as [ | b ]. *)
    intros; simpl; reflexivity.
    intros; discriminate.

  intro [ | b ].
    intros; discriminate.
    intros h; injection h; intros h2.
    simpl; apply hi; assumption

简短的版本如下：

intros.
split.
revert b.
induction a as [ | a hi]; intros [ | b ]; simpl in *; intuition.
discriminate.
discriminate.

遵循同样的模式(不要忘记在目标中泛化b )，您应该能够完成下半部分的证明。