2
Coqの誘導原理を証明しようとしています。データ構造の定義のために、この原理を2つのネストされた誘導によって表示することが義務付けられています。外部誘導は、Fixpoint構築物を介して行われ、内部誘導は、原理list_indで行われる。 問題が発生するのは、内部誘導の誘導引数が関数の結果である、つまりdfs tです。 Iは、dfs tの最初の要素を外側帰納法の仮定を適用できるようにする必要があり、内側誘導工程において関数の値にネストされた帰納法を使用したFixpointプルーフ
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で誘導を行うとき、これは、不正な再帰を招くため不可能です。
私の目には、「正常な」アプローチがtと簡素化に誘導を行うことであろうが、dfs (choice t1 t2)だけdfs t1 ++ dfs t2に減少し、ケースt = choice t1 t2には、これは常に最初の問題に戻ってしまいます。
誰かがこの証明を続ける方法を提案していますか？
EDITは：それはコードを表示するには少しくらいかもしれないと思ったが、ここでは、次のとおりです。
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.は失敗します。
あなたはおそらく、このような 'リットルforallは、長さl <= N 'のような、より一般的な誘導の原理を使用する必要がある、しかし、財産の具体的な例なしにそれは難しいです言う。 – ejgallego