Require subst0_subst0.
Require pr0_subst0.
+Require cpr0_defs.
Require pr2_lift.
+Require pr2_gen.
Require pr3_defs.
-(*#* #caption "main properties of predicate \\texttt{pr3}" *)
+(*#* #caption "main properties of the relation $\\PrT{}{}{}$" *)
(*#* #clauses *)
(*#* #stop file *)
Section pr3_context. (****************************************************)
- Theorem pr3_pr0_pr2_t : (u1,u2:?) (pr0 u1 u2) ->
- (c:?; t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) ->
- (pr3 (CTail c k u1) t1 t2).
- Intros.
- Inversion H0; Clear H0; XAuto.
+ Theorem pr3_pr0_pr2_t: (u1,u2:?) (pr0 u1 u2) ->
+ (c:?; t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) ->
+ (pr3 (CTail c k u1) t1 t2).
+ Intros; Inversion H0; Clear H0; XAuto.
NewInduction i.
-(* case 1 : pr2_delta i = 0 *)
- DropGenBase; Inversion H0; Clear H0 H3 H4 c k.
- Rewrite H5 in H; Clear H5 u2.
+(* case 1 : pr2_delta i = 0 *)
+ DropGenBase; Inversion H0; Clear H0 H4 H5 H6 c k t.
+ Rewrite H7 in H; Clear H7 u2.
Pr0Subst0; XEAuto.
(* case 2 : pr2_delta i > 0 *)
NewInduction k; DropGenBase; XEAuto.
Qed.
- Theorem pr3_pr2_pr2_t : (c:?; u1,u2:?) (pr2 c u1 u2) ->
- (t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) ->
- (pr3 (CTail c k u1) t1 t2).
+ Theorem pr3_pr2_pr2_t: (c:?; u1,u2:?) (pr2 c u1 u2) ->
+ (t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) ->
+ (pr3 (CTail c k u1) t1 t2).
Intros until 1; Inversion H; Clear H; Intros.
-(* case 1 : pr2_pr0 *)
+(* case 1 : pr2_free *)
EApply pr3_pr0_pr2_t; [ Apply H0 | XAuto ].
(* case 2 : pr2_delta *)
- Inversion H; [ XAuto | NewInduction i0 ].
+ Inversion H; [ XAuto | NewInduction i0 ].
(* case 2.1 : i0 = 0 *)
- DropGenBase; Inversion H2; Clear H2.
- Rewrite <- H5; Rewrite H6 in H; Rewrite <- H7 in H3; Clear H5 H6 H7 d0 k u0.
- Subst0Subst0; Arith9'In H4 i; XDEAuto 7.
+ DropGenBase; Inversion H4; Clear H3 H4 H7 t t4.
+ Rewrite <- H9; Rewrite H10 in H; Rewrite <- H11 in H6; Clear H9 H10 H11 d0 k u0.
+ Subst0Subst0; Arith9'In H4 i; Clear H2 H H6 u2.
+ Pr0Subst0; Apply pr3_sing with t2:=x0; XEAuto.
(* case 2.2 : i0 > 0 *)
Clear IHi0; NewInduction k; DropGenBase; XEAuto.
Qed.
- Theorem pr3_pr2_pr3_t : (c:?; u2,t1,t2:?; k:?)
- (pr3 (CTail c k u2) t1 t2) ->
- (u1:?) (pr2 c u1 u2) ->
- (pr3 (CTail c k u1) t1 t2).
+ Theorem pr3_pr2_pr3_t: (c:?; u2,t1,t2:?; k:?)
+ (pr3 (CTail c k u2) t1 t2) ->
+ (u1:?) (pr2 c u1 u2) ->
+ (pr3 (CTail c k u1) t1 t2).
Intros until 1; XElim H; Intros.
-(* case 1 : pr3_r *)
+(* case 1 : pr3_refl *)
XAuto.
-(* case 2 : pr3_u *)
+(* case 2 : pr3_sing *)
EApply pr3_t.
EApply pr3_pr2_pr2_t; [ Apply H2 | Apply H ].
XAuto.
Qed.
-(*#* #start file *)
-
(*#* #caption "reduction inside context items" *)
(*#* #cap #cap t1, t2 #alpha c in E, u1 in V1, u2 in V2, k in z *)
- Theorem pr3_pr3_pr3_t : (c:?; u1,u2:?) (pr3 c u1 u2) ->
- (t1,t2:?; k:?) (pr3 (CTail c k u2) t1 t2) ->
- (pr3 (CTail c k u1) t1 t2).
-
-(*#* #stop file *)
-
+ Theorem pr3_pr3_pr3_t: (c:?; u1,u2:?) (pr3 c u1 u2) ->
+ (t1,t2:?; k:?) (pr3 (CTail c k u2) t1 t2) ->
+ (pr3 (CTail c k u1) t1 t2).
Intros until 1; XElim H; Intros.
-(* case 1 : pr3_r *)
+(* case 1 : pr3_refl *)
XAuto.
-(* case 2 : pr3_u *)
+(* case 2 : pr3_sing *)
EApply pr3_pr2_pr3_t; [ Apply H1; XAuto | XAuto ].
Qed.
Tactic Definition Pr3Context :=
Match Context With
| [ H1: (pr0 ?2 ?3); H2: (pr2 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
- LApply (pr3_pr0_pr2_t ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
- LApply (H1 ?1 ?5 ?6 ?4); [ Clear H1 H2; Intros | XAuto ]
+ LApply (pr3_pr0_pr2_t ?2 ?3); [ Intros H_x | XAuto ];
+ LApply (H_x ?1 ?5 ?6 ?4); [ Clear H_x H2; Intros | XAuto ]
| [ H1: (pr0 ?2 ?3); H2: (pr3 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
LApply (pr3_pr2_pr3_t ?1 ?3 ?5 ?6 ?4); [ Clear H2; Intros H2 | XAuto ];
- LApply (H2 ?2); [ Clear H1 H2; Intros | XAuto ]
+ LApply (H2 ?2); [ Clear H2; Intros | XAuto ]
| [ H1: (pr2 ?1 ?2 ?3); H2: (pr2 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
- LApply (pr3_pr2_pr2_t ?1 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
- LApply (H1 ?5 ?6 ?4); [ Clear H1 H2; Intros | XAuto ]
+ LApply (pr3_pr2_pr2_t ?1 ?2 ?3); [ Intros H_x | XAuto ];
+ LApply (H_x ?5 ?6 ?4); [ Clear H_x H2; Intros | XAuto ]
| [ H1: (pr2 ?1 ?2 ?3); H2: (pr3 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
LApply (pr3_pr2_pr3_t ?1 ?3 ?5 ?6 ?4); [ Clear H2; Intros H2 | XAuto ];
- LApply (H2 ?2); [ Clear H1 H2; Intros | XAuto ]
+ LApply (H2 ?2); [ Clear H2; Intros | XAuto ]
| [ H1: (pr3 ?1 ?2 ?3); H2: (pr3 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
- LApply (pr3_pr3_pr3_t ?1 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
- LApply (H1 ?5 ?6 ?4); [ Clear H1 H2; Intros | XAuto ].
+ LApply (pr3_pr3_pr3_t ?1 ?2 ?3); [ Intros H_x | XAuto ];
+ LApply (H_x ?5 ?6 ?4); [ Clear H_x H2; Intros | XAuto ].
Section pr3_lift. (*******************************************************)
-(*#* #start file *)
-
(*#* #caption "conguence with lift" *)
(*#* #cap #cap c, t1, t2 #alpha e in D, d in i *)
- Theorem pr3_lift : (c,e:?; h,d:?) (drop h d c e) ->
- (t1,t2:?) (pr3 e t1 t2) ->
- (pr3 c (lift h d t1) (lift h d t2)).
-
-(*#* #stop file *)
-
+ Theorem pr3_lift: (c,e:?; h,d:?) (drop h d c e) ->
+ (t1,t2:?) (pr3 e t1 t2) ->
+ (pr3 c (lift h d t1) (lift h d t2)).
Intros until 2; XElim H0; Intros; XEAuto.
Qed.
Hints Resolve pr3_lift : ltlc.
+ Section pr3_cpr0. (*******************************************************)
+
+ Theorem pr3_cpr0_t: (c1,c2:?) (cpr0 c2 c1) -> (t1,t2:?) (pr3 c1 t1 t2) ->
+ (pr3 c2 t1 t2).
+ Intros until 1; XElim H; Intros.
+(* case 1 : cpr0_refl *)
+ XAuto.
+(* case 2 : cpr0_comp *)
+ Pr3Context; Clear H1.
+ XElim H2; Intros.
+(* case 2.1 : pr3_refl *)
+ XAuto.
+(* case 2.2 : pr3_sing *)
+ EApply pr3_t; [ Idtac | XEAuto ]. Clear H2 H3 c1 c2 t1 t2 t4 u2.
+ Inversion_clear H1.
+(* case 2.2.1 : pr2_free *)
+ XAuto.
+(* case 2.2.1 : pr2_delta *)
+ Cpr0Drop; Pr0Subst0; Apply pr3_sing with t2:=x; XEAuto.
+ Qed.
+
+ End pr3_cpr0.
projects / helm.git / blobdiff