(****************************************************************************) (* *) (* The formal system \lambda\delta *) (* *) (* Author: Ferruccio Guidi *) (* *) (* This file is distributed under the terms of the *) (* GNU General Public License Version 2 *) (* *) (****************************************************************************) Require Export pr1_defs. Require Export pr2_defs. Inductive pr3 [c:C] : T -> T -> Prop := | pr3_refl: (t:?) (pr3 c t t) | pr3_sing: (t2,t1:?) (pr2 c t1 t2) -> (t3:?) (pr3 c t2 t3) -> (pr3 c t1 t3). Hints Resolve pr3_refl : ld. Section pr3_gen_base. (***************************************************) Lemma pr3_gen_sort: (c:?; x:?; n:?) (pr3 c (TSort n) x) -> x = (TSort n). Proof. Intros; InsertEq H '(TSort n); XElim H; Clear y x; Intros. (* case 1: pr3_refl *) XAuto. (* case 2: pr3_sing *) Subst; Clear H0; Pr2GenBase; Subst; XAuto. Qed. Tactic Definition IH := ( Match Context With | [ H: (u,t:T) (THead (Bind Abst) ?1 ?2) = (THead (Bind Abst) u t) -> ? |- ? ] -> LApply (H ?1 ?2); [ Clear H; Intros H | XAuto ]; XDecompose H | [ H: (u,t:T) (THead (Flat Cast) ?1 ?2) = (THead (Flat Cast) u t) -> ? |- ? ] -> LApply (H ?1 ?2); [ Clear H; Intros H | XAuto ]; XDecompose H ). Hints Resolve pr3_sing : ld. Lemma pr3_gen_abst: (c:?; u1,t1,x:?) (pr3 c (THead (Bind Abst) u1 t1) x) -> (EX u2 t2 | x = (THead (Bind Abst) u2 t2) & (pr3 c u1 u2) & (b:?; u:?) (pr3 (CHead c (Bind b) u) t1 t2) ). Proof. Intros until 1; InsertEq H '(THead (Bind Abst) u1 t1); UnIntro H t1; UnIntro H u1; XElim H; Clear y x; Intros; Rename x into u0; Rename x0 into t0. (* case 1 : pr3_refl *) XDEAuto 2. (* case 2 : pr3_sing *) Rewrite H2 in H; Clear H0 H2 t1; Pr2GenBase. Rewrite H0 in H1; Clear H0 t2; IH; XDEAuto 4. Qed. Lemma pr3_gen_cast: (c:?; u1,t1,x:?) (pr3 c (THead (Flat Cast) u1 t1) x) -> (EX u2 t2 | x = (THead (Flat Cast) u2 t2) & (pr3 c u1 u2) & (pr3 c t1 t2) ) \/ (pr3 c t1 x). Proof. Intros; InsertEq H '(THead (Flat Cast) u1 t1); UnIntro H t1; UnIntro H u1; XElim H; Clear y x; Intros; Rename x into u0; Rename x0 into t0. (* case 1: pr3_refl *) Rewrite H; Clear H t; XDEAuto 3. (* case 2: pr3_sing *) Rewrite H2 in H; Clear H2 t1; Pr2GenBase. (* case 2.1: short step: compatinility *) Rewrite H3 in H1; Clear H0 H3 t2; IH; Try Rewrite H0; XDEAuto 5. (* case 2.2: short step: tau *) XDEAuto 3. Qed. Hints Resolve clear_pr2_trans : ld. Lemma clear_pr3_trans: (c2:?; t1,t2:?) (pr3 c2 t1 t2) -> (c1:?) (clear c1 c2) -> (pr3 c1 t1 t2). Proof. Intros; XElim H; Clear t1 t2; Intros; [ XAuto | XDEAuto 3 ]. Qed. End pr3_gen_base. Tactic Definition Pr3GenBase := ( Match Context With | [ H: (pr3 ?1 (TSort ?2) ?3) |- ? ] -> LApply (pr3_gen_sort ?1 ?3 ?2); [ Clear H; Intros | XAuto ] | [ H: (pr3 ?1 (THead (Bind Abst) ?2 ?3) ?4) |- ? ] -> LApply (pr3_gen_abst ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ]; XDecompose H | [ H: (pr3 ?1 (THead (Flat Cast) ?2 ?3) ?4) |- ? ] -> LApply (pr3_gen_cast ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ]; XDecompose H ). Section pr3_props. (******************************************************) Hints Resolve pr3_sing : ld. Lemma pr3_pr2: (c,t1,t2:?) (pr2 c t1 t2) -> (pr3 c t1 t2). Proof. XDEAuto 2. Qed. Theorem pr3_t: (t2,t1,c:?) (pr3 c t1 t2) -> (t3:?) (pr3 c t2 t3) -> (pr3 c t1 t3). Proof. Intros until 1; XElim H; XDEAuto 3. Qed. Lemma pr3_thin_dx: (c:?; t1,t2:?) (pr3 c t1 t2) -> (u:?; f:?) (pr3 c (THead (Flat f) u t1) (THead (Flat f) u t2) ). Proof. Intros; XElim H; XDEAuto 3. Qed. Lemma pr3_head_1: (c:?; u1,u2:?) (pr3 c u1 u2) -> (k:?; t:?) (pr3 c (THead k u1 t) (THead k u2 t)). Proof. Intros until 1; XElim H; Intros. (* case 1: pr3_refl *) XAuto. (* case 2: pr3_sing *) EApply pr3_sing; [ Apply pr2_head_1; Apply H | XAuto ]. Qed. Lemma pr3_head_2: (c:?; u,t1,t2:?; k:?) (pr3 (CHead c k u) t1 t2) -> (pr3 c (THead k u t1) (THead k u t2)). Proof. Intros until 1; XElim H; Intros. (* case 1: pr3_refl *) XAuto. (* case 2: pr3_sing *) EApply pr3_sing; [ Apply pr2_head_2; Apply H | XAuto ]. Qed. Hints Resolve pr3_head_1 pr3_head_2 : ld. Theorem pr3_head_21: (c:?; u1,u2:?) (pr3 c u1 u2) -> (k:?; t1,t2:?) (pr3 (CHead c k u1) t1 t2) -> (pr3 c (THead k u1 t1) (THead k u2 t2)). Proof. Intros. EApply pr3_t; [ Apply pr3_head_2 | Apply pr3_head_1 ]; XAuto. Qed. Theorem pr3_head_12: (c:?; u1,u2:?) (pr3 c u1 u2) -> (k:?; t1,t2:?) (pr3 (CHead c k u2) t1 t2) -> (pr3 c (THead k u1 t1) (THead k u2 t2)). Proof. Intros. EApply pr3_t; [ Apply pr3_head_1 | Apply pr3_head_2 ]; XAuto. Qed. Lemma pr3_pr1: (t1,t2:?) (pr1 t1 t2) -> (c:?) (pr3 c t1 t2). Proof. Intros until 1; XElim H; XDEAuto 3. Qed. Lemma pr3_cflat: (c:?; t1,t2:?) (pr3 c t1 t2) -> (f:?; v:?) (pr3 (CHead c (Flat f) v) t1 t2). Proof. Intros until 1; XElim H; Clear t1 t2; XDEAuto 3. Qed. Hints Resolve pr3_head_12 pr3_head_21 pr3_cflat : ld. Theorem pr3_flat: (c:?; u1,u2:?) (pr3 c u1 u2) -> (t1,t2:?) (pr3 c t1 t2) -> (f:?) (pr3 c (THead (Flat f) u1 t1) (THead (Flat f) u2 t2)). Proof. XAuto. Qed. End pr3_props. Tactic Definition Pr3T t := ( Match Context With | [ H: (pr3 ?1 ?2 ?3) |- ? ] -> LApply (pr3_t ?3 ?2 ?1); [ Clear H; Intros H | XAuto ]; LApply (H t); [ Clear H; Intros | XDEAuto 4 ] ). Hints Resolve pr3_flat pr3_pr2 pr3_pr1 pr3_thin_dx pr3_cflat pr3_head_12 pr3_head_21 : ld.