-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 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
+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 pc1_props.vo pc3_defs.vo pc3_props.vo pc3_gen.vo pc3_subst0.vo pc3_gen_context.vo ty0_defs.vo ty0_gen.vo ty0_lift.vo ty0_props.vo ty0_subst0.vo ty0_gen_context.vo csub0_defs.vo csub0_props.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_gen.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 pc1_props.vo pc3_props.vo pc3_gen.vo ty0_defs.vo ty0_gen.vo ty0_lift.vo ty0_props.vo ty0_subst0.vo ty0_gen_context.vo csub0_defs.vo csub0_props.vo
+csub0_props.vo: csub0_props.v pc3_props.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 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_subst0.vo: ty0_subst0.v drop_props.vo csubst0_defs.vo fsubst0_defs.vo pc3_props.vo pc3_subst0.vo ty0_defs.vo ty0_gen.vo ty0_lift.vo ty0_props.vo
+ty0_props.vo: ty0_props.v drop_props.vo pc3_props.vo ty0_defs.vo ty0_gen.vo ty0_lift.vo
ty0_lift.vo: ty0_lift.v lift_props.vo drop_props.vo pc3_props.vo ty0_defs.vo
+ty0_gen.vo: ty0_gen.v 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 fsubst0_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_props.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 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
+pc1_props.vo: pc1_props.v pr1_confluence.vo pc1_defs.vo
+pc1_defs.vo: pc1_defs.v pr0_defs.vo pr1_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
Require Export pr3_subst1.
Require Export pr3_gen_context.
Require Export pc1_defs.
+Require Export pc1_props.
Require Export pc3_defs.
Require Export pc3_props.
Require Export pc3_gen.
Require Export pc3_subst0.
Require Export pc3_gen_context.
Require Export ty0_defs.
+Require Export ty0_gen.
Require Export ty0_lift.
Require Export ty0_props.
Require Export ty0_subst0.
Require Export ty0_gen_context.
Require Export csub0_defs.
+Require Export csub0_props.
Require Export ty0_sred.
Require Export ty0_sred_props.
pr3_subst1.v
pr3_gen_context.v
pc1_defs.v
+pc1_props.v
pc3_defs.v
pc3_props.v
pc3_gen.v
pc3_subst0.v
pc3_gen_context.v
ty0_defs.v
+ty0_gen.v
ty0_lift.v
ty0_props.v
ty0_subst0.v
ty0_gen_context.v
csub0_defs.v
+csub0_props.v
ty0_sred.v
ty0_sred_props.v
LambdaDelta.v
pr3_subst1.v\
pr3_gen_context.v\
pc1_defs.v\
+ pc1_props.v\
pc3_defs.v\
pc3_props.v\
pc3_gen.v\
pc3_subst0.v\
pc3_gen_context.v\
ty0_defs.v\
+ ty0_gen.v\
ty0_lift.v\
ty0_props.v\
ty0_subst0.v\
ty0_gen_context.v\
csub0_defs.v\
+ csub0_props.v\
ty0_sred.v\
ty0_sred_props.v\
LambdaDelta.v
pr3_subst1.vo\
pr3_gen_context.vo\
pc1_defs.vo\
+ pc1_props.vo\
pc3_defs.vo\
pc3_props.vo\
pc3_gen.vo\
pc3_subst0.vo\
pc3_gen_context.vo\
ty0_defs.vo\
+ ty0_gen.vo\
ty0_lift.vo\
ty0_props.vo\
ty0_subst0.vo\
ty0_gen_context.vo\
csub0_defs.vo\
+ csub0_props.vo\
ty0_sred.vo\
ty0_sred_props.vo\
LambdaDelta.vo
pr3_subst1.vo\
pr3_gen_context.vo\
pc1_defs.vo\
+ pc1_props.vo\
pc3_defs.vo\
pc3_props.vo\
pc3_gen.vo\
pc3_subst0.vo\
pc3_gen_context.vo\
ty0_defs.vo\
+ ty0_gen.vo\
ty0_lift.vo\
ty0_props.vo\
ty0_subst0.vo\
ty0_gen_context.vo\
csub0_defs.vo\
+ csub0_props.vo\
ty0_sred.vo\
ty0_sred_props.vo\
LambdaDelta.vo
Require Export terms_defs.
- Inductive Set C := CSort : nat -> C
- | CTail : C -> K -> T -> C.
+ Inductive Set C := CSort: nat -> C
+ | CTail: C -> K -> T -> C.
Hint f3CKT : ltlc := Resolve (f_equal3 C K T).
Tactic Definition CGenBase :=
Match Context With
+ | [ H: (CSort ?) = (CSort ?) |- ? ] -> Inversion H; Clear H
| [ H: (CTail ? ? ?) = (CTail ? ? ?) |- ? ] -> Inversion H; Clear H
| _ -> TGenBase.
Section app_props. (******************************************************)
- Theorem app_csort : (t:?; i,n:?) (app (CSort n) i t) = t.
+ Theorem app_csort: (t:?; i,n:?) (app (CSort n) i t) = t.
XElim i; Intros; Simpl; XAuto.
Qed.
- Theorem app_O : (c:?; t:?) (app c (0) t) = t.
+ Theorem app_O: (c:?; t:?) (app c (0) t) = t.
XElim c; XAuto.
Qed.
Require Export pr0_defs.
(*#* #caption "current axioms for the relation $\\CprZ{}{}$",
- "reflexivity", "compaibility"
+ "reflexivity", "compatibility"
*)
(*#* #cap #cap c, c1, c2 #alpha u1 in V1, u2 in V2, k in z *)
Inductive csub0 [g:G] : C -> C -> Prop :=
(* structural rules *)
- | csub0_sort : (n:?) (csub0 g (CSort n) (CSort n))
- | csub0_tail : (c1,c2:?) (csub0 g c1 c2) -> (k,u:?)
- (csub0 g (CTail c1 k u) (CTail c2 k u))
+ | csub0_sort: (n:?) (csub0 g (CSort n) (CSort n))
+ | csub0_tail: (c1,c2:?) (csub0 g c1 c2) -> (k,u:?)
+ (csub0 g (CTail c1 k u) (CTail c2 k u))
(* axioms *)
- | csub0_void : (c1,c2:?) (csub0 g c1 c2) -> (b:?) ~b=Void -> (u1,u2:?)
- (csub0 g (CTail c1 (Bind Void) u1) (CTail c2 (Bind b) u2))
- | csub0_abst : (c1,c2:?) (csub0 g c1 c2) -> (u,t:?) (ty0 g c2 u t) ->
+ | csub0_void: (c1,c2:?) (csub0 g c1 c2) -> (b:?) ~b=Void -> (u1,u2:?)
+ (csub0 g (CTail c1 (Bind Void) u1) (CTail c2 (Bind b) u2))
+ | csub0_abst: (c1,c2:?) (csub0 g c1 c2) -> (u,t:?) (ty0 g c2 u t) ->
(csub0 g (CTail c1 (Bind Abst) t) (CTail c2 (Bind Abbr) u)).
Hint csub0 : ltlc := Constructors csub0.
Section csub0_props. (****************************************************)
- Theorem csub0_refl : (g:?; c:?) (csub0 g c c).
+ Theorem csub0_refl: (g:?; c:?) (csub0 g c c).
XElim c; XAuto.
Qed.
Section csub0_drop. (*****************************************************)
- Theorem csub0_drop_abbr : (g:?; n:?; c1,c2:?) (csub0 g c1 c2) -> (d1,u:?)
- (drop n (0) c1 (CTail d1 (Bind Abbr) u)) ->
- (EX d2 | (csub0 g d1 d2) &
- (drop n (0) c2 (CTail d2 (Bind Abbr) u))
- ).
+ Theorem csub0_drop_abbr: (g:?; n:?; c1,c2:?) (csub0 g c1 c2) -> (d1,u:?)
+ (drop n (0) c1 (CTail d1 (Bind Abbr) u)) ->
+ (EX d2 | (csub0 g d1 d2) &
+ (drop n (0) c2 (CTail d2 (Bind Abbr) u))
+ ).
XElim n.
(* case 1 : n = 0 *)
Intros; DropGenBase; Rewrite H0 in H; Inversion H; XEAuto.
XElim H; XEAuto.
Qed.
- Theorem csub0_drop_abst : (g:?; n:?; c1,c2:?) (csub0 g c1 c2) -> (d1,t:?)
- (drop n (0) c1 (CTail d1 (Bind Abst) t)) ->
- (EX d2 | (csub0 g d1 d2) &
- (drop n (0) c2 (CTail d2 (Bind Abst) t))
+ Theorem csub0_drop_abst: (g:?; n:?; c1,c2:?) (csub0 g c1 c2) -> (d1,t:?)
+ (drop n (0) c1 (CTail d1 (Bind Abst) t)) ->
+ (EX d2 | (csub0 g d1 d2) &
+ (drop n (0) c2 (CTail d2 (Bind Abst) t))
- ) \/
- (EX d2 u | (csub0 g d1 d2) &
- (drop n (0) c2 (CTail d2 (Bind Abbr) u)) &
- (ty0 g d2 u t)
- ).
+ ) \/
+ (EX d2 u | (csub0 g d1 d2) &
+ (drop n (0) c2 (CTail d2 (Bind Abbr) u)) &
+ (ty0 g d2 u t)
+ ).
XElim n.
(* case 1 : n = 0 *)
Intros; DropGenBase; Rewrite H0 in H; Inversion H; XEAuto.
LApply (csub0_drop_abst ?1 ?4 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
LApply (H1 ?5 ?6); [ Clear H1 H2; Intros H1 | XAuto ];
XElim H1; Intros H1; XElim H1; Intros.
-
- Section csub0_pc3. (*****************************************************)
-
- Theorem csub0_pr2 : (g:?; c1:?; t1,t2:?) (pr2 c1 t1 t2) ->
- (c2:?) (csub0 g c1 c2) -> (pr2 c2 t1 t2).
- Intros until 1; XElim H; Intros.
-(* case 1 : pr2_free *)
- XAuto.
-(* case 2 : pr2_delta *)
- CSub0Drop; XEAuto.
- Qed.
-
- Theorem csub0_pc2 : (g:?; c1:?; t1,t2:?) (pc2 c1 t1 t2) ->
- (c2:?) (csub0 g c1 c2) -> (pc2 c2 t1 t2).
- Intros until 1; XElim H; Intros.
-(* case 1 : pc2_r *)
- Apply pc2_r; EApply csub0_pr2; XEAuto.
-(* case 2 : pc2_x *)
- Apply pc2_x; EApply csub0_pr2; XEAuto.
- Qed.
-
- Theorem csub0_pc3 : (g:?; c1:?; t1,t2:?) (pc3 c1 t1 t2) ->
- (c2:?) (csub0 g c1 c2) -> (pc3 c2 t1 t2).
- Intros until 1; XElim H; Intros.
-(* case 1 : pc3_r *)
- XAuto.
-(* case 2 : pc3_u *)
- EApply pc3_u; [ EApply csub0_pc2; XEAuto | XAuto ].
- Qed.
-
- End csub0_pc3.
-
- Hints Resolve csub0_pc3 : ltlc.
-
- Section csub0_ty0. (*****************************************************)
-
- Theorem csub0_ty0 : (g:?; c1:?; t1,t2:?) (ty0 g c1 t1 t2) ->
- (c2:?) (wf0 g c2) -> (csub0 g c1 c2) ->
- (ty0 g c2 t1 t2).
- Intros until 1; XElim H; Intros.
-(* case 1 : ty0_conv *)
- EApply ty0_conv; XEAuto.
-(* case 2 : ty0_sort *)
- XEAuto.
-(* case 3 : ty0_abbr *)
- CSub0Drop; EApply ty0_abbr; XEAuto.
-(* case 4 : ty0_abst *)
- CSub0Drop; [ EApply ty0_abst | EApply ty0_abbr ]; XEAuto.
-(* case 5 : ty0_bind *)
- EApply ty0_bind; XEAuto.
-(* case 6 : ty0_appl *)
- EApply ty0_appl; XEAuto.
-(* case 7 : ty0_cast *)
- EApply ty0_cast; XAuto.
- Qed.
-
- Theorem csub0_ty0_ld : (g:?; c:?; u,v:?) (ty0 g c u v) -> (t1,t2:?)
- (ty0 g (CTail c (Bind Abst) v) t1 t2) ->
- (ty0 g (CTail c (Bind Abbr) u) t1 t2).
- Intros; EApply csub0_ty0; XEAuto.
- Qed.
-
- End csub0_ty0.
-
- Hints Resolve csub0_ty0 csub0_ty0_ld : ltlc.
-
- Tactic Definition CSub0Ty0 :=
- Match Context With
- [ _: (ty0 ?1 ?2 ?4 ?); _: (ty0 ?1 ?2 ?3 ?7); _: (pc3 ?2 ?4 ?7);
- H: (ty0 ?1 (CTail ?2 (Bind Abst) ?4) ?5 ?6) |- ? ] ->
- LApply (csub0_ty0_ld ?1 ?2 ?3 ?4); [ Intros H_x | EApply ty0_conv; XEAuto ];
- LApply (H_x ?5 ?6); [ Clear H_x H; Intros | XAuto ].
--- /dev/null
+(*#* #stop file *)
+
+Require pc3_props.
+Require csub0_defs.
+
+ Section csub0_pc3. (*****************************************************)
+
+ Theorem csub0_pr2: (g:?; c1:?; t1,t2:?) (pr2 c1 t1 t2) ->
+ (c2:?) (csub0 g c1 c2) -> (pr2 c2 t1 t2).
+ Intros until 1; XElim H; Intros.
+(* case 1: pr2_free *)
+ XAuto.
+(* case 2: pr2_delta *)
+ CSub0Drop; XEAuto.
+ Qed.
+
+ Hints Resolve csub0_pr2.
+
+ Opaque pc3.
+
+ Theorem csub0_pc3: (g:?; c1:?; t1,t2:?) (pc3 c1 t1 t2) ->
+ (c2:?) (csub0 g c1 c2) -> (pc3 c2 t1 t2).
+ Intros until 1; XElimUsing pc3_ind_left H; XEAuto.
+ Qed.
+
+ End csub0_pc3.
+
+ Hints Resolve csub0_pc3 : ltlc.
+
+ Section csub0_ty0. (*****************************************************)
+
+ Theorem csub0_ty0: (g:?; c1:?; t1,t2:?) (ty0 g c1 t1 t2) ->
+ (c2:?) (wf0 g c2) -> (csub0 g c1 c2) ->
+ (ty0 g c2 t1 t2).
+ Intros until 1; XElim H; Intros.
+(* case 1: ty0_conv *)
+ EApply ty0_conv; XEAuto.
+(* case 2: ty0_sort *)
+ XEAuto.
+(* case 3: ty0_abbr *)
+ CSub0Drop; EApply ty0_abbr; XEAuto.
+(* case 4: ty0_abst *)
+ CSub0Drop; [ EApply ty0_abst | EApply ty0_abbr ]; XEAuto.
+(* case 5: ty0_bind *)
+ EApply ty0_bind; XEAuto.
+(* case 6: ty0_appl *)
+ EApply ty0_appl; XEAuto.
+(* case 7: ty0_cast *)
+ EApply ty0_cast; XAuto.
+ Qed.
+
+ Theorem csub0_ty0_ld: (g:?; c:?; u,v:?) (ty0 g c u v) -> (t1,t2:?)
+ (ty0 g (CTail c (Bind Abst) v) t1 t2) ->
+ (ty0 g (CTail c (Bind Abbr) u) t1 t2).
+ Intros; EApply csub0_ty0; XEAuto.
+ Qed.
+
+ End csub0_ty0.
+
+ Hints Resolve csub0_ty0 csub0_ty0_ld : ltlc.
+
+ Tactic Definition CSub0Ty0 :=
+ Match Context With
+ [ _: (ty0 ?1 ?2 ?4 ?); _: (ty0 ?1 ?2 ?3 ?7); _: (pc3 ?2 ?4 ?7);
+ H: (ty0 ?1 (CTail ?2 (Bind Abst) ?4) ?5 ?6) |- ? ] ->
+ LApply (csub0_ty0_ld ?1 ?2 ?3 ?4); [ Intros H_x | EApply ty0_conv; XEAuto ];
+ LApply (H_x ?5 ?6); [ Clear H_x H; Intros | XAuto ].
Require Export subst0_defs.
Require Export drop_defs.
-(*#* #caption "current axioms for strict substitution in contexts",
+(*#* #caption "axioms for strict substitution in contexts",
"substituted tail item: second operand",
"substituted tail item: first operand",
"substituted tail item: both operands"
*)
(*#* #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_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)).
+ Inductive drop: nat -> nat -> C -> C -> Prop :=
+ | drop_sort: (h,d,n:?) (drop h d (CSort n) (CSort n))
+ | 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 *)
Section drop_gen_base. (**************************************************)
- Theorem drop_gen_sort : (n,h,d:?; x:?)
- (drop h d (CSort n) x) -> x = (CSort n).
+ Theorem drop_gen_sort: (n,h,d:?; x:?)
+ (drop h d (CSort n) x) -> x = (CSort n).
Intros until 1; InsertEq H '(CSort n); XElim H; Intros;
Try Inversion H1; XAuto.
Qed.
- Theorem drop_gen_refl : (x,e:?) (drop (0) (0) x e) -> x = e.
+ Theorem drop_gen_refl: (x,e:?) (drop (0) (0) x e) -> x = e.
Intros until 1; Repeat InsertEq H '(0); XElim H; Intros.
-(* case 1 : drop_sort *)
+(* case 1: drop_sort *)
XAuto.
-(* case 2 : drop_comp *)
+(* case 2: drop_comp *)
Rewrite H0; XAuto.
-(* case 3 : drop_drop *)
+(* case 3: drop_drop *)
Inversion H2.
-(* case 4 : drop_skip *)
+(* case 4: drop_skip *)
Inversion H1.
Qed.
- Theorem drop_gen_drop : (k:?; c,x:?; u:?; h:?)
- (drop (S h) (0) (CTail c k u) x) ->
- (drop (r k h) (0) c x).
+ Theorem drop_gen_drop: (k:?; c,x:?; u:?; h:?)
+ (drop (S h) (0) (CTail c k u) x) ->
+ (drop (r k h) (0) c x).
Intros until 1;
InsertEq H '(CTail c k u); InsertEq H '(0); InsertEq H '(S h);
XElim H; Intros.
-(* case 1 : drop_sort *)
+(* case 1: drop_sort *)
Inversion H1.
-(* case 2 : drop_comp *)
+(* case 2: drop_comp *)
Inversion H1.
-(* case 3 : drop_drop *)
+(* case 3: drop_drop *)
Inversion H1; Inversion H3.
Rewrite <- H5; Rewrite <- H6; Rewrite <- H7; XAuto.
-(* case 4 : drop_skip *)
+(* case 4: drop_skip *)
Inversion H2.
Qed.
- Theorem drop_gen_skip_r : (c,x:?; u:?; h,d:?; k:?)
- (drop h (S d) x (CTail c k u)) ->
- (EX e | x = (CTail e k (lift h (r k d) u)) & (drop h (r k d) e c)).
+ Theorem drop_gen_skip_r: (c,x:?; u:?; h,d:?; k:?)
+ (drop h (S d) x (CTail c k u)) ->
+ (EX e | x = (CTail e k (lift h (r k d) u)) & (drop h (r k d) e c)).
Intros; Inversion_clear H; XEAuto.
Qed.
- Theorem drop_gen_skip_l : (c,x:?; u:?; h,d:?; k:?)
- (drop h (S d) (CTail c k u) x) ->
- (EX e v | x = (CTail e k v) &
- u = (lift h (r k d) v) &
- (drop h (r k d) c e)
- ).
+ Theorem drop_gen_skip_l: (c,x:?; u:?; h,d:?; k:?)
+ (drop h (S d) (CTail c k u) x) ->
+ (EX e v | x = (CTail e k v) &
+ u = (lift h (r k d) v) &
+ (drop h (r k d) c e)
+ ).
Intros; Inversion_clear H; XEAuto.
Qed.
Hints Resolve drop_refl : ltlc.
- Theorem drop_S : (b:?; c,e:?; u:?; h:?)
- (drop h (0) c (CTail e (Bind b) u)) ->
- (drop (S h) (0) c e).
+ Theorem drop_S: (b:?; c,e:?; u:?; h:?)
+ (drop h (0) c (CTail e (Bind b) u)) ->
+ (drop (S h) (0) c e).
XElim c.
(* case 1: CSort *)
Intros; DropGenBase; Inversion H.
Match Context With
[ _: (drop ?1 (0) ?2 (CTail ?3 (Bind ?4) ?5)) |- ? ] ->
LApply (drop_S ?4 ?2 ?3 ?5 ?1); [ Intros | XAuto ].
-
Require Export subst0_defs.
Require Export csubst0_defs.
-(*#* #caption "axioms for strict substitution in focalized terms",
+(*#* #caption "\\kern-1.2pt axioms for strict substitution in focalized terms",
"substituted term part",
"substituted context part",
"substituted both parts"
| [ H1: (le ?1 ?2); H2: (lt ?2 (plus ?1 ?3));
H3: (TLRef ?2) = (lift ?3 ?1 ?4) |- ? ] ->
Apply (lift_gen_lref_false ?3 ?1 ?2 H1 H2 ?4 H3); XAuto
- | [ H: (TLRef ?1) = (lift (1) ?1 ?2) |- ? ] ->
+ | [ _: (TLRef ?1) = (lift (S ?1) (0) ?2) |- ? ] ->
+ EApply lift_gen_lref_false; [ Idtac | Idtac | XEAuto ]; XEAuto
+ | [ H: (TLRef ?1) = (lift (1) ?1 ?2) |- ? ] ->
LApply (lift_gen_lref_false (1) ?1 ?1); [ Intros H_x | XAuto ];
LApply H_x; [ Clear H_x; Intros H_x | Arith7' ?1; XAuto ];
LApply (H_x ?2); [ Clear H_x; Intros H_x | XAuto ];
(*#* #stop file *)
Require Export pr0_defs.
+Require Export pr1_defs.
- Inductive pc0 [t1,t2:T] : Prop :=
- | pc0_r : (pr0 t1 t2) -> (pc0 t1 t2)
- | pc0_x : (pr0 t2 t1) -> (pc0 t1 t2).
+ Definition pc1 := [t1,t2:?] (EX t | (pr1 t1 t) & (pr1 t2 t)).
- Hint pc0 : ltlc := Constructors pc0.
+ Hints Unfold pc1 : ltlc.
- Inductive pc1 : T -> T -> Prop :=
- | pc1_r : (t:?) (pc1 t t)
- | pc1_u : (t2,t1:?) (pc0 t1 t2) -> (t3:?) (pc1 t2 t3) -> (pc1 t1 t3).
-
- Hint pc1 : ltlc := Constructors pc1.
-
- Section pc0_props. (******************************************************)
-
- Theorem pc0_s : (t2,t1:?) (pc0 t1 t2) -> (pc0 t2 t1).
- Intros.
- Inversion H; XAuto.
- Qed.
-
- End pc0_props.
-
- Hints Resolve pc0_s : ltlc.
+ Tactic Definition Pc1Unfold :=
+ Match Context With
+ [ H: (pc1 ?2 ?3) |- ? ] -> Unfold pc1 in H; XDecompose H.
Section pc1_props. (******************************************************)
- Theorem pc1_pr0_r : (t1,t2:?) (pr0 t1 t2) -> (pc1 t1 t2).
+ Theorem pc1_pr0_r: (t1,t2:?) (pr0 t1 t2) -> (pc1 t1 t2).
XEAuto.
Qed.
- Theorem pc1_pr0_x : (t1,t2:?) (pr0 t2 t1) -> (pc1 t1 t2).
+ Theorem pc1_pr0_x: (t1,t2:?) (pr0 t2 t1) -> (pc1 t1 t2).
XEAuto.
Qed.
- Theorem pc1_pc0 : (t1,t2:?) (pc0 t1 t2) -> (pc1 t1 t2).
- XEAuto.
+ Theorem pc1_pr0_u: (t2,t1:?) (pr0 t1 t2) ->
+ (t3:?) (pc1 t2 t3) -> (pc1 t1 t3).
+ Intros; Pc1Unfold; XEAuto.
Qed.
-
- Theorem pc1_t : (t2,t1:?) (pc1 t1 t2) ->
- (t3:?) (pc1 t2 t3) -> (pc1 t1 t3).
- Intros t2 t1 H; XElim H; XEAuto.
+
+ Theorem pc1_refl: (t:?) (pc1 t t).
+ XEAuto.
Qed.
- Hints Resolve pc1_t : ltlc.
-
- Theorem pc1_s : (t2,t1:?) (pc1 t1 t2) -> (pc1 t2 t1).
- Intros; XElim H; XEAuto.
+ Theorem pc1_s: (t2,t1:?) (pc1 t1 t2) -> (pc1 t2 t1).
+ Intros; Pc1Unfold; XEAuto.
Qed.
Theorem pc1_tail_1: (u1,u2:?) (pc1 u1 u2) ->
(t:?; k:?) (pc1 (TTail k u1 t) (TTail k u2 t)).
- Intros; XElim H; Intros.
-(* case 1: pc1_r *)
- XAuto.
-(* case 2: pc1_u *)
- XElim H; Intros; XEAuto.
+ Intros; Pc1Unfold; XEAuto.
Qed.
Theorem pc1_tail_2: (t1,t2:?) (pc1 t1 t2) ->
(u:?; k:?) (pc1 (TTail k u t1) (TTail k u t2)).
- Intros; XElim H; Intros.
-(* case 1: pc1_r *)
- XAuto.
-(* case 2: pc1_u *)
- XElim H; Intros; XEAuto.
- Qed.
-
- Theorem pc1_tail: (u1,u2:?) (pc1 u1 u2) -> (t1,t2:?) (pc1 t1 t2) ->
- (k:?) (pc1 (TTail k u1 t1) (TTail k u2 t2)).
- Intros; EApply pc1_t; [ EApply pc1_tail_1 | EApply pc1_tail_2 ]; XAuto.
+ Intros; Pc1Unfold; XEAuto.
Qed.
End pc1_props.
- Hints Resolve pc1_pr0_r pc1_pr0_x pc1_pc0 pc1_t pc1_s
- pc1_tail_1 pc1_tail_2 pc1_tail : ltlc.
+ Hints Resolve pc1_refl pc1_pr0_u pc1_pr0_r pc1_pr0_x pc1_s
+ pc1_tail_1 pc1_tail_2 : ltlc.
--- /dev/null
+Require pr1_confluence.
+Require pc1_defs.
+
+(*#* #stop file *)
+
+ Section pc1_trans. (******************************************************)
+
+ Theorem pc1_t: (t2,t1:?) (pc1 t1 t2) ->
+ (t3:?) (pc1 t2 t3) -> (pc1 t1 t3).
+ Intros; Repeat Pc1Unfold; Pr1Confluence; XEAuto.
+ Qed.
+
+ Theorem pc1_pr0_u2: (t0,t1:?) (pr0 t0 t1) ->
+ (t2:?) (pc1 t0 t2) -> (pc1 t1 t2).
+ Intros; Apply (pc1_t t0); XAuto.
+ Qed.
+
+ Theorem pc1_tail: (u1,u2:?) (pc1 u1 u2) -> (t1,t2:?) (pc1 t1 t2) ->
+ (k:?) (pc1 (TTail k u1 t1) (TTail k u2 t2)).
+ Intros; EApply pc1_t; [ EApply pc1_tail_1 | EApply pc1_tail_2 ]; XAuto.
+ Qed.
+
+ End pc1_trans.
+
+ Hints Resolve pc1_t pc1_tail : ltlc.
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 *)
+(*#* #caption "the relation $\\PcT{}{}{}$" *)
+(*#* #cap #cap c, t, t1, t2 *)
- 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).
+ Definition pc3 := [c:?; t1,t2:?] (EX t | (pr3 c t1 t) & (pr3 c t2 t)).
(*#* #stop file *)
- Hint pc3 : ltlc := Constructors pc3.
+ Hints Unfold pc3 : ltlc.
- Section pc2_props. (******************************************************)
-
- Theorem pc2_s : (c,t2,t1:?) (pc2 c t1 t2) -> (pc2 c t2 t1).
- Intros.
- Inversion H; XAuto.
- Qed.
-
- Theorem pc2_shift : (h:?; c,e:?) (drop h (0) c e) ->
- (t1,t2:?) (pc2 c t1 t2) ->
- (pc2 e (app c h t1) (app c h t2)).
- Intros until 2; XElim H0; Intros.
-(* case 1 : pc2_r *)
- XAuto.
-(* case 2 : pc2_x *)
- XEAuto.
- Qed.
-
- End pc2_props.
-
- Hints Resolve pc2_s pc2_shift : ltlc.
+ Tactic Definition Pc3Unfold :=
+ Match Context With
+ [ H: (pc3 ?1 ?2 ?3) |- ? ] -> Unfold pc3 in H; XDecompose H.
Section pc3_props. (******************************************************)
- Theorem pc3_pr2_r : (c,t1,t2:?) (pr2 c t1 t2) -> (pc3 c t1 t2).
+ Theorem pc3_pr2_r: (c,t1,t2:?) (pr2 c t1 t2) -> (pc3 c t1 t2).
XEAuto.
Qed.
- Theorem pc3_pr2_x : (c,t1,t2:?) (pr2 c t2 t1) -> (pc3 c t1 t2).
+ Theorem pc3_pr2_x: (c,t1,t2:?) (pr2 c t2 t1) -> (pc3 c t1 t2).
XEAuto.
Qed.
- Theorem pc3_pc2 : (c,t1,t2:?) (pc2 c t1 t2) -> (pc3 c t1 t2).
+ Theorem pc3_pr3_r: (c:?; t1,t2) (pr3 c t1 t2) -> (pc3 c t1 t2).
XEAuto.
Qed.
- Theorem pc3_t : (t2,c,t1:?) (pc3 c t1 t2) ->
- (t3:?) (pc3 c t2 t3) -> (pc3 c t1 t3).
- Intros t2 c t1 H; XElim H; XEAuto.
- Qed.
-
- Hints Resolve pc3_t : ltlc.
-
- Theorem pc3_s : (c,t2,t1:?) (pc3 c t1 t2) -> (pc3 c t2 t1).
- Intros; XElim H; [ XAuto | XEAuto ].
- Qed.
-
- Hints Resolve pc3_s : ltlc.
-
- Theorem pc3_pr3_r : (c:?; t1,t2) (pr3 c t1 t2) -> (pc3 c t1 t2).
- Intros; XElim H; XEAuto.
- Qed.
-
- Theorem pc3_pr3_x : (c:?; t1,t2) (pr3 c t2 t1) -> (pc3 c t1 t2).
- Intros; XElim H; XEAuto.
- Qed.
-
- Hints Resolve pc3_pr3_r pc3_pr3_x : ltlc.
-
- Theorem pc3_pr3_t : (c:?; t1,t0:?) (pr3 c t1 t0) ->
- (t2:?) (pr3 c t2 t0) -> (pc3 c t1 t2).
- Intros; Apply (pc3_t t0); XAuto.
+ Theorem pc3_pr3_x: (c:?; t1,t2) (pr3 c t2 t1) -> (pc3 c t1 t2).
+ XEAuto.
Qed.
- Theorem pc3_thin_dx : (c:? ;t1,t2:?) (pc3 c t1 t2) ->
- (u:?; f:?) (pc3 c (TTail (Flat f) u t1)
- (TTail (Flat f) u t2)).
- Intros; XElim H; [XAuto | Intros ].
- EApply pc3_u; [ Inversion H | Apply H1 ]; XAuto.
+ Theorem pc3_pr3_t: (c:?; t1,t0:?) (pr3 c t1 t0) ->
+ (t2:?) (pr3 c t2 t0) -> (pc3 c t1 t2).
+ XEAuto.
Qed.
- Theorem pc3_tail_1 : (c:?; u1,u2:?) (pc3 c u1 u2) ->
- (k:?; t:?) (pc3 c (TTail k u1 t) (TTail k u2 t)).
- Intros until 1; XElim H; Intros.
-(* case 1 : pc3_r *)
- XAuto.
-(* case 2 : pc3_u *)
- EApply pc3_u; [ Inversion H | Apply H1 ]; XAuto.
+ Theorem pc3_pr2_u: (c:?; t2,t1:?) (pr2 c t1 t2) ->
+ (t3:?) (pc3 c t2 t3) -> (pc3 c t1 t3).
+ Intros; Pc3Unfold; XEAuto.
Qed.
-
- Theorem pc3_tail_2 : (c:?; u,t1,t2:?; k:?) (pc3 (CTail c k u) t1 t2) ->
- (pc3 c (TTail k u t1) (TTail k u t2)).
- Intros.
- XElim H; [ Idtac | Intros; Inversion H ]; XEAuto.
+
+ Theorem pc3_refl: (c:?; t:?) (pc3 c t t).
+ XEAuto.
Qed.
- Theorem pc3_tail_12 : (c:?; u1,u2:?) (pc3 c u1 u2) ->
- (k:?; t1,t2:?) (pc3 (CTail c k u2) t1 t2) ->
- (pc3 c (TTail k u1 t1) (TTail k u2 t2)).
- Intros.
- EApply pc3_t; [ Apply pc3_tail_1 | Apply pc3_tail_2 ]; XAuto.
+ Theorem pc3_s: (c,t2,t1:?) (pc3 c t1 t2) -> (pc3 c t2 t1).
+ Intros; Pc3Unfold; XEAuto.
Qed.
- Theorem pc3_tail_21 : (c:?; u1,u2:?) (pc3 c u1 u2) ->
- (k:?; t1,t2:?) (pc3 (CTail c k u1) t1 t2) ->
- (pc3 c (TTail k u1 t1) (TTail k u2 t2)).
- Intros.
- EApply pc3_t; [ Apply pc3_tail_2 | Apply pc3_tail_1 ]; XAuto.
+ Theorem pc3_thin_dx: (c:? ;t1,t2:?) (pc3 c t1 t2) ->
+ (u:?; f:?) (pc3 c (TTail (Flat f) u t1)
+ (TTail (Flat f) u t2)).
+ Intros; Pc3Unfold; XEAuto.
Qed.
- Theorem pc3_pr3_u : (c:?; t2,t1:?) (pr2 c t1 t2) ->
- (t3:?) (pc3 c t2 t3) -> (pc3 c t1 t3).
- XEAuto.
+ Theorem pc3_tail_1: (c:?; u1,u2:?) (pc3 c u1 u2) ->
+ (k:?; t:?) (pc3 c (TTail k u1 t) (TTail k u2 t)).
+ Intros; Pc3Unfold; XEAuto.
Qed.
- Theorem pc3_pr3_u2 : (c:?; t0,t1:?) (pr2 c t0 t1) ->
- (t2:?) (pc3 c t0 t2) -> (pc3 c t1 t2).
- Intros; Apply (pc3_t t0); XAuto.
+ Theorem pc3_tail_2: (c:?; u,t1,t2:?; k:?) (pc3 (CTail c k u) t1 t2) ->
+ (pc3 c (TTail k u t1) (TTail k u t2)).
+ Intros; Pc3Unfold; XEAuto.
Qed.
- Theorem pc3_shift : (h:?; c,e:?) (drop h (0) c e) ->
- (t1,t2:?) (pc3 c t1 t2) ->
- (pc3 e (app c h t1) (app c h t2)).
- Intros until 2; XElim H0; Clear t1 t2; Intros.
-(* case 1 : pc3_r *)
- XAuto.
-(* case 2 : pc3_u *)
- XEAuto.
+ Theorem pc3_shift: (h:?; c,e:?) (drop h (0) c e) ->
+ (t1,t2:?) (pc3 c t1 t2) ->
+ (pc3 e (app c h t1) (app c h t2)).
+ Intros; Pc3Unfold; XEAuto.
Qed.
Theorem pc3_pc1: (t1,t2:?) (pc1 t1 t2) -> (c:?) (pc3 c t1 t2).
- Intros; XElim H; Intros.
-(* case 1: pc1_r *)
- XAuto.
-(* case 2 : pc1_u *)
- XElim H; XEAuto.
+ Intros; Pc1Unfold; XEAuto.
Qed.
-
+
End pc3_props.
- Hints Resolve pc3_pr2_r pc3_pr2_x pc3_pc2 pc3_pr3_r pc3_pr3_x
- pc3_t pc3_s pc3_pr3_t pc3_thin_dx pc3_tail_1 pc3_tail_2
- pc3_tail_12 pc3_tail_21 pc3_pr3_u pc3_shift pc3_pc1 : ltlc.
-
- Tactic Definition Pc3T :=
- Match Context With
- | [ _: (pr3 ?1 ?2 (TTail ?3 ?4 ?5)); _: (pc3 ?1 ?6 ?4) |- ? ] ->
- 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 ].
+ Hints Resolve pc3_refl pc3_pr2_r pc3_pr2_x pc3_pr3_r pc3_pr3_x
+ pc3_s pc3_pr3_t pc3_thin_dx pc3_tail_1 pc3_tail_2
+ pc3_pr2_u pc3_shift pc3_pc1 : ltlc.
Section pc3_gen. (********************************************************)
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.
+ Intros; Pc3Unfold; Repeat Pr3GenBase.
+ Rewrite H0 in H; Clear H0 x c.
+ TGenBase; XAuto.
Qed.
Theorem pc3_gen_abst: (c:?; u1,u2,t1,t2:?)
(pc3 c u1 u2) /\
(b:?; u:?) (pc3 (CTail c (Bind b) u) t1 t2).
Intros.
- Pc3Confluence; Repeat Pr3GenBase; Rewrite H0 in H1; Clear H0 x.
- Inversion H1; Rewrite H0 in H4; Rewrite H6 in H5.
+ Pc3Unfold; Repeat Pr3GenBase; Rewrite H1 in H; Clear H1 x.
+ TGenBase; Rewrite H1 in H4; Rewrite H6 in H5.
XEAuto.
Qed.
(e:?) (drop h d c e) ->
(pc3 e t1 t2).
Intros.
- Pc3Confluence; Repeat Pr3Gen; Rewrite H2 in H1; Clear H2 x.
- LiftGen; Rewrite H in H3; XEAuto.
+ Pc3Unfold; Repeat Pr3Gen; Rewrite H2 in H; Clear H2 x.
+ LiftGen; Rewrite H in H4; XEAuto.
Qed.
Theorem pc3_gen_not_abst: (b:?) ~b=Abst -> (c:?; t1,t2,u1,u2:?)
(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;
+ Try EqFalse; Pc3Unfold; Repeat Pr3Gen;
+ Try (Rewrite H0 in H3; TGenBase);
+ Rewrite H1 in H0; Clear H H1 x;
EApply pc3_pr3_t; XEAuto.
Qed.
Theorem pc3_gen_lift_abst: (c:?; t,t2,u2:?; h,d:?)
(pc3 c (lift h d t)
- (TTail (Bind Abst) u2 t2)
+ (TTail (Bind Abst) u2 t2)
) ->
(e:?) (drop h d c e) ->
(EX u1 t1 | (pr3 e t (TTail (Bind Abst) u1 t1)) &
(b:B; u:T)(pr3 (CTail c (Bind b) u) t2 (lift h (S d) t1))
).
Intros.
- Pc3Confluence; Repeat Pr3Gen; Rewrite H in H2; Clear H x.
+ Pc3Unfold; Repeat Pr3Gen; Rewrite H1 in H; Clear H1 x.
LiftGenBase; Rewrite H in H3; Rewrite H1 in H4; Rewrite H2 in H5; XEAuto.
Qed.
_: (drop ?2 ?3 ?1 ?7) |- ? ] ->
LApply (pc3_gen_lift_abst ?1 ?4 ?6 ?5 ?2 ?3); [ Intros H_x | XAuto ];
LApply (H_x ?7); [ Clear H_x; Intros H_x | XAuto ];
- XElim H_x; Intros.
+ XElim H_x; Intros
+ | _ -> Pr3Gen.
(x1:?) (subst1 d u t1 (lift (1) d x1)) ->
(x2:?) (subst1 d u t2 (lift (1) d x2)) ->
(pc3 a x1 x2).
- Intros; Pc3Confluence; Repeat Pr3GenContext.
- Subst1Confluence; Rewrite H in H3; Clear H x3; XEAuto.
+ Intros; Pc3Unfold; Repeat Pr3GenContext.
+ Subst1Confluence; Rewrite H3 in H5; Clear H3 x3; XEAuto.
Qed.
End pc3_gen_context.
Require pr3_confluence.
Require pc3_defs.
- Section pc3_confluence. (*************************************************)
+ Section pc3_trans. (******************************************************)
- 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 *)
- XEAuto.
-(* case 2: pc3_u *)
- Clear H0; XElim H1; Intros.
- Inversion_clear H; [ XEAuto | Pr3Confluence; XEAuto ].
+ Theorem pc3_t: (t2,c,t1:?) (pc3 c t1 t2) ->
+ (t3:?) (pc3 c t2 t3) -> (pc3 c t1 t3).
+ Intros; Repeat Pc3Unfold; Pr3Confluence; XEAuto.
Qed.
- End pc3_confluence.
+ Theorem pc3_pr2_u2: (c:?; t0,t1:?) (pr2 c t0 t1) ->
+ (t2:?) (pc3 c t0 t2) -> (pc3 c t1 t2).
+ Intros; Apply (pc3_t t0); XAuto.
+ Qed.
+
+ Theorem pc3_tail_12: (c:?; u1,u2:?) (pc3 c u1 u2) ->
+ (k:?; t1,t2:?) (pc3 (CTail c k u2) t1 t2) ->
+ (pc3 c (TTail k u1 t1) (TTail k u2 t2)).
+ Intros.
+ EApply pc3_t; [ Apply pc3_tail_1 | Apply pc3_tail_2 ]; XAuto.
+ Qed.
+
+ Theorem pc3_tail_21: (c:?; u1,u2:?) (pc3 c u1 u2) ->
+ (k:?; t1,t2:?) (pc3 (CTail c k u1) t1 t2) ->
+ (pc3 c (TTail k u1 t1) (TTail k u2 t2)).
+ Intros.
+ EApply pc3_t; [ Apply pc3_tail_2 | Apply pc3_tail_1 ]; XAuto.
+ Qed.
+
+ End pc3_trans.
+
+ Hints Resolve pc3_t pc3_tail_12 pc3_tail_21 : ltlc.
- Tactic Definition Pc3Confluence :=
+ Tactic Definition Pc3T :=
Match Context With
- [ H: (pc3 ?1 ?2 ?3) |- ? ] ->
- LApply (pc3_confluence ?1 ?2 ?3); [ Clear H; Intros H | XAuto ];
- XElim H; Intros.
+ | [ _: (pr3 ?1 ?2 (TTail ?3 ?4 ?5)); _: (pc3 ?1 ?6 ?4) |- ? ] ->
+ 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_context. (****************************************************)
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 pc3_pr2_u.
EApply pr2_delta; XEAuto.
Apply pc3_pr2_x; EApply pr2_delta; [ Idtac | XEAuto | XEAuto ]; XEAuto.
(* case 2.2: i0 > 0 *)
(* case 1: pr3_refl *)
XAuto.
(* case 2: pr3_sing *)
- Apply H1; Pc3Confluence.
+ Apply H1; Pc3Unfold.
EApply pc3_t; [ Idtac | Apply pc3_s ]; EApply pc3_pr2_pr3_t; XEAuto.
Qed.
(pc3 c (lift h d t1) (lift h d t2)).
Intros.
- Pc3Confluence.
- EApply pc3_pr3_t; (EApply pr3_lift; [ XEAuto | Apply H0 Orelse Apply H1 ]).
+ Pc3Unfold.
+ EApply pc3_pr3_t; (EApply pr3_lift; [ XEAuto | Apply H1 Orelse Apply H2 ]).
Qed.
End pc3_lift.
XAuto.
(* case 1.2.2: pr2_delta *)
Cpr0Drop; Pr0Subst0.
- EApply pc3_pr3_u; [ EApply pr2_delta; XEAuto | XAuto ].
+ EApply pc3_pr2_u; [ EApply pr2_delta; XEAuto | XAuto ].
Qed.
Theorem pc3_cpr0_t: (c1,c2:?) (cpr0 c1 c2) ->
(* case 1: cpr0_refl *)
XAuto.
(* case 2: cpr0_comp *)
- Pc3Context; Pc3Confluence.
+ Pc3Context; Pc3Unfold.
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).
- Intros; Pc3Confluence.
+ Intros; Pc3Unfold.
EApply pc3_t; [ Idtac | Apply pc3_s ]; EApply pc3_cpr0_t; XEAuto.
Qed.
End pc3_cpr0.
Hints Resolve pc3_cpr0 : ltlc.
+
+ Section pc3_ind_left. (***************************************************)
+
+ Inductive pc3_left [c:C] : T -> T -> Prop :=
+ | pc3_left_r : (t:?) (pc3_left c t t)
+ | pc3_left_ur: (t1,t2:?) (pr2 c t1 t2) -> (t3:?) (pc3_left c t2 t3) ->
+ (pc3_left c t1 t3)
+ | pc3_left_ux: (t1,t2:?) (pr2 c t1 t2) -> (t3:?) (pc3_left c t1 t3) ->
+ (pc3_left c t2 t3).
+
+ Hint pc3_left: ltlc := Constructors pc3_left.
+
+ Remark pc3_left_pr3: (c:?; t1,t2:?) (pr3 c t1 t2) -> (pc3_left c t1 t2).
+ Intros; XElim H; XEAuto.
+ Qed.
+
+ Remark pc3_left_trans: (c:?; t1,t2:?) (pc3_left c t1 t2) ->
+ (t3:?) (pc3_left c t2 t3) -> (pc3_left c t1 t3).
+ Intros until 1; XElim H; XEAuto.
+ Qed.
+
+ Hints Resolve pc3_left_trans : ltlc.
+
+ Remark pc3_left_sym: (c:?; t1,t2:?) (pc3_left c t1 t2) ->
+ (pc3_left c t2 t1).
+ Intros; XElim H; XEAuto.
+ Qed.
+
+ Hints Resolve pc3_left_sym pc3_left_pr3 : ltlc.
+
+ Remark pc3_left_pc3: (c:?; t1,t2:?) (pc3 c t1 t2) -> (pc3_left c t1 t2).
+ Intros; Pc3Unfold; XEAuto.
+ Qed.
+
+ Remark pc3_pc3_left: (c:?; t1,t2:?) (pc3_left c t1 t2) -> (pc3 c t1 t2).
+ Intros; XElim H; XEAuto.
+ Qed.
+
+ Hints Resolve pc3_left_pc3 pc3_pc3_left : ltlc.
+
+ Theorem pc3_ind_left: (c:C; P:(T->T->Prop))
+ ((t:T) (P t t)) ->
+ ((t1,t2:T) (pr2 c t1 t2) -> (t3:T) (pc3 c t2 t3) -> (P t2 t3) -> (P t1 t3)) ->
+ ((t1,t2:T) (pr2 c t1 t2) -> (t3:T) (pc3 c t1 t3) -> (P t1 t3) -> (P t2 t3)) ->
+ (t,t0:T) (pc3 c t t0) -> (P t t0).
+ Intros; ElimType (pc3_left c t t0); XEAuto.
+ Qed.
+
+ End pc3_ind_left.
Require fsubst0_defs.
Require pr0_subst0.
Require pc3_defs.
+Require pc3_props.
Section pc3_fsubst0. (****************************************************)
(* case 1: pr2_free *)
Intros until 2; XElim H0; Intros.
(* case 1.1: fsubst0_snd *)
- Pr0Subst0; [ XAuto | Apply (pc3_pr3_u c1 x); XEAuto ].
+ Pr0Subst0; [ XAuto | Apply (pc3_pr2_u c1 x); XEAuto ].
(* case 1.2: fsubst0_fst *)
XAuto.
(* case 1.3: fsubst0_both *)
- Pr0Subst0; CSubst0Drop; [ XAuto | Apply (pc3_pr3_u c0 x); XEAuto ].
+ Pr0Subst0; CSubst0Drop; [ XAuto | Apply (pc3_pr2_u c0 x); XEAuto ].
(* case 2 : pr2_delta *)
Intros until 4; XElim H2; Intros.
(* case 2.1: fsubst0_snd. *)
(* 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.
+ Apply (pc3_pr2_u c0 x); XEAuto.
(* 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 *)
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.
+ Apply (pc3_pr2_u c0 x); XEAuto.
(* case 2.2.5: i >= i0 *)
XEAuto.
(* 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.
+ CSubst0Drop; Apply pc3_pr2_u2 with t0 := t1; 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_u2 c0 t1); [ Idtac | Apply (pc3_pr3_u c0 x) ]; XEAuto.
+ Apply (pc3_pr2_u2 c0 t1); [ Idtac | Apply (pc3_pr2_u c0 x) ]; 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_u2 c0 t1); [ Idtac | Apply pc3_pr2_r ]; XEAuto.
+ CSubst0Drop; Apply (pc3_pr2_u2 c0 t1); [ 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_u2 c0 t1); [ Idtac | Apply (pc3_pr3_u c0 x) ]; XEAuto.
+ Apply (pc3_pr2_u2 c0 t1); [ Idtac | Apply (pc3_pr2_u c0 x) ]; XEAuto.
(* case 2.3.5: i >= i0 *)
- CSubst0Drop; Apply (pc3_pr3_u2 c0 t1); XEAuto.
+ CSubst0Drop; Apply (pc3_pr2_u2 c0 t1); XEAuto.
Qed.
Theorem pc3_pr2_fsubst0_back: (c1:?; t,t1:?) (pr2 c1 t t1) ->
(* case 1: pr2_free *)
Intros until 2; XElim H0; Intros.
(* case 1.1: fsubst0_snd. *)
- Apply (pc3_pr3_u c1 t2); XEAuto.
+ Apply (pc3_pr2_u c1 t2); XEAuto.
(* case 1.2: fsubst0_fst. *)
XAuto.
(* case 1.3: fsubst0_both. *)
- CSubst0Drop; Apply (pc3_pr3_u c0 t2); XEAuto.
+ CSubst0Drop; Apply (pc3_pr2_u c0 t2); XEAuto.
(* case 2: pr2_delta *)
Intros until 4; XElim H2; Intros.
(* case 2.1: fsubst0_snd. *)
(* case 2.2.2: i < i0, csubst0_bind *)
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.
+ Apply (pc3_pr2_u c0 x); XEAuto.
(* 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 *)
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.
+ Apply (pc3_pr2_u c0 x); XEAuto.
(* case 2.2.5: i >= i0 *)
XEAuto.
(* 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:=t2; Try Apply pc3_pr3_r; XEAuto.
+ CSubst0Drop; Apply pc3_pr2_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 t0) ]; XEAuto.
+ Apply (pc3_pr2_u c0 x); [ Idtac | Apply (pc3_pr2_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.
+ CSubst0Drop; Apply (pc3_pr2_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.
+ Apply (pc3_pr2_u c0 x); [ Idtac | Apply (pc3_pr2_u2 c0 t0) ]; XEAuto.
(* case 2.3.5: i >= i0 *)
- CSubst0Drop; Apply (pc3_pr3_u c0 t0); XEAuto.
+ CSubst0Drop; Apply (pc3_pr2_u c0 t0); XEAuto.
Qed.
- Theorem pc3_pc2_fsubst0: (c1:?; t1,t:?) (pc2 c1 t1 t) ->
- (i:?; u,c2,t2:?) (fsubst0 i u c1 t1 c2 t2) ->
- (e:?) (drop i (0) c1 (CTail e (Bind Abbr) u)) ->
- (pc3 c2 t2 t).
- Intros until 1; XElim H; Intros.
-(* case 1: pc2_r *)
- EApply pc3_pr2_fsubst0; XEAuto.
-(* case 2: pc2_x *)
- Apply pc3_s; EApply pc3_pr2_fsubst0_back; XEAuto.
- Qed.
+ Opaque pc3.
Theorem pc3_fsubst0: (c1:?; t1,t:?) (pc3 c1 t1 t) ->
(i:?; u,c2,t2:?) (fsubst0 i u c1 t1 c2 t2) ->
(e:?) (drop i (0) c1 (CTail e (Bind Abbr) u)) ->
(pc3 c2 t2 t).
- Intros until 1; XElim H.
-(* case 1: pc3_r *)
+ Intros until 1; XElimUsing pc3_ind_left H.
+(* case 1: pc3_refl *)
Intros until 1; XElim H; Intros; Try CSubst0Drop; XEAuto.
-(* case 2: pc3_u *)
+(* case 2: pc3_pr2_u *)
+ Intros until 4; XElim H2; Intros;
+ (Apply (pc3_t t2); [ EApply pc3_pr2_fsubst0; XEAuto | XEAuto ]).
+(* case 2: pc3_pr2_u2 *)
Intros until 4; XElim H2; Intros;
- (Apply (pc3_t t2); [ EApply pc3_pc2_fsubst0; XEAuto | XEAuto ]).
+ (Apply (pc3_t t0); [ Apply pc3_s; EApply pc3_pr2_fsubst0_back; XEAuto | XEAuto ]).
Qed.
End pc3_fsubst0.
- Hints Resolve pc3_fsubst0.
+ Hints Resolve pc3_fsubst0 : ltlc.
Require Export subst0_defs.
(*#* #caption "axioms for the relation $\\PrZ{}{}$",
- "reflexivity", "compaibility", "$\\beta$-contraction", "$\\upsilon$-swap",
+ "reflexivity", "compatibility", "$\\beta$-contraction", "$\\upsilon$-swap",
"$\\delta$-expansion", "$\\zeta$-contraction", "$\\epsilon$-contraction"
*)
(*#* #cap #cap t, t1, t2 #alpha u in V, u1 in V1, u2 in V2, v1 in W1, v2 in W2, w in T, k in z *)
Require Export pr0_defs.
Inductive pr1 : T -> T -> Prop :=
- | pr1_r : (t:?) (pr1 t t)
- | pr1_u : (t2,t1:?) (pr0 t1 t2) -> (t3:?) (pr1 t2 t3) -> (pr1 t1 t3).
+ | pr1_r: (t:?) (pr1 t t)
+ | pr1_u: (t2,t1:?) (pr0 t1 t2) -> (t3:?) (pr1 t2 t3) -> (pr1 t1 t3).
Hint pr1 : ltlc := Constructors pr1.
Section pr1_props. (******************************************************)
- Theorem pr1_pr0 : (t1,t2:?) (pr0 t1 t2) -> (pr1 t1 t2).
+ Theorem pr1_pr0: (t1,t2:?) (pr0 t1 t2) -> (pr1 t1 t2).
XEAuto.
Qed.
- Theorem pr1_t : (t2,t1:?) (pr1 t1 t2) ->
+ Theorem pr1_t: (t2,t1:?) (pr1 t1 t2) ->
(t3:?) (pr1 t2 t3) -> (pr1 t1 t3).
- Intros t2 t1 H; XElim H; XEAuto.
+ Intros until 1; XElim H; XEAuto.
+ Qed.
+
+ Theorem pr1_tail_1: (u1,u2:?) (pr1 u1 u2) ->
+ (t:?; k:?) (pr1 (TTail k u1 t) (TTail k u2 t)).
+ Intros; XElim H; XEAuto.
+ Qed.
+
+ Theorem pr1_tail_2: (t1,t2:?) (pr1 t1 t2) ->
+ (u:?; k:?) (pr1 (TTail k u t1) (TTail k u t2)).
+ Intros; XElim H; XEAuto.
Qed.
End pr1_props.
- Hints Resolve pr1_pr0 pr1_t : ltlc.
+ Hints Resolve pr1_pr0 pr1_t pr1_tail_1 pr1_tail_2 : ltlc.
Intros until 1; XElim H; XEAuto.
Qed.
+ Theorem pr3_thin_dx: (c:?; t1,t2:?) (pr3 c t1 t2) ->
+ (u:?; f:?) (pr3 c (TTail (Flat f) u t1)
+ (TTail (Flat f) u t2)).
+ Intros; 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)).
Intros until 1; XElim H; Intros.
End pr3_props.
Hints Resolve pr3_pr2 pr3_t pr3_pr1
- pr3_tail_12 pr3_tail_21 pr3_shift : ltlc.
+ pr3_thin_dx pr3_tail_12 pr3_tail_21 pr3_shift : ltlc.
Require Export Base.
- Inductive Set B := Abbr : B
- | Abst : B
- | Void : B.
+ Inductive Set B := Abbr: B
+ | Abst: B
+ | Void: B.
- Inductive Set F := Appl : F
- | Cast : F.
+ Inductive Set F := Appl: F
+ | Cast: F.
- Inductive Set K := Bind : B -> K
- | Flat : F -> K.
+ Inductive Set K := Bind: B -> K
+ | Flat: F -> K.
- Inductive Set T := TSort : nat -> T
- | TLRef : nat -> T
- | TTail : K -> T -> T -> T.
+ Inductive Set T := TSort: 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: (TSort ?) = (TSort ?) |- ? ] -> Inversion H; Clear H
+ | [ H: (TLRef ?) = (TLRef ?) |- ? ] -> Inversion H; Clear H
| [ H: (TTail ? ? ?) = (TTail ? ? ?) |- ? ] -> Inversion H; Clear H
| _ -> Idtac.
End s_props.
- Hints Resolve s_le s_lt s_inj.
+ Hints Resolve s_le s_lt s_inj : ltlc.
Tactic Definition SRw :=
Repeat (Rewrite s_S Orelse Rewrite s_plus_sym).
(*#* #stop record *)
Record G : Set := {
- f : nat -> nat;
- f_inc : (n:?) (lt n (f n))
+ next : nat -> nat;
+ base : nat;
+ next_lt : (n:?) (lt n (next n));
+ base_next: (n:?) (le base n) -> (next n) = (S n)
}.
(*#* #start record *)
-(*#* #caption "typing",
+(*#* #caption "current axioms for typing",
"well formed context sort", "well formed context binder",
"conversion rule", "typed sort", "typed reference to abbreviation",
"typed reference to abstraction", "typed binder", "typed application",
"typed cast"
*)
+(*#* #cap #cap c, d, t, t0, t1, t2, w #alpha m in h, n in i, u in V, v in U *)
+
Inductive wf0 [g:G] : C -> Prop :=
- | wf0_sort : (m:?) (wf0 g (CSort m))
- | wf0_bind : (c:?; u,t:?) (ty0 g c u t) ->
- (b:?) (wf0 g (CTail c (Bind b) u))
+ | wf0_sort: (m:?) (wf0 g (CSort m))
+ | wf0_bind: (c:?; u,t:?) (ty0 g c u t) ->
+ (b:?) (wf0 g (CTail c (Bind b) u))
with ty0 [g:G] : C -> T -> T -> Prop :=
(* structural rules *)
- | ty0_conv : (c:?; t2,t:?) (ty0 g c t2 t) ->
- (u,t1:?) (ty0 g c u t1) -> (pc3 c t1 t2) ->
- (ty0 g c u t2)
+ | ty0_conv: (c:?; t2,t:?) (ty0 g c t2 t) ->
+ (u,t1:?) (ty0 g c u t1) -> (pc3 c t1 t2) ->
+ (ty0 g c u t2)
(* axiom rules *)
- | ty0_sort : (c:?) (wf0 g c) ->
- (m:?) (ty0 g c (TSort m) (TSort (f g m)))
- | ty0_abbr : (c:?) (wf0 g c) ->
- (n:?; d:?; u:?) (drop n (0) c (CTail d (Bind Abbr) u)) ->
- (t:?) (ty0 g d u t) ->
- (ty0 g c (TLRef n) (lift (S n) (0) t))
- | ty0_abst : (c:?) (wf0 g c) ->
- (n:?; d:?; u:?) (drop n (0) c (CTail d (Bind Abst) u)) ->
- (t:?) (ty0 g d u t) ->
- (ty0 g c (TLRef n) (lift (S n) (0) u))
- | ty0_bind : (c:?; u,t:?) (ty0 g c u t) ->
- (b:?; t1,t2:?) (ty0 g (CTail c (Bind b) u) t1 t2) ->
- (t0:?) (ty0 g (CTail c (Bind b) u) t2 t0) ->
- (ty0 g c (TTail (Bind b) u t1) (TTail (Bind b) u t2))
- | ty0_appl : (c:?; w,u:?) (ty0 g c w u) ->
- (v,t:?) (ty0 g c v (TTail (Bind Abst) u t)) ->
- (ty0 g c (TTail (Flat Appl) w v)
- (TTail (Flat Appl) w (TTail (Bind Abst) u t))
- )
- | ty0_cast : (c:?; t1,t2:?) (ty0 g c t1 t2) ->
- (t0:?) (ty0 g c t2 t0) ->
- (ty0 g c (TTail (Flat Cast) t2 t1) t2).
+ | ty0_sort: (c:?) (wf0 g c) ->
+ (m:?) (ty0 g c (TSort m) (TSort (next g m)))
+ | ty0_abbr: (c:?) (wf0 g c) ->
+ (n:?; d:?; u:?) (drop n (0) c (CTail d (Bind Abbr) u)) ->
+ (t:?) (ty0 g d u t) ->
+ (ty0 g c (TLRef n) (lift (S n) (0) t))
+ | ty0_abst: (c:?) (wf0 g c) ->
+ (n:?; d:?; u:?) (drop n (0) c (CTail d (Bind Abst) u)) ->
+ (t:?) (ty0 g d u t) ->
+ (ty0 g c (TLRef n) (lift (S n) (0) u))
+ | ty0_bind: (c:?; u,t:?) (ty0 g c u t) ->
+ (b:?; t1,t2:?) (ty0 g (CTail c (Bind b) u) t1 t2) ->
+ (t0:?) (ty0 g (CTail c (Bind b) u) t2 t0) ->
+ (ty0 g c (TTail (Bind b) u t1) (TTail (Bind b) u t2))
+ | ty0_appl: (c:?; w,u:?) (ty0 g c w u) ->
+ (v,t:?) (ty0 g c v (TTail (Bind Abst) u t)) ->
+ (ty0 g c (TTail (Flat Appl) w v)
+ (TTail (Flat Appl) w (TTail (Bind Abst) u t))
+ )
+ | ty0_cast: (c:?; t1,t2:?) (ty0 g c t1 t2) ->
+ (t0:?) (ty0 g c t2 t0) ->
+ (ty0 g c (TTail (Flat Cast) t2 t1) t2).
+
+(*#* #stop file *)
Hint wf0 : ltlc := Constructors wf0.
Hint ty0 : ltlc := Constructors ty0.
-(*#* #caption "generation lemma of typing" #clauses ty0_gen_base *)
-
- Section ty0_gen_base. (***************************************************)
-
-(*#* #caption "generation lemma for sort" *)
-(*#* #cap #cap c #alpha x in T, n in h *)
-
- Theorem ty0_gen_sort: (g:?; c:?; x:?; n:?)
- (ty0 g c (TSort n) x) ->
- (pc3 c (TSort (f g n)) x).
-
-(*#* #stop proof *)
-
- Intros until 1; InsertEq H '(TSort n); XElim H; Intros.
-(* case 1 : ty0_conv *)
- XEAuto.
-(* case 2 : ty0_sort *)
- Inversion H0; XAuto.
-(* case 3 : ty0_abbr *)
- Inversion H3.
-(* case 4 : ty0_abst *)
- Inversion H3.
-(* case 5 : ty0_bind *)
- Inversion H5.
-(* case 6 : ty0_appl *)
- Inversion H3.
-(* case 7 : ty0_cast *)
- Inversion H3.
- Qed.
-
-(*#* #start proof *)
-
-(*#* #caption "generation lemma for bound reference" *)
-(*#* #cap #cap c, e #alpha x in T, t in U, u in V, n in i *)
-
- Theorem ty0_gen_lref: (g:?; c:?; x:?; n:?) (ty0 g c (TLRef n) x) ->
- (EX e u t | (pc3 c (lift (S n) (0) t) x) &
- (drop n (0) c (CTail e (Bind Abbr) u)) &
- (ty0 g e u t)
- ) \/
- (EX e u t | (pc3 c (lift (S n) (0) u) x) &
- (drop n (0) c (CTail e (Bind Abst) u)) &
- (ty0 g e u t)
- ).
-
-(*#* #stop proof *)
-
- Intros until 1; InsertEq H '(TLRef n); XElim H; Intros.
-(* case 1 : ty0_conv *)
- LApply H2; [ Clear H2; Intros H2 | XAuto ].
- XElim H2; Intros; XElim H2; XEAuto.
-(* case 2 : ty0_sort *)
- Inversion H0.
-(* case 3 : ty0_abbr *)
- Inversion H3 ; Rewrite H5 in H0; XEAuto.
-(* case 4 : ty0_abst *)
- Inversion H3; Rewrite H5 in H0; XEAuto.
-(* case 5 : ty0_bind *)
- Inversion H5.
-(* case 6 : ty0_appl *)
- Inversion H3.
-(* case 7 : ty0_cast *)
- Inversion H3.
- Qed.
-
-(*#* #start proof *)
-
-(*#* #caption "generation lemma for binder" *)
-(*#* #cap #cap c #alpha x in T, t1 in U1, t2 in U2, u in V, t in U, t0 in U3 *)
-
- Theorem ty0_gen_bind: (g:?; b:?; c:?; u,t1,x:?) (ty0 g c (TTail (Bind b) u t1) x) ->
- (EX t2 t t0 | (pc3 c (TTail (Bind b) u t2) x) &
- (ty0 g c u t) &
- (ty0 g (CTail c (Bind b) u) t1 t2) &
- (ty0 g (CTail c (Bind b) u) t2 t0)
- ).
-
-(*#* #stop proof *)
-
- Intros until 1; InsertEq H '(TTail (Bind b) u t1); XElim H; Intros.
-(* case 1 : ty0_conv *)
- LApply H2; [ Clear H2; Intros H2 | XAuto ].
- XElim H2; XEAuto.
-(* case 2 : ty0_sort *)
- Inversion H0.
-(* case 3 : ty0_abbr *)
- Inversion H3.
-(* case 4 : ty0_abst *)
- Inversion H3.
-(* case 5 : ty0_bind *)
- Inversion H5.
- Rewrite H7 in H1; Rewrite H7 in H3.
- Rewrite H8 in H; Rewrite H8 in H1; Rewrite H8 in H3.
- Rewrite H9 in H1; XEAuto.
-(* case 6 : ty0_appl *)
- Inversion H3.
-(* case 7 : ty0_cast *)
- Inversion H3.
- Qed.
-
-(*#* #start proof *)
-
-(*#* #caption "generation lemma for application" *)
-(*#* #cap #cap c #alpha x in T, v in U1, w in V1, u in V2, t in U2 *)
-
- Theorem ty0_gen_appl: (g:?; c:?; w,v,x:?) (ty0 g c (TTail (Flat Appl) w v) x) ->
- (EX u t | (pc3 c (TTail (Flat Appl) w (TTail (Bind Abst) u t)) x) &
- (ty0 g c v (TTail (Bind Abst) u t)) &
- (ty0 g c w u)
- ).
-
-(*#* #stop proof *)
-
- Intros until 1; InsertEq H '(TTail (Flat Appl) w v); XElim H; Intros.
-(* case 1 : ty0_conv *)
- LApply H2; [ Clear H2; Intros H2 | XAuto ].
- XElim H2; XEAuto.
-(* case 2 : ty0_sort *)
- Inversion H0.
-(* case 3 : ty0_abbr *)
- Inversion H3.
-(* case 4 : ty0_abst *)
- Inversion H3.
-(* case 5 : ty0_bind *)
- Inversion H5.
-(* case 6 : ty0_appl *)
- Inversion H3; Rewrite H5 in H; Rewrite H6 in H1; XEAuto.
-(* case 7 : ty0_cast *)
- Inversion H3.
- Qed.
-
-(*#* #start proof *)
-
-(*#* #caption "generation lemma for cast" *)
-(*#* #cap #cap c #alpha x in T, t2 in V, t1 in U *)
-
- Theorem ty0_gen_cast: (g:?; c:?; t1,t2,x:?)
- (ty0 g c (TTail (Flat Cast) t2 t1) x) ->
- (pc3 c t2 x) /\ (ty0 g c t1 t2).
-
-(*#* #stop proof *)
-
- Intros until 1; InsertEq H '(TTail (Flat Cast) t2 t1); XElim H; Intros.
-(* case 1 : ty0_conv *)
- LApply H2; [ Clear H2; Intros H2 | XAuto ].
- XElim H2; XEAuto.
-(* case 2 : ty0_sort *)
- Inversion H0.
-(* case 3 : ty0_abbr *)
- Inversion H3.
-(* case 4 : ty0_abst *)
- Inversion H3.
-(* case 5 : ty0_bind *)
- Inversion H5.
-(* case 6 : ty0_appl *)
- Inversion H3.
-(* case 7 : ty0_cast *)
- Inversion H3; Rewrite H5 in H; Rewrite H5 in H1; Rewrite H6 in H; XAuto.
- Qed.
-
- End ty0_gen_base.
-
- Tactic Definition Ty0GenBase :=
- Match Context With
- | [ H: (ty0 ?1 ?2 (TSort ?3) ?4) |- ? ] ->
- LApply (ty0_gen_sort ?1 ?2 ?4 ?3); [ Clear H; Intros | XAuto ]
- | [ H: (ty0 ?1 ?2 (TLRef ?3) ?4) |- ? ] ->
- LApply (ty0_gen_lref ?1 ?2 ?4 ?3); [ Clear H; Intros H | XAuto ];
- XElim H; Intros H; XElim H; Intros
- | [ H: (ty0 ?1 ?2 (TTail (Bind ?3) ?4 ?5) ?6) |- ? ] ->
- LApply (ty0_gen_bind ?1 ?3 ?2 ?4 ?5 ?6); [ Clear H; Intros H | XAuto ];
- XElim H; Intros
- | [ H: (ty0 ?1 ?2 (TTail (Flat Appl) ?3 ?4) ?5) |- ? ] ->
- LApply (ty0_gen_appl ?1 ?2 ?3 ?4 ?5); [ Clear H; Intros H | XAuto ];
- XElim H; Intros
- | [ H: (ty0 ?1 ?2 (TTail (Flat Cast) ?3 ?4) ?5) |- ? ] ->
- LApply (ty0_gen_cast ?1 ?2 ?4 ?3 ?5); [ Clear H; Intros H | XAuto ];
- XElim H; Intros.
-
Section wf0_props. (******************************************************)
- Theorem wf0_ty0 : (g:?; c:?; u,t:?) (ty0 g c u t) -> (wf0 g c).
+ Theorem wf0_ty0: (g:?; c:?; u,t:?) (ty0 g c u t) -> (wf0 g c).
Intros; XElim H; XAuto.
Qed.
Hints Resolve wf0_ty0 : ltlc.
- Theorem wf0_drop_O : (c,e:?; h:?) (drop h (0) c e) ->
- (g:?) (wf0 g c) -> (wf0 g e).
+ Theorem wf0_drop_O: (c,e:?; h:?) (drop h (0) c e) ->
+ (g:?) (wf0 g c) -> (wf0 g e).
XElim c.
(* case 1 : CSort *)
Intros; DropGenBase; Rewrite H; XAuto.
Section wf0_facilities. (*************************************************)
- Theorem wf0_drop_wf0 : (g:?; c:?) (wf0 g c) ->
- (b:?; e:?; u:?; h:?)
- (drop h (0) c (CTail e (Bind b) u)) -> (wf0 g e).
+ Theorem wf0_drop_wf0: (g:?; c:?) (wf0 g c) ->
+ (b:?; e:?; u:?; h:?)
+ (drop h (0) c (CTail e (Bind b) u)) -> (wf0 g e).
Intros.
Wf0DropO; Inversion H1; XEAuto.
Qed.
- Theorem ty0_drop_wf0 : (g:?; c:?; t1,t2:?) (ty0 g c t1 t2) ->
- (b:?; e:?; u:?; h:?)
- (drop h (0) c (CTail e (Bind b) u)) -> (wf0 g e).
+ Theorem ty0_drop_wf0: (g:?; c:?; t1,t2:?) (ty0 g c t1 t2) ->
+ (b:?; e:?; u:?; h:?)
+ (drop h (0) c (CTail e (Bind b) u)) -> (wf0 g e).
Intros.
EApply wf0_drop_wf0; [ Idtac | EApply H0 ]; XEAuto.
Qed.
_: (drop ?5 (0) ?2 (CTail ?6 (Bind ?7) ?8)) |- ? ] ->
LApply (wf0_drop_wf0 ?1 ?2); [ Intros H_x | XAuto ];
LApply (H_x ?7 ?6 ?8 ?5); [ Clear H_x; Intros | XAuto ].
-
-(*#* #start file *)
-
-(*#* #single *)
--- /dev/null
+Require pc3_props.
+Require ty0_defs.
+
+(*#* #caption "generation lemma of typing" #clauses *)
+
+ Section ty0_gen_base. (***************************************************)
+
+(*#* #caption "generation lemma for sorts" *)
+(*#* #cap #cap c #alpha x in T, n in h *)
+
+ Theorem ty0_gen_sort: (g:?; c:?; x:?; n:?)
+ (ty0 g c (TSort n) x) ->
+ (pc3 c (TSort (next g n)) x).
+
+(*#* #stop proof *)
+
+ Intros until 1; InsertEq H '(TSort n); XElim H; Intros.
+(* case 1 : ty0_conv *)
+ XEAuto.
+(* case 2 : ty0_sort *)
+ Inversion H0; XAuto.
+(* case 3 : ty0_abbr *)
+ Inversion H3.
+(* case 4 : ty0_abst *)
+ Inversion H3.
+(* case 5 : ty0_bind *)
+ Inversion H5.
+(* case 6 : ty0_appl *)
+ Inversion H3.
+(* case 7 : ty0_cast *)
+ Inversion H3.
+ Qed.
+
+(*#* #start proof *)
+
+(*#* #caption "generation lemma for bound references" *)
+(*#* #cap #cap c, e #alpha x in T, t in U, u in V, n in i *)
+
+ Theorem ty0_gen_lref: (g:?; c:?; x:?; n:?) (ty0 g c (TLRef n) x) ->
+ (EX e u t | (pc3 c (lift (S n) (0) t) x) &
+ (drop n (0) c (CTail e (Bind Abbr) u)) &
+ (ty0 g e u t)
+ ) \/
+ (EX e u t | (pc3 c (lift (S n) (0) u) x) &
+ (drop n (0) c (CTail e (Bind Abst) u)) &
+ (ty0 g e u t)
+ ).
+
+(*#* #stop proof *)
+
+ Intros until 1; InsertEq H '(TLRef n); XElim H; Intros.
+(* case 1 : ty0_conv *)
+ LApply H2; [ Clear H2; Intros H2 | XAuto ].
+ XElim H2; Intros; XElim H2; XEAuto.
+(* case 2 : ty0_sort *)
+ Inversion H0.
+(* case 3 : ty0_abbr *)
+ Inversion H3 ; Rewrite H5 in H0; XEAuto.
+(* case 4 : ty0_abst *)
+ Inversion H3; Rewrite H5 in H0; XEAuto.
+(* case 5 : ty0_bind *)
+ Inversion H5.
+(* case 6 : ty0_appl *)
+ Inversion H3.
+(* case 7 : ty0_cast *)
+ Inversion H3.
+ Qed.
+
+(*#* #start proof *)
+
+(*#* #caption "generation lemma for binders" *)
+(*#* #cap #cap c #alpha x in T, t1 in U1, t2 in U2, u in V, t in U, t0 in U3 *)
+
+ Theorem ty0_gen_bind: (g:?; b:?; c:?; u,t1,x:?) (ty0 g c (TTail (Bind b) u t1) x) ->
+ (EX t2 t t0 | (pc3 c (TTail (Bind b) u t2) x) &
+ (ty0 g c u t) &
+ (ty0 g (CTail c (Bind b) u) t1 t2) &
+ (ty0 g (CTail c (Bind b) u) t2 t0)
+ ).
+
+(*#* #stop proof *)
+
+ Intros until 1; InsertEq H '(TTail (Bind b) u t1); XElim H; Intros.
+(* case 1 : ty0_conv *)
+ LApply H2; [ Clear H2; Intros H2 | XAuto ].
+ XElim H2; XEAuto.
+(* case 2 : ty0_sort *)
+ Inversion H0.
+(* case 3 : ty0_abbr *)
+ Inversion H3.
+(* case 4 : ty0_abst *)
+ Inversion H3.
+(* case 5 : ty0_bind *)
+ Inversion H5.
+ Rewrite H7 in H1; Rewrite H7 in H3.
+ Rewrite H8 in H; Rewrite H8 in H1; Rewrite H8 in H3.
+ Rewrite H9 in H1; XEAuto.
+(* case 6 : ty0_appl *)
+ Inversion H3.
+(* case 7 : ty0_cast *)
+ Inversion H3.
+ Qed.
+
+(*#* #start proof *)
+
+(*#* #caption "generation lemma for applications" *)
+(*#* #cap #cap c #alpha x in T, v in U1, w in V1, u in V2, t in U2 *)
+
+ Theorem ty0_gen_appl: (g:?; c:?; w,v,x:?) (ty0 g c (TTail (Flat Appl) w v) x) ->
+ (EX u t | (pc3 c (TTail (Flat Appl) w (TTail (Bind Abst) u t)) x) &
+ (ty0 g c v (TTail (Bind Abst) u t)) &
+ (ty0 g c w u)
+ ).
+
+(*#* #stop proof *)
+
+ Intros until 1; InsertEq H '(TTail (Flat Appl) w v); XElim H; Intros.
+(* case 1 : ty0_conv *)
+ LApply H2; [ Clear H2; Intros H2 | XAuto ].
+ XElim H2; XEAuto.
+(* case 2 : ty0_sort *)
+ Inversion H0.
+(* case 3 : ty0_abbr *)
+ Inversion H3.
+(* case 4 : ty0_abst *)
+ Inversion H3.
+(* case 5 : ty0_bind *)
+ Inversion H5.
+(* case 6 : ty0_appl *)
+ Inversion H3; Rewrite H5 in H; Rewrite H6 in H1; XEAuto.
+(* case 7 : ty0_cast *)
+ Inversion H3.
+ Qed.
+
+(*#* #start proof *)
+
+(*#* #caption "generation lemma for type casts" *)
+(*#* #cap #cap c #alpha x in T, t2 in V, t1 in U *)
+
+ Theorem ty0_gen_cast: (g:?; c:?; t1,t2,x:?)
+ (ty0 g c (TTail (Flat Cast) t2 t1) x) ->
+ (pc3 c t2 x) /\ (ty0 g c t1 t2).
+
+(*#* #stop proof *)
+
+ Intros until 1; InsertEq H '(TTail (Flat Cast) t2 t1); XElim H; Intros.
+(* case 1 : ty0_conv *)
+ LApply H2; [ Clear H2; Intros H2 | XAuto ].
+ XElim H2; XEAuto.
+(* case 2 : ty0_sort *)
+ Inversion H0.
+(* case 3 : ty0_abbr *)
+ Inversion H3.
+(* case 4 : ty0_abst *)
+ Inversion H3.
+(* case 5 : ty0_bind *)
+ Inversion H5.
+(* case 6 : ty0_appl *)
+ Inversion H3.
+(* case 7 : ty0_cast *)
+ Inversion H3; Rewrite H5 in H; Rewrite H5 in H1; Rewrite H6 in H; XAuto.
+ Qed.
+
+ End ty0_gen_base.
+
+ Tactic Definition Ty0GenBase :=
+ Match Context With
+ | [ H: (ty0 ?1 ?2 (TSort ?3) ?4) |- ? ] ->
+ LApply (ty0_gen_sort ?1 ?2 ?4 ?3); [ Clear H; Intros | XAuto ]
+ | [ H: (ty0 ?1 ?2 (TLRef ?3) ?4) |- ? ] ->
+ LApply (ty0_gen_lref ?1 ?2 ?4 ?3); [ Clear H; Intros H | XAuto ];
+ XElim H; Intros H; XElim H; Intros
+ | [ H: (ty0 ?1 ?2 (TTail (Bind ?3) ?4 ?5) ?6) |- ? ] ->
+ LApply (ty0_gen_bind ?1 ?3 ?2 ?4 ?5 ?6); [ Clear H; Intros H | XAuto ];
+ XElim H; Intros
+ | [ H: (ty0 ?1 ?2 (TTail (Flat Appl) ?3 ?4) ?5) |- ? ] ->
+ LApply (ty0_gen_appl ?1 ?2 ?3 ?4 ?5); [ Clear H; Intros H | XAuto ];
+ XElim H; Intros
+ | [ H: (ty0 ?1 ?2 (TTail (Flat Cast) ?3 ?4) ?5) |- ? ] ->
+ LApply (ty0_gen_cast ?1 ?2 ?4 ?3 ?5); [ Clear H; Intros H | XAuto ];
+ XElim H; Intros.
+
+(*#* #start file *)
+
+(*#* #single *)
(ty0 g a y1 y2)
).
Intros until 1; XElim H; Intros.
-(* case 1 : ty0_conv *)
+(* 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 *)
+(* case 2: ty0_sort *)
EApply ex3_2_intro; Try Rewrite lift_sort; XAuto.
-(* case 3 : ty0_abbr *)
+(* case 3: ty0_abbr *)
Apply (lt_eq_gt_e n d0); Intros; Clear c t1 t2.
-(* case 3.1 : n < d0 *)
+(* 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.
Pattern 4 d0; Rewrite (le_plus_minus (S n) d0); [ Idtac | XAuto ].
EApply ex3_2_intro;
[ Rewrite lift_lref_lt | Rewrite lift_d | EApply ty0_abbr ]; XEAuto.
-(* case 3.2 : n = d0 *)
+(* 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 subst1_single; Rewrite lift_free; Simpl; XEAuto
| Rewrite lift_free; Simpl; XEAuto
| XEAuto ].
-(* case 3.3 : n > d0 *)
+(* 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)).
| Rewrite lift_free; Simpl
| Pattern 2 n; Rewrite (minus_x_SO n)
]; XEAuto.
-(* case 4 : ty0_abst *)
+(* case 4: ty0_abst *)
Apply (lt_eq_gt_e n d0); Intros; Clear c t1 t2.
-(* case 4.1 : n < d0 *)
+(* 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.
Pattern 4 d0; Rewrite (le_plus_minus (S n) d0); [ Idtac | XAuto ].
EApply ex3_2_intro;
[ Rewrite lift_lref_lt | Rewrite lift_d | EApply ty0_abst ]; XEAuto.
-(* case 4.2 : n = d0 *)
+(* case 4.2: n = d0 *)
Rewrite H7; Rewrite H7 in H0; DropDis; Inversion H0.
-(* case 4.3 : n > d0 *)
+(* 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)).
| Rewrite lift_free; Simpl
| Pattern 2 n; Rewrite (minus_x_SO n)
]; XEAuto.
-(* case 5 : ty0_bind *)
+(* 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 *)
+(* 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 *)
+(* 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.
(ty0 g a y1 y2)
).
Intros until 1; XElim H; Intros.
-(* case 1 : ty0_conv *)
+(* case 1: ty0_conv *)
Repeat IH d a; Rewrite H0 in H3; Rewrite H7 in H3; Pc3Gen; XEAuto.
-(* case 2 : ty0_sort *)
+(* case 2: ty0_sort *)
EApply ex3_2_intro; Try Rewrite lift_sort; XEAuto.
-(* case 3 : ty0_abbr *)
+(* case 3: ty0_abbr *)
Apply (lt_eq_gt_e n d0); Intros.
-(* case 3.1 : n < d0 *)
+(* 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.
Rewrite <- lift_d; [ Idtac | XAuto ].
Rewrite <- le_plus_minus; [ Idtac | XAuto ].
EApply ex3_2_intro; [ Rewrite lift_lref_lt | Idtac | EApply ty0_abbr ]; XEAuto.
-(* case 3.2 : n = d0 *)
+(* case 3.2: n = d0 *)
Rewrite H6 in H0; DropDis; Inversion H0.
-(* case 3.3 : n > d0 *)
+(* 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)).
| Rewrite lift_free; Simpl
| Pattern 2 n; Rewrite (minus_x_SO n)
]; XEAuto.
-(* case 4 : ty0_abst *)
+(* case 4: ty0_abst *)
Apply (lt_eq_gt_e n d0); Intros.
-(* case 4.1 : n < d0 *)
+(* 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.
Rewrite <- lift_d; [ Idtac | XAuto ].
Rewrite <- le_plus_minus; [ Idtac | XAuto ].
EApply ex3_2_intro; [ Rewrite lift_lref_lt | Idtac | EApply ty0_abst ]; XEAuto.
-(* case 4.2 : n = d0 *)
+(* case 4.2: n = d0 *)
Rewrite H6 in H0; DropDis; Inversion H0.
-(* case 4.3 : n > d0 *)
+(* 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)).
| Rewrite lift_free; [ Simpl | Simpl | Idtac ]
| Pattern 2 n; Rewrite (minus_x_SO n)
]; XEAuto.
-(* case 5 : ty0_bind *)
+(* 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 *)
+(* 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 *)
+(* 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.
Require drop_props.
Require pc3_props.
Require ty0_defs.
+Require ty0_gen.
Require ty0_lift.
Section ty0_correct. (****************************************************)
Hints Resolve ty0_shift : ltlc.
-(*#* #start file *)
-
Section ty0_unique. (*****************************************************)
+ Opaque pc3.
+
+(*#* #start file *)
+
(*#* #caption "uniqueness of types" *)
(*#* #cap #cap c, t1, t2 #alpha u in T *)
Require pr0_lift.
Require pr0_subst1.
Require cpr0_defs.
+Require pc1_props.
Require pc3_props.
Require pc3_gen.
Require ty0_defs.
+Require ty0_gen.
Require ty0_lift.
Require ty0_props.
Require ty0_subst0.
Require ty0_gen_context.
Require csub0_defs.
+Require csub0_props.
(*#* #caption "subject reduction" #clauses *)
]; XEAuto
| Idtac ].
Rewrite <- lift_bind; Apply pc3_pc1;
- Apply (pc1_u (TTail (Flat Appl) v2 (TTail (Bind b) u2 (lift (1) (0) (TTail (Bind Abst) u t0))))); XAuto.
+ Apply (pc1_pr0_u2 (TTail (Flat Appl) v2 (TTail (Bind b) u2 (lift (1) (0) (TTail (Bind Abst) u t0))))); XAuto.
(* case 7: ty0_cast *)
Intros; Inversion H5; Clear H5.
(* case 7.1: pr0_refl *)
(*#* #start file *)
-(*#* #caption "general case" *)
+(*#* #caption "general case without the reduction in the context" *)
(*#* #cap #cap c #alpha t1 in T, t2 in T1, t in T2 *)
Theorem ty0_sred_pr3: (c:?; t1,t2:?) (pr3 c t1 t2) ->
Require pc3_props.
Require pc3_gen.
Require ty0_defs.
+Require ty0_gen.
Require ty0_props.
Require ty0_sred.
(*#* #caption "generation lemma for lift" *)
(*#* #cap #cap t2 #alpha c in C1, e in C2, t1 in T, x in T1, d in i *)
- Theorem ty0_gen_lift : (g:?; c:?; t1,x:?; h,d:?)
- (ty0 g c (lift h d t1) x) ->
- (e:?) (wf0 g e) -> (drop h d c e) ->
- (EX t2 | (pc3 c (lift h d t2) x) & (ty0 g e t1 t2)).
+ Theorem ty0_gen_lift: (g:?; c:?; t1,x:?; h,d:?)
+ (ty0 g c (lift h d t1) x) ->
+ (e:?) (wf0 g e) -> (drop h d c e) ->
+ (EX t2 | (pc3 c (lift h d t2) x) & (ty0 g e t1 t2)).
(*#* #stop file *)
Intros until 1; InsertEq H '(lift h d t1);
UnIntro H d; UnIntro H t1; XElim H; Intros;
Rename x0 into t3; Rename x1 into d0.
-(* case 1 : ty0_conv *)
+(* case 1: ty0_conv *)
IH e; XEAuto.
-(* case 2 : ty0_sort *)
+(* case 2: ty0_sort *)
LiftGenBase; Rewrite H0; Clear H0 t.
EApply ex2_intro; [ Rewrite lift_sort; XAuto | XAuto ].
-(* case 3 : ty0_abbr *)
+(* case 3: ty0_abbr *)
Apply (lt_le_e n d0); Intros.
-(* case 3.1 : n < d0 *)
+(* case 3.1: n < d0 *)
LiftGenBase; DropS; Rewrite H3; Clear H3 t3.
Rewrite (le_plus_minus (S n) d0); [ Idtac | XAuto ].
Rewrite (lt_plus_minus n d0) in H5; [ DropDis; IH x1 | XAuto ].
EApply ex2_intro;
[ Rewrite lift_d; [ EApply pc3_lift; XEAuto | XEAuto ]
| EApply ty0_abbr; XEAuto ].
-(* case 3.2 : n >= d0 *)
+(* case 3.2: n >= d0 *)
Apply (lt_le_e n (plus d0 h)); Intros.
-(* case 3.2.1 : n < d0 + h *)
+(* case 3.2.1: n < d0 + h *)
LiftGenBase.
-(* case 3.2.2 : n >= d0 + h *)
+(* case 3.2.2: n >= d0 + h *)
Rewrite (le_plus_minus_sym h n) in H3; [ Idtac | XEAuto ].
LiftGenBase; DropDis; Rewrite H3; Clear H3 t3.
EApply ex2_intro; [ Idtac | EApply ty0_abbr; XEAuto ].
Rewrite lift_free; [ Idtac | XEAuto | XAuto ].
Rewrite <- plus_n_Sm; Rewrite <- le_plus_minus; XEAuto.
-(* case 4 : ty0_abst *)
+(* case 4: ty0_abst *)
Apply (lt_le_e n d0); Intros.
-(* case 4.1 : n < d0 *)
+(* case 4.1: n < d0 *)
LiftGenBase; Rewrite H3; Clear H3 t3.
Rewrite (le_plus_minus (S n) d0); [ Idtac | XAuto ].
Rewrite (lt_plus_minus n d0) in H5; [ DropDis; Rewrite H0; IH x1 | XAuto ].
EApply ex2_intro; [ Rewrite lift_d | EApply ty0_abst ]; XEAuto.
-(* case 4.2 : n >= d0 *)
+(* case 4.2: n >= d0 *)
Apply (lt_le_e n (plus d0 h)); Intros.
-(* case 4.2.1 : n < d0 + h *)
+(* case 4.2.1: n < d0 + h *)
LiftGenBase.
-(* case 4.2.2 : n >= d0 + h *)
+(* case 4.2.2: n >= d0 + h *)
Rewrite (le_plus_minus_sym h n) in H3; [ Idtac | XEAuto ].
LiftGenBase; DropDis; Rewrite H3; Clear H3 t3.
EApply ex2_intro; [ Idtac | EApply ty0_abst; XEAuto ].
Rewrite lift_free; [ Idtac | XEAuto | XAuto ].
Rewrite <- plus_n_Sm; Rewrite <- le_plus_minus; XEAuto.
-(* case 5 : ty0_bind *)
+(* case 5: ty0_bind *)
LiftGenBase; Rewrite H5; Rewrite H8; Rewrite H8 in H2; Clear H5 t3.
Move H0 after H2; IH e; IH '(CTail e (Bind b) x0); Ty0Correct.
EApply ex2_intro; [ Rewrite lift_bind; XEAuto | XEAuto ].
-(* case 6 : ty0_appl *)
+(* case 6: ty0_appl *)
LiftGenBase; Rewrite H3; Rewrite H6; Clear H3 c t3 x y.
IH e; IH e; Pc3Gen; Pc3T; Pc3Gen; Pc3T.
Move H3 after H12; Ty0Correct; Ty0SRed; Ty0GenBase; Wf0Ty0.
[ EApply ty0_conv
| EApply ty0_conv; [ EApply ty0_bind | Idtac | Idtac ] ]
]; XEAuto.
-(* case 7 : ty0_cast *)
+(* case 7: ty0_cast *)
LiftGenBase; Rewrite H3; Rewrite H6; Rewrite H6 in H0.
IH e; IH e; Pc3Gen; XEAuto.
Qed.
LApply H0; [ Clear H0 H1; Intros H0 | XAuto ];
XElim H0; Intros
| [ H0: (ty0 ?1 ?2 (lift ?3 ?4 ?5) ?6);
- _ : (wf0 ?1 ?7) |- ? ] ->
+ _: (wf0 ?1 ?7) |- ? ] ->
LApply (ty0_gen_lift ?1 ?2 ?5 ?6 ?3 ?4); [ Clear H0; Intros H0 | XAuto ];
LApply (H0 ?7); [ Clear H0; Intros H0 | XAuto ];
LApply H0; [ Clear H0; Intros H0 | XAuto ];
(*#* #caption "drop preserves well-formedness" *)
(*#* #cap #alpha c in C1, e in C2, d in i *)
- Theorem wf0_drop : (c,e:?; d,h:?) (drop h d c e) ->
- (g:?) (wf0 g c) -> (wf0 g e).
+ Theorem wf0_drop: (c,e:?; d,h:?) (drop h d c e) ->
+ (g:?) (wf0 g c) -> (wf0 g e).
(*#* #stop proof *)
XElim c.
-(* case 1 : CSort *)
+(* case 1: CSort *)
Intros; DropGenBase; Rewrite H; XAuto.
-(* case 2 : CTail k *)
+(* case 2: CTail k *)
Intros c IHc; XElim k; (
XElim d;
[ XEAuto
| Intros d IHd; Intros;
DropGenBase; Rewrite H; Rewrite H1 in H0; Clear IHd H H1 e t;
Inversion H0; Clear H3 H4 b0 u ]).
-(* case 2.1 : Bind, d > 0 *)
+(* case 2.1: Bind, d > 0 *)
Ty0Gen; XEAuto.
Qed.
(*#* #caption "type reduction" *)
(*#* #cap #cap c, t1, t2 #alpha u in T *)
- Theorem ty0_tred : (g:?; c:?; u,t1:?) (ty0 g c u t1) ->
- (t2:?) (pr3 c t1 t2) -> (ty0 g c u t2).
+ Theorem ty0_tred: (g:?; c:?; u,t1:?) (ty0 g c u t1) ->
+ (t2:?) (pr3 c t1 t2) -> (ty0 g c u t2).
(*#* #stop proof *)
(*#* #caption "subject conversion" *)
(*#* #cap #cap c, u1, u2, t1, t2 *)
- Theorem ty0_sconv : (g:?; c:?; u1,t1:?) (ty0 g c u1 t1) ->
- (u2,t2:?) (ty0 g c u2 t2) ->
- (pc3 c u1 u2) -> (pc3 c t1 t2).
+ Theorem ty0_sconv: (g:?; c:?; u1,t1:?) (ty0 g c u1 t1) ->
+ (u2,t2:?) (ty0 g c u2 t2) ->
+ (pc3 c u1 u2) -> (pc3 c t1 t2).
(*#* #stop file *)
- Intros; Pc3Confluence; Repeat Ty0SRed; XEAuto.
+ Intros; Pc3Unfold; Repeat Ty0SRed; XEAuto.
Qed.
Require pc3_props.
Require pc3_subst0.
Require ty0_defs.
+Require ty0_gen.
Require ty0_lift.
Require ty0_props.
projects / helm.git / commitdiff