证明自然数的对称性

Question

我是coq的初学者。我想证明一个关于自然数的布尔等式的对称性。我已经应用了归纳和析构命令，但它不起作用。请指导我证明这个定理。

Fixpoint  beqnat(n m : nat): bool:= 
  match n with 
  |0=> match m with
      |0=> true
      |S m' => false
      end 
  |S n'=> match m with
         |0=>false
         |S m'=> beqnat n' m'
         end  
  end. 

  Theorem beq sys:  
    forall(n m:nat), 
      beqnat n m = beqnat m n.

Answer 1

接下来是对n的归纳，然后是对m的销毁

Theorem beq_sym: forall n m : nat, beqnat n m = beqnat m n.
Proof.
  induction n as [|n' IH]; destruct m; auto.
  apply IH.
Qed.

要了解正在发生的情况：

1. Do induction n，它在每个子目标上为n = 0和n = S n'.
2. Do simpl提供子目标，以查看第一个代码是如何减少的。
3. 现在您需要对m执行一些操作，以减少第二个< match/with >d15>。归纳不是必需的，因为您的beqnat在n上是结构化递归的(键入Print beqnat并查找{struct n}进行确认)，而不是m。所以，destruct m就足够了。同样，使用simpl来了解原因。
4. 第二个子目标中对beqnat的递归调用需要归纳假设。