귀납 命題에 대한 Coq - disj_conj_intro_patterns

Question

Coq에서 임의의 귀납적 명제 정의가 주어지면 귀납적 명제에 유도 전술을 호출 할 때 합리적인 disj_conj_intro_pattern을 유도하는 일반적인 공식이 있습니까?

일반적으로 귀납적 정의의 생성자 중 하나에 대한 완전한 intro_pattern은 두 개 이상의 가설과 하나 이상의 귀납적 가설을 요구할 수 있으며,이 경우 패턴에 제공된 이름의 순서는 모두 하나의 가설과 그에 상응하는 귀납적 가설, 그 다음에 가설과 귀납적 가설로 구성된 하나 이상의 추가 짝이 뒤 따른다. 가설 및 유도 가설 두 쌍을 가지고 각각의 MAPP와 MStarApp이 예에서

Inductive exp_match {T} : list T -> reg_exp T -> Prop := 
| MEmpty : exp_match [] EmptyStr 
| MChar : forall x, exp_match [x] (Char x) 
| MApp : forall s1 re1 s2 re2, 
      exp_match s1 re1 -> 
      exp_match s2 re2 -> 
      exp_match (s1 ++ s2) (App re1 re2) 
| MUnionL : forall s1 re1 re2, 
       exp_match s1 re1 -> 
       exp_match s1 (Union re1 re2) 
| MUnionR : forall re1 s2 re2, 
       exp_match s2 re2 -> 
       exp_match s2 (Union re1 re2) 
| MStar0 : forall re, exp_match [] (Star re) 
| MStarApp : forall s1 s2 re, 
       exp_match s1 re -> 
       exp_match s2 (Star re) -> 
       exp_match (s1 ++ s2) (Star re). 

Notation "s =~ re" := (exp_match s re) (at level 80). 

Theorem in_re_match : forall T (s : list T) (re : reg_exp T) (x : T), 
    s =~ re -> 
    In x s -> 
    In x (re_chars re). 
Proof. 
    intros T s re x Hmatch Hin. 
    induction Hmatch 
    as [ 
     |x' 
     |s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2 
     |s1 re1 re2 Hmatch IH|re1 s2 re2 Hmatch IH 
     |re|s1 s2 re Hmatch1 IH1 Hmatch2 IH2]. 

의 intro_patterns -이 두 생성자 각 양식

의 표현을 포함 아마도 때문에 : 예를 들어, 소프트웨어 재단은 다음을 포함한다

X -> Y -> Z이 약

, 현재의 참조 설명서에만

말 것 이 같은 용어를 유도 동작하지만 문맥 도입 변수 이름 disj_conj_intro_pattern의 이름을 사용 disj_conj_intro_pattern

0

유도 용어. disj_conj_intro_pattern은 일반적으로 [ p11 ... p1n1 | ... | pm1 ... pmnm] m은 생성자의 수입니다. 용어 유형입니다. i 번째 목표의 컨텍스트에서 유도에 의해 도입 된 각 변수는 목록에서 pi1 ... pini의 이름을 순서로 가져옵니다. 이름이 충분하지 않은 경우 유도는 나머지 변수가 도입 될 이름을 만듭니다 (이름은 ). 보다 일반적으로 pij는 임의의 이항/결합 소개 패턴 (8.3.2 절 참조) 일 수 있습니다. 인스턴스의 경우 생성자가 하나 인 귀납적 유형의 경우 [p1 ... pn] 대신 표기법 (p1, ..., pn)을 사용할 수 있습니다.

이하지 주어진 유도 정의에 대한 완전한 disj_conj_intro_pattern에 대한 올바른 양식을 결정하는 방법을 지정하는 것 같다 않습니다.

위의 경험적 관찰은 1) 각 생성자의 형식적 매개 변수가 먼저오고, 생성자의 가설이 해당 유도 성 가설과 쌍을 이룹니다. 2) 가설의 쌍과 귀납적 가설의 갯수는 생성자의 가설의 수, 그 문제의 합에 따라 결정된다. 아니면 더 이상 거기에 있습니까?

참조 설명서의 전술 장과 제 1 장의 Gallina 문법 패턴에 대한 매우 일반적인 토론 외에도 관련 문서가 있습니까?

Answer 1

질문을 올바르게 이해하면 대답은 '예'입니다. 귀납을위한 소개 패턴을 ​​파생시킬 수 있습니다.

는

COQ 자동으로 접미어로 _ind 추가 어떤 유도 정의 및 이름 유도 원리를 생성하므로 exp_match 용 유도 원리 exp_match_ind된다. 명령을 사용하여 exp_match_ind 유형을 탐색하면 필요한 인트로 패턴을 생성 할 수 있습니다.

Check exp_match_ind. 

(* output: 
exp_match_ind 
    : forall (T : Type) (P : list T -> reg_exp T -> Prop), 
     P [] EmptyStr -> 
     (forall x : T, P [x] (Char x)) -> 
     (forall (s1 : list T) (re1 : reg_exp T) 
      (s2 : list T) (re2 : reg_exp T), 
     s1 =~ re1 -> 
     P s1 re1 -> 
     s2 =~ re2 -> P s2 re2 -> P (s1 ++ s2) (App re1 re2)) -> 
     (forall (s1 : list T) (re1 re2 : reg_exp T), 
     s1 =~ re1 -> P s1 re1 -> P s1 (Union re1 re2)) -> 
     (forall (re1 : reg_exp T) (s2 : list T) (re2 : reg_exp T), 
     s2 =~ re2 -> P s2 re2 -> P s2 (Union re1 re2)) -> 
     (forall re : reg_exp T, P [] (Star re)) -> 
     (forall (s1 s2 : list T) (re : reg_exp T), 
     s1 =~ re -> 
     P s1 re -> 
     s2 =~ Star re -> P s2 (Star re) -> P (s1 ++ s2) (Star re)) -> 
     forall (l : list T) (r : reg_exp T), l =~ r -> 
     P l r 
*) 

이 유형은 (초기 forall "헤더"를 건너 뛸 경우) 하위 목표의 무리를 증명해야 그 목표 P l r을 증명하는 것을 말한다.

P [] EmptyStr 

우리가 induction Hmatch as [ |로 시작하는 그 이유는, 어떤 가설이 없습니다 - |의 왼쪽에 아무것도주의 사항 :

1) MEmpty 경우 : 최상위 레벨에있는 모든 ->는 서브 골을 분리합니다.

2) MChar 경우 :

(forall x : T, P [x] (Char x)) 

이 경우 인트로 패턴은 간단하다 : 어떤 x' 위해 우리는 P [x'] (Char x')을 증명해야합니다. 이 시점에서 우리의 패턴이된다 : [ | x' ...

3) MApp 경우 : 정리 in_re_match에 사용되는 것들에 따라 위의 의견에

(forall (s1 : list T) (re1 : reg_exp T) 
     (s2 : list T) (re2 : reg_exp T), (* s1 re1 s2 re2 *) 
     s1 =~ re1 ->      (* Hmatch1 *) 
     P s1 re1 ->      (* IH1 *) 
     s2 =~ re2 ->      (* Hmatch2 *) 
     P s2 re2 ->      (* IH2 *) 
     P (s1 ++ s2) (App re1 re2))  (* the current subgoal *) 

내가 표시 한 변수와 가설. 이 점에서 우리의 패턴은 다음과 같습니다. [ | x' | s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2 ...

나머지 부분 골은 유사하게 수행 할 수 있으므로 정리에 사용되는 패턴이 생깁니다.