Coq 증명에서 유도 가설을 강화하는 방법은 무엇입니까?

Question

저는 실제 업무에서 문맥 자유 문법의 응용 프로그램을 공식화하려고합니다. 하나의 보조 정리를 증명하는 데 문제가 있습니다. 나는 문제를 개략적으로 설명하기 위해 상황을 단순화하려고 노력했지만, 여전히 조금 성가시다. 다음과 같이

그래서 나는 촘스키 정상적인 형태와 단말기의 목록 derivability에 CFG 정의 :

내가 예를 들어, 터미널 및 몇 가지 추가 정보를 저장하는 객체가

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). 

:

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

과 주어진 비 터미널 (헬퍼 함수 사용)에서 파생 가능한 모든 객체 목록을 정의하려고합니다.

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). 

는 paths의 모든 요소가 비 터미널에서 파생 될 수 있다는

그리고 지금은 유도에 의해 paths에 대한 증거 사실에 노력하고있어 (paths의 각 생성자는 실제로 rule의 생성자에 해당) :

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. 

이 구조는 각각 서브 우퍼 3 개를 생성합니다. 첫 번째 및 두 번째는 Der_eps 및 Der_ter 생성자를 각각 적용하여 증명했습니다. 그러나 3 subgoal의 컨텍스트 내 목표를 증명 관련이없는, 그것은이 있습니다

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는 l가 l1 및 l2에서 일부 요소의 연결이 있다는 것을 의미하지만, IHpt1 및 IHpt2의 소재지는 l2하고, true를하다 l1에는 빈 목록이 있는데, 이는 일반적으로 사실이 아니기 때문에이 컨텍스트로 목표를 증명하는 것은 불가능합니다. l이 contains에, IHpt1, IHpt2 다른 목록 될 경우

문제

가 해결 될 수 있지만, 불행하게도 나는 COQ에게 설명하는 방법을 모르겠어요. 어쨌든 어떤 식 으로든 IHpt1과 IHpt2을 변경하여 목표를 증명하거나 다른 방법으로 전체 사실을 입증 할 수 있습니까?

나는 paths_ind을 보려고했으나 행복하지 않았습니다.

Answer 1

유도 가설이 충분히 강하지는 않은 것처럼 보입니다. 더 많은 다형성 목표로 induction pt을 수행하면 시작한 특정 l에 묶이지 않은 유용한 가설을 얻게됩니다.

당신이 시도해야합니다

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