0

This is a really elementary question, and I apologize, but I've been trying to use Coq to prove the following theorem, and just can't seem to figure out how to do it. 

(* 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.

What I have been trying to do is apply induction on tree1 followed by tree2, but this doesn't really work correctly. It seems I need to apply induction to both simultaneously, but can't figure out how.

4

1 回答 1

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.

通过在我们的归纳假设induction之前应用是多态的，这允许我们在最终情况下使用它。introstree2

于 2013-11-04T05:24:21.870 回答