Coq 在树结构上的归纳

Question

这是一个非常基本的问题，我很抱歉，但我一直在尝试使用 Coq 来证明以下定理，但似乎无法弄清楚如何去做。

(* Binary tree definition. *)
Inductive btree : Type := 
  | EmptyTree
  | Node : btree -> btree -> btree.
(* Checks if two trees are equal. *)

Fixpoint isEqual (tree1 : btree) (tree2 : btree) : bool :=
  match tree1, tree2 with
    | EmptyTree, EmptyTree => true
    | EmptyTree, _ => false
    | _, EmptyTree => false
    | Node n11 n12, Node n21 n22 => (andb (isEqual n11 n21) (isEqual n12 n22))
end.

Lemma isEqual_implies_equal : forall tree1 tree2 : btree, 
(isEqual tree1 tree2) = true -> tree1 = tree2.

我一直在尝试做的是在 tree1 上应用归纳，然后是 tree2，但这并不能正常工作。看来我需要同时对两者应用归纳，但不知道如何。

Answer 1

我可以用简单的归纳法证明这一点

Require Import Bool. (* Sorry! Forgot to add that the first time *)

Lemma isEqual_implies_equal : forall tree1 tree2 : btree, 
(isEqual tree1 tree2) = true -> tree1 = tree2.
  induction tree1, tree2; intuition eauto.
  inversion H.
  inversion H.
  apply andb_true_iff in H.
  intuition eauto; fold isEqual in *.
  apply IHtree1_1 in H0.
  apply IHtree1_2 in H1.
  congruence.
Qed.

(* An automated version *)
Lemma isEqual_implies_equal' : forall tree1 tree2 : btree, 
(isEqual tree1 tree2) = true -> tree1 = tree2.
  induction tree1, tree2; intuition; simpl in *;
  repeat match goal with
            | [ H : false = true |- _ ]   => inversion H
            | [ H : (_ && _) = true |- _] => apply andb_true_iff in H; intuition
            | [ IH : context[ _ = _ -> _], 
                H : _ = _ |- _]           => apply IH in H
         end; congruence.
  Qed.

通过在intros 之前应用induction，我们的归纳假设在tree2 上具有多态性，这允许我们在最终情况下使用它。