Require pr3_defs.
Require pr3_props.
- Section pr3_gen_void. (***************************************************)
+ Section pr3_gen_lift. (***************************************************)
+
+(*#* #caption "generation lemma for lift" *)
+(*#* #cap #cap c #alpha e in D, t1 in U1, t2 in U2, x in T, d in i *)
+
+ Theorem pr3_gen_lift: (c:?; t1,x:?; h,d:?) (pr3 c (lift h d t1) x) ->
+ (e:?) (drop h d c e) ->
+ (EX t2 | x = (lift h d t2) & (pr3 e t1 t2)).
+ Intros until 1; InsertEq H '(lift h d t1);
+ UnIntro H t1; XElim H; Clear y x; Intros; Rename x into t4.
+(* case 1 : pr3_refl *)
+ XEAuto.
+(* case 2 : pr3_sing *)
+ Rewrite H2 in H; Pr2Gen.
+ LApply (H1 x); [ Clear H1; Intros H1 | XAuto ].
+ LApply (H1 e); [ Clear H1; Intros H1 | XAuto ].
+ XElim H1; XEAuto.
+ Qed.
+
+ End pr3_gen_lift.
+
+ Section pr3_gen_lref. (***************************************************)
+
+ Theorem pr3_gen_lref: (c:?; x:?; n:?) (pr3 c (TLRef n) x) ->
+ x = (TLRef n) \/
+ (EX d u v | (drop n (0) c (CTail d (Bind Abbr) u)) &
+ (pr3 d u v) &
+ x = (lift (S n) (0) v)
+ ).
+ Intros; InsertEq H '(TLRef n); XElim H; Clear y x; Intros.
+(* case 1: pr3_refl *)
+ XAuto.
+(* case 2: pr3_sing *)
+ Rewrite H2 in H; Clear H2 t1; Pr2GenBase.
+(* case 2.1: pr2_free *)
+ XAuto.
+(* case 2.2: pr2_delta *)
+ Rewrite H4 in H0; Clear H1 H4 t2.
+ LApply (pr3_gen_lift c x1 t3 (S n) (0)); [ Clear H0; Intros | XAuto ].
+ LApply (H x0); [ Clear H; Intros | XEAuto ].
+ XElim H; XEAuto.
+ Qed.
+
+ End pr3_gen_lref.
+
+ Section pr3_gen_bind. (***************************************************)
Tactic Definition IH :=
Match Context With
- [ H: (u,t:T) (TTail (Bind Void) ?1 ?2) = (TTail (Bind Void) u t) -> ? |- ? ] ->
+ | [ H: (u,t:T) (TTail (Bind Void) ?1 ?2) = (TTail (Bind Void) u t) -> ? |- ? ] ->
LApply (H ?1 ?2); [ Clear H; Intros H | XAuto ];
- XElim H1; Intros H1; XElim H1; Intros.
-
- Theorem pr3_gen_void : (c:?; u1,t1,x:?) (pr3 c (TTail (Bind Void) u1 t1) x) ->
- (EX u2 t2 | x = (TTail (Bind Void) u2 t2) &
- (pr3 c u1 u2) & (b:?; u:?)
- (pr3 (CTail c (Bind b) u) t1 t2)
- ) \/
- (EX u | (pr3 c u1 u) &
- (pr3 (CTail c (Bind Void) u) t1 (lift (1) (0) x))
- ).
+ XDecompose H
+ | [ H: (u,t:T) (TTail (Bind Abbr) ?1 ?2) = (TTail (Bind Abbr) u t) -> ? |- ? ] ->
+ LApply (H ?1 ?2); [ Clear H; Intros H | XAuto ];
+ XDecompose H.
+
+ Theorem pr3_gen_void: (c:?; u1,t1,x:?) (pr3 c (TTail (Bind Void) u1 t1) x) ->
+ (EX u2 t2 | x = (TTail (Bind Void) u2 t2) &
+ (pr3 c u1 u2) & (b:?; u:?)
+ (pr3 (CTail c (Bind b) u) t1 t2)
+ ) \/
+ (pr3 (CTail c (Bind Void) u1) t1 (lift (1) (0) x)).
Intros until 1; InsertEq H '(TTail (Bind Void) u1 t1);
UnIntro t1 H; UnIntro u1 H; XElim H; Intros.
-(* case 1 : pr3_r *)
+(* case 1 : pr3_refl *)
Rewrite H; XEAuto.
-(* case 2 : pr3_u *)
+(* case 2 : pr3_sing *)
Rewrite H2 in H; Clear H2 t0; Pr2Gen.
(* case 2.1 : short step: compatibility *)
- Rewrite H in H0; Rewrite H in H1; Clear H t2; IH.
-(* case 2.1.1 : long step: compatibility *)
- Rewrite H; Rewrite H in H0; XEAuto.
-(* case 2.1.2 : long step: zeta *)
- XEAuto.
+ Rewrite H3 in H1; Clear H0 H3 t2.
+ IH; Try Pr3Context; Try Rewrite H2; XEAuto.
(* case 2.2 : short step: zeta *)
- Clear H1; Right.
- EApply ex2_intro; [ XAuto | Idtac ].
- EApply pr3_u; [ Idtac | EApply pr3_lift ].
- XEAuto. XAuto. XAuto.
+ XEAuto.
Qed.
- End pr3_gen_void.
-
- Section pr3_gen_abbr. (***************************************************)
-
- Tactic Definition IH :=
- LApply (H1 x0 x1); [ Clear H1; Intros H1 | XAuto ];
- XElim H1;
- [ Intros H1; XElim H1;
- Do 4 Intro; Intros H_x; XElim H_x;
- [ Intros | Intros H_x; XElim H_x; Intros ]
- | Intros H1; XElim H1; Intros ].
-
- Theorem pr3_gen_abbr : (c:?; u1,t1,x:?) (pr3 c (TTail (Bind Abbr) u1 t1) x) ->
- (EX u2 t2 | x = (TTail (Bind Abbr) u2 t2) &
- (pr3 c u1 u2) &
- ((b:?; u:?) (pr3 (CTail c (Bind b) u) t1 t2)) \/
- (EX u3 t3 y | (pr3 c (TTail (Bind Abbr) u3 t3) x) &
- (pr3 c u1 u3) &
- (b:?; u:?) (pr3 (CTail c (Bind b) u) t1 y) &
- (subst0 (0) u3 y t3)
- )
- ) \/
- (EX u | (pr3 c u1 u) &
- (pr3 (CTail c (Bind Abbr) u) t1 (lift (1) (0) x))
- ).
+ Theorem pr3_gen_abbr: (c:?; u1,t1,x:?) (pr3 c (TTail (Bind Abbr) u1 t1) x) ->
+ (EX u2 t2 | x = (TTail (Bind Abbr) u2 t2) &
+ (pr3 c u1 u2) &
+ (pr3 (CTail c (Bind Abbr) u1) t1 t2)
+ ) \/
+ (pr3 (CTail c (Bind Abbr) u1) t1 (lift (1) (0) x)).
Intros until 1; InsertEq H '(TTail (Bind Abbr) u1 t1);
UnIntro H t1; UnIntro H u1; XElim H; Clear y x; Intros;
Rename x into u1; Rename x0 into t4.
-(* case 1 : pr3_r *)
+(* case 1: pr3_refl *)
Rewrite H; XEAuto.
-(* case 2 : pr3_u *)
+(* case 2: pr3_sing *)
Rewrite H2 in H; Clear H2 t1; Pr2Gen.
-(* case 2.1 : short step: compatibility *)
- Rewrite H in H0; Rewrite H in H1; Clear H t2; IH.
-(* case 2.1.1 : long step: compatibility *)
- Rewrite H; Rewrite H in H0; Clear H t3.
- Left; EApply ex3_2_intro; XEAuto.
-(* case 2.1.2 : long step: delta *)
- Rewrite H; Rewrite H in H0; Rewrite H in H4; Clear H t3.
- Left; EApply ex3_2_intro;
- [ XEAuto | XEAuto
- | Right; EApply ex4_3_intro;
- [ EApply pr3_t; [ XAuto | Apply H4 ] | XEAuto | Idtac | Apply H7 ] ].
+(* case 2.1: short step: compatibility *)
+ Rewrite H3 in H1; Clear H0 H3 t2.
+ IH; Repeat Pr3Context;
+ Try (Rewrite H0; Clear H0 t3; Left; EApply ex3_2_intro);
XEAuto.
-(* case 2.1.3 : long step: zeta *)
+(* case 2.2: short step: beta *)
+ Rewrite H3 in H1; Clear H0 H3 t1.
+ IH; Repeat Pr3Context;
+ Try (Rewrite H0; Clear H0 t3; Left; EApply ex3_2_intro);
XEAuto.
-(* case 2.2 : short step: delta *)
- Rewrite H in H0; Rewrite H in H1; Clear H t2; IH.
-(* case 2.2.1 : long step: compatibility *)
- Left; EApply ex3_2_intro;
- [ XEAuto | XEAuto
- | Right; EApply ex4_3_intro; [ Rewrite H | Idtac | Idtac | Apply H4 ] ].
- XAuto. XAuto. XAuto.
-(* case 2.2.2 : long step: delta *)
- Left; EApply ex3_2_intro;
- [ XEAuto | XEAuto
- | Right; EApply ex4_3_intro;
- [ EApply pr3_t; [ Apply pr3_tail_12 | Apply H5 ]
- | Idtac | Idtac | Apply H4 ] ].
- XAuto. EApply pr3_t; [ Apply H7 | XEAuto ]. XAuto. XAuto.
-(* case 2.2.3 : long step: zeta *)
- Right; Apply ex2_intro with x := x0; [ XAuto | Idtac ].
- Apply pr3_u with t2 := x; [ XAuto | Idtac ].
- Apply pr3_u with t2 := x1; [ XEAuto | Idtac ].
- Pr3Context; XAuto.
-(* case 2.3 : short step: zeta *)
- Clear H1; Right.
- EApply ex2_intro; [ XAuto | Idtac ].
- EApply pr3_u; [ Idtac | EApply pr3_lift ].
- XEAuto. XAuto. XAuto.
- Qed.
-
- End pr3_gen_abbr.
-
- Section pr3_gen_abst. (***************************************************)
-
- Theorem pr3_gen_abst : (c:?; u1,t1,x:?)
- (pr3 c (TTail (Bind Abst) u1 t1) x) ->
- (EX u2 t2 | x = (TTail (Bind Abst) u2 t2) &
- (pr3 c u1 u2) & (b:?; u:?)
- (pr3 (CTail c (Bind b) u) t1 t2)
- ).
- Intros until 1; InsertEq H '(TTail (Bind Abst) u1 t1);
- UnIntro H t1; UnIntro H u1; XElim H; Clear y x; Intros;
- Rename x into u1; Rename x0 into t4.
-(* case 1 : pr3_r *)
- Rewrite H; XEAuto.
-(* case 2 : pr3_u *)
- Rewrite H2 in H; Clear H2 t1.
- Pr2GenBase.
- LApply (H1 x0 x1); [ Clear H H1; Intros | XAuto ].
- XElim H; XEAuto.
- Qed.
-
- End pr3_gen_abst.
-
- Section pr3_gen_lift. (***************************************************)
-
-(*#* #start file *)
-
-(*#* #caption "generation lemma for lift" *)
-(*#* #cap #cap c #alpha e in D, t1 in U1, t2 in U2, x in T, d in i *)
-
- Theorem pr3_gen_lift : (c:?; t1,x:?; h,d:?) (pr3 c (lift h d t1) x) ->
- (e:?) (drop h d c e) ->
- (EX t2 | x = (lift h d t2) & (pr3 e t1 t2)).
-
-(*#* #stop file *)
-
- Intros until 1; InsertEq H '(lift h d t1);
- UnIntro H t1; XElim H; Clear y x; Intros; Rename x into t4.
-(* case 1 : pr3_r *)
+(* case 2.3: short step: delta *)
+ Rewrite H3 in H1; Clear H0 H3 t2.
+ IH; Repeat Pr3Context;
+ Try (Rewrite H0; Clear H0 t3; Left; EApply ex3_2_intro);
+ XDEAuto 7.
+(* case 2.4: short step: zeta *)
XEAuto.
-(* case 2 : pr3_u *)
- Rewrite H2 in H; Pr2Gen.
- LApply (H1 x); [ Clear H1; Intros H1 | XAuto ].
- LApply (H1 e); [ Clear H1; Intros H1 | XAuto ].
- XElim H1; XEAuto.
Qed.
- End pr3_gen_lift.
+ End pr3_gen_bind.
Tactic Definition Pr3Gen :=
Match Context With
- | [ H: (pr3 ?1 (TTail (Bind Abst) ?2 ?3) ?4) |- ? ] ->
- LApply (pr3_gen_abst ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
- XElim H; Intros
- | [ H: (pr3 ?1 (TTail (Bind Abbr) ?2 ?3) ?4) |- ? ] ->
- LApply (pr3_gen_abbr ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
- XElim H;
- [ Intros H; XElim H;
- Do 4 Intro; Intros H_x; XElim H_x;
- [ Intros | Intros H_x; XElim H_x; Intros ]
- | Intros H; XElim H; Intros ]
+ | [ H: (pr3 ?1 (TLRef ?2) ?3) |- ? ] ->
+ LApply (pr3_gen_lref ?1 ?3 ?2); [ Clear H; Intros H | XAuto ];
+ XDecompose H
| [ H: (pr3 ?1 (TTail (Bind Void) ?2 ?3) ?4) |- ? ] ->
LApply (pr3_gen_void ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
- XElim H; Intros H; XElim H; Intros
+ XDecompose H
+ | [ H: (pr3 ?1 (TTail (Bind Abbr) ?2 ?3) ?4) |- ? ] ->
+ LApply (pr3_gen_abbr ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
+ XDecompose H
| [ H0: (pr3 ?1 (lift ?2 ?3 ?4) ?5);
H1: (drop ?2 ?3 ?1 ?6) |- ? ] ->
LApply (pr3_gen_lift ?1 ?4 ?5 ?2 ?3); [ Clear H0; Intros H0 | XAuto ];
LApply (H0 ?6); [ Clear H0; Intros H0 | XAuto ];
- XElim H0; Intros
- | _ -> Pr2Gen.
+ XDecompose H0
+ | _ -> Pr3GenBase.
projects / helm.git / blobdiff