-LambdaDelta.vo: LambdaDelta.v terms_defs.vo tlt_defs.vo contexts_defs.vo lift_defs.vo lift_gen.vo lift_props.vo lift_tlt.vo subst0_defs.vo subst0_gen.vo subst0_lift.vo subst0_subst0.vo subst0_confluence.vo subst0_tlt.vo subst1_defs.vo subst1_gen.vo subst1_lift.vo subst1_subst1.vo subst1_confluence.vo drop_defs.vo drop_props.vo csubst0_defs.vo csubst1_defs.vo pr0_defs.vo pr0_lift.vo pr0_gen.vo pr0_subst0.vo pr0_confluence.vo pr0_subst1.vo pr1_defs.vo pr1_confluence.vo pr2_defs.vo pr2_lift.vo pr2_gen.vo pr2_confluence.vo pr2_subst1.vo pr2_gen_context.vo pr3_defs.vo pr3_props.vo pr3_gen.vo pr3_confluence.vo pr3_subst1.vo pr3_gen_context.vo cpr0_defs.vo cpr0_props.vo pc1_defs.vo pc3_defs.vo pc3_props.vo pc3_gen.vo pc3_subst0.vo pc3_gen_context.vo ty0_defs.vo ty0_lift.vo ty0_props.vo ty0_subst0.vo ty0_gen_context.vo csub0_defs.vo ty0_sred.vo ty0_sred_props.vo
+LambdaDelta.vo: LambdaDelta.v base_tactics.vo base_hints.vo base_types.vo base_blt.vo base_rewrite.vo Base.vo terms_defs.vo tlt_defs.vo contexts_defs.vo lift_defs.vo lift_gen.vo lift_props.vo lift_tlt.vo drop_defs.vo drop_props.vo subst0_defs.vo subst0_gen.vo subst0_lift.vo subst0_subst0.vo subst0_confluence.vo subst0_tlt.vo subst1_defs.vo subst1_gen.vo subst1_lift.vo subst1_subst1.vo subst1_confluence.vo csubst0_defs.vo csubst1_defs.vo fsubst0_defs.vo pr0_defs.vo pr0_lift.vo pr0_gen.vo pr0_subst0.vo pr0_confluence.vo pr0_subst1.vo pr1_defs.vo pr1_confluence.vo cpr0_defs.vo pr2_defs.vo pr2_lift.vo pr2_gen.vo pr2_confluence.vo pr2_subst1.vo pr2_gen_context.vo pr3_defs.vo pr3_props.vo pr3_gen.vo pr3_confluence.vo pr3_subst1.vo pr3_gen_context.vo pc1_defs.vo pc3_defs.vo pc3_props.vo pc3_gen.vo pc3_subst0.vo pc3_gen_context.vo ty0_defs.vo ty0_lift.vo ty0_props.vo ty0_subst0.vo ty0_gen_context.vo csub0_defs.vo ty0_sred.vo ty0_sred_props.vo
ty0_sred_props.vo: ty0_sred_props.v lift_props.vo drop_props.vo pc3_props.vo pc3_gen.vo ty0_defs.vo ty0_props.vo ty0_sred.vo
-ty0_sred.vo: ty0_sred.v lift_gen.vo subst1_gen.vo csubst1_defs.vo pr0_lift.vo pr0_subst1.vo cpr0_defs.vo cpr0_props.vo pc3_props.vo pc3_gen.vo ty0_defs.vo ty0_lift.vo ty0_props.vo ty0_subst0.vo ty0_gen_context.vo csub0_defs.vo
+ty0_sred.vo: ty0_sred.v lift_gen.vo subst1_gen.vo csubst1_defs.vo pr0_lift.vo pr0_subst1.vo cpr0_defs.vo pc3_props.vo pc3_gen.vo ty0_defs.vo ty0_lift.vo ty0_props.vo ty0_subst0.vo ty0_gen_context.vo csub0_defs.vo
csub0_defs.vo: csub0_defs.v ty0_defs.vo
ty0_gen_context.vo: ty0_gen_context.v lift_gen.vo lift_props.vo subst1_defs.vo subst1_lift.vo subst1_confluence.vo drop_props.vo csubst1_defs.vo pc3_gen.vo pc3_gen_context.vo ty0_defs.vo ty0_lift.vo
-ty0_subst0.vo: ty0_subst0.v drop_props.vo csubst0_defs.vo pc3_props.vo pc3_subst0.vo ty0_defs.vo ty0_lift.vo ty0_props.vo
+ty0_subst0.vo: ty0_subst0.v drop_props.vo csubst0_defs.vo fsubst0_defs.vo pc3_props.vo pc3_subst0.vo ty0_defs.vo ty0_lift.vo ty0_props.vo
ty0_props.vo: ty0_props.v drop_props.vo pc3_props.vo ty0_defs.vo ty0_lift.vo
ty0_lift.vo: ty0_lift.v lift_props.vo drop_props.vo pc3_props.vo ty0_defs.vo
ty0_defs.vo: ty0_defs.v pc3_defs.vo
pc3_gen_context.vo: pc3_gen_context.v subst1_confluence.vo csubst1_defs.vo pr3_gen_context.vo pc3_defs.vo pc3_props.vo
-pc3_subst0.vo: pc3_subst0.v subst0_subst0.vo csubst0_defs.vo pr0_subst0.vo pc3_defs.vo
+pc3_subst0.vo: pc3_subst0.v subst0_subst0.vo fsubst0_defs.vo pr0_subst0.vo pc3_defs.vo
pc3_gen.vo: pc3_gen.v lift_gen.vo pr3_props.vo pr3_gen.vo pc3_defs.vo pc3_props.vo
-pc3_props.vo: pc3_props.v subst0_subst0.vo pr0_subst0.vo pr3_defs.vo pr3_props.vo pr3_confluence.vo cpr0_defs.vo cpr0_props.vo pc3_defs.vo
+pc3_props.vo: pc3_props.v subst0_subst0.vo pr0_subst0.vo cpr0_defs.vo pr3_defs.vo pr3_props.vo pr3_confluence.vo pc3_defs.vo
pc3_defs.vo: pc3_defs.v pr2_defs.vo pr3_defs.vo pc1_defs.vo
pc1_defs.vo: pc1_defs.v pr0_defs.vo
-cpr0_props.vo: cpr0_props.v pr0_subst0.vo pr3_defs.vo pr3_props.vo cpr0_defs.vo
-cpr0_defs.vo: cpr0_defs.v contexts_defs.vo pr0_defs.vo
pr3_gen_context.vo: pr3_gen_context.v csubst1_defs.vo pr2_gen_context.vo pr3_defs.vo
pr3_subst1.vo: pr3_subst1.v subst1_defs.vo pr2_subst1.vo pr3_defs.vo
pr3_confluence.vo: pr3_confluence.v pr2_confluence.vo pr3_defs.vo
pr3_gen.vo: pr3_gen.v pr2_gen.vo pr3_defs.vo pr3_props.vo
-pr3_props.vo: pr3_props.v subst0_subst0.vo pr0_subst0.vo pr2_lift.vo pr3_defs.vo
+pr3_props.vo: pr3_props.v subst0_subst0.vo pr0_subst0.vo cpr0_defs.vo pr2_lift.vo pr2_gen.vo pr3_defs.vo
pr3_defs.vo: pr3_defs.v pr1_defs.vo pr2_defs.vo
-pr2_gen_context.vo: pr2_gen_context.v drop_props.vo subst1_gen.vo subst1_subst1.vo subst1_confluence.vo csubst1_defs.vo pr0_gen.vo pr0_subst1.vo pr2_defs.vo pr2_subst1.vo
+pr2_gen_context.vo: pr2_gen_context.v drop_props.vo subst1_gen.vo subst1_subst1.vo subst1_confluence.vo csubst1_defs.vo pr0_gen.vo pr0_subst1.vo pr2_defs.vo pr2_gen.vo pr2_subst1.vo
pr2_subst1.vo: pr2_subst1.v subst1_defs.vo subst1_confluence.vo drop_props.vo pr0_subst1.vo pr2_defs.vo
pr2_confluence.vo: pr2_confluence.v subst0_confluence.vo drop_props.vo pr0_subst0.vo pr0_confluence.vo pr2_defs.vo
-pr2_gen.vo: pr2_gen.v subst0_gen.vo drop_props.vo pr0_gen.vo pr2_defs.vo
+pr2_gen.vo: pr2_gen.v subst0_gen.vo subst0_lift.vo drop_props.vo pr0_gen.vo pr0_subst0.vo pr2_defs.vo
pr2_lift.vo: pr2_lift.v subst0_lift.vo drop_props.vo pr0_lift.vo pr2_defs.vo
pr2_defs.vo: pr2_defs.v drop_defs.vo pr0_defs.vo
+cpr0_defs.vo: cpr0_defs.v contexts_defs.vo drop_defs.vo pr0_defs.vo
pr1_confluence.vo: pr1_confluence.v pr0_confluence.vo pr1_defs.vo
pr1_defs.vo: pr1_defs.v pr0_defs.vo
pr0_subst1.vo: pr0_subst1.v subst1_defs.vo pr0_defs.vo pr0_subst0.vo
pr0_gen.vo: pr0_gen.v lift_gen.vo lift_props.vo subst0_gen.vo pr0_defs.vo pr0_lift.vo
pr0_lift.vo: pr0_lift.v lift_props.vo subst0_lift.vo pr0_defs.vo
pr0_defs.vo: pr0_defs.v subst0_defs.vo
+fsubst0_defs.vo: fsubst0_defs.v subst0_defs.vo csubst0_defs.vo
csubst1_defs.vo: csubst1_defs.v subst1_defs.vo csubst0_defs.vo
csubst0_defs.vo: csubst0_defs.v contexts_defs.vo subst0_defs.vo drop_defs.vo
-drop_props.vo: drop_props.v lift_gen.vo drop_defs.vo
-drop_defs.vo: drop_defs.v contexts_defs.vo lift_defs.vo
subst1_confluence.vo: subst1_confluence.v lift_gen.vo subst0_gen.vo subst0_confluence.vo subst1_defs.vo subst1_gen.vo
subst1_subst1.vo: subst1_subst1.v subst0_subst0.vo subst1_defs.vo
subst1_lift.vo: subst1_lift.v lift_props.vo subst0_lift.vo subst1_defs.vo
subst0_lift.vo: subst0_lift.v lift_props.vo subst0_defs.vo
subst0_gen.vo: subst0_gen.v lift_props.vo subst0_defs.vo
subst0_defs.vo: subst0_defs.v lift_defs.vo
+drop_props.vo: drop_props.v lift_gen.vo drop_defs.vo
+drop_defs.vo: drop_defs.v contexts_defs.vo lift_defs.vo
lift_tlt.vo: lift_tlt.v tlt_defs.vo lift_defs.vo
lift_props.vo: lift_props.v lift_defs.vo
lift_gen.vo: lift_gen.v lift_defs.vo
Hint f3CKT : ltlc := Resolve (f_equal3 C K T).
+ Tactic Definition CGenBase :=
+ Match Context With
+ | [ H: (CTail ? ? ?) = (CTail ? ? ?) |- ? ] -> Inversion H; Clear H
+ | _ -> TGenBase.
+
Definition r: K -> nat -> nat := [k;i] Cases k of
| (Bind _) => i
| (Flat _) => (S i)
-(*#* #stop file *)
-
Require Export contexts_defs.
+Require Export drop_defs.
Require Export pr0_defs.
+(*#* #caption "current axioms for the relation $\\CprZ{}{}$",
+ "reflexivity", "compaibility"
+*)
+(*#* #cap #cap c, c1, c2 #alpha u1 in V1, u2 in V2, k in z *)
+
Inductive cpr0 : C -> C -> Prop :=
| cpr0_refl : (c:?) (cpr0 c c)
- | cpr0_cont : (c1,c2:?) (cpr0 c1 c2) -> (u1,u2:?) (pr0 u1 u2) ->
+ | cpr0_comp : (c1,c2:?) (cpr0 c1 c2) -> (u1,u2:?) (pr0 u1 u2) ->
(k:?) (cpr0 (CTail c1 k u1) (CTail c2 k u2)).
+(*#* #stop file *)
+
Hint cpr0 : ltlc := Constructors cpr0.
+
+ Section cpr0_drop. (******************************************************)
+
+ Theorem cpr0_drop : (c1,c2:?) (cpr0 c1 c2) -> (h:?; e1:?; u1:?; k:?)
+ (drop h (0) c1 (CTail e1 k u1)) ->
+ (EX e2 u2 | (drop h (0) c2 (CTail e2 k u2)) &
+ (cpr0 e1 e2) & (pr0 u1 u2)
+ ).
+ Intros until 1; XElim H.
+(* case 1 : cpr0_refl *)
+ XEAuto.
+(* case 2 : cpr0_comp *)
+ XElim h.
+(* case 2.1 : h = 0 *)
+ Intros; DropGenBase.
+ Inversion H2; Rewrite H6 in H1; Rewrite H4 in H; XEAuto.
+(* case 2.2 : h > 0 *)
+ XElim k; Intros; DropGenBase.
+(* case 2.2.1 : Bind *)
+ LApply (H0 n e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ].
+ XElim H0; XEAuto.
+(* case 2.2.2 : Flat *)
+ LApply (H0 (S n) e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ].
+ XElim H0; XEAuto.
+ Qed.
+
+ Theorem cpr0_drop_back : (c1,c2:?) (cpr0 c2 c1) -> (h:?; e1:?; u1:?; k:?)
+ (drop h (0) c1 (CTail e1 k u1)) ->
+ (EX e2 u2 | (drop h (0) c2 (CTail e2 k u2)) &
+ (cpr0 e2 e1) & (pr0 u2 u1)
+ ).
+ Intros until 1; XElim H.
+(* case 1 : cpr0_refl *)
+ XEAuto.
+(* case 2 : cpr0_comp *)
+ XElim h.
+(* case 2.1 : h = 0 *)
+ Intros; DropGenBase.
+ Inversion H2; Rewrite H6 in H1; Rewrite H4 in H; XEAuto.
+(* case 2.2 : h > 0 *)
+ XElim k; Intros; DropGenBase.
+(* case 2.2.1 : Bind *)
+ LApply (H0 n e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ].
+ XElim H0; XEAuto.
+(* case 2.2.2 : Flat *)
+ LApply (H0 (S n) e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ].
+ XElim H0; XEAuto.
+ Qed.
+
+ End cpr0_drop.
+
+ Tactic Definition Cpr0Drop :=
+ Match Context With
+ | [ _: (drop ?1 (0) ?2 (CTail ?3 ?4 ?5));
+ _: (cpr0 ?2 ?6) |- ? ] ->
+ LApply (cpr0_drop ?2 ?6); [ Intros H_x | XAuto ];
+ LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ];
+ XElim H_x; Intros
+ | [ _: (drop ?1 (0) ?2 (CTail ?3 ?4 ?5));
+ _: (cpr0 ?6 ?2) |- ? ] ->
+ LApply (cpr0_drop_back ?2 ?6); [ Intros H_x | XAuto ];
+ LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ];
+ XElim H_x; Intros
+ | [ _: (drop ?1 (0) (CTail ?2 ?7 ?8) (CTail ?3 ?4 ?5));
+ _: (cpr0 ?2 ?6) |- ? ] ->
+ LApply (cpr0_drop (CTail ?2 ?7 ?8) (CTail ?6 ?7 ?8)); [ Intros H_x | XAuto ];
+ LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ];
+ XElim H_x; Intros
+ | [ _: (drop ?1 (0) (CTail ?2 ?7 ?8) (CTail ?3 ?4 ?5));
+ _: (cpr0 ?6 ?2) |- ? ] ->
+ LApply (cpr0_drop_back (CTail ?2 ?7 ?8) (CTail ?6 ?7 ?8)); [ Intros H_x | XAuto ];
+ LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ];
+ XElim H_x; Intros.
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 *)
+(* case 1 : pr2_free *)
XAuto.
(* case 2 : pr2_delta *)
CSub0Drop; XEAuto.
-(*#* #stop file *)
-
Require Export contexts_defs.
Require Export subst0_defs.
Require Export drop_defs.
+(*#* #caption "current axioms for strict substitution in contexts",
+ "substituted tail item: second operand",
+ "substituted tail item: first operand",
+ "substituted tail item: both operands"
+*)
+(*#* #cap #cap c, c1, c2 #alpha v in W, u in V, u1 in V1, u2 in V2, k in z, r in q *)
+
Inductive csubst0 : nat -> T -> C -> C -> Prop :=
- | csubst0_fst : (k:?; i:?; u,v,w:?) (subst0 (r k i) v u w) -> (c:?)
- (csubst0 (S i) v (CTail c k u) (CTail c k w))
- | csubst0_snd : (k:?; i:?; c1,c2:?; v:?) (csubst0 (r k i) v c1 c2) ->
+ | csubst0_snd : (k:?; i:?; v,u1,u2:?) (subst0 (r k i) v u1 u2) -> (c:?)
+ (csubst0 (S i) v (CTail c k u1) (CTail c k u2))
+ | csubst0_fst : (k:?; i:?; c1,c2:?; v:?) (csubst0 (r k i) v c1 c2) ->
(u:?) (csubst0 (S i) v (CTail c1 k u) (CTail c2 k u))
- | csubst0_both : (k:?; i:?; u,v,w:?) (subst0 (r k i) v u w) ->
+ | csubst0_both : (k:?; i:?; v,u1,u2:?) (subst0 (r k i) v u1 u2) ->
(c1,c2:?) (csubst0 (r k i) v c1 c2) ->
- (csubst0 (S i) v (CTail c1 k u) (CTail c2 k w)).
+ (csubst0 (S i) v (CTail c1 k u1) (CTail c2 k u2)).
- Hint csubst0 : ltlc := Constructors csubst0.
-
- Inductive fsubst0 [i:nat; v:T; c1:C; t1:T] : C -> T -> Prop :=
- | fsubst0_t : (t2:?) (subst0 i v t1 t2) -> (fsubst0 i v c1 t1 c1 t2)
- | fsubst0_c : (c2:?) (csubst0 i v c1 c2) -> (fsubst0 i v c1 t1 c2 t1)
- | fsubst0_b : (t2:?) (subst0 i v t1 t2) ->
- (c2:?) (csubst0 i v c1 c2) -> (fsubst0 i v c1 t1 c2 t2).
+(*#* #stop file *)
- Hint fsubst0 : ltlc := Constructors fsubst0.
+ Hint csubst0 : ltlc := Constructors csubst0.
Section csubst0_gen_base. (***********************************************)
)).
Intros until 1; InsertEq H '(S i); InsertEq H '(CTail c1 k u1).
XCase H; Clear x v y y0; Intros; Inversion H1.
-(* case 1: csubst0_fst *)
+(* case 1: csubst0_snd *)
Inversion H0; Rewrite H3 in H; Rewrite H5 in H; Rewrite H6 in H; XEAuto.
-(* case 2: csubst0_snd *)
+(* case 2: csubst0_fst *)
Inversion H0; Rewrite H3 in H; Rewrite H4 in H; Rewrite H5 in H; XEAuto.
(* case 2: csubst0_both *)
Inversion H2; Rewrite H5 in H; Rewrite H6 in H; Rewrite H7 in H;
(* case 2.2: n > 0 *)
Intros until 3; Clear H0; InsertEq H2 '(S i); XElim H0; Intros.
DropGenBase.
-(* case 2.2.1: csubst0_fst *)
+(* case 2.2.1: csubst0_snd *)
XAuto.
-(* case 2.2.2: csubst0_snd *)
+(* case 2.2.2: csubst0_fst *)
XReplaceIn H0 i0 i; DropGenBase; NewInduction k; XEAuto.
(* case 2.2.3: csubst0_both *)
XReplaceIn H0 i0 i; XReplaceIn H2 i0 i.
(* case 2.2: n > 0 *)
Intros until 3; Clear H0; InsertEq H2 '(S i); XElim H0; Clear c1 c2 v y;
Intros; DropGenBase.
-(* case 2.2.1: csubst0_fst *)
+(* case 2.2.1: csubst0_snd *)
XEAuto.
-(* case 2.2.2: csubst0_snd *)
+(* case 2.2.2: csubst0_fst *)
Replace i0 with i; XAuto; XReplaceIn H0 i0 i; XReplaceIn H2 i0 i; Clear H3 i0.
Apply (r_dis k); Intros; Rewrite (H3 i) in H0; Rewrite (H3 n) in H4.
(* case 2.2.2.1: bind *)
(* case 2.2 : n > 0 *)
Intros until 3; Clear H0; InsertEq H2 '(S i); XElim H0; Intros;
DropGenBase.
-(* case 2.2.1 : csubst0_fst *)
+(* case 2.2.1 : csubst0_snd *)
XAuto.
-(* case 2.2.2 : csubst0_snd *)
+(* case 2.2.2 : csubst0_fst *)
XReplaceIn H0 i0 i; NewInduction k; XEAuto.
(* case 2.2.3 : csubst0_both *)
XReplaceIn H0 i0 i; XReplaceIn H2 i0 i; NewInduction k; XEAuto.
-(*#* #stop file *)
-
Require Export contexts_defs.
Require Export lift_defs.
+(*#* #caption "current axioms for dropping",
+ "base case", "untouched tail item",
+ "dropped tail item", "updated tail item"
+*)
+(*#* #cap #alpha c in C1, e in C2, u in V, k in z, n in k, d in i, r in q *)
+
Inductive drop : nat -> nat -> C -> C -> Prop :=
| drop_sort : (h,d,n:?) (drop h d (CSort n) (CSort n))
- | drop_tail : (c,e:?) (drop (0) (0) c e) ->
+ | drop_comp : (c,e:?) (drop (0) (0) c e) ->
(k:?; u:?) (drop (0) (0) (CTail c k u) (CTail e k u))
| drop_drop : (k:?; h:?; c,e:?) (drop (r k h) (0) c e) ->
(u:?) (drop (S h) (0) (CTail c k u) e)
| drop_skip : (k:?; h,d:?; c,e:?) (drop h (r k d) c e) -> (u:?)
(drop h (S d) (CTail c k (lift h (r k d) u)) (CTail e k u)).
+(*#* #stop file *)
+
Hint drop : ltlc := Constructors drop.
Hint discr : ltlc := Extern 4 (drop ? ? ? ?) Simpl.
Intros until 1; Repeat InsertEq H '(0); XElim H; Intros.
(* case 1 : drop_sort *)
XAuto.
-(* case 2 : drop_tail *)
+(* case 2 : drop_comp *)
Rewrite H0; XAuto.
(* case 3 : drop_drop *)
Inversion H2.
XElim H; Intros.
(* case 1 : drop_sort *)
Inversion H1.
-(* case 2 : drop_tail *)
+(* case 2 : drop_comp *)
Inversion H1.
(* case 3 : drop_drop *)
Inversion H1; Inversion H3.
+(*#* #stop file *)
+
Require lift_gen.
Require drop_defs.
Section confluence. (*****************************************************)
-(*#* #stop macro *)
-
Tactic Definition IH :=
Match Context With
[ H1: (drop ?1 ?2 c ?3); H2: (drop ?1 ?2 c ?4) |- ? ] ->
LApply (H ?4 ?2 ?1); [ Clear H H2; Intros H | XAuto ];
LApply (H ?3); [ Clear H H1; Intros | XAuto ].
-(*#* #start macro *)
-
(*#* #caption "confluence, first case" *)
(*#* #cap #alpha c in C, x1 in C1, x2 in C2, d in i *)
Theorem drop_mono : (c,x1:?; d,h:?) (drop h d c x1) ->
(x2:?) (drop h d c x2) -> x1 = x2.
-
-(*#* #stop proof *)
-
XElim c.
(* case 1: CSort *)
Intros; Repeat DropGenBase; Rewrite H0; XAuto.
LiftGen; IH; XAuto.
Qed.
-(*#* #start proof *)
-
(*#* #caption "confluence, second case" *)
(*#* #cap #alpha c in C1, c0 in E1, e in C2, e0 in E2, u in V1, v in V2, i in k, d in i *)
(drop i (0) e (CTail e0 (Bind b) v)) &
(drop h d c0 e0)
).
-
-(*#* #stop proof *)
-
XElim i.
(* case 1 : i = 0 *)
Intros until 1.
XElim H; XEAuto.
Qed.
-(*#* #start proof *)
-
(*#* #caption "confluence, third case" *)
(*#* #cap #alpha c in C, a in C1, e in C2, i in k, d in i *)
Theorem drop_conf_ge: (i:?; a,c:?) (drop i (0) c a) ->
(e:?; h,d:?) (drop h d c e) -> (le (plus d h) i) ->
(drop (minus i h) (0) e a).
-
-(*#* #stop proof *)
-
XElim i.
(* case 1 : i = 0 *)
Intros until 1.
Rewrite <- minus_Sn_m; XEAuto.
Qed.
-(*#* #start proof *)
-
End confluence.
Section transitivity. (***************************************************)
(c1,c2:?; h:?) (drop h d c1 c2) ->
(e2:?) (drop i (0) c2 e2) ->
(EX e1 | (drop i (0) c1 e1) & (drop h (minus d i) e1 e2)).
-
-(*#* #stop proof *)
-
XElim i.
(* case 1 : i = 0 *)
Intros.
XElim IHc; XEAuto.
Qed.
-(*#* #start proof *)
-
(*#* #caption "transitivity, second case" *)
(*#* #cap #alpha c1 in C1, c2 in C, e2 in C2, d in i, i in k *)
Theorem drop_trans_ge : (i:?; c1,c2:?; d,h:?) (drop h d c1 c2) ->
(e2:?) (drop i (0) c2 e2) -> (le d i) ->
(drop (plus i h) (0) c1 e2).
-
-(*#* #stop proof *)
-
XElim i.
(* case 1: i = 0 *)
Intros.
DropGenBase; Apply drop_drop; NewInduction k; Simpl; XEAuto. (**) (* explicit constructor *)
Qed.
-(*#* #start proof *)
-
End transitivity.
-(*#* #stop macro *)
-
Tactic Definition DropDis :=
Match Context With
[ H1: (drop ?1 ?2 ?3 ?4); H2: (drop ?1 ?2 ?3 ?5) |- ? ] ->
LApply (H1 ?6); [ Clear H1 H2; Intros H1 | XAuto ];
LApply H1; [ Clear H1; Intros | XAuto ].
-(*#* #start macro *)
-
(*#* #single *)
-(*#* #stop file *)
-
Require Export pr2_defs.
Require Export pr3_defs.
Require Export pc1_defs.
+(*#* #stop file *)
+
Inductive pc2 [c:C; t1,t2:T] : Prop :=
| pc2_r : (pr2 c t1 t2) -> (pc2 c t1 t2)
| pc2_x : (pr2 c t2 t1) -> (pc2 c t1 t2).
Hint pc2 : ltlc := Constructors pc2.
+(*#* #start file *)
+
+(*#* #caption "axioms for the relation $\\PcT{}{}{}$",
+ "reflexivity", "single step transitivity"
+*)
+(*#* #cap #cap c, t, t1, t2, t3 *)
+
Inductive pc3 [c:C] : T -> T -> Prop :=
| pc3_r : (t:?) (pc3 c t t)
| pc3_u : (t2,t1:?) (pc2 c t1 t2) ->
(t3:?) (pc3 c t2 t3) -> (pc3 c t1 t3).
+(*#* #stop file *)
+
Hint pc3 : ltlc := Constructors pc3.
Section pc2_props. (******************************************************)
LApply (pc3_t (TTail ?3 ?4 ?5) ?1 ?2); [ Intros H_x | XAuto ];
LApply (H_x (TTail ?3 ?6 ?5)); [ Clear H_x; Intros | Apply pc3_s; XAuto ]
| [ _: (pc3 ?1 ?2 ?3); _: (pr3 ?1 ?3 ?4) |- ? ] ->
+ LApply (pc3_t ?3 ?1 ?2); [ Intros H_x | XAuto ];
+ LApply (H_x ?4); [ Clear H_x; Intros | XAuto ]
+ | [ _: (pc3 ?1 ?2 ?3); _: (pc3 ?1 ?4 ?3) |- ? ] ->
LApply (pc3_t ?3 ?1 ?2); [ Intros H_x | XAuto ];
LApply (H_x ?4); [ Clear H_x; Intros | XAuto ].
Section pc3_gen. (********************************************************)
- Theorem pc3_gen_abst : (c:?; u1,u2,t1,t2:?)
- (pc3 c (TTail (Bind Abst) u1 t1)
- (TTail (Bind Abst) u2 t2)
- ) ->
- (pc3 c u1 u2) /\
- (b:?; u:?) (pc3 (CTail c (Bind b) u) t1 t2).
+ Theorem pc3_gen_sort: (c:?; m,n:?) (pc3 c (TSort m) (TSort n)) -> m = n.
+ Intros; Pc3Confluence; Repeat Pr3GenBase.
+ Rewrite H in H0; Clear H x c.
+ Inversion H0; XAuto.
+ Qed.
+
+ Theorem pc3_gen_abst: (c:?; u1,u2,t1,t2:?)
+ (pc3 c (TTail (Bind Abst) u1 t1)
+ (TTail (Bind Abst) u2 t2)
+ ) ->
+ (pc3 c u1 u2) /\
+ (b:?; u:?) (pc3 (CTail c (Bind b) u) t1 t2).
Intros.
- Pc3Confluence; Pr3Gen; Pr3Gen; Rewrite H0 in H; Clear H0 x.
- Inversion H; Rewrite H5 in H1; Rewrite H6 in H2.
- Split; XEAuto.
+ Pc3Confluence; Repeat Pr3GenBase; Rewrite H0 in H1; Clear H0 x.
+ Inversion H1; Rewrite H0 in H4; Rewrite H6 in H5.
+ XEAuto.
Qed.
Theorem pc3_gen_lift: (c:?; t1,t2:?; h,d:?)
(e:?) (drop h d c e) ->
(pc3 e t1 t2).
Intros.
- Pc3Confluence; Pr3Gen; Pr3Gen; Rewrite H1 in H; Clear H1 x.
- LiftGen; Rewrite H in H2; XEAuto.
+ Pc3Confluence; Repeat Pr3Gen; Rewrite H2 in H1; Clear H2 x.
+ LiftGen; Rewrite H in H3; XEAuto.
Qed.
- Theorem pc3_gen_not_abst : (b:?) ~b=Abst -> (c:?; t1,t2,u1,u2:?)
- (pc3 c (TTail (Bind b) u1 t1)
- (TTail (Bind Abst) u2 t2)
- ) ->
- (pc3 (CTail c (Bind b) u1) t1
- (lift (1) (0) (TTail (Bind Abst) u2 t2))
- )
- .
- Intros b; XElim b; Intros;
- Try EqFalse; Pc3Confluence; Pr3Gen; Pr3Gen;
- Try (Rewrite H1 in H0; Inversion H0);
- Rewrite H1 in H4; Pr3Context;
+ Theorem pc3_gen_not_abst: (b:?) ~b=Abst -> (c:?; t1,t2,u1,u2:?)
+ (pc3 c (TTail (Bind b) u1 t1)
+ (TTail (Bind Abst) u2 t2)
+ ) ->
+ (pc3 (CTail c (Bind b) u1) t1
+ (lift (1) (0) (TTail (Bind Abst) u2 t2))
+ ).
+ XElim b; Intros;
+ Try EqFalse; Pc3Confluence; Repeat Pr3Gen;
+ Try (Rewrite H3 in H0; TGenBase);
+ Rewrite H0 in H2; Clear H H0 x;
EApply pc3_pr3_t; XEAuto.
Qed.
- Theorem pc3_gen_lift_abst : (c:?; t,t2,u2:?; h,d:?)
- (pc3 c (lift h d t)
+ Theorem pc3_gen_lift_abst: (c:?; t,t2,u2:?; h,d:?)
+ (pc3 c (lift h d t)
(TTail (Bind Abst) u2 t2)
- ) ->
- (e:?) (drop h d c e) ->
- (EX u1 t1 | (pr3 e t (TTail (Bind Abst) u1 t1)) &
- (pr3 c u2 (lift h d u1)) &
- (b:B; u:T)(pr3 (CTail c (Bind b) u) t2 (lift h (S d) t1))
- ).
+ ) ->
+ (e:?) (drop h d c e) ->
+ (EX u1 t1 | (pr3 e t (TTail (Bind Abst) u1 t1)) &
+ (pr3 c u2 (lift h d u1)) &
+ (b:B; u:T)(pr3 (CTail c (Bind b) u) t2 (lift h (S d) t1))
+ ).
Intros.
- Pc3Confluence; Pr3Gen; Pr3Gen; Rewrite H1 in H; Clear H1 x.
- LiftGenBase; Rewrite H in H4; Rewrite H1 in H2; Rewrite H5 in H3; XEAuto.
+ Pc3Confluence; Repeat Pr3Gen; Rewrite H in H2; Clear H x.
+ LiftGenBase; Rewrite H in H3; Rewrite H1 in H4; Rewrite H2 in H5; XEAuto.
Qed.
End pc3_gen.
Tactic Definition Pc3Gen :=
Match Context With
+ | [H: (pc3 ?1 (TSort ?2) (TSort ?3)) |- ? ] ->
+ LApply (pc3_gen_sort ?1 ?2 ?3); [ Clear H; Intros | XAuto ]
| [ _: (pc3 ?1 (lift ?2 ?3 ?4) (lift ?2 ?3 ?5));
_: (drop ?2 ?3 ?1 ?6) |- ? ] ->
LApply (pc3_gen_lift ?1 ?4 ?5 ?2 ?3); [ Intros H_x | XAuto ];
Require subst0_subst0.
Require pr0_subst0.
+Require cpr0_defs.
Require pr3_defs.
Require pr3_props.
Require pr3_confluence.
-Require cpr0_defs.
-Require cpr0_props.
Require pc3_defs.
Section pc3_confluence. (*************************************************)
- Theorem pc3_confluence : (c:?; t1,t2:?) (pc3 c t1 t2) ->
- (EX t0 | (pr3 c t1 t0) & (pr3 c t2 t0)).
+ Theorem pc3_confluence: (c:?; t1,t2:?) (pc3 c t1 t2) ->
+ (EX t0 | (pr3 c t1 t0) & (pr3 c t2 t0)).
Intros; XElim H; Intros.
-(* case 1 : pc3_r *)
+(* case 1: pc3_r *)
XEAuto.
-(* case 2 : pc3_u *)
+(* case 2: pc3_u *)
Clear H0; XElim H1; Intros.
Inversion_clear H; [ XEAuto | Pr3Confluence; XEAuto ].
Qed.
Section pc3_context. (****************************************************)
- Theorem pc3_pr0_pr2_t : (u1,u2:?) (pr0 u2 u1) ->
- (c:?; t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) ->
- (pc3 (CTail c k u1) t1 t2).
+ Theorem pc3_pr0_pr2_t: (u1,u2:?) (pr0 u2 u1) ->
+ (c:?; t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) ->
+ (pc3 (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.
- Pr0Subst0; XEAuto.
-(* case 2 : pr2_delta i > 0 *)
+(* 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; Apply pc3_pr3_t with t0:=x; XEAuto.
+(* case 2: pr2_delta i > 0 *)
NewInduction k; DropGenBase; XEAuto.
Qed.
- Theorem pc3_pr2_pr2_t : (c:?; u1,u2:?) (pr2 c u2 u1) ->
- (t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) ->
- (pc3 (CTail c k u1) t1 t2).
+ Theorem pc3_pr2_pr2_t: (c:?; u1,u2:?) (pr2 c u2 u1) ->
+ (t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) ->
+ (pc3 (CTail c k u1) t1 t2).
Intros until 1; Inversion H; Clear H; Intros.
-(* case 1 : pr2_pr0 *)
+(* case 1: pr2_free *)
EApply pc3_pr0_pr2_t; [ Apply H0 | XAuto ].
-(* case 2 : pr2_delta *)
+(* case 2: pr2_delta *)
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.
+(* case 2.1: i0 = 0 *)
+ 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.
+ Pr0Subst0; Subst0Subst0; Arith9'In H6 i.
EApply pc3_pr3_u.
EApply pr2_delta; XEAuto.
- Apply pc3_pr2_x; EApply pr2_delta; [ Idtac | XEAuto ]; XEAuto.
-(* case 2.2 : i0 > 0 *)
+ Apply pc3_pr2_x; EApply pr2_delta; [ Idtac | XEAuto | XEAuto ]; XEAuto.
+(* case 2.2: i0 > 0 *)
Clear IHi0; NewInduction k; DropGenBase; XEAuto.
Qed.
- Theorem pc3_pr2_pr3_t : (c:?; u2,t1,t2:?; k:?)
- (pr3 (CTail c k u2) t1 t2) ->
- (u1:?) (pr2 c u2 u1) ->
- (pc3 (CTail c k u1) t1 t2).
+ Theorem pc3_pr2_pr3_t: (c:?; u2,t1,t2:?; k:?)
+ (pr3 (CTail c k u2) t1 t2) ->
+ (u1:?) (pr2 c u2 u1) ->
+ (pc3 (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 pc3_t.
EApply pc3_pr2_pr2_t; [ Apply H2 | Apply H ].
XAuto.
Qed.
- Theorem pc3_pr3_pc3_t : (c:?; u1,u2:?) (pr3 c u2 u1) ->
- (t1,t2:?; k:?) (pc3 (CTail c k u2) t1 t2) ->
- (pc3 (CTail c k u1) t1 t2).
+ Theorem pc3_pr3_pc3_t: (c:?; u1,u2:?) (pr3 c u2 u1) ->
+ (t1,t2:?; k:?) (pc3 (CTail c k u2) t1 t2) ->
+ (pc3 (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 *)
Apply H1; Pc3Confluence.
EApply pc3_t; [ Idtac | Apply pc3_s ]; EApply pc3_pr2_pr3_t; XEAuto.
Qed.
Section pc3_lift. (*******************************************************)
- Theorem pc3_lift : (c,e:?; h,d:?) (drop h d c e) ->
- (t1,t2:?) (pc3 e t1 t2) ->
- (pc3 c (lift h d t1) (lift h d t2)).
+ Theorem pc3_lift: (c,e:?; h,d:?) (drop h d c e) ->
+ (t1,t2:?) (pc3 e t1 t2) ->
+ (pc3 c (lift h d t1) (lift h d t2)).
Intros.
Pc3Confluence.
Section pc3_cpr0. (*******************************************************)
- Remark pc3_cpr0_t_aux : (c1,c2:?) (cpr0 c1 c2) ->
- (k:?; u,t1,t2:?) (pr3 (CTail c1 k u) t1 t2) ->
- (pc3 (CTail c2 k u) t1 t2).
+ Remark pc3_cpr0_t_aux: (c1,c2:?) (cpr0 c1 c2) ->
+ (k:?; u,t1,t2:?) (pr3 (CTail c1 k u) t1 t2) ->
+ (pc3 (CTail c2 k u) t1 t2).
Intros; XElim H0; Intros.
-(* case 1.1 : pr3_r *)
+(* case 1.1: pr3_refl *)
XAuto.
-(* case 1.2 : pr3_u *)
+(* case 1.2: pr3_sing *)
EApply pc3_t; [ Idtac | XEAuto ]. Clear H2 t1 t2.
Inversion_clear H0.
-(* case 1.2.1 : pr2_pr0 *)
+(* case 1.2.1: pr2_free *)
XAuto.
-(* case 1.2.2 : pr2_delta *)
+(* case 1.2.2: pr2_delta *)
Cpr0Drop; Pr0Subst0.
EApply pc3_pr3_u; [ EApply pr2_delta; XEAuto | XAuto ].
Qed.
- Theorem pc3_cpr0_t : (c1,c2:?) (cpr0 c1 c2) ->
- (t1,t2:?) (pr3 c1 t1 t2) ->
- (pc3 c2 t1 t2).
+ Theorem pc3_cpr0_t: (c1,c2:?) (cpr0 c1 c2) ->
+ (t1,t2:?) (pr3 c1 t1 t2) ->
+ (pc3 c2 t1 t2).
Intros until 1; XElim H; Intros.
-(* case 1 : cpr0_refl *)
+(* case 1: cpr0_refl *)
XAuto.
-(* case 2 : cpr0_cont *)
+(* case 2: cpr0_comp *)
Pc3Context; Pc3Confluence.
EApply pc3_t; [ Idtac | Apply pc3_s ]; EApply pc3_cpr0_t_aux; XEAuto.
Qed.
- Theorem pc3_cpr0 : (c1,c2:?) (cpr0 c1 c2) -> (t1,t2:?) (pc3 c1 t1 t2) ->
- (pc3 c2 t1 t2).
+ Theorem pc3_cpr0: (c1,c2:?) (cpr0 c1 c2) -> (t1,t2:?) (pc3 c1 t1 t2) ->
+ (pc3 c2 t1 t2).
Intros; Pc3Confluence.
EApply pc3_t; [ Idtac | Apply pc3_s ]; EApply pc3_cpr0_t; XEAuto.
Qed.
(*#* #stop file *)
Require subst0_subst0.
-Require csubst0_defs.
+Require fsubst0_defs.
Require pr0_subst0.
Require pc3_defs.
(e:?) (drop i (0) c1 (CTail e (Bind Abbr) u)) ->
(pc3 c2 t2 t).
Intros until 1; XElim H.
-(* case 1: pr2_pr0 *)
+(* case 1: pr2_free *)
Intros until 2; XElim H0; Intros.
-(* case 1.1: fsubst0_t *)
+(* case 1.1: fsubst0_snd *)
Pr0Subst0; [ XAuto | Apply (pc3_pr3_u c1 x); XEAuto ].
-(* case 1.2: fsubst0_c *)
+(* case 1.2: fsubst0_fst *)
XAuto.
-(* case 1.3: fsubst0_b *)
+(* case 1.3: fsubst0_both *)
Pr0Subst0; CSubst0Drop; [ XAuto | Apply (pc3_pr3_u c0 x); XEAuto ].
(* case 2 : pr2_delta *)
- Intros until 3; XElim H1; Intros.
-(* case 2.1: fsubst0_t. *)
+ Intros until 4; XElim H2; Intros.
+(* case 2.1: fsubst0_snd. *)
Apply (pc3_t t1); [ Apply pc3_s; XEAuto | XEAuto ].
-(* case 2.2: fsubst0_c. *)
+(* case 2.2: fsubst0_fst. *)
Apply (lt_le_e i i0); Intros; CSubst0Drop.
(* case 2.2.1: i < i0, none *)
XEAuto.
-(* case 2.2.2: i < i0, csubst0_fst *)
- Inversion H; Rewrite <- H7 in H4; Rewrite <- H8 in H4; Rewrite <- H8 in H5; Rewrite <- H9 in H5; Clear H H7 H8 H9 c2 t2 x0 x1 x2.
- Subst0Subst0; Rewrite <- lt_plus_minus_r in H6; [ CSubst0Drop | XAuto ].
+(* case 2.2.2: i < i0, csubst0_snd *)
+ CGenBase; Rewrite <- H8 in H5; Rewrite <- H9 in H5; Rewrite <- H9 in H6; Rewrite <- H10 in H6; Clear H8 H9 H10 c2 t3 x0 x1 x2.
+ Subst0Subst0; Rewrite <- lt_plus_minus_r in H7; [ CSubst0Drop | XAuto ].
Apply (pc3_pr3_u c0 x); XEAuto.
-(* case 2.2.3: i < i0, csubst0_snd *)
- Inversion H; Rewrite <- H7 in H5; Rewrite <- H8 in H4; Rewrite <- H8 in H5; Rewrite <- H9 in H4; Clear H H7 H8 H9 c2 t2 x0 x1 x3.
+(* case 2.2.3: i < i0, csubst0_fst *)
+ CGenBase; Rewrite <- H8 in H6; Rewrite <- H9 in H5; Rewrite <- H9 in H6; Rewrite <- H10 in H5; Clear H8 H9 H10 c2 t3 x0 x1 x3.
Apply pc3_pr2_r; XEAuto.
(* case 2.2.4: i < i0, csubst0_both *)
- Inversion H; Rewrite <- H8 in H6; Rewrite <- H9 in H4; Rewrite <- H9 in H5; Rewrite <- H9 in H6; Rewrite <- H10 in H5; Clear H H8 H9 H10 c2 t2 x0 x1 x3.
- Subst0Subst0; Rewrite <- lt_plus_minus_r in H7; [ CSubst0Drop | XAuto ].
+ CGenBase; Rewrite <- H9 in H7; Rewrite <- H10 in H5; Rewrite <- H10 in H6; Rewrite <- H10 in H7; Rewrite <- H11 in H6; Clear H9 H10 H11 c2 t3 x0 x1 x3.
+ Subst0Subst0; Rewrite <- lt_plus_minus_r in H8; [ CSubst0Drop | XAuto ].
Apply (pc3_pr3_u c0 x); XEAuto.
(* case 2.2.5: i >= i0 *)
XEAuto.
-(* case 2.3: fsubst0_b *)
+(* case 2.3: fsubst0_both *)
Apply (lt_le_e i i0); Intros; CSubst0Drop.
(* case 2.3.1 : i < i0, none *)
CSubst0Drop; Apply pc3_pr3_u2 with t0 := t1; XEAuto.
-(* case 2.3.2 : i < i0, csubst0_fst *)
- Inversion H; Rewrite <- H8 in H5; Rewrite <- H9 in H5; Rewrite <- H9 in H6; Rewrite <- H10 in H6; Clear H H8 H9 H10 c2 t2 x0 x1 x2.
- Subst0Subst0; Rewrite <- lt_plus_minus_r in H7; [ CSubst0Drop | XAuto ].
+(* case 2.3.2 : i < i0, csubst0_snd *)
+ CGenBase; Rewrite <- H9 in H6; Rewrite <- H10 in H6; Rewrite <- H10 in H7; Rewrite <- H11 in H7; Clear H9 H10 H11 c2 t3 x0 x1 x2.
+ Subst0Subst0; Rewrite <- lt_plus_minus_r in H8; [ CSubst0Drop | XAuto ].
Apply (pc3_pr3_u2 c0 t1); [ Idtac | Apply (pc3_pr3_u c0 x) ]; XEAuto.
-(* case 2.3.3: i < i0, csubst0_snd *)
- Inversion H; Rewrite <- H8 in H6; Rewrite <- H9 in H5; Rewrite <- H9 in H6; Rewrite <- H10 in H5; Clear H H8 H9 H10 c2 t2 x0 x1 x3.
+(* case 2.3.3: i < i0, csubst0_fst *)
+ CGenBase; Rewrite <- H9 in H7; Rewrite <- H10 in H6; Rewrite <- H10 in H7; Rewrite <- H11 in H6; Clear H9 H10 H11 c2 t3 x0 x1 x3.
CSubst0Drop; Apply (pc3_pr3_u2 c0 t1); [ Idtac | Apply pc3_pr2_r ]; XEAuto.
(* case 2.3.4: i < i0, csubst0_both *)
- Inversion H; Rewrite <- H9 in H7; Rewrite <- H10 in H5; Rewrite <- H10 in H6; Rewrite <- H10 in H7; Rewrite <- H11 in H6; Clear H H9 H10 H11 c2 t2 x0 x1 x3.
- Subst0Subst0; Rewrite <- lt_plus_minus_r in H8; [ CSubst0Drop | XAuto ].
+ CGenBase; Rewrite <- H10 in H8; Rewrite <- H11 in H6; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H7; Clear H10 H11 H12 c2 t3 x0 x1 x3.
+ Subst0Subst0; Rewrite <- lt_plus_minus_r in H9; [ CSubst0Drop | XAuto ].
Apply (pc3_pr3_u2 c0 t1); [ Idtac | Apply (pc3_pr3_u c0 x) ]; XEAuto.
(* case 2.3.5: i >= i0 *)
CSubst0Drop; Apply (pc3_pr3_u2 c0 t1); XEAuto.
(e:?) (drop i (0) c1 (CTail e (Bind Abbr) u)) ->
(pc3 c2 t t2).
Intros until 1; XElim H.
-(* case 1: pr2_pr0 *)
+(* case 1: pr2_free *)
Intros until 2; XElim H0; Intros.
-(* case 1.1: fsubst0_t. *)
- Apply (pc3_pr3_u c1 t1); XEAuto.
-(* case 1.2: fsubst0_c. *)
+(* case 1.1: fsubst0_snd. *)
+ Apply (pc3_pr3_u c1 t2); XEAuto.
+(* case 1.2: fsubst0_fst. *)
XAuto.
-(* case 1.3: fsubst0_c. *)
- CSubst0Drop; Apply (pc3_pr3_u c0 t1); XEAuto.
+(* case 1.3: fsubst0_both. *)
+ CSubst0Drop; Apply (pc3_pr3_u c0 t2); XEAuto.
(* case 2: pr2_delta *)
- Intros until 3; XElim H1; Intros.
-(* case 2.1: fsubst0_t. *)
- Apply (pc3_t t1); XEAuto.
-(* case 2.2: fsubst0_c. *)
+ Intros until 4; XElim H2; Intros.
+(* case 2.1: fsubst0_snd. *)
+ Apply (pc3_t t2); Apply pc3_pr3_r; XEAuto.
+(* case 2.2: fsubst0_fst. *)
Apply (lt_le_e i i0); Intros; CSubst0Drop.
(* case 2.2.1: i < i0, none *)
XEAuto.
(* case 2.2.2: i < i0, csubst0_bind *)
- Inversion H; Rewrite <- H7 in H4; Rewrite <- H8 in H4; Rewrite <- H8 in H5; Rewrite <- H9 in H5; Clear H H7 H8 H9 c2 t2 x0 x1 x2.
- Subst0Subst0; Rewrite <- lt_plus_minus_r in H6; [ CSubst0Drop | XAuto ].
+ CGenBase; Rewrite <- H8 in H5; Rewrite <- H9 in H5; Rewrite <- H9 in H6; Rewrite <- H10 in H6; Clear H8 H9 H10 c2 t3 x0 x1 x2.
+ Subst0Subst0; Rewrite <- lt_plus_minus_r in H7; [ CSubst0Drop | XAuto ].
Apply (pc3_pr3_u c0 x); XEAuto.
-(* case 2.2.3: i < i0, csubst0_snd *)
- Inversion H; Rewrite <- H7 in H5; Rewrite <- H8 in H4; Rewrite <- H8 in H5; Rewrite <- H9 in H4; Clear H H7 H8 H9 c2 t2 x0 x1 x3.
+(* case 2.2.3: i < i0, csubst0_fst *)
+ CGenBase; Rewrite <- H8 in H6; Rewrite <- H9 in H5; Rewrite <- H9 in H6; Rewrite <- H10 in H5; Clear H8 H9 H10 c2 t3 x0 x1 x3.
Apply pc3_pr2_r; XEAuto.
(* case 2.2.4: i < i0, csubst0_both *)
- Inversion H; Rewrite <- H8 in H6; Rewrite <- H9 in H4; Rewrite <- H9 in H5; Rewrite <- H9 in H6; Rewrite <- H10 in H5; Clear H H8 H9 H10 c2 t2 x0 x1 x3.
- Subst0Subst0; Rewrite <- lt_plus_minus_r in H7; [ CSubst0Drop | XAuto ].
+ CGenBase; Rewrite <- H9 in H7; Rewrite <- H10 in H5; Rewrite <- H10 in H6; Rewrite <- H10 in H7; Rewrite <- H11 in H6; Clear H9 H10 H11 c2 t3 x0 x1 x3.
+ Subst0Subst0; Rewrite <- lt_plus_minus_r in H8; [ CSubst0Drop | XAuto ].
Apply (pc3_pr3_u c0 x); XEAuto.
(* case 2.2.5: i >= i0 *)
XEAuto.
-(* case 2.3: fsubst0_b *)
+(* case 2.3: fsubst0_both *)
Apply (lt_le_e i i0); Intros; CSubst0Drop.
(* case 2.3.1 : i < i0, none *)
- CSubst0Drop; Apply pc3_pr3_u with t2 := t1; XEAuto.
-(* case 2.3.2 : i < i0, csubst0_fst *)
- Inversion H; Rewrite <- H8 in H5; Rewrite <- H9 in H5; Rewrite <- H9 in H6; Rewrite <- H10 in H6; Clear H H8 H9 H10 c2 t2 x0 x1 x2.
- Subst0Subst0; Rewrite <- lt_plus_minus_r in H7; [ CSubst0Drop | XAuto ].
- Apply (pc3_pr3_u c0 x); [ Idtac | Apply (pc3_pr3_u2 c0 t1) ]; XEAuto.
-(* case 2.3.3: i < i0, csubst0_snd *)
- Inversion H; Rewrite <- H8 in H6; Rewrite <- H9 in H5; Rewrite <- H9 in H6; Rewrite <- H10 in H5; Clear H H8 H9 H10 c2 t2 x0 x1 x3.
- CSubst0Drop; Apply (pc3_pr3_u c0 t1); [ Idtac | Apply pc3_pr2_r ]; XEAuto.
-(* case 2.3.4: i < i0, csubst0_both *)
- Inversion H; Rewrite <- H9 in H7; Rewrite <- H10 in H5; Rewrite <- H10 in H6; Rewrite <- H10 in H7; Rewrite <- H11 in H6; Clear H H9 H10 H11 c2 t2 x0 x1 x3.
+ CSubst0Drop; Apply pc3_pr3_u with t2:=t2; Try Apply pc3_pr3_r; XEAuto.
+(* case 2.3.2 : i < i0, csubst0_snd *)
+ CGenBase; Rewrite <- H9 in H6; Rewrite <- H10 in H6; Rewrite <- H10 in H7; Rewrite <- H11 in H7; Clear H9 H10 H11 c2 t3 x0 x1 x2.
Subst0Subst0; Rewrite <- lt_plus_minus_r in H8; [ CSubst0Drop | XAuto ].
- Apply (pc3_pr3_u c0 x); [ Idtac | Apply (pc3_pr3_u2 c0 t1) ]; XEAuto.
+ Apply (pc3_pr3_u c0 x); [ Idtac | Apply (pc3_pr3_u2 c0 t0) ]; XEAuto.
+(* case 2.3.3: i < i0, csubst0_fst *)
+ CGenBase; Rewrite <- H9 in H7; Rewrite <- H10 in H6; Rewrite <- H10 in H7; Rewrite <- H11 in H6; Clear H9 H10 H11 c2 t3 x0 x1 x3.
+ CSubst0Drop; Apply (pc3_pr3_u c0 t0); [ Idtac | Apply pc3_pr2_r ]; XEAuto.
+(* case 2.3.4: i < i0, csubst0_both *)
+ CGenBase; Rewrite <- H10 in H8; Rewrite <- H11 in H6; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H7; Clear H10 H11 H12 c2 t3 x0 x1 x3.
+ Subst0Subst0; Rewrite <- lt_plus_minus_r in H9; [ CSubst0Drop | XAuto ].
+ Apply (pc3_pr3_u c0 x); [ Idtac | Apply (pc3_pr3_u2 c0 t0) ]; XEAuto.
(* case 2.3.5: i >= i0 *)
- CSubst0Drop; Apply (pc3_pr3_u c0 t1); XEAuto.
+ CSubst0Drop; Apply (pc3_pr3_u c0 t0); XEAuto.
Qed.
Theorem pc3_pc2_fsubst0: (c1:?; t1,t:?) (pc2 c1 t1 t) ->
Section pr2_confluence. (*************************************************)
-(* case 1.1 : pr2_pr0 pr2_pr0 ***********************************************)
+(* case 1.1 : pr2_free pr2_free *********************************************)
- Remark pr2_pr0_pr0: (c:?; t0,t1,t2:?)
- (pr0 t0 t1) -> (pr0 t0 t2) ->
- (EX t:T | (pr2 c t1 t) & (pr2 c t2 t)).
+ Remark pr2_free_free: (c:?; t0,t1,t2:?)
+ (pr0 t0 t1) -> (pr0 t0 t2) ->
+ (EX t:T | (pr2 c t1 t) & (pr2 c t2 t)).
Intros; Pr0Confluence; XEAuto.
Qed.
-(* case 1.2 : pr2_pr0 pr2_delta *********************************************)
+(* case 1.2 : pr2_free pr2_delta ********************************************)
- Remark pr2_pr0_delta: (c,d:?; t0,t1,t2,u:?; i:?)
- (pr0 t0 t1) ->
- (drop i (0) c (CTail d (Bind Abbr) u)) ->
- (subst0 i u t0 t2) ->
- (EX t | (pr2 c t1 t) & (pr2 c t2 t)).
- Intros; Pr0Subst0; XEAuto.
+ Remark pr2_free_delta: (c,d:?; t0,t1,t2,t4,u:?; i:?)
+ (pr0 t0 t1) ->
+ (drop i (0) c (CTail d (Bind Abbr) u)) ->
+ (pr0 t0 t4) ->
+ (subst0 i u t4 t2) ->
+ (EX t | (pr2 c t1 t) & (pr2 c t2 t)).
+ Intros; Pr0Confluence; Pr0Subst0; XEAuto.
Qed.
(* case 2.2 : pr2_delta pr2_delta *******************************************)
- Remark pr2_delta_delta: (c,d,d0:?; t0,t1,t2,u,u0:?; i,i0:?)
+ Remark pr2_delta_delta: (c,d,d0:?; t0,t1,t2,t3,t4,u,u0:?; i,i0:?)
(drop i (0) c (CTail d (Bind Abbr) u)) ->
- (subst0 i u t0 t1) ->
+ (pr0 t0 t3) ->
+ (subst0 i u t3 t1) ->
(drop i0 (0) c (CTail d0 (Bind Abbr) u0)) ->
- (subst0 i0 u0 t0 t2) ->
+ (pr0 t0 t4) ->
+ (subst0 i0 u0 t4 t2) ->
(EX t:T | (pr2 c t1 t) & (pr2 c t2 t)).
- Intros.
+ Intros; Pr0Confluence; Repeat Pr0Subst0;
+ [ XEAuto | XEAuto | XEAuto | Idtac ].
Apply (neq_eq_e i i0); Intros.
(* case 1 : i != i0 *)
Subst0Confluence; XEAuto.
(* case 2 : i = i0 *)
- Rewrite H3 in H; Rewrite H3 in H0; Clear H3 i.
- DropDis; Inversion H1; Rewrite H5 in H0; Clear H1 H4 H5 d u.
- Subst0Confluence; [ Rewrite H1; XEAuto | XEAuto | XEAuto | XEAuto ].
+ Rewrite H5 in H; Rewrite H5 in H3; Clear H5 i.
+ DropDis; Inversion H2; Rewrite H7 in H3; Clear H2 H6 H7 d u.
+ Subst0Confluence; [ Rewrite H2 in H0; XEAuto | XEAuto | XEAuto | XEAuto ].
Qed.
(* main *********************************************************************)
- Hints Resolve pr2_pr0_pr0 pr2_pr0_delta pr2_delta_delta : ltlc.
-
-(*#* #start file *)
+ Hints Resolve pr2_free_free pr2_free_delta pr2_delta_delta : ltlc.
(*#* #caption "confluence with itself: Church-Rosser property" *)
(*#* #cap #cap c, t0, t1, t2, t *)
- Theorem pr2_confluence : (c,t0,t1:?) (pr2 c t0 t1) ->
- (t2:?) (pr2 c t0 t2) ->
- (EX t | (pr2 c t1 t) & (pr2 c t2 t)).
-
-(*#* #stop file *)
-
- Intros; Inversion H; Inversion H0; XEAuto.
+ Theorem pr2_confluence: (c,t0,t1:?) (pr2 c t0 t1) ->
+ (t2:?) (pr2 c t0 t2) ->
+ (EX t | (pr2 c t1 t) & (pr2 c t2 t)).
+ Intros; Inversion H; Inversion H0; XDEAuto 3.
Qed.
End pr2_confluence.
XElim H1; Intros
| _ -> Pr0Confluence.
-(*#* #start file *)
-
(*#* #single *)
-(*#* #stop file *)
-
Require Export drop_defs.
Require Export pr0_defs.
- Inductive pr2 [c:C; t1,t2:T] : Prop :=
+(*#* #caption "current axioms for the relation $\\PrS{}{}{}$",
+ "context-free case", "context-dependent $\\delta$-expansion"
+*)
+(*#* #cap #cap c, d, t, t1, t2 #alpha u in V *)
+
+ Inductive pr2 [c:C; t1:T] : T -> Prop :=
(* structural rules *)
- | pr2_pr0 : (pr0 t1 t2) -> (pr2 c t1 t2)
+ | pr2_free : (t2:?) (pr0 t1 t2) -> (pr2 c t1 t2)
(* axiom rules *)
- | pr2_delta : (d:?; u:?; i:?)
- (drop i (0) c (CTail d (Bind Abbr) u)) ->
- (subst0 i u t1 t2) -> (pr2 c t1 t2).
+ | pr2_delta: (d:?; u:?; i:?)
+ (drop i (0) c (CTail d (Bind Abbr) u)) ->
+ (t2:?) (pr0 t1 t2) -> (t:?) (subst0 i u t2 t) ->
+ (pr2 c t1 t).
+
+(*#* #stop file *)
Hint pr2 : ltlc := Constructors pr2.
Section pr2_gen_base. (***************************************************)
- Theorem pr2_gen_sort : (c:?; x:?; n:?) (pr2 c (TSort n) x) ->
- x = (TSort n).
- Intros; Inversion H;
- Try Subst0GenBase; XEAuto.
+ Theorem pr2_gen_sort: (c:?; x:?; n:?) (pr2 c (TSort n) x) ->
+ x = (TSort n).
+ Intros; Inversion H; Pr0GenBase;
+ [ XAuto | Rewrite H1 in H2; Subst0GenBase ].
Qed.
- Theorem pr2_gen_bref : (c:?; x:?; n:?) (pr2 c (TBRef n) x) ->
- x = (TBRef n) \/
- (EX d u | (drop n (0) c (CTail d (Bind Abbr) u)) &
- x = (lift (S n) (0) u)
- ).
- Intros; Inversion H;
- Try Subst0GenBase; Try Rewrite <- H1 in H0; XEAuto.
+ Theorem pr2_gen_lref: (c:?; x:?; n:?) (pr2 c (TLRef n) x) ->
+ x = (TLRef n) \/
+ (EX d u | (drop n (0) c (CTail d (Bind Abbr) u)) &
+ x = (lift (S n) (0) u)
+ ).
+ Intros; Inversion H; Pr0GenBase;
+ [ XAuto | Rewrite H1 in H2; Subst0GenBase; Rewrite <- H2 in H0; XEAuto ].
Qed.
- Theorem pr2_gen_abst : (c:?; u1,t1,x:?)
- (pr2 c (TTail (Bind Abst) u1 t1) x) ->
- (EX u2 t2 | x = (TTail (Bind Abst) u2 t2) &
- (pr2 c u1 u2) & (b:?; u:?)
- (pr2 (CTail c (Bind b) u) t1 t2)
- ).
- Intros; Inversion H;
- Try Pr0GenBase; Try Subst0GenBase; XDEAuto 6.
+ Theorem pr2_gen_abst: (c:?; u1,t1,x:?)
+ (pr2 c (TTail (Bind Abst) u1 t1) x) ->
+ (EX u2 t2 | x = (TTail (Bind Abst) u2 t2) &
+ (pr2 c u1 u2) & (b:?; u:?)
+ (pr2 (CTail c (Bind b) u) t1 t2)
+ ).
+ Intros; Inversion H; Pr0GenBase;
+ [ XEAuto | Rewrite H1 in H2; Subst0GenBase; XDEAuto 6 ].
Qed.
- Theorem pr2_gen_appl : (c:?; u1,t1,x:?)
- (pr2 c (TTail (Flat Appl) u1 t1) x) -> (OR
- (EX u2 t2 | x = (TTail (Flat Appl) u2 t2) &
- (pr2 c u1 u2) & (pr2 c t1 t2)
- ) |
- (EX y1 z1 u2 t2 | t1 = (TTail (Bind Abst) y1 z1) &
- x = (TTail (Bind Abbr) u2 t2) &
- (pr0 u1 u2) & (pr0 z1 t2)
- ) |
- (EX b y1 z1 u2 v2 t2 |
- ~b=Abst &
- t1 = (TTail (Bind b) y1 z1) &
- x = (TTail (Bind b) v2 (TTail (Flat Appl) (lift (1) (0) u2) t2)) &
- (pr0 u1 u2) & (pr0 y1 v2) & (pr0 z1 t2))
- ).
- Intros; Inversion H;
- Try Pr0GenBase; Try Subst0GenBase; XEAuto.
+ Theorem pr2_gen_appl: (c:?; u1,t1,x:?)
+ (pr2 c (TTail (Flat Appl) u1 t1) x) -> (OR
+ (EX u2 t2 | x = (TTail (Flat Appl) u2 t2) &
+ (pr2 c u1 u2) & (pr2 c t1 t2)
+ ) |
+ (EX y1 z1 u2 t2 | t1 = (TTail (Bind Abst) y1 z1) &
+ x = (TTail (Bind Abbr) u2 t2) &
+ (pr2 c u1 u2) & (b:?; u:?)
+ (pr2 (CTail c (Bind b) u) z1 t2)
+ ) |
+ (EX b y1 z1 z2 u2 v2 t2 |
+ ~b=Abst &
+ t1 = (TTail (Bind b) y1 z1) &
+ x = (TTail (Bind b) v2 z2) &
+ (pr2 c u1 u2) & (pr2 c y1 v2) & (pr0 z1 t2))
+ ).
+ Intros; Inversion H; Pr0GenBase;
+ Try Rewrite H1 in H2; Try Rewrite H4 in H2; Try Rewrite H5 in H2;
+ Try Subst0GenBase; XDEAuto 7.
Qed.
- Theorem pr2_gen_cast : (c:?; u1,t1,x:?)
- (pr2 c (TTail (Flat Cast) u1 t1) x) ->
- (EX u2 t2 | x = (TTail (Flat Cast) u2 t2) &
- (pr2 c u1 u2) & (pr2 c t1 t2)
- ) \/
- (pr0 t1 x).
- Intros; Inversion H;
- Try Pr0GenBase; Try Subst0GenBase; XEAuto.
+ Theorem pr2_gen_cast: (c:?; u1,t1,x:?)
+ (pr2 c (TTail (Flat Cast) u1 t1) x) ->
+ (EX u2 t2 | x = (TTail (Flat Cast) u2 t2) &
+ (pr2 c u1 u2) & (pr2 c t1 t2)
+ ) \/
+ (pr2 c t1 x).
+ Intros; Inversion H; Pr0GenBase;
+ Try Rewrite H1 in H2; Try Subst0GenBase; XEAuto.
Qed.
End pr2_gen_base.
Tactic Definition Pr2GenBase :=
Match Context With
- | [ H: (pr2 ?1 (TTail (Bind Abst) ?2 ?3) ?4) |- ? ] ->
+ | [ H: (pr2 ?1 (TSort ?2) ?3) |- ? ] ->
+ LApply (pr2_gen_sort ?1 ?3 ?2); [ Clear H; Intros | XAuto ]
+ | [ H: (pr2 ?1 (TLRef ?2) ?3) |- ? ] ->
+ LApply (pr2_gen_lref ?1 ?3 ?2); [ Clear H; Intros H | XAuto ];
+ XDecompose H
+ | [ H: (pr2 ?1 (TTail (Bind Abst) ?2 ?3) ?4) |- ? ] ->
LApply (pr2_gen_abst ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
- XElim H; Intros.
+ XDecompose H
+ | [ H: (pr2 ?1 (TTail (Flat Appl) ?2 ?3) ?4) |- ? ] ->
+ LApply (pr2_gen_appl ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
+ XDecompose H
+ | [ H: (pr2 ?1 (TTail (Flat Cast) ?2 ?3) ?4) |- ? ] ->
+ LApply (pr2_gen_cast ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
+ XDecompose H.
Section pr2_props. (******************************************************)
- Theorem pr2_thin_dx : (c:?; t1,t2:?) (pr2 c t1 t2) ->
- (u:?; f:?) (pr2 c (TTail (Flat f) u t1)
- (TTail (Flat f) u t2)).
- Intros; Inversion H; XEAuto.
+ Theorem pr2_thin_dx: (c:?; t1,t2:?) (pr2 c t1 t2) ->
+ (u:?; f:?) (pr2 c (TTail (Flat f) u t1)
+ (TTail (Flat f) u t2)).
+ Intros; XElim H; XEAuto.
Qed.
- Theorem pr2_tail_1 : (c:?; u1,u2:?) (pr2 c u1 u2) ->
- (k:?; t:?) (pr2 c (TTail k u1 t) (TTail k u2 t)).
- Intros; Inversion H; XEAuto.
+ Theorem pr2_tail_1: (c:?; u1,u2:?) (pr2 c u1 u2) ->
+ (k:?; t:?) (pr2 c (TTail k u1 t) (TTail k u2 t)).
+ Intros; XElim H; XEAuto.
Qed.
- Theorem pr2_tail_2 : (c:?; u,t1,t2:?; k:?) (pr2 (CTail c k u) t1 t2) ->
- (pr2 c (TTail k u t1) (TTail k u t2)).
- XElim k; Intros;
- (Inversion H; [ XAuto | Clear H ];
- (NewInduction i; DropGenBase; [ Inversion H; XEAuto | XEAuto ])).
+ Theorem pr2_tail_2: (c:?; u,t1,t2:?; k:?) (pr2 (CTail c k u) t1 t2) ->
+ (pr2 c (TTail k u t1) (TTail k u t2)).
+ XElim k; Intros; (
+ XElim H; [ XAuto | XElim i; Intros; DropGenBase; CGenBase; XEAuto ]).
Qed.
-
+
Hints Resolve pr2_tail_2 : ltlc.
- Theorem pr2_shift : (i:?; c,e:?) (drop i (0) c e) ->
- (t1,t2:?) (pr2 c t1 t2) ->
- (pr2 e (app c i t1) (app c i t2)).
+ Theorem pr2_shift: (i:?; c,e:?) (drop i (0) c e) ->
+ (t1,t2:?) (pr2 c t1 t2) ->
+ (pr2 e (app c i t1) (app c i t2)).
XElim i.
-(* case 1 : i = 0 *)
- Intros.
- DropGenBase; Rewrite H in H0.
+(* case 1: i = 0 *)
+ Intros; DropGenBase; Rewrite H in H0.
Repeat Rewrite app_O; XAuto.
-(* case 2 : i > 0 *)
+(* case 2: i > 0 *)
XElim c.
-(* case 2.1 : CSort *)
+(* case 2.1: CSort *)
Intros; DropGenBase; Rewrite H0; XAuto.
-(* case 2.2 : CTail *)
+(* case 2.2: CTail *)
XElim k; Intros; Simpl; DropGenBase; XAuto.
Qed.
-
+
End pr2_props.
Hints Resolve pr2_thin_dx pr2_tail_1 pr2_tail_2 pr2_shift : ltlc.
(*#* #stop file *)
Require subst0_gen.
+Require subst0_lift.
Require drop_props.
Require pr0_gen.
+Require pr0_subst0.
Require pr2_defs.
Section pr2_gen. (********************************************************)
- Theorem pr2_gen_abbr : (c:?; u1,t1,x:?)
- (pr2 c (TTail (Bind Abbr) u1 t1) x) ->
- (EX u2 t2 | x = (TTail (Bind Abbr) u2 t2) &
- (pr2 c u1 u2) &
- ((b:?; u:?) (pr2 (CTail c (Bind b) u) t1 t2)) \/
- (EX y | (pr0 t1 y) & (subst0 (0) u2 y t2))
- ) \/
- (pr0 t1 (lift (1) (0) x)).
- Intros; Inversion H;
- Try Pr0Gen; Try Subst0Gen; XDEAuto 8.
+ Theorem pr2_gen_abbr: (c:?; u1,t1,x:?)
+ (pr2 c (TTail (Bind Abbr) u1 t1) x) ->
+ (EX u2 t2 | x = (TTail (Bind Abbr) u2 t2) &
+ (pr2 c u1 u2) & (OR
+ (b:?; u:?) (pr2 (CTail c (Bind b) u) t1 t2) |
+ (EX u | (pr0 u1 u) & (pr2 (CTail c (Bind Abbr) u) t1 t2)) |
+ (EX y z | (pr2 (CTail c (Bind Abbr) u1) t1 y) & (pr0 y z) & (pr2 (CTail c (Bind Abbr) u1) z t2))
+ )) \/ (b:?; u:?)
+ (pr2 (CTail c (Bind b) u) t1 (lift (1) (0) x)).
+ Intros; Inversion H;
+ Pr0Gen; Try Rewrite H1 in H2; Try Subst0Gen; Try Pr0Subst0; XDEAuto 10.
Qed.
- Theorem pr2_gen_void : (c:?; u1,t1,x:?)
- (pr2 c (TTail (Bind Void) u1 t1) x) ->
- (EX u2 t2 | x = (TTail (Bind Void) u2 t2) &
- (pr2 c u1 u2) & (b:?; u:?)
- (pr2 (CTail c (Bind b) u) t1 t2)
- ) \/
- (pr0 t1 (lift (1) (0) x)).
- Intros; Inversion H;
- Try Pr0Gen; Try Subst0Gen; XDEAuto 7.
+ Theorem pr2_gen_void: (c:?; u1,t1,x:?)
+ (pr2 c (TTail (Bind Void) u1 t1) x) ->
+ (EX u2 t2 | x = (TTail (Bind Void) u2 t2) &
+ (pr2 c u1 u2) & (b:?; u:?)
+ (pr2 (CTail c (Bind b) u) t1 t2)
+ ) \/ (b:?; u:?)
+ (pr2 (CTail c (Bind b) u) t1 (lift (1) (0) x)).
+ Intros; Inversion H;
+ Try Pr0Gen; Try Rewrite H1 in H2; Try Subst0Gen; XDEAuto 7.
Qed.
-(*#* #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 pr2_gen_lift : (c:?; t1,x:?; h,d:?) (pr2 c (lift h d t1) x) ->
- (e:?) (drop h d c e) ->
- (EX t2 | x = (lift h d t2) & (pr2 e t1 t2)).
-
-(*#* #stop file *)
-
+ Theorem pr2_gen_lift: (c:?; t1,x:?; h,d:?) (pr2 c (lift h d t1) x) ->
+ (e:?) (drop h d c e) ->
+ (EX t2 | x = (lift h d t2) & (pr2 e t1 t2)).
Intros.
- Inversion H; Clear H.
-(* case 1 : pr2_pr0 *)
- Pr0Gen; XEAuto.
+ Inversion H; Clear H; Pr0Gen.
+(* case 1 : pr2_free *)
+ XEAuto.
(* case 2 : pr2_delta *)
+ Rewrite H in H3; Clear H H4 t t2.
Apply (lt_le_e i d); Intros.
(* case 2.1 : i < d *)
- Rewrite (lt_plus_minus i d) in H0; [ Idtac | XAuto ].
- Rewrite (lt_plus_minus i d) in H2; [ Idtac | XAuto ].
- DropDis; Rewrite H0 in H2; Clear H0 u.
+ Rewrite (lt_plus_minus i d) in H0; [ Idtac | XAuto ].
+ Rewrite (lt_plus_minus i d) in H3; [ Idtac | XAuto ].
+ DropDis; Rewrite H0 in H3; Clear H0 u.
Subst0Gen; Rewrite <- lt_plus_minus in H0; XEAuto.
(* case 2.2 : i >= d *)
Apply (lt_le_e i (plus d h)); Intros.
(* case 2.2.1 : i < d + h *)
- EApply subst0_gen_lift_false; [ Apply H | Apply H3 | XEAuto ].
+ EApply subst0_gen_lift_false; [ Apply H | Apply H4 | XEAuto ].
(* case 2.2.2 : i >= d + h *)
DropDis; Subst0Gen; XEAuto.
Qed.
Match Context With
| [ H: (pr2 ?1 (TTail (Bind Abbr) ?2 ?3) ?4) |- ? ] ->
LApply (pr2_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 ]
+ XDecompose H
| [ H: (pr2 ?1 (TTail (Bind Void) ?2 ?3) ?4) |- ? ] ->
LApply (pr2_gen_void ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
- XElim H; [ Intros H; XElim H; Intros | Intros ]
+ XDecompose H
| [ H0: (pr2 ?1 (lift ?2 ?3 ?4) ?5);
H1: (drop ?2 ?3 ?1 ?6) |- ? ] ->
LApply (pr2_gen_lift ?1 ?4 ?5 ?2 ?3); [ Clear H0; Intros H0 | XAuto ];
LApply (H0 ?6); [ Clear H0; Intros H0 | XAuto ];
- XElim H0; Intros
+ XDecompose H0
| _ -> Pr2GenBase.
+
Require pr0_gen.
Require pr0_subst1.
Require pr2_defs.
+Require pr2_gen.
Require pr2_subst1.
Section pr2_gen_context. (************************************************)
(EX x2 | (subst1 d u t2 (lift (1) d x2)) &
(pr2 a x1 x2)
).
- Intros until 1; XElim H; Intros.
-(* case 1: pr2_pr0 *)
- Pr0Subst1; Pr0Gen; Rewrite H in H3; Clear H x; XEAuto.
+ Intros until 1; XElim H; Intros;
+ Pr0Subst1; Pr0Gen.
+(* case 1: pr2_free *)
+ Rewrite H in H3; Clear H x; XEAuto.
(* case 2: pr2_delta *)
+ Rewrite H0 in H5; Clear H0 x.
Apply (lt_eq_gt_e i d0); Intros.
(* case 2.1: i < d0 *)
Subst1Confluence; CSubst1Drop.
Rewrite minus_x_Sy in H; [ Idtac | XAuto ].
- CSubst1GenBase; Rewrite H in H6; Clear H x0.
- Rewrite (lt_plus_minus i d0) in H3; [ Idtac | XAuto ].
- DropDis; Rewrite H in H7; Clear H x2.
+ CSubst1GenBase; Rewrite H in H7; Clear H x2.
+ Rewrite (lt_plus_minus i d0) in H4; [ Idtac | XAuto ].
+ DropDis; Rewrite H in H8; Clear H x3.
Subst1Subst1; Pattern 2 d0 in H; Rewrite (lt_plus_minus i d0) in H; [ Idtac | XAuto ].
- Subst1Gen; Rewrite H in H9; Simpl in H9; Clear H x2.
- Rewrite <- lt_plus_minus in H9; [ Idtac | XAuto ].
- Rewrite <- lt_plus_minus_r in H9; XEAuto.
+ Subst1Gen; Rewrite H in H10; Simpl in H10; Clear H x3.
+ Rewrite <- lt_plus_minus in H10; [ Idtac | XAuto ].
+ Rewrite <- lt_plus_minus_r in H10; XEAuto.
(* case 2.2: i = d0 *)
- Rewrite H5 in H; Rewrite H5 in H0; Clear H5 i.
- DropDis; Inversion H; Rewrite <- H7 in H0; Rewrite <- H7 in H1; Rewrite <- H7; Clear H H6 H7 e u.
+ Rewrite H0 in H; Rewrite H0 in H1; Clear H0 i.
+ DropDis; Inversion H; Rewrite <- H8 in H1; Rewrite <- H8 in H2; Rewrite <- H8; Clear H H7 H8 e u.
Subst1Confluence; Subst1Gen; Rewrite H0 in H; Clear H0 x; XEAuto.
(* case 2.3: i > d0 *)
- Subst1Confluence; Subst1Gen; Rewrite H4 in H0; Clear H1 H4 x.
+ Subst1Confluence; Subst1Gen; Rewrite H5 in H1; Clear H2 H5 x.
CSubst1Drop; DropDis; XEAuto.
Qed.
+(*#* #stop file *)
+
Require subst0_lift.
Require drop_props.
Require pr0_lift.
Theorem pr2_lift : (c,e:?; h,d:?) (drop h d c e) ->
(t1,t2:?) (pr2 e t1 t2) ->
(pr2 c (lift h d t1) (lift h d t2)).
-
-(*#* #stop file *)
-
Intros until 2; XElim H0; Intros.
-(* case 1 : pr2_pr0 *)
+(* case 1 : pr2_free *)
XAuto.
(* case 2 : pr2_delta *)
Apply (lt_le_e i d); Intros; DropDis.
Section pr2_subst1_props. (***********************************************)
Theorem pr2_delta1: (c,d:?; u:?; i:?) (drop i (0) c (CTail d (Bind Abbr) u)) ->
- (t1,t2:?) (subst1 i u t1 t2) -> (pr2 c t1 t2).
- Intros; XElim H0; Clear t2; XEAuto.
+ (t1,t2:?) (pr0 t1 t2) -> (t:?) (subst1 i u t2 t) ->
+ (pr2 c t1 t).
+ Intros; XElim H1; Clear t; XEAuto.
Qed.
Hints Resolve pr2_delta1 : ltlc.
(t1,t2:?) (pr2 c t1 t2) ->
(w1:?) (subst1 i v t1 w1) ->
(EX w2 | (pr2 c w1 w2) & (subst1 i v t2 w2)).
- Intros until 2; XElim H0; Intros.
-(* case 1: pr2_pr0 *)
- Pr0Subst1; XEAuto.
+ Intros until 2; XElim H0; Intros;
+ Pr0Subst1.
+(* case 1: pr2_free *)
+ XEAuto.
(* case 2: pr2_delta *)
Apply (neq_eq_e i i0); Intros.
(* case 2.1: i <> i0 *)
Subst1Confluence; XEAuto.
(* case 2.2: i = i0 *)
- Rewrite <- H3 in H0; Rewrite <- H3 in H1; Clear H3 i0.
- DropDis; Inversion H0; Rewrite H5 in H2; Clear H0 H4 H5 e v.
+ Rewrite <- H4 in H0; Rewrite <- H4 in H2; Clear H4 i0.
+ DropDis; Inversion H0; Rewrite H6 in H3; Clear H0 H5 H6 e v.
Subst1Confluence; XEAuto.
Qed.
Section pr3_confluence. (*************************************************)
+(*#* #stop theorem *)
+
(*#* #caption "confluence with single step reduction: strip lemma" *)
(*#* #cap #cap c, t0, t1, t2, t *)
Theorem pr3_strip : (c:?; t0,t1:?) (pr3 c t0 t1) -> (t2:?) (pr2 c t0 t2) ->
(EX t | (pr3 c t1 t) & (pr3 c t2 t)).
-
-(*#* #stop proof *)
-
Intros until 1; XElim H; Intros.
-(* case 1 : pr3_r *)
+(* case 1 : pr3_refl *)
XEAuto.
-(* case 2 : pr3_u *)
+(* case 2 : pr3_sing *)
Pr2Confluence.
LApply (H1 x); [ Clear H1 H2; Intros H1 | XAuto ].
XElim H1; Intros; XEAuto.
Qed.
-(*#* #start proof *)
+(*#* #start theorem *)
(*#* #caption "confluence with itself: Church-Rosser property" *)
(*#* #cap #cap c, t0, t1, t2, t *)
(*#* #stop file *)
Intros until 1; XElim H; Intros.
-(* case 1 : pr3_r *)
+(* case 1 : pr3_refl *)
XEAuto.
-(* case 2 : pr3_u *)
+(* case 2 : pr3_sing *)
LApply (pr3_strip c t3 t5); [ Clear H2; Intros H2 | XAuto ].
LApply (H2 t2); [ Clear H H2; Intros H | XAuto ].
XElim H; Intros.
-(*#* #stop file *)
-
Require Export pr1_defs.
Require Export pr2_defs.
+(*#* #caption "axioms for the relation $\\PrT{}{}{}$",
+ "reflexivity", "single step transitivity"
+*)
+(*#* #cap #cap c, t, t1, t2, t3 *)
+
Inductive pr3 [c:C] : T -> T -> Prop :=
- | pr3_r : (t:?) (pr3 c t t)
- | pr3_u : (t2,t1:?) (pr2 c t1 t2) ->
- (t3:?) (pr3 c t2 t3) -> (pr3 c t1 t3).
+ | pr3_refl: (t:?) (pr3 c t t)
+ | pr3_sing: (t2,t1:?) (pr2 c t1 t2) ->
+ (t3:?) (pr3 c t2 t3) -> (pr3 c t1 t3).
+
+(*#* #stop file *)
Hint pr3: ltlc := Constructors pr3.
+ Section pr3_gen_base. (***************************************************)
+
+ Theorem pr3_gen_sort: (c:?; x:?; n:?) (pr3 c (TSort n) x) ->
+ x = (TSort n).
+ Intros; InsertEq H '(TSort n); XElim H; Clear y x; Intros.
+(* case 1: pr3_refl *)
+ XAuto.
+(* case 2: pr3_sing *)
+ Rewrite H2 in H; Clear H2 t1; Pr2GenBase; XAuto.
+ Qed.
+
+ Tactic Definition IH :=
+ Match Context With
+ | [ H: (u,t:T) (TTail (Bind Abst) ?1 ?2) = (TTail (Bind Abst) u t) -> ? |- ? ] ->
+ LApply (H ?1 ?2); [ Clear H; Intros H | XAuto ];
+ XDecompose H
+ | [ H: (u,t:T) (TTail (Flat Appl) ?1 ?2) = (TTail (Flat Appl) u t) -> ? |- ? ] ->
+ LApply (H ?1 ?2); [ Clear H; Intros H | XAuto ];
+ XDecompose H
+ | [ H: (u,t:T) (TTail (Flat Cast) ?1 ?2) = (TTail (Flat Cast) u t) -> ? |- ? ] ->
+ LApply (H ?1 ?2); [ Clear H; Intros H | XAuto ];
+ XDecompose H.
+
+ 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 u0; Rename x0 into t0.
+(* case 1 : pr3_refl *)
+ XEAuto.
+(* case 2 : pr3_sing *)
+ Rewrite H2 in H; Clear H0 H2 t1; Pr2GenBase.
+ Rewrite H0 in H1; Clear H0 t2; IH; XEAuto.
+ Qed.
+
+ Theorem pr3_gen_appl: (c:?; u1,t1,x:?)
+ (pr3 c (TTail (Flat Appl) u1 t1) x) -> (OR
+ (EX u2 t2 | x = (TTail (Flat Appl) u2 t2) &
+ (pr3 c u1 u2) & (pr3 c t1 t2)
+ ) |
+ (EX y1 z1 u2 t2 | (pr3 c (TTail (Bind Abbr) u2 t2) x) &
+ (pr3 c u1 u2) &
+ (pr3 c t1 (TTail (Bind Abst) y1 z1)) &
+ (b:?; u:?) (pr3 (CTail c (Bind b) u) z1 t2)
+ ) |
+ (EX b y1 z1 z2 u2 v2 t2 |
+ (pr3 c (TTail (Bind b) v2 z2) x) & ~b=Abst &
+ (pr3 c u1 u2) &
+ (pr3 c t1 (TTail (Bind b) y1 z1)) &
+ (pr3 c y1 v2) & (pr0 z1 t2))
+ ).
+ Intros; InsertEq H '(TTail (Flat Appl) u1 t1).
+ UnIntro t1 H; UnIntro u1 H.
+ XElim H; Clear y x; Intros;
+ Rename x into u0; Rename x0 into t0.
+(* case 1: pr3_refl *)
+ XEAuto.
+(* case 2: pr3_sing *)
+ Rewrite H2 in H; Clear H2 t1; Pr2GenBase.
+(* case 2.1: short step: compatibility *)
+ Rewrite H3 in H1; Clear H0 H3 t2.
+ IH; Try (Rewrite H0; Clear H0 t3); XDEAuto 6.
+(* case 2.2: short step: beta *)
+ Rewrite H4 in H0; Rewrite H3; Clear H1 H3 H4 t0 t2; XEAuto.
+(* case 2.3: short step: upsilon *)
+ Rewrite H5 in H0; Rewrite H4; Clear H1 H4 H5 t0 t2; XEAuto.
+ Qed.
+
+ Theorem pr3_gen_cast: (c:?; u1,t1,x:?)
+ (pr3 c (TTail (Flat Cast) u1 t1) x) ->
+ (EX u2 t2 | x = (TTail (Flat Cast) u2 t2) &
+ (pr3 c u1 u2) & (pr3 c t1 t2)
+ ) \/
+ (pr3 c t1 x).
+ Intros; InsertEq H '(TTail (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; XEAuto.
+(* 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; XEAuto.
+(* case 2.2: short step: epsilon *)
+ XEAuto.
+ 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 (TTail (Bind Abst) ?2 ?3) ?4) |- ? ] ->
+ LApply (pr3_gen_abst ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
+ XDecompose H
+ | [ H: (pr3 ?1 (TTail (Flat Appl) ?2 ?3) ?4) |- ? ] ->
+ LApply (pr3_gen_appl ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
+ XDecompose H
+ | [ H: (pr3 ?1 (TTail (Flat Cast) ?2 ?3) ?4) |- ? ] ->
+ LApply (pr3_gen_cast ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
+ XDecompose H.
+
Section pr3_props. (******************************************************)
- Theorem pr3_pr2 : (c,t1,t2:?) (pr2 c t1 t2) -> (pr3 c t1 t2).
+ Theorem pr3_pr2: (c,t1,t2:?) (pr2 c t1 t2) -> (pr3 c t1 t2).
XEAuto.
Qed.
- Theorem pr3_t : (t2,t1,c:?) (pr3 c t1 t2) ->
+ Theorem pr3_t: (t2,t1,c:?) (pr3 c t1 t2) ->
(t3:?) (pr3 c t2 t3) -> (pr3 c t1 t3).
Intros until 1; XElim H; XEAuto.
Qed.
- Theorem pr3_tail_1 : (c:?; u1,u2:?) (pr3 c u1 u2) ->
- (k:?; t:?) (pr3 c (TTail k u1 t) (TTail k u2 t)).
+ Theorem pr3_tail_1: (c:?; u1,u2:?) (pr3 c u1 u2) ->
+ (k:?; t:?) (pr3 c (TTail k u1 t) (TTail k u2 t)).
Intros until 1; XElim H; Intros.
-(* case 1 : pr3_r *)
+(* case 1: pr3_refl *)
XAuto.
-(* case 2 : pr3_u *)
- EApply pr3_u; [ Apply pr2_tail_1; Apply H | XAuto ].
+(* case 2: pr3_sing *)
+ EApply pr3_sing; [ Apply pr2_tail_1; Apply H | XAuto ].
Qed.
- Theorem pr3_tail_2 : (c:?; u,t1,t2:?; k:?) (pr3 (CTail c k u) t1 t2) ->
- (pr3 c (TTail k u t1) (TTail k u t2)).
+ Theorem pr3_tail_2: (c:?; u,t1,t2:?; k:?) (pr3 (CTail c k u) t1 t2) ->
+ (pr3 c (TTail k u t1) (TTail k u t2)).
Intros until 1; XElim H; Intros.
-(* case 1 : pr3_r *)
+(* case 1: pr3_refl *)
XAuto.
-(* case 2 : pr3_u *)
- EApply pr3_u; [ Apply pr2_tail_2; Apply H | XAuto ].
+(* case 2: pr3_sing *)
+ EApply pr3_sing; [ Apply pr2_tail_2; Apply H | XAuto ].
Qed.
Hints Resolve pr3_tail_1 pr3_tail_2 : ltlc.
- Theorem pr3_tail_21 : (c:?; u1,u2:?) (pr3 c u1 u2) ->
- (k:?; t1,t2:?) (pr3 (CTail c k u1) t1 t2) ->
- (pr3 c (TTail k u1 t1) (TTail k u2 t2)).
+ Theorem pr3_tail_21: (c:?; u1,u2:?) (pr3 c u1 u2) ->
+ (k:?; t1,t2:?) (pr3 (CTail c k u1) t1 t2) ->
+ (pr3 c (TTail k u1 t1) (TTail k u2 t2)).
Intros.
EApply pr3_t; [ Apply pr3_tail_2 | Apply pr3_tail_1 ]; XAuto.
Qed.
- Theorem pr3_tail_12 : (c:?; u1,u2:?) (pr3 c u1 u2) ->
- (k:?; t1,t2:?) (pr3 (CTail c k u2) t1 t2) ->
- (pr3 c (TTail k u1 t1) (TTail k u2 t2)).
+ Theorem pr3_tail_12: (c:?; u1,u2:?) (pr3 c u1 u2) ->
+ (k:?; t1,t2:?) (pr3 (CTail c k u2) t1 t2) ->
+ (pr3 c (TTail k u1 t1) (TTail k u2 t2)).
Intros.
EApply pr3_t; [ Apply pr3_tail_1 | Apply pr3_tail_2 ]; XAuto.
Qed.
- Theorem pr3_shift : (h:?; c,e:?) (drop h (0) c e) ->
- (t1,t2:?) (pr3 c t1 t2) ->
- (pr3 e (app c h t1) (app c h t2)).
+ Theorem pr3_shift: (h:?; c,e:?) (drop h (0) c e) ->
+ (t1,t2:?) (pr3 c t1 t2) ->
+ (pr3 e (app c h t1) (app c h t2)).
Intros until 2; XElim H0; Clear t1 t2; Intros.
-(* case 1 : pr3_r *)
+(* case 1: pr3_refl *)
XAuto.
-(* case 2 : pr3_u *)
+(* case 2: pr3_sing *)
XEAuto.
Qed.
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.
(pr3 a x1 x2)
).
Intros until 1; XElim H; Intros.
-(* case 1: pr3_r *)
+(* case 1: pr3_refl *)
XEAuto.
-(* case 1: pr3_r *)
+(* case 1: pr3_refl *)
Pr2GenContext.
LApply (H1 e u d); [ Clear H1; Intros H1 | XAuto ].
LApply (H1 a0); [ Clear H1; Intros H1 | XAuto ].
LApply (H1 ?7); [ Clear H1; Intros H1 | XAuto ];
XElim H1; Intros
| _ -> Pr2Subst1.
-
| Flat : F -> K.
Inductive Set T := TSort : nat -> T
- | TBRef : nat -> T
+ | TLRef : nat -> T
| TTail : K -> T -> T -> T.
Hint f3KTT : ltlc := Resolve (f_equal3 K T T).
+ Tactic Definition TGenBase :=
+ Match Context With
+ | [ H: (TTail ? ? ?) = (TTail ? ? ?) |- ? ] -> Inversion H; Clear H
+ | _ -> Idtac.
+
Definition s: K -> nat -> nat := [k;i] Cases k of
| (Bind _) => (S i)
| (Flat _) => i
projects / helm.git / commitdiff