X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fcsub0_defs.v;h=2949e83d986cbd6fbda470aa2c2c43911b62edfd;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=7aa8a2c9bbff429c9457ebbdd02bcd9b5162601a;hpb=1b21075e987872a2e3103203b4e67c939e4a9f6a;p=helm.git diff --git a/helm/coq-contribs/LAMBDA-TYPES/csub0_defs.v b/helm/coq-contribs/LAMBDA-TYPES/csub0_defs.v index 7aa8a2c9b..2949e83d9 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/csub0_defs.v +++ b/helm/coq-contribs/LAMBDA-TYPES/csub0_defs.v @@ -4,20 +4,20 @@ Require Export ty0_defs. Inductive csub0 [g:G] : C -> C -> Prop := (* structural rules *) - | csub0_sort : (n:?) (csub0 g (CSort n) (CSort n)) - | csub0_tail : (c1,c2:?) (csub0 g c1 c2) -> (k,u:?) - (csub0 g (CTail c1 k u) (CTail c2 k u)) + | csub0_sort: (n:?) (csub0 g (CSort n) (CSort n)) + | csub0_tail: (c1,c2:?) (csub0 g c1 c2) -> (k,u:?) + (csub0 g (CTail c1 k u) (CTail c2 k u)) (* axioms *) - | csub0_void : (c1,c2:?) (csub0 g c1 c2) -> (b:?) ~b=Void -> (u1,u2:?) - (csub0 g (CTail c1 (Bind Void) u1) (CTail c2 (Bind b) u2)) - | csub0_abst : (c1,c2:?) (csub0 g c1 c2) -> (u,t:?) (ty0 g c2 u t) -> + | csub0_void: (c1,c2:?) (csub0 g c1 c2) -> (b:?) ~b=Void -> (u1,u2:?) + (csub0 g (CTail c1 (Bind Void) u1) (CTail c2 (Bind b) u2)) + | csub0_abst: (c1,c2:?) (csub0 g c1 c2) -> (u,t:?) (ty0 g c2 u t) -> (csub0 g (CTail c1 (Bind Abst) t) (CTail c2 (Bind Abbr) u)). Hint csub0 : ltlc := Constructors csub0. Section csub0_props. (****************************************************) - Theorem csub0_refl : (g:?; c:?) (csub0 g c c). + Theorem csub0_refl: (g:?; c:?) (csub0 g c c). XElim c; XAuto. Qed. @@ -27,11 +27,11 @@ Require Export ty0_defs. Section csub0_drop. (*****************************************************) - Theorem csub0_drop_abbr : (g:?; n:?; c1,c2:?) (csub0 g c1 c2) -> (d1,u:?) - (drop n (0) c1 (CTail d1 (Bind Abbr) u)) -> - (EX d2 | (csub0 g d1 d2) & - (drop n (0) c2 (CTail d2 (Bind Abbr) u)) - ). + Theorem csub0_drop_abbr: (g:?; n:?; c1,c2:?) (csub0 g c1 c2) -> (d1,u:?) + (drop n (0) c1 (CTail d1 (Bind Abbr) u)) -> + (EX d2 | (csub0 g d1 d2) & + (drop n (0) c2 (CTail d2 (Bind Abbr) u)) + ). XElim n. (* case 1 : n = 0 *) Intros; DropGenBase; Rewrite H0 in H; Inversion H; XEAuto. @@ -60,16 +60,16 @@ Require Export ty0_defs. XElim H; XEAuto. Qed. - Theorem csub0_drop_abst : (g:?; n:?; c1,c2:?) (csub0 g c1 c2) -> (d1,t:?) - (drop n (0) c1 (CTail d1 (Bind Abst) t)) -> - (EX d2 | (csub0 g d1 d2) & - (drop n (0) c2 (CTail d2 (Bind Abst) t)) + Theorem csub0_drop_abst: (g:?; n:?; c1,c2:?) (csub0 g c1 c2) -> (d1,t:?) + (drop n (0) c1 (CTail d1 (Bind Abst) t)) -> + (EX d2 | (csub0 g d1 d2) & + (drop n (0) c2 (CTail d2 (Bind Abst) t)) - ) \/ - (EX d2 u | (csub0 g d1 d2) & - (drop n (0) c2 (CTail d2 (Bind Abbr) u)) & - (ty0 g d2 u t) - ). + ) \/ + (EX d2 u | (csub0 g d1 d2) & + (drop n (0) c2 (CTail d2 (Bind Abbr) u)) & + (ty0 g d2 u t) + ). XElim n. (* case 1 : n = 0 *) Intros; DropGenBase; Rewrite H0 in H; Inversion H; XEAuto. @@ -112,75 +112,3 @@ Require Export ty0_defs. LApply (csub0_drop_abst ?1 ?4 ?2 ?3); [ Clear H1; Intros H1 | XAuto ]; LApply (H1 ?5 ?6); [ Clear H1 H2; Intros H1 | XAuto ]; XElim H1; Intros H1; XElim H1; Intros. - - Section csub0_pc3. (*****************************************************) - - Theorem csub0_pr2 : (g:?; c1:?; t1,t2:?) (pr2 c1 t1 t2) -> - (c2:?) (csub0 g c1 c2) -> (pr2 c2 t1 t2). - Intros until 1; XElim H; Intros. -(* case 1 : pr2_pr0 *) - XAuto. -(* case 2 : pr2_delta *) - CSub0Drop; XEAuto. - Qed. - - Theorem csub0_pc2 : (g:?; c1:?; t1,t2:?) (pc2 c1 t1 t2) -> - (c2:?) (csub0 g c1 c2) -> (pc2 c2 t1 t2). - Intros until 1; XElim H; Intros. -(* case 1 : pc2_r *) - Apply pc2_r; EApply csub0_pr2; XEAuto. -(* case 2 : pc2_x *) - Apply pc2_x; EApply csub0_pr2; XEAuto. - Qed. - - Theorem csub0_pc3 : (g:?; c1:?; t1,t2:?) (pc3 c1 t1 t2) -> - (c2:?) (csub0 g c1 c2) -> (pc3 c2 t1 t2). - Intros until 1; XElim H; Intros. -(* case 1 : pc3_r *) - XAuto. -(* case 2 : pc3_u *) - EApply pc3_u; [ EApply csub0_pc2; XEAuto | XAuto ]. - Qed. - - End csub0_pc3. - - Hints Resolve csub0_pc3 : ltlc. - - Section csub0_ty0. (*****************************************************) - - Theorem csub0_ty0 : (g:?; c1:?; t1,t2:?) (ty0 g c1 t1 t2) -> - (c2:?) (wf0 g c2) -> (csub0 g c1 c2) -> - (ty0 g c2 t1 t2). - Intros until 1; XElim H; Intros. -(* case 1 : ty0_conv *) - EApply ty0_conv; XEAuto. -(* case 2 : ty0_sort *) - XEAuto. -(* case 3 : ty0_abbr *) - CSub0Drop; EApply ty0_abbr; XEAuto. -(* case 4 : ty0_abst *) - CSub0Drop; [ EApply ty0_abst | EApply ty0_abbr ]; XEAuto. -(* case 5 : ty0_bind *) - EApply ty0_bind; XEAuto. -(* case 6 : ty0_appl *) - EApply ty0_appl; XEAuto. -(* case 7 : ty0_cast *) - EApply ty0_cast; XAuto. - Qed. - - Theorem csub0_ty0_ld : (g:?; c:?; u,v:?) (ty0 g c u v) -> (t1,t2:?) - (ty0 g (CTail c (Bind Abst) v) t1 t2) -> - (ty0 g (CTail c (Bind Abbr) u) t1 t2). - Intros; EApply csub0_ty0; XEAuto. - Qed. - - End csub0_ty0. - - Hints Resolve csub0_ty0 csub0_ty0_ld : ltlc. - - Tactic Definition CSub0Ty0 := - Match Context With - [ _: (ty0 ?1 ?2 ?4 ?); _: (ty0 ?1 ?2 ?3 ?7); _: (pc3 ?2 ?4 ?7); - H: (ty0 ?1 (CTail ?2 (Bind Abst) ?4) ?5 ?6) |- ? ] -> - LApply (csub0_ty0_ld ?1 ?2 ?3 ?4); [ Intros H_x | EApply ty0_conv; XEAuto ]; - LApply (H_x ?5 ?6); [ Clear H_x H; Intros | XAuto ].