Wie Induktion Hypothese in Coq Beweis stärken?

Question

Ich versuche die Anwendung von kontextfreien Grammatiken in der Praxis zu formalisieren. Ich habe Probleme, ein Lemma zu beweisen. Ich habe versucht, meinen Kontext zu vereinfachen, um das Problem zu umreißen, aber es ist immer noch etwas umständlich. So

I definiert CFG in Chomsky Normalform und Ableitbarkeit Liste der Terminals wie folgt:

Require Import List. 
Import ListNotations. 

Inductive ter : Type := T : nat -> ter. 
Inductive var : Type := V : nat -> var. 
Inductive eps : Type := E : eps. 

Inductive rule : Type := 
    | Rt : var -> ter -> rule 
    | Rv : var -> var -> var -> rule 
    | Re : var -> eps -> rule. 

Definition grammar := list rule. 

Inductive der_ter_list : grammar -> var -> list ter -> Prop := 
    | Der_eps : forall (g : grammar) (v : var) (e : eps), 
     In (Re v e) g -> der_ter_list g v [] 
    | Der_ter : forall (g : grammar) (v : var) (t : ter), 
     In (Rt v t) g -> der_ter_list g v [t] 
    | Der_var : forall (g : grammar) (v v1 v2 : var) (tl1 tl2 : list ter), 
     In (Rv v v1 v2) g -> der_ter_list g v1 tl1 -> der_ter_list g v2 tl2 -> 
     der_ter_list g v (tl1 ++ tl2). 

ich Objekte, die speichern Terminal und einige zusätzliche Informationen, zum Beispiel:

Inductive obj : Set := Get_obj : nat -> ter -> obj. 

Und Ich versuche, alle möglichen Listen von Objekten zu definieren, die von gegebenem Nichtterminal ableitbar sind (mit Hilfsfunktionen):

Fixpoint get_all_pairs (l1 l2 : list (list obj)) : list (list obj) := match l1 with 
    | [] => [] 
    | l::t => (map (fun x => l ++ x) l2) ++ get_all_pairs t l2 
    end. 

Fixpoint getLabels (objs : list obj) : list ter := match objs with 
    | [] => [] 
    | (Get_obj yy ter)::t => ter::(getLabels t) 
    end. 

Inductive paths : grammar -> var -> list (list obj) -> Prop := 
    | Empty_paths : forall (g : grammar) (v : var) (e : eps), 
     In (Re v e) g -> paths g v [[]] 
    | One_obj_path : forall (g : grammar) (v : var) (n : nat) (t : ter) (objs : list obj), 
     In (Rt v t) g -> In (Get_obj n t) objs -> paths g v [[Get_obj n t]] 
    | Combine_paths : forall (g : grammar) (v v1 v2 : var) (l1 l2 : list (list obj)), 
     In (Rv v v1 v2) g -> paths g v1 l1 -> paths g v2 l2 -> paths g v (get_all_pairs l1 l2). 

(Jeder Konstruktor paths entspricht tatsächlich Konstruktor rule)

Und nun zum Beweis der Tat über paths durch Induktion Ich versuche, dass jedes Element in paths aus Nicht-End ableiten:

Theorem derives_all_path : forall (g: grammar) (v : var) 
    (ll : list (list obj)) (pths : paths g v ll), forall (l : list obj), 
     In l ll -> der_ter_list g v (getLabels l). 
Proof. 
    intros g v ll pt l contains. 
    induction pt. 

Diese Konstruktion erzeugt 3 Teilziele, 1. und 2. Ich habe bewiesen, indem ich Der_eps und Der_ter Konstruktoren anwendet. Aber Kontext 3. subgoal ist nicht relevant, um mein Ziel zu beweisen, hat es:

contains : In l (get_all_pairs l1 l2) 
IHpt1 : In l l1 -> der_ter_list g v1 (getLabels l) 
IHpt2 : In l l2 -> der_ter_list g v2 (getLabels l) 

contains bedeutet also, dass l Verkettung einiger Elemente aus l1 und l2, aber Räumlichkeiten in IHpt1 und IHpt2 wahr sind iff l2 und l1 hat leere Listen, was im Allgemeinen nicht wahr ist, daher ist es unmöglich, in diesem Kontext ein Ziel zu beweisen.

Das Problem kann, wenn lIHpt1 in contains, aufgelöst werden, wird IHpt2 verschiedene Listen, aber leider weiß ich nicht, wie es zu Coq zu erklären. Ist es irgendwie möglich, IHpt1 und IHpt2 zu ändern, um das Ziel zu beweisen, oder eine andere Möglichkeit, die ganze Tatsache zu beweisen?

Ich habe versucht, auf paths_ind zu schauen, aber es hat mich nicht glücklich gemacht.

Answer 1

Es scheint, dass Ihre Induktions-Hypothese nicht stark genug ist. Wenn Sie auf einem mehr polymorphen Ziel ausführen, erhalten Sie nützlichere Hypothesen, die nicht mit dem spezifischen l, mit dem Sie begonnen haben, verknüpft sind.

sollten Sie versuchen:

intros g v ll pt; induction pt; intros l contains.