有關函數值的嵌套歸納的定點證明

Question

我試圖在Coq中證明歸納原理。由於數據結構的定義，必須通過兩個嵌套式導入來顯示該原理。外部感應通過Fixpoint構造完成，內部感應通過原理list_ind完成。 發生的問題是現在內部歸納的歸納論證是一個函數的結果，即dfs t。

Inductive SearchTree (A : Type) : Type := 
    | empty : SearchTree A 
    | leaf : A -> SearchTree A 
    | choice : SearchTree A -> SearchTree A -> SearchTree A. 

Fixpoint dfs (A : Type) (t: SearchTree A) : list A := 
    match t with 
    | empty => nil 
    | leaf x => cons x nil 
    | choice t1 t2 => app (dfs t1) (dfs t2) 
    end. 

在內部感應步驟我需要能夠與外歸納假設適用於dfs t第一個元素。但是：當在dfs t上進行歸納時，這是不可能的，因爲它會導致形式不規則的遞歸。

我眼中的「正常」的方法是做t和簡化歸納，但萬一t = choice t1 t2這會導致產生回到最初的問題作爲dfs (choice t1 t2)只減少了dfs t1 ++ dfs t2。

有人有建議如何繼續這個證明？

編輯：認爲這可能是一個有點多，顯示代碼，但在這裏它是：發生證明​​

 

Require Import Setoid. 
Require Import Coq.Lists.List. 

Set Implicit Arguments. 
Set Contextual Implicit. 

Section list. 
    Section listEquality. 

    Variable A : Type. 
    Variable eqA : A -> A -> Prop. 

    Inductive EqL : list A -> list A -> Prop := 
    | EqL_nil : EqL nil nil 
    | EqL_cons : forall (x y : A) (xs ys : list A), 
     eqA x y -> 
     EqL xs ys -> 
     EqL (cons x xs) (cons y ys). 

    End listEquality. 
End list. 

Section SearchTree. 

    Inductive SearchTree (A : Type) : Type := 
    | empty : SearchTree A 
    | leaf : A -> SearchTree A 
    | choice : SearchTree A -> SearchTree A -> SearchTree A. 

    Fixpoint dfs (A : Type) (t: SearchTree A) : list A := 
    match t with 
    | empty => nil 
    | leaf x => cons x nil 
    | choice t1 t2 => app (dfs t1) (dfs t2) 
    end. 

    Section DFSEquality. 

    Variable A : Type. 
    Variable eqA : relation A. 

    Definition EqDFS (t1 t2: SearchTree A) : Prop := 
     EqL eqA (dfs t1) (dfs t2). 

    End DFSEquality. 
End SearchTree. 

Section List. 
    Inductive List A := 
    | Nil : List A 
    | Cons : SearchTree A -> SearchTree (List A) -> List A. 
End List. 

Section EqND. 
    Variable A : Type. 
    Variable eqA : relation A. 
    Inductive EqND : List A -> List A -> Prop := 
    | Eq_Nil : EqND Nil Nil 
    | Eq_Cons : forall tx ty txs tys, 
     EqDFS eqA tx ty -> 
     EqDFS EqND txs tys -> 
     EqND (Cons tx txs) (Cons ty tys). 
End EqND. 

Section EqNDInd. 
    Variable A : Type. 
    Variable eqA : relation A. 
    Variable P : List A -> List A -> Prop. 
    Hypothesis BC : P Nil Nil. 
    Hypothesis ST: forall mx my mxs mys, 
     EqDFS eqA mx my 
     -> EqDFS (fun xs ys => EqND eqA xs ys /\ P xs ys) mxs mys 
     -> P (Cons mx mxs) (Cons my mys). 

    Fixpoint IND (xs ys : List A) { struct xs } : EqND eqA xs ys -> P xs ys. 
    Proof. 
     intro eq. 
     destruct xs,ys. 
     + exact BC. 
     + inversion eq. 
     + inversion eq. 
     + inversion eq. subst. apply ST. 
     ++ exact H2. 
     ++ unfold EqDFS in *. 
      generalize dependent (dfs s2). 
      induction (dfs s0). 
      +++ intros. inversion H4. constructor. 
      +++ intros. inversion H4. subst. constructor. 
       ++++ split. 
        * exact H1. 
        * apply IND. exact H1. (* Guarded. *) 
       ++++ clear IND. firstorder. 
    Admitted. 
End EqNDInd. 

 

問題，註釋掉Guarded.失敗。

Answer 1

要使用嵌套遞歸，您必須使用「修復1」策略，例如使用原始修復構造。歸納原則不會給你正確的遞歸調用。請注意，反轉可能會導致混淆警衛檢查器的重寫。實際上，如果你希望「嵌套」固定點不在原始列表的子項上，而是在[dfs t]上，那麼它不再是結構遞歸，你需要使用有根據的遞歸證明遞歸。我在玫瑰樹上有類似的example，其中使用了有根據的嵌套遞歸。

Answer 2

，我們在您嘗試了兩個問題：

• 你寫​​防止循環參數是eq: EqND eqA xs ys，而這將是一個自然的方式。

• 正如@Matthieu Sozeau所言，多次反演引入了噪聲。

令人驚訝的是，證據很短。

這裏是我的解決方案：

Fixpoint IND (xs ys : List A) (eq: EqND eqA xs ys) : P xs ys. 
Proof. 
    destruct eq. 
    - assumption. 
    - apply ST. 
    + assumption. 
    + unfold EqDFS in H0 |- *. induction H0. 
     * constructor. 
     * constructor. 
     -- split. 
      ++ assumption. 
      ++ apply IND. assumption. 
     -- assumption. 
Qed.