Coq在樹狀結構中的感應

這是一個非常基本的問題，我很抱歉，但我一直試圖用Coq來證明下面的定理，並且似乎無法弄清楚如何去做。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，但這並不能正確工作。看來我需要同時對兩者進行歸納，但無法弄清楚。

來源

2013-11-04 jcb

我能夠證明這一點用簡單的感應

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.

通過應用inductionintros之前我們歸納假設是多態在tree2這使得我們在最後的情況下使用它。

來源

2013-11-04 05:24:21 jozefg

很酷，謝謝，基本上爲我工作，但我不得不做一些調整。首先，我沒有定義andb_true_iff - 我猜測這是在某個庫中，但我得到了要點，併爲它做了我自己的定理（參見上文）。我想我可以問的最重要的問題是：爲什麼我可以使用IHtree1_1和IHtree1_2，當他們都引用tree2而不是像tree2_1或（節點tree2_1 tree2_2）或類似的東西？我覺得這個答案將會被包含在你的短語「多態樹2，它允許我們在最後的情況下使用它」。那麼tree2沒有定義？ – jcb

很酷。需要導入布爾。訣竅。我對Coq真的很陌生（你可能已經收集到了），所以這些應該是顯而易見的事情還沒有。 – jcb

@quadelirus沒有一個是我的錯:)我只是從emacs複製和粘貼，卻沒有意識到我的導入位於頂端 – jozefg

Coq在樹狀結構中的感應

回答

相關問題