--- /dev/null
+(*#* #stop file *)
+
+Require lift_gen.
+Require lift_props.
+Require subst1_defs.
+Require subst1_lift.
+Require subst1_confluence.
+Require drop_props.
+Require csubst1_defs.
+Require pc3_gen.
+Require pc3_gen_context.
+Require ty0_defs.
+Require ty0_lift.
+
+(* NOTE: these break the recursion between ty0_sred_cpr0_pr0 and ty0_gen_lift *)
+
+ Section ty0_gen_cabbr. (**************************************************)
+
+ Tactic Definition IH d a0 a :=
+ Match Context With
+ [ H: (e:?; u:?; d:?) ? -> (a0:?) ? -> (a:?) ? -> ? -> ? |- ? ] ->
+ LApply (H e u0 d); [ Clear H; Intros H | XAuto ];
+ LApply (H a0); [ Clear H; Intros H | XAuto ];
+ LApply (H a); [ Clear H; Intros H | XEAuto ];
+ LApply H; [ Clear H; Intros H | XAuto ];
+ XElim H; Intros.
+
+(* NOTE: This can be generalized removing the last three premises *)
+ Theorem ty0_gen_cabbr: (g:?; c:?; t1,t2:?) (ty0 g c t1 t2) ->
+ (e:?; u:?; d:?) (drop d (0) c (CTail e (Bind Abbr) u)) ->
+ (a0:?) (csubst1 d u c a0) ->
+ (a:?) (wf0 g a) -> (drop (1) d a0 a) ->
+ (EX y1 y2 | (subst1 d u t1 (lift (1) d y1)) &
+ (subst1 d u t2 (lift (1) d y2)) &
+ (ty0 g a y1 y2)
+ ).
+ Intros until 1; XElim H; Intros.
+(* case 1 : ty0_conv *)
+ Repeat IH d a0 a; EApply ex3_2_intro;
+ [ XEAuto | XEAuto | EApply ty0_conv; Try EApply pc3_gen_cabbr; XEAuto ].
+(* case 2 : ty0_sort *)
+ EApply ex3_2_intro; Try Rewrite lift_sort; XAuto.
+(* case 3 : ty0_abbr *)
+ Apply (lt_eq_gt_e n d0); Intros; Clear c t1 t2.
+(* case 3.1 : n < d0 *)
+ Clear H1; DropDis; Rewrite minus_x_Sy in H1; [ DropGenBase | XAuto ].
+ CSubst1Drop; Rewrite minus_x_Sy in H0; [ Idtac | XAuto ].
+ CSubst1GenBase; Rewrite H0 in H8; Clear H0 x; Simpl in H9.
+ Rewrite (lt_plus_minus n d0) in H6; [ Idtac | XAuto ].
+ DropDis; Rewrite H0 in H9; Clear H0 x0.
+ IH '(minus d0 (S n)) x1 x3.
+ Subst1Confluence; Rewrite H0 in H11; Clear H0 x0.
+ Pattern 3 d0; Rewrite (le_plus_minus_sym (S n) d0); [ Idtac | XAuto ].
+ Pattern 4 d0; Rewrite (le_plus_minus (S n) d0); [ Idtac | XAuto ].
+ EApply ex3_2_intro;
+ [ Rewrite lift_bref_lt | Rewrite lift_d | EApply ty0_abbr ]; XEAuto.
+(* case 3.2 : n = d0 *)
+ Rewrite H7; Rewrite H7 in H0; Clear H2 H7 n.
+ DropDis; Inversion H0; Rewrite H8 in H4; Clear H0 H7 H8 e u0.
+ CSubst1Drop; DropDis.
+ EApply ex3_2_intro;
+ [ EApply subst1_single; Rewrite lift_free; Simpl; XEAuto
+ | Rewrite lift_free; Simpl; XEAuto
+ | XEAuto ].
+(* case 3.3 : n > d0 *)
+ Clear H2 H3 e; CSubst1Drop; DropDis.
+ Pattern 1 n; Rewrite (lt_plus_minus (0) n); [ Idtac | XEAuto ].
+ Arith4c '(0) '(minus n (1)).
+ EApply ex3_2_intro;
+ [ Rewrite lift_bref_ge
+ | Rewrite lift_free; Simpl
+ | Pattern 2 n; Rewrite (minus_x_SO n)
+ ]; XEAuto.
+(* case 4 : ty0_abst *)
+ Apply (lt_eq_gt_e n d0); Intros; Clear c t1 t2.
+(* case 4.1 : n < d0 *)
+ Clear H1; DropDis; Rewrite minus_x_Sy in H1; [ DropGenBase | XAuto ].
+ CSubst1Drop; Rewrite minus_x_Sy in H0; [ Idtac | XAuto ].
+ CSubst1GenBase; Rewrite H0 in H8; Clear H0 x; Simpl in H9.
+ Rewrite (lt_plus_minus n d0) in H6; [ Idtac | XAuto ].
+ DropDis; Rewrite H0 in H9; Clear H0 x0.
+ IH '(minus d0 (S n)) x1 x3.
+ Subst1Confluence; Rewrite H0 in H11; Clear H0 x0.
+ Pattern 3 d0; Rewrite (le_plus_minus_sym (S n) d0); [ Idtac | XAuto ].
+ Pattern 4 d0; Rewrite (le_plus_minus (S n) d0); [ Idtac | XAuto ].
+ EApply ex3_2_intro;
+ [ Rewrite lift_bref_lt | Rewrite lift_d | EApply ty0_abst ]; XEAuto.
+(* case 4.2 : n = d0 *)
+ Rewrite H7; Rewrite H7 in H0; DropDis; Inversion H0.
+(* case 4.3 : n > d0 *)
+ Clear H2 H3 e; CSubst1Drop; DropDis.
+ Pattern 1 n; Rewrite (lt_plus_minus (0) n); [ Idtac | XEAuto ].
+ Arith4c '(0) '(minus n (1)).
+ EApply ex3_2_intro;
+ [ Rewrite lift_bref_ge
+ | Rewrite lift_free; Simpl
+ | Pattern 2 n; Rewrite (minus_x_SO n)
+ ]; XEAuto.
+(* case 5 : ty0_bind *)
+ IH d a0 a; Clear H H1 H3 c t1 t2.
+ IH '(S d) '(CTail a0 (Bind b) (lift (1) d x0)) '(CTail a (Bind b) x0).
+ IH '(S d) '(CTail a0 (Bind b) (lift (1) d x0)) '(CTail a (Bind b) x0).
+ Subst1Confluence; Rewrite H4 in H11; Clear H4 x5.
+ EApply ex3_2_intro; Try Rewrite lift_bind; XEAuto.
+(* case 6 : ty0_appl *)
+ Repeat IH d a0 a; Clear H H1 c t1 t2.
+ Subst1GenBase; SymEqual; LiftGenBase; Rewrite H in H8; Rewrite H11 in H1; Rewrite H12 in H7; Clear H H11 H12 x1 x4 x5.
+ Subst1Confluence; Rewrite H in H8; Clear H x6.
+ EApply ex3_2_intro; Try Rewrite lift_flat;
+ [ Idtac | EApply subst1_tail; [ Idtac | Rewrite lift_bind ] | Idtac ]; XEAuto.
+(* case 7 : ty0_cast *)
+ Rename u into u0; Repeat IH d a0 a; Clear H H1 c t1 t2.
+ Subst1Confluence; Rewrite H in H10; Clear H x3.
+ EApply ex3_2_intro; [ Rewrite lift_flat | Idtac | Idtac ]; XEAuto.
+ Qed.
+
+ End ty0_gen_cabbr.
+
+ Section ty0_gen_cvoid. (**************************************************)
+
+ Tactic Definition IH d a :=
+ Match Context With
+ [ H: (e:?; u:?; d:?) ? -> (a:?) ? -> ? -> ? |- ? ] ->
+ LApply (H e u0 d); [ Clear H; Intros H | XAuto ];
+ LApply (H a); [ Clear H; Intros H | XEAuto ];
+ LApply H; [ Clear H; Intros H | XAuto ];
+ XElim H; Intros.
+
+(* NOTE: This can be generalized removing the last two premises *)
+ Theorem ty0_gen_cvoid: (g:?; c:?; t1,t2:?) (ty0 g c t1 t2) ->
+ (e:?; u:?; d:?) (drop d (0) c (CTail e (Bind Void) u)) ->
+ (a:?) (wf0 g a) -> (drop (1) d c a) ->
+ (EX y1 y2 | t1 = (lift (1) d y1) &
+ t2 = (lift (1) d y2) &
+ (ty0 g a y1 y2)
+ ).
+ Intros until 1; XElim H; Intros.
+(* case 1 : ty0_conv *)
+ Repeat IH d a; Rewrite H0 in H3; Rewrite H7 in H3; Pc3Gen; XEAuto.
+(* case 2 : ty0_sort *)
+ EApply ex3_2_intro; Try Rewrite lift_sort; XEAuto.
+(* case 3 : ty0_abbr *)
+ Apply (lt_eq_gt_e n d0); Intros.
+(* case 3.1 : n < d0 *)
+ DropDis; Rewrite minus_x_Sy in H7; [ DropGenBase | XAuto ].
+ Rewrite (lt_plus_minus n d0) in H5; [ Idtac | XAuto ].
+ DropDis; Rewrite H0 in H2; Clear H0 H1 u.
+ IH '(minus d0 (S n)) x1; Rewrite H1; Clear H1 t.
+ LiftGen; Rewrite <- H0 in H2; Clear H0 x2.
+ Rewrite <- lift_d; [ Idtac | XAuto ].
+ Rewrite <- le_plus_minus; [ Idtac | XAuto ].
+ EApply ex3_2_intro; [ Rewrite lift_bref_lt | Idtac | EApply ty0_abbr ]; XEAuto.
+(* case 3.2 : n = d0 *)
+ Rewrite H6 in H0; DropDis; Inversion H0.
+(* case 3.3 : n > d0 *)
+ Clear H2 H3 c e t1 t2 u0; DropDis.
+ Pattern 1 n; Rewrite (lt_plus_minus (0) n); [ Idtac | XEAuto ].
+ Arith4c '(0) '(minus n (1)).
+ EApply ex3_2_intro;
+ [ Rewrite lift_bref_ge
+ | Rewrite lift_free; Simpl
+ | Pattern 2 n; Rewrite (minus_x_SO n)
+ ]; XEAuto.
+(* case 4 : ty0_abst *)
+ Apply (lt_eq_gt_e n d0); Intros.
+(* case 4.1 : n < d0 *)
+ DropDis; Rewrite minus_x_Sy in H7; [ DropGenBase | XAuto ].
+ Rewrite (lt_plus_minus n d0) in H5; [ Idtac | XAuto ].
+ DropDis; Rewrite H0; Rewrite H0 in H2; Clear H0 H1 u.
+ IH '(minus d0 (S n)) x1; Clear H1 t.
+ LiftGen; Rewrite <- H0 in H2; Clear H0 x2.
+ Rewrite <- lift_d; [ Idtac | XAuto ].
+ Rewrite <- le_plus_minus; [ Idtac | XAuto ].
+ EApply ex3_2_intro; [ Rewrite lift_bref_lt | Idtac | EApply ty0_abst ]; XEAuto.
+(* case 4.2 : n = d0 *)
+ Rewrite H6 in H0; DropDis; Inversion H0.
+(* case 4.3 : n > d0 *)
+ Clear H2 H3 c e t1 t2 u0; DropDis.
+ Pattern 1 n; Rewrite (lt_plus_minus (0) n); [ Idtac | XEAuto ].
+ Arith4c '(0) '(minus n (1)).
+ EApply ex3_2_intro;
+ [ Rewrite lift_bref_ge
+ | Rewrite lift_free; [ Simpl | Simpl | Idtac ]
+ | Pattern 2 n; Rewrite (minus_x_SO n)
+ ]; XEAuto.
+(* case 5 : ty0_bind *)
+ IH d a; Rewrite H0; Rewrite H0 in H2; Rewrite H0 in H4; Clear H H0 H1 H3 H8 u t.
+ IH '(S d) '(CTail a (Bind b) x0); Rewrite H; Rewrite H in H2; Clear H H0 t3 t4.
+ IH '(S d) '(CTail a (Bind b) x0); Rewrite H; Clear H t0.
+ LiftGen; Rewrite <- H in H2; Clear H x5.
+ LiftTailRwBack; XEAuto.
+(* case 6 : ty0_appl *)
+ IH d a; Rewrite H2; Clear H H1 H2 v.
+ LiftGenBase; Rewrite H in H7; Rewrite H1; Rewrite H1 in H0; Rewrite H2; Clear H H1 H2 u t x1.
+ IH d a; Rewrite H; Clear H w.
+ LiftGen; Rewrite <- H in H1; Clear H x4.
+ LiftTailRwBack; XEAuto.
+(* case 7 : ty0_cast *)
+ Rename u into u0.
+ IH d a; Rewrite H2 in H0; Rewrite H2; Clear H H1 H2 H6 t3 t4.
+ IH d a; Rewrite H; Clear H t0.
+ LiftGen; Rewrite <- H in H1; Clear H x3.
+ LiftTailRwBack; XEAuto.
+ Qed.
+
+ End ty0_gen_cvoid.
+
+ Tactic Definition Ty0GenContext :=
+ Match Context With
+ | [ H: (ty0 ?1 (CTail ?2 (Bind Abbr) ?3) ?4 ?5) |- ? ] ->
+ LApply (ty0_gen_cabbr ?1 (CTail ?2 (Bind Abbr) ?3) ?4 ?5); [ Clear H; Intros H | XAuto ];
+ LApply (H ?2 ?3 (0)); [ Clear H; Intros H | XAuto ];
+ LApply (H (CTail ?2 (Bind Abbr) ?3)); [ Clear H; Intros H | XAuto ];
+ LApply (H ?2); [ Clear H; Intros H | XAuto ];
+ LApply H; [ Clear H; Intros H | XAuto ];
+ XElim H; Intros
+ | [ H: (ty0 ?1 (CTail ?2 (Bind Void) ?3) ?4 ?5) |- ? ] ->
+ LApply (ty0_gen_cvoid ?1 (CTail ?2 (Bind Void) ?3) ?4 ?5); [ Clear H; Intros H | XAuto ];
+ LApply (H ?2 ?3 (0)); [ Clear H; Intros H | XAuto ];
+ LApply (H ?2); [ Clear H; Intros H | XAuto ];
+ LApply H; [ Clear H; Intros H | XAuto ];
+ XElim H; Intros
+ | _ -> Ty0GenBase.
+
+(*#* #start file *)
+
+(*#* #single *)
projects / helm.git / blobdiff