+Require Export base_tactics.
+Require Export base_hints.
+Require Export base_types.
+Require Export base_blt.
+Require Export base_rewrite.
+Require Export Base.
Require Export terms_defs.
Require Export tlt_defs.
Require Export contexts_defs.
Require Export lift_gen.
Require Export lift_props.
Require Export lift_tlt.
+Require Export drop_defs.
+Require Export drop_props.
Require Export subst0_defs.
Require Export subst0_gen.
Require Export subst0_lift.
Require Export subst1_lift.
Require Export subst1_subst1.
Require Export subst1_confluence.
-Require Export drop_defs.
-Require Export drop_props.
Require Export csubst0_defs.
Require Export csubst1_defs.
+Require Export fsubst0_defs.
Require Export pr0_defs.
Require Export pr0_lift.
Require Export pr0_gen.
Require Export pr0_subst1.
Require Export pr1_defs.
Require Export pr1_confluence.
+Require Export cpr0_defs.
Require Export pr2_defs.
Require Export pr2_lift.
Require Export pr2_gen.
Require Export pr3_confluence.
Require Export pr3_subst1.
Require Export pr3_gen_context.
-Require Export cpr0_defs.
-Require Export cpr0_props.
Require Export pc1_defs.
Require Export pc3_defs.
Require Export pc3_props.
lift_gen.v
lift_props.v
lift_tlt.v
+drop_defs.v
+drop_props.v
subst0_defs.v
subst0_gen.v
subst0_lift.v
subst1_lift.v
subst1_subst1.v
subst1_confluence.v
-drop_defs.v
-drop_props.v
csubst0_defs.v
csubst1_defs.v
+fsubst0_defs.v
pr0_defs.v
pr0_lift.v
pr0_gen.v
pr0_subst1.v
pr1_defs.v
pr1_confluence.v
+cpr0_defs.v
pr2_defs.v
pr2_lift.v
pr2_gen.v
pr3_confluence.v
pr3_subst1.v
pr3_gen_context.v
-cpr0_defs.v
-cpr0_props.v
pc1_defs.v
pc3_defs.v
pc3_props.v
lift_gen.v\
lift_props.v\
lift_tlt.v\
+ drop_defs.v\
+ drop_props.v\
subst0_defs.v\
subst0_gen.v\
subst0_lift.v\
subst1_lift.v\
subst1_subst1.v\
subst1_confluence.v\
- drop_defs.v\
- drop_props.v\
csubst0_defs.v\
csubst1_defs.v\
+ fsubst0_defs.v\
pr0_defs.v\
pr0_lift.v\
pr0_gen.v\
pr0_subst1.v\
pr1_defs.v\
pr1_confluence.v\
+ cpr0_defs.v\
pr2_defs.v\
pr2_lift.v\
pr2_gen.v\
pr3_confluence.v\
pr3_subst1.v\
pr3_gen_context.v\
- cpr0_defs.v\
- cpr0_props.v\
pc1_defs.v\
pc3_defs.v\
pc3_props.v\
lift_gen.vo\
lift_props.vo\
lift_tlt.vo\
+ drop_defs.vo\
+ drop_props.vo\
subst0_defs.vo\
subst0_gen.vo\
subst0_lift.vo\
subst1_lift.vo\
subst1_subst1.vo\
subst1_confluence.vo\
- drop_defs.vo\
- drop_props.vo\
csubst0_defs.vo\
csubst1_defs.vo\
+ fsubst0_defs.vo\
pr0_defs.vo\
pr0_lift.vo\
pr0_gen.vo\
pr0_subst1.vo\
pr1_defs.vo\
pr1_confluence.vo\
+ cpr0_defs.vo\
pr2_defs.vo\
pr2_lift.vo\
pr2_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\
lift_gen.vo\
lift_props.vo\
lift_tlt.vo\
+ drop_defs.vo\
+ drop_props.vo\
subst0_defs.vo\
subst0_gen.vo\
subst0_lift.vo\
subst1_lift.vo\
subst1_subst1.vo\
subst1_confluence.vo\
- drop_defs.vo\
- drop_props.vo\
csubst0_defs.vo\
csubst1_defs.vo\
+ fsubst0_defs.vo\
pr0_defs.vo\
pr0_lift.vo\
pr0_gen.vo\
pr0_subst1.vo\
pr1_defs.vo\
pr1_confluence.vo\
+ cpr0_defs.vo\
pr2_defs.vo\
pr2_lift.vo\
pr2_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\
The latest version of this development is maintained in the CVS repository
of the HELM project <helm.cs.unibo.it> and can be downloaded at:
- www.cs.unibo.it/cgi-bin/viewcvs.cgi/helm/coq-contribs/LAMBDA-TYPES.tgz
+ www.cs.unibo.it/cgi-bin/viewcvs.cgi/helm/coq-contribs/LAMBDA-TYPES
[ "EX" ident($v0) ident($v1) "|" constr($c0) "&" constr($c1) "&" constr($c2) ] ->
[ (ex3_2 ? ? [$v0;$v1]$c0 [$v0;$v1]$c1 [$v0;$v1]$c2) ].
+(* ex_3 *)
+
+Inductive ex_3 [A0,A1,A2:Set; P0:A0->A1->A2->Prop] : Prop :=
+ ex_3_intro : (x0:A0; x1:A1; x2:A2)(P0 x0 x1 x2)->(ex_3 A0 A1 A2 P0).
+
+Hint ex_3 : ltlc := Constructors ex_3.
+
+Syntactic Definition Ex_3 := ex_3 | 1.
+
+Grammar constr constr10 :=
+ | ex_3implicit
+ [ "EX" ident($v0) ident($v1) ident($v2) "|" constr($c0) ] ->
+ [ (ex_3 ? ? ? [$v0;$v1;$v2]$c0) ].
+
(* ex3_3 *)
Inductive ex3_3 [A0,A1,A2:Set; P0,P1,P2:A0->A1->A2->Prop] : Prop :=
[ "EX" ident($v0) ident($v1) ident($v2) ident($v3) ident($v4) "|" constr($c0) "&" constr($c1) "&" constr($c2) "&" constr($c3) ] ->
[ (ex4_5 ? ? ? ? ? [$v0;$v1;$v2;$v3;$v4]$c0 [$v0;$v1;$v2;$v3;$v4]$c1 [$v0;$v1;$v2;$v3;$v4]$c2 [$v0;$v1;$v2;$v3;$v4]$c3) ].
+(* ex5_5 *)
+
+Inductive ex5_5 [A0,A1,A2,A3,A4:Set; P0,P1,P2,P3,P4:A0->A1->A2->A3->A4->Prop] : Prop :=
+ ex5_5_intro : (x0:A0; x1:A1; x2:A2; x3:A3; x4:A4)(P0 x0 x1 x2 x3 x4)->(P1 x0 x1 x2 x3 x4)->(P2 x0 x1 x2 x3 x4)->(P3 x0 x1 x2 x3 x4)->(P4 x0 x1 x2 x3 x4)->(ex5_5 A0 A1 A2 A3 A4 P0 P1 P2 P3 P4).
+
+Hint ex5_5 : ltlc := Constructors ex5_5.
+
+Syntactic Definition Ex5_5 := ex5_5 | 1.
+
+Grammar constr constr10 :=
+ | ex5_5implicit
+ [ "EX" ident($v0) ident($v1) ident($v2) ident($v3) ident($v4) "|" constr($c0) "&" constr($c1) "&" constr($c2) "&" constr($c3) "&" constr($c4) ] ->
+ [ (ex5_5 ? ? ? ? ? [$v0;$v1;$v2;$v3;$v4]$c0 [$v0;$v1;$v2;$v3;$v4]$c1 [$v0;$v1;$v2;$v3;$v4]$c2 [$v0;$v1;$v2;$v3;$v4]$c3 [$v0;$v1;$v2;$v3;$v4]$c4) ].
+
(* ex6_6 *)
Inductive ex6_6 [A0,A1,A2,A3,A4,A5:Set; P0,P1,P2,P3,P4,P5:A0->A1->A2->A3->A4->A5->Prop] : Prop :=
[ "EX" ident($v0) ident($v1) ident($v2) ident($v3) ident($v4) ident($v5) "|" constr($c0) "&" constr($c1) "&" constr($c2) "&" constr($c3) "&" constr($c4) "&" constr($c5) ] ->
[ (ex6_6 ? ? ? ? ? ? [$v0;$v1;$v2;$v3;$v4;$v5]$c0 [$v0;$v1;$v2;$v3;$v4;$v5]$c1 [$v0;$v1;$v2;$v3;$v4;$v5]$c2 [$v0;$v1;$v2;$v3;$v4;$v5]$c3 [$v0;$v1;$v2;$v3;$v4;$v5]$c4 [$v0;$v1;$v2;$v3;$v4;$v5]$c5) ].
+(* ex6_7 *)
+
+Inductive ex6_7 [A0,A1,A2,A3,A4,A5,A6:Set; P0,P1,P2,P3,P4,P5:A0->A1->A2->A3->A4->A5->A6->Prop] : Prop :=
+ ex6_7_intro : (x0:A0; x1:A1; x2:A2; x3:A3; x4:A4; x5:A5; x6:A6)(P0 x0 x1 x2 x3 x4 x5 x6)->(P1 x0 x1 x2 x3 x4 x5 x6)->(P2 x0 x1 x2 x3 x4 x5 x6)->(P3 x0 x1 x2 x3 x4 x5 x6)->(P4 x0 x1 x2 x3 x4 x5 x6)->(P5 x0 x1 x2 x3 x4 x5 x6)->(ex6_7 A0 A1 A2 A3 A4 A5 A6 P0 P1 P2 P3 P4 P5).
+
+Hint ex6_7 : ltlc := Constructors ex6_7.
+
+Syntactic Definition Ex6_7 := ex6_7 | 1.
+
+Grammar constr constr10 :=
+ | ex6_7implicit
+ [ "EX" ident($v0) ident($v1) ident($v2) ident($v3) ident($v4) ident($v5) ident($v6) "|" constr($c0) "&" constr($c1) "&" constr($c2) "&" constr($c3) "&" constr($c4) "&" constr($c5) ] ->
+ [ (ex6_7 ? ? ? ? ? ? ? [$v0;$v1;$v2;$v3;$v4;$v5;$v6]$c0 [$v0;$v1;$v2;$v3;$v4;$v5;$v6]$c1 [$v0;$v1;$v2;$v3;$v4;$v5;$v6]$c2 [$v0;$v1;$v2;$v3;$v4;$v5;$v6]$c3 [$v0;$v1;$v2;$v3;$v4;$v5;$v6]$c4 [$v0;$v1;$v2;$v3;$v4;$v5;$v6]$c5) ].
+
+(* extended Decompose tactic *)
+
+Tactic Definition XDecompose H :=
+ Decompose [and or ex ex2 or3 or4 ex2_2 ex3_2 ex_3 ex3_3 ex4_3 ex3_4 ex4_4 ex4_5 ex5_5 ex6_6 ex6_7] H; Clear H.
+
Require Export terms_defs.
- Fixpoint bref_map [g:nat->nat; d:nat; t:T] : T := Cases t of
+ Fixpoint lref_map [g:nat->nat; d:nat; t:T] : T := Cases t of
| (TSort n) => (TSort n)
- | (TBRef n) =>
- if (blt n d) then (TBRef n) else (TBRef (g n))
+ | (TLRef n) =>
+ if (blt n d) then (TLRef n) else (TLRef (g n))
| (TTail k u t) =>
- (TTail k (bref_map g d u) (bref_map g (s k d) t))
+ (TTail k (lref_map g d u) (lref_map g (s k d) t))
end.
Definition lift : nat -> nat -> T -> T :=
- [h](bref_map [x](plus x h)).
+ [h](lref_map [x](plus x h)).
Section lift_rw. (********************************************************)
XAuto.
Qed.
- Theorem lift_bref_lt: (n:?; h,d:?) (lt n d) ->
- (lift h d (TBRef n)) = (TBRef n).
+ Theorem lift_lref_lt: (n:?; h,d:?) (lt n d) ->
+ (lift h d (TLRef n)) = (TLRef n).
Intros; Unfold lift; Simpl.
Replace (blt n d) with true; XAuto.
Qed.
- Theorem lift_bref_ge: (n:?; h,d:?) (le d n) ->
- (lift h d (TBRef n)) = (TBRef (plus n h)).
+ Theorem lift_lref_ge: (n:?; h,d:?) (le d n) ->
+ (lift h d (TLRef n)) = (TLRef (plus n h)).
Intros; Unfold lift; Simpl.
Replace (blt n d) with false; XAuto.
End lift_rw.
- Hints Resolve lift_bref_lt lift_bind lift_flat : ltlc.
+ Hints Resolve lift_lref_lt lift_bind lift_flat : ltlc.
Tactic Definition LiftTailRw :=
Repeat (Rewrite lift_tail Orelse Rewrite lift_bind Orelse Rewrite lift_flat).
XElim t; Intros.
(* case 1 : TSort *)
XAuto.
-(* case 2 : TBRef n0 *)
+(* case 2 : TLRef n0 *)
Apply (lt_le_e n0 d); Intros.
(* case 2.1 : n0 < d *)
- Rewrite lift_bref_lt in H; [ Inversion H | XAuto ].
+ Rewrite lift_lref_lt in H; [ Inversion H | XAuto ].
(* case 2.2 : n0 >= d *)
- Rewrite lift_bref_ge in H; [ Inversion H | XAuto ].
+ Rewrite lift_lref_ge in H; [ Inversion H | XAuto ].
(* case 3 : TTail k *)
Rewrite lift_tail in H1; Inversion H1.
Qed.
- Theorem lift_gen_bref_lt: (h,d,n:?) (lt n d) ->
- (t:?) (TBRef n) = (lift h d t) ->
- t = (TBRef n).
+ Theorem lift_gen_lref_lt: (h,d,n:?) (lt n d) ->
+ (t:?) (TLRef n) = (lift h d t) ->
+ t = (TLRef n).
XElim t; Intros.
(* case 1 : TSort *)
XAuto.
-(* case 2 : TBRef n0 *)
+(* case 2 : TLRef n0 *)
Apply (lt_le_e n0 d); Intros.
(* case 2.1 : n0 < d *)
- Rewrite lift_bref_lt in H0; XAuto.
+ Rewrite lift_lref_lt in H0; XAuto.
(* case 2.2 : n0 >= d *)
- Rewrite lift_bref_ge in H0; [ Inversion H0; Clear H0 | XAuto ].
+ Rewrite lift_lref_ge in H0; [ Inversion H0; Clear H0 | XAuto ].
Rewrite H3 in H; Clear H3 n.
EApply le_false; [ Apply H1 | XEAuto ].
(* case 3 : TTail k *)
Rewrite lift_tail in H2; Inversion H2.
Qed.
- Theorem lift_gen_bref_false: (h,d,n:?) (le d n) -> (lt n (plus d h)) ->
- (t:?) (TBRef n) = (lift h d t) ->
+ Theorem lift_gen_lref_false: (h,d,n:?) (le d n) -> (lt n (plus d h)) ->
+ (t:?) (TLRef n) = (lift h d t) ->
(P:Prop) P.
XElim t; Intros.
(* case 1 : TSort *)
Inversion H1.
-(* case 2 : TBRef n0 *)
+(* case 2 : TLRef n0 *)
Apply (lt_le_e n0 d); Intros.
(* case 2.1 : n0 < d *)
- Rewrite lift_bref_lt in H1; [ Inversion H1; Clear H1 | XAuto ].
+ Rewrite lift_lref_lt in H1; [ Inversion H1; Clear H1 | XAuto ].
Rewrite <- H4 in H2; Clear H4 n0.
EApply le_false; [ Apply H | XEAuto ].
(* case 2.2 : n0 >= d *)
- Rewrite lift_bref_ge in H1; [ Inversion H1; Clear H1 | XAuto ].
+ Rewrite lift_lref_ge in H1; [ Inversion H1; Clear H1 | XAuto ].
Rewrite H4 in H0; Clear H4.
EApply le_false; [ Apply H2 | XEAuto ].
(* case 3 : TTail k *)
Rewrite lift_tail in H3; Inversion H3.
Qed.
- Theorem lift_gen_bref_ge: (h,d,n:?) (le d n) ->
- (t:?) (TBRef (plus n h)) = (lift h d t) ->
- t = (TBRef n).
+ Theorem lift_gen_lref_ge: (h,d,n:?) (le d n) ->
+ (t:?) (TLRef (plus n h)) = (lift h d t) ->
+ t = (TLRef n).
XElim t; Intros.
(* case 1 : TSort *)
Inversion H0.
-(* case 2 : TBRef n0 *)
+(* case 2 : TLRef n0 *)
Apply (lt_le_e n0 d); Intros.
(* case 2.1 : n0 < d *)
- Rewrite lift_bref_lt in H0; [ Inversion H0; Clear H0 | XAuto ].
+ Rewrite lift_lref_lt in H0; [ Inversion H0; Clear H0 | XAuto ].
Rewrite <- H3 in H1; Clear H3 n0.
EApply le_false; [ Apply H | XEAuto ].
(* case 2.2 : n0 >= d *)
- Rewrite lift_bref_ge in H0; [ Inversion H0; XEAuto | XAuto ].
+ Rewrite lift_lref_ge in H0; [ Inversion H0; XEAuto | XAuto ].
(* case 3 : TTail k *)
Rewrite lift_tail in H2; Inversion H2.
Qed.
XElim x; Intros.
(* case 1 : TSort *)
Inversion H.
-(* case 2 : TBRef n *)
+(* case 2 : TLRef n *)
Apply (lt_le_e n d); Intros.
(* case 2.1 : n < d *)
- Rewrite lift_bref_lt in H; [ Inversion H | XAuto ].
+ Rewrite lift_lref_lt in H; [ Inversion H | XAuto ].
(* case 2.2 : n >= d *)
- Rewrite lift_bref_ge in H; [ Inversion H | XAuto ].
+ Rewrite lift_lref_ge in H; [ Inversion H | XAuto ].
(* case 3 : TTail k *)
Rewrite lift_tail in H1; Inversion H1.
XEAuto.
XElim x; Intros.
(* case 1 : TSort *)
Inversion H.
-(* case 2 : TBRef n *)
+(* case 2 : TLRef n *)
Apply (lt_le_e n d); Intros.
(* case 2.1 : n < d *)
- Rewrite lift_bref_lt in H; [ Inversion H | XAuto ].
+ Rewrite lift_lref_lt in H; [ Inversion H | XAuto ].
(* case 2.2 : n >= d *)
- Rewrite lift_bref_ge in H; [ Inversion H | XAuto ].
+ Rewrite lift_lref_ge in H; [ Inversion H | XAuto ].
(* case 3 : TTail k *)
Rewrite lift_tail in H1; Inversion H1.
XEAuto.
| [ H: (TSort ?0) = (lift ?1 ?2 ?3) |- ? ] ->
LApply (lift_gen_sort ?1 ?2 ?0 ?3); [ Clear H; Intros | XAuto ]
| [ H1: (le ?1 ?2); H2: (lt ?2 (plus ?1 ?3));
- H3: (TBRef ?2) = (lift ?3 ?1 ?4) |- ? ] ->
- Apply (lift_gen_bref_false ?3 ?1 ?2 H1 H2 ?4 H3); XAuto
- | [ H: (TBRef ?1) = (lift (1) ?1 ?2) |- ? ] ->
- LApply (lift_gen_bref_false (1) ?1 ?1); [ Intros H_x | XAuto ];
+ 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) |- ? ] ->
+ 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 ];
Apply H_x
- | [ H: (TBRef (plus ?0 ?1)) = (lift ?1 ?2 ?3) |- ? ] ->
- LApply (lift_gen_bref_ge ?1 ?2 ?0); [ Intros H_x | XAuto ];
+ | [ H: (TLRef (plus ?0 ?1)) = (lift ?1 ?2 ?3) |- ? ] ->
+ LApply (lift_gen_lref_ge ?1 ?2 ?0); [ Intros H_x | XAuto ];
LApply (H_x ?3); [ Clear H_x H; Intros | XAuto ]
- | [ H1: (TBRef ?0) = (lift ?1 ?2 ?3); H2: (lt ?0 ?4) |- ? ] ->
- LApply (lift_gen_bref_lt ?1 ?2 ?0);
+ | [ H1: (TLRef ?0) = (lift ?1 ?2 ?3); H2: (lt ?0 ?4) |- ? ] ->
+ LApply (lift_gen_lref_lt ?1 ?2 ?0);
[ Intros H_x | Apply lt_le_trans with m:=?4; XEAuto ];
LApply (H_x ?3); [ Clear H_x H1; Intros | XAuto ]
- | [ H: (TBRef ?0) = (lift ?1 ?2 ?3) |- ? ] ->
- LApply (lift_gen_bref_lt ?1 ?2 ?0); [ Intros H_x | XEAuto ];
+ | [ H: (TLRef ?0) = (lift ?1 ?2 ?3) |- ? ] ->
+ LApply (lift_gen_lref_lt ?1 ?2 ?0); [ Intros H_x | XEAuto ];
LApply (H_x ?3); [ Clear H_x H; Intros | XAuto ]
| [ H: (TTail (Bind ?0) ?1 ?2) = (lift ?3 ?4 ?5) |- ? ] ->
LApply (lift_gen_bind ?0 ?1 ?2 ?5 ?3 ?4); [ Clear H; Intros H | XAuto ];
XElim t; Intros.
(* case 1: TSort *)
XAuto.
-(* case 2: TBRef n *)
+(* case 2: TLRef n *)
Apply (lt_le_e n d); Intros.
(* case 2.1: n < d *)
- Rewrite lift_bref_lt; XAuto.
+ Rewrite lift_lref_lt; XAuto.
(* case 2.2: n >= d *)
- Rewrite lift_bref_ge; XAuto.
+ Rewrite lift_lref_ge; XAuto.
(* case 3: TTail *)
LiftTailRw; XAuto.
Qed.
- Theorem lift_bref_gt : (d,n:?) (lt d n) ->
- (lift (1) d (TBRef (pred n))) = (TBRef n).
+ Theorem lift_lref_gt : (d,n:?) (lt d n) ->
+ (lift (1) d (TLRef (pred n))) = (TLRef n).
Intros.
- Rewrite lift_bref_ge.
+ Rewrite lift_lref_ge.
(* case 1: first branch *)
Rewrite <- plus_sym; Simpl; Rewrite <- (S_pred n d); XAuto.
(* case 2: second branch *)
End lift_props.
- Hints Resolve lift_r lift_bref_gt : ltlc.
+ Hints Resolve lift_r lift_lref_gt : ltlc.
| [ H1: (lift ?1 ?2 t0) = (lift ?1 ?2 ?3) |- ? ] ->
LApply (H0 ?3 ?1 ?2); [ Clear H0 H1; Intros | XAuto ].
-(*#* #start file *)
-
(*#* #caption "main properties of lift" #clauses lift_props *)
(*#* #caption "injectivity" *)
(*#* #cap #alpha x in T1, t in T2, d in i *)
Theorem lift_inj : (x,t:?; h,d:?) (lift h d x) = (lift h d t) -> x = t.
-
-(*#* #stop file *)
-
XElim x.
(* case 1 : TSort *)
Intros; Rewrite lift_sort in H; LiftGenBase; XAuto.
-(* case 2 : TBRef n *)
+(* case 2 : TLRef n *)
Intros; Apply (lt_le_e n d); Intros.
(* case 2.1 : n < d *)
- Rewrite lift_bref_lt in H; [ LiftGenBase; XAuto | XAuto ].
+ Rewrite lift_lref_lt in H; [ LiftGenBase; XAuto | XAuto ].
(* case 2.2 : n >= d *)
- Rewrite lift_bref_ge in H; [ LiftGenBase; XAuto | XAuto ].
+ Rewrite lift_lref_ge in H; [ LiftGenBase; XAuto | XAuto ].
(* case 3 : TTail k *)
XElim k; Intros; [ Rewrite lift_bind in H1 | Rewrite lift_flat in H1 ];
LiftGenBase; Rewrite H1; IH; IH; XAuto.
LApply H0; [ Clear H0 H_x; Intros H0 | XAuto ];
XElim H0; Intros.
-(*#* #start file *)
-
(*#* #caption "generation lemma for lift" *)
(*#* #cap #cap t1 #alpha t2 in T, x in T2, d1 in i1, d2 in i2 *)
(EX t2 | x = (lift h1 d1 t2) &
t1 = (lift h2 d2 t2)
).
-
-(*#* #stop file *)
-
XElim t1; Intros.
(* case 1 : TSort *)
Rewrite lift_sort in H0.
LiftGenBase; Rewrite H0; Clear H0 x.
EApply ex2_intro; Rewrite lift_sort; XAuto.
-(* case 2 : TBRef n *)
+(* case 2 : TLRef n *)
Apply (lt_le_e n d1); Intros.
(* case 2.1 : n < d1 *)
- Rewrite lift_bref_lt in H0; [ Idtac | XAuto ].
+ Rewrite lift_lref_lt in H0; [ Idtac | XAuto ].
LiftGenBase; Rewrite H0; Clear H0 x.
- EApply ex2_intro; Rewrite lift_bref_lt; XEAuto.
+ EApply ex2_intro; Rewrite lift_lref_lt; XEAuto.
(* case 2.2 : n >= d1 *)
- Rewrite lift_bref_ge in H0; [ Idtac | XAuto ].
+ Rewrite lift_lref_ge in H0; [ Idtac | XAuto ].
Apply (lt_le_e n d2); Intros.
(* case 2.2.1 : n < d2 *)
LiftGenBase; Rewrite H0; Clear H0 x.
- EApply ex2_intro; [ Rewrite lift_bref_ge | Rewrite lift_bref_lt ]; XEAuto.
+ EApply ex2_intro; [ Rewrite lift_lref_ge | Rewrite lift_lref_lt ]; XEAuto.
(* case 2.2.2 : n >= d2 *)
Apply (lt_le_e n (plus d2 h2)); Intros.
(* case 2.2.2.1 : n < d2 + h2 *)
- EApply lift_gen_bref_false; [ Idtac | Idtac | Apply H0 ];
+ EApply lift_gen_lref_false; [ Idtac | Idtac | Apply H0 ];
[ XAuto | Rewrite plus_permute_2_in_3; XAuto ].
(* case 2.2.2.2 : n >= d2 + h2 *)
Rewrite (le_plus_minus_sym h2 (plus n h1)) in H0; [ Idtac | XEAuto ].
EApply ex2_intro;
[ Rewrite le_minus_plus; [ Idtac | XEAuto ]
| Rewrite (le_plus_minus_sym h2 n); [ Idtac | XEAuto ] ];
- Rewrite lift_bref_ge; XEAuto.
+ Rewrite lift_lref_ge; XEAuto.
(* case 3 : TTail k *)
NewInduction k.
(* case 3.1 : Bind *)
XElim t; Intros.
(* case 1: TSort *)
Repeat Rewrite lift_sort; XAuto.
-(* case 2: TBRef n *)
+(* case 2: TLRef n *)
Apply (lt_le_e n d); Intros.
(* case 2.1: n < d *)
- Repeat Rewrite lift_bref_lt; XEAuto.
+ Repeat Rewrite lift_lref_lt; XEAuto.
(* case 2.2: n >= d *)
- Repeat Rewrite lift_bref_ge; XEAuto.
+ Repeat Rewrite lift_lref_ge; XEAuto.
(* case 3: TTail k *)
LiftTailRw; XAuto.
Qed.
XElim t; Intros.
(* case 1: TSort *)
Repeat Rewrite lift_sort; XAuto.
-(* case 2: TBRef n *)
+(* case 2: TLRef n *)
Apply (lt_le_e n e); Intros.
(* case 2.1: n < e *)
- Cut (lt n d); Intros; Repeat Rewrite lift_bref_lt; XEAuto.
+ Cut (lt n d); Intros; Repeat Rewrite lift_lref_lt; XEAuto.
(* case 2.2: n >= e *)
- Rewrite lift_bref_ge; [ Idtac | XAuto ].
+ Rewrite lift_lref_ge; [ Idtac | XAuto ].
Rewrite plus_sym; Apply (lt_le_e n d); Intros.
(* case 2.2.1: n < d *)
- Do 2 (Rewrite lift_bref_lt; [ Idtac | XAuto ]).
- Rewrite lift_bref_ge; XAuto.
+ Do 2 (Rewrite lift_lref_lt; [ Idtac | XAuto ]).
+ Rewrite lift_lref_ge; XAuto.
(* case 2.2.2: n >= d *)
- Repeat Rewrite lift_bref_ge; XAuto.
+ Repeat Rewrite lift_lref_ge; XAuto.
(* case 3: TTail k *)
LiftTailRw; SRw; XAuto.
Qed.
XElim t; Intros.
(* case 1: TSort *)
XAuto.
-(* case 2: TBRef n *)
+(* case 2: TLRef n *)
Apply (lt_le_e n d); Intros.
(* case 2.1: n < d *)
- Rewrite lift_bref_lt; XAuto.
+ Rewrite lift_lref_lt; XAuto.
(* case 2.2: n >= d *)
- Rewrite lift_bref_ge; [ Simpl | XAuto ].
+ Rewrite lift_lref_ge; [ Simpl | XAuto ].
Rewrite (H n); XAuto.
(* case 3: TTail k *)
XElim k; Intros; LiftTailRw; Simpl.
XElim t; Intros.
(* case 1: TSort *)
XAuto.
-(* case 2: TBRef *)
+(* case 2: TLRef *)
Apply (lt_le_e n d); Intros.
(* case 2.1: n < d *)
- Repeat Rewrite lift_bref_lt; Simpl; XAuto.
+ Repeat Rewrite lift_lref_lt; Simpl; XAuto.
(* case 2.2: n >= d *)
- Repeat Rewrite lift_bref_ge; Simpl; Try Rewrite <- plus_n_Sm; XAuto.
+ Repeat Rewrite lift_lref_ge; Simpl; Try Rewrite <- plus_n_Sm; XAuto.
(* case 3: TTail k *)
XElim k; Intros; LiftTailRw; Simpl.
(* case 1 : bind b *)
Hints Resolve lift_tlt_dx : ltlc.
-(*#* #start file *)
-
(*#* #single *)
LApply (H_x ?3); [ Clear H_x; Intros H_x | XAuto ];
XElim H_x; Clear H0 H1; Intros.
-(* case pr0_cong pr0_gamma pr0_refl *****************************************)
-
- Remark pr0_cong_gamma_refl: (b:?) ~ b = Abst ->
- (u0,u3:?) (pr0 u0 u3) ->
- (t4,t5:?) (pr0 t4 t5) ->
- (u2,v2,x:?) (pr0 u2 x) -> (pr0 v2 x) ->
- (EX t:T | (pr0 (TTail (Flat Appl) u2 (TTail (Bind b) u0 t4)) t) &
- (pr0 (TTail (Bind b) u3 (TTail (Flat Appl) (lift (1) (0) v2) t5)) t)).
+(* case pr0_cong pr0_upsilon pr0_refl ***************************************)
+
+ Remark pr0_cong_upsilon_refl: (b:?) ~ b = Abst ->
+ (u0,u3:?) (pr0 u0 u3) ->
+ (t4,t5:?) (pr0 t4 t5) ->
+ (u2,v2,x:?) (pr0 u2 x) -> (pr0 v2 x) ->
+ (EX t:T | (pr0 (TTail (Flat Appl) u2 (TTail (Bind b) u0 t4)) t) &
+ (pr0 (TTail (Bind b) u3 (TTail (Flat Appl) (lift (1) (0) v2) t5)) t)).
Intros.
Apply ex2_intro with x:=(TTail (Bind b) u3 (TTail (Flat Appl) (lift (1) (0) x) t5)); XAuto.
Qed.
-(* case pr0_cong pr0_gamma pr0_cong *****************************************)
+(* case pr0_cong pr0_upsilon pr0_cong ***************************************)
- Remark pr0_cong_gamma_cong: (b:?) ~ b = Abst ->
- (u2,v2,x:?) (pr0 u2 x) -> (pr0 v2 x) ->
- (t2,t5,x0:?) (pr0 t2 x0) -> (pr0 t5 x0) ->
- (u5,u3,x1:?) (pr0 u5 x1) -> (pr0 u3 x1) ->
- (EX t:T | (pr0 (TTail (Flat Appl) u2 (TTail (Bind b) u5 t2)) t) &
- (pr0 (TTail (Bind b) u3 (TTail (Flat Appl) (lift (1) (0) v2) t5)) t)).
+ Remark pr0_cong_upsilon_cong: (b:?) ~ b = Abst ->
+ (u2,v2,x:?) (pr0 u2 x) -> (pr0 v2 x) ->
+ (t2,t5,x0:?) (pr0 t2 x0) -> (pr0 t5 x0) ->
+ (u5,u3,x1:?) (pr0 u5 x1) -> (pr0 u3 x1) ->
+ (EX t:T | (pr0 (TTail (Flat Appl) u2 (TTail (Bind b) u5 t2)) t) &
+ (pr0 (TTail (Bind b) u3 (TTail (Flat Appl) (lift (1) (0) v2) t5)) t)).
Intros.
Apply ex2_intro with x:=(TTail (Bind b) x1 (TTail (Flat Appl) (lift (1) (0) x) x0)); XAuto.
Qed.
-(* case pr0_cong pr0_gamma pr0_delta *****************************************)
+(* case pr0_cong pr0_upsilon pr0_delta **************************************)
- Remark pr0_cong_gamma_delta: ~ Abbr = Abst ->
- (u5,t2,w:?) (subst0 (0) u5 t2 w) ->
- (u2,v2,x:?) (pr0 u2 x) -> (pr0 v2 x) ->
- (t5,x0:?) (pr0 t2 x0) -> (pr0 t5 x0) ->
- (u3,x1:?) (pr0 u5 x1) -> (pr0 u3 x1) ->
- (EX t:T | (pr0 (TTail (Flat Appl) u2 (TTail (Bind Abbr) u5 w)) t) &
- (pr0 (TTail (Bind Abbr) u3 (TTail (Flat Appl) (lift (1) (0) v2) t5)) t)).
+ Remark pr0_cong_upsilon_delta: ~ Abbr = Abst ->
+ (u5,t2,w:?) (subst0 (0) u5 t2 w) ->
+ (u2,v2,x:?) (pr0 u2 x) -> (pr0 v2 x) ->
+ (t5,x0:?) (pr0 t2 x0) -> (pr0 t5 x0) ->
+ (u3,x1:?) (pr0 u5 x1) -> (pr0 u3 x1) ->
+ (EX t:T | (pr0 (TTail (Flat Appl) u2 (TTail (Bind Abbr) u5 w)) t) &
+ (pr0 (TTail (Bind Abbr) u3 (TTail (Flat Appl) (lift (1) (0) v2) t5)) t)).
Intros; Pr0Subst0.
(* case 1: x0 is a lift *)
Apply ex2_intro with x:=(TTail (Bind Abbr) x1 (TTail (Flat Appl) (lift (1) (0) x) x0)); XAuto.
Apply ex2_intro with x:=(TTail (Bind Abbr) x1 (TTail (Flat Appl) (lift (1) (0) x) x2)); XEAuto.
Qed.
-(* case pr0_cong pr0_gamma pr0_zeta *****************************************)
+(* case pr0_cong pr0_upsilon pr0_zeta ***************************************)
- Remark pr0_cong_gamma_zeta: (b:?) ~ b = Abst ->
- (u0,u3:?) (pr0 u0 u3) ->
- (u2,v2,x0:?) (pr0 u2 x0) -> (pr0 v2 x0) ->
- (x,t3,x1:?) (pr0 x x1) -> (pr0 t3 x1) ->
- (EX t:T | (pr0 (TTail (Flat Appl) u2 t3) t) &
- (pr0 (TTail (Bind b) u3 (TTail (Flat Appl) (lift (1) (0) v2) (lift (1) (0) x))) t)).
+ Remark pr0_cong_upsilon_zeta: (b:?) ~ b = Abst ->
+ (u0,u3:?) (pr0 u0 u3) ->
+ (u2,v2,x0:?) (pr0 u2 x0) -> (pr0 v2 x0) ->
+ (x,t3,x1:?) (pr0 x x1) -> (pr0 t3 x1) ->
+ (EX t:T | (pr0 (TTail (Flat Appl) u2 t3) t) &
+ (pr0 (TTail (Bind b) u3 (TTail (Flat Appl) (lift (1) (0) v2) (lift (1) (0) x))) t)).
Intros; LiftTailRwBack; XEAuto.
Qed.
Intros; Pr0Subst0; XEAuto.
Qed.
-(* case pr0_gamma pr0_gamma *************************************************)
+(* case pr0_upsilon pr0_upsilon *********************************************)
- Remark pr0_gamma_gamma: (b:?) ~ b = Abst ->
- (v1,v2,x0:?) (pr0 v1 x0) -> (pr0 v2 x0) ->
- (u1,u2,x1:?) (pr0 u1 x1) -> (pr0 u2 x1) ->
- (t1,t2,x2:?) (pr0 t1 x2) -> (pr0 t2 x2) ->
- (EX t:T | (pr0 (TTail (Bind b) u1 (TTail (Flat Appl) (lift (1) (0) v1) t1)) t) &
- (pr0 (TTail (Bind b) u2 (TTail (Flat Appl) (lift (1) (0) v2) t2)) t)).
+ Remark pr0_upsilon_upsilon: (b:?) ~ b = Abst ->
+ (v1,v2,x0:?) (pr0 v1 x0) -> (pr0 v2 x0) ->
+ (u1,u2,x1:?) (pr0 u1 x1) -> (pr0 u2 x1) ->
+ (t1,t2,x2:?) (pr0 t1 x2) -> (pr0 t2 x2) ->
+ (EX t:T | (pr0 (TTail (Bind b) u1 (TTail (Flat Appl) (lift (1) (0) v1) t1)) t) &
+ (pr0 (TTail (Bind b) u2 (TTail (Flat Appl) (lift (1) (0) v2) t2)) t)).
Intros.
Apply ex2_intro with x:=(TTail (Bind b) x1 (TTail (Flat Appl) (lift (1) (0) x0) x2)); XAuto.
Qed.
(* main *********************************************************************)
- Hints Resolve pr0_cong_gamma_refl pr0_cong_gamma_cong : ltlc.
- Hints Resolve pr0_cong_gamma_delta pr0_cong_gamma_zeta : ltlc.
+ Hints Resolve pr0_cong_upsilon_refl pr0_cong_upsilon_cong : ltlc.
+ Hints Resolve pr0_cong_upsilon_delta pr0_cong_upsilon_zeta : ltlc.
Hints Resolve pr0_cong_delta : ltlc.
- Hints Resolve pr0_gamma_gamma : ltlc.
+ Hints Resolve pr0_upsilon_upsilon : ltlc.
Hints Resolve pr0_delta_delta pr0_delta_epsilon : ltlc.
-(*#* #start proof *)
+(*#* #start file *)
(*#* #caption "confluence with itself: Church-Rosser property" *)
(*#* #cap #cap t0, t1, t2, t *)
- Theorem pr0_confluence : (t0,t1:?) (pr0 t0 t1) -> (t2:?) (pr0 t0 t2) ->
- (EX t | (pr0 t1 t) & (pr0 t2 t)).
-
+ Theorem pr0_confluence: (t0,t1:?) (pr0 t0 t1) -> (t2:?) (pr0 t0 t2) ->
+ (EX t | (pr0 t1 t) & (pr0 t2 t)).
+
(*#* #stop file *)
-
+
XElimUsing tlt_wf_ind t0; Intros.
Inversion H0; Inversion H1; Clear H0 H1;
- XSubst; Repeat IH; XEAuto.
+ XSubst; Repeat IH; XDEAuto 4.
Qed.
End pr0_confluence.
-(*#* #stop file *)
-
Require Export subst0_defs.
+(*#* #caption "axioms for the relation $\\PrZ{}{}$",
+ "reflexivity", "compaibility", "$\\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 *)
+
Inductive pr0 : T -> T -> Prop :=
(* structural rules *)
- | pr0_refl : (t:?) (pr0 t t)
- | pr0_thin : (u1,u2:?) (pr0 u1 u2) -> (t1,t2:?) (pr0 t1 t2) ->
- (k:?) (pr0 (TTail k u1 t1) (TTail k u2 t2))
+ | pr0_refl : (t:?) (pr0 t t)
+ | pr0_comp : (u1,u2:?) (pr0 u1 u2) -> (t1,t2:?) (pr0 t1 t2) ->
+ (k:?) (pr0 (TTail k u1 t1) (TTail k u2 t2))
(* axiom rules *)
- | pr0_beta : (k,v1,v2:?) (pr0 v1 v2) -> (t1,t2:?) (pr0 t1 t2) ->
- (pr0 (TTail (Flat Appl) v1 (TTail (Bind Abst) k t1))
- (TTail (Bind Abbr) v2 t2))
- | pr0_gamma : (b:?) ~b=Abst -> (v1,v2:?) (pr0 v1 v2) ->
- (u1,u2:?) (pr0 u1 u2) -> (t1,t2:?) (pr0 t1 t2) ->
- (pr0 (TTail (Flat Appl) v1 (TTail (Bind b) u1 t1))
- (TTail (Bind b) u2 (TTail (Flat Appl) (lift (1) (0) v2) t2)))
- | pr0_delta : (u1,u2:?) (pr0 u1 u2) -> (t1,t2:?) (pr0 t1 t2) ->
- (w:?) (subst0 (0) u2 t2 w) ->
- (pr0 (TTail (Bind Abbr) u1 t1) (TTail (Bind Abbr) u2 w))
- | pr0_zeta : (b:?) ~b=Abst -> (t1,t2:?) (pr0 t1 t2) ->
- (u:?) (pr0 (TTail (Bind b) u (lift (1) (0) t1)) t2)
- | pr0_eps : (t1,t2:?) (pr0 t1 t2) ->
- (u:?) (pr0 (TTail (Flat Cast) u t1) t2).
+ | pr0_beta : (u,v1,v2:?) (pr0 v1 v2) -> (t1,t2:?) (pr0 t1 t2) ->
+ (pr0 (TTail (Flat Appl) v1 (TTail (Bind Abst) u t1))
+ (TTail (Bind Abbr) v2 t2))
+ | pr0_upsilon: (b:?) ~b=Abst -> (v1,v2:?) (pr0 v1 v2) ->
+ (u1,u2:?) (pr0 u1 u2) -> (t1,t2:?) (pr0 t1 t2) ->
+ (pr0 (TTail (Flat Appl) v1 (TTail (Bind b) u1 t1))
+ (TTail (Bind b) u2 (TTail (Flat Appl) (lift (1) (0) v2) t2)))
+ | pr0_delta : (u1,u2:?) (pr0 u1 u2) -> (t1,t2:?) (pr0 t1 t2) ->
+ (w:?) (subst0 (0) u2 t2 w) ->
+ (pr0 (TTail (Bind Abbr) u1 t1) (TTail (Bind Abbr) u2 w))
+ | pr0_zeta : (b:?) ~b=Abst -> (t1,t2:?) (pr0 t1 t2) ->
+ (u:?) (pr0 (TTail (Bind b) u (lift (1) (0) t1)) t2)
+ | pr0_epsilon: (t1,t2:?) (pr0 t1 t2) ->
+ (u:?) (pr0 (TTail (Flat Cast) u t1) t2).
+
+(*#* #stop file *)
Hint pr0 : ltlc := Constructors pr0.
- Section pr0_gen. (********************************************************)
+ Section pr0_gen_base. (***************************************************)
Theorem pr0_gen_sort : (x:?; n:?) (pr0 (TSort n) x) -> x = (TSort n).
Intros; Inversion H; XAuto.
Qed.
- Theorem pr0_gen_bref : (x:?; n:?) (pr0 (TBRef n) x) -> x = (TBRef n).
+ Theorem pr0_gen_lref : (x:?; n:?) (pr0 (TLRef n) x) -> x = (TLRef n).
Intros; Inversion H; XAuto.
Qed.
Intros; Inversion H; XEAuto.
Qed.
- End pr0_gen.
+ End pr0_gen_base.
- Hints Resolve pr0_gen_sort pr0_gen_bref : ltlc.
+ Hints Resolve pr0_gen_sort pr0_gen_lref : ltlc.
Tactic Definition Pr0GenBase :=
Match Context With
- | [ H: (pr0 (TTail (Bind Abst) ?1 ?2) ?3) |- ? ] ->
+ | [ H: (pr0 (TSort ?1) ?2) |- ? ] ->
+ LApply (pr0_gen_sort ?2 ?1); [ Clear H; Intros | XAuto ]
+ | [ H: (pr0 (TLRef ?1) ?2) |- ? ] ->
+ LApply (pr0_gen_lref ?2 ?1); [ Clear H; Intros | XAuto ]
+ | [ H: (pr0 (TTail (Bind Abst) ?1 ?2) ?3) |- ? ] ->
LApply (pr0_gen_abst ?1 ?2 ?3); [ Clear H; Intros H | XAuto ];
XElim H; Intros
| [ H: (pr0 (TTail (Flat Appl) ?1 ?2) ?3) |- ? ] ->
XElim H_x; Intro; Intros H_x; Intro;
Try Rewrite H_x; Try Rewrite H_x in H3; Clear H_x.
-(*#* #start file *)
-
(*#* #caption "generation lemma for lift" *)
(*#* #cap #alpha t1 in U1, t2 in U2, x in T, d in i *)
Theorem pr0_gen_lift : (t1,x:?; h,d:?) (pr0 (lift h d t1) x) ->
(EX t2 | x = (lift h d t2) & (pr0 t1 t2)).
-
-(*#* #stop file *)
-
Intros until 1; InsertEq H '(lift h d t1);
UnIntro H d; UnIntro H t1; XElim H; Clear y x; Intros;
Rename x into t3; Rename x0 into d.
LiftGen; Rewrite H3; Clear H3 t0.
LiftGen; Rewrite H3; Clear H3 H5 x1 k.
IH; IH; XEAuto.
-(* case 4 : pr0_gamma *)
+(* case 4 : pr0_upsilon *)
LiftGen; Rewrite H6; Clear H6 t0.
LiftGen; Rewrite H6; Clear H6 x1.
IH; IH; IH.
Require subst0_lift.
Require pr0_defs.
-(*#* #caption "main properties of predicate \\texttt{pr0}" *)
+(*#* #caption "main properties of the relation $\\PrZ{}{}$" *)
(*#* #clauses pr0_props *)
+(*#* #stop file *)
+
Section pr0_lift. (*******************************************************)
(*#* #caption "conguence with lift" *)
Theorem pr0_lift: (t1,t2:?) (pr0 t1 t2) ->
(h,d:?) (pr0 (lift h d t1) (lift h d t2)).
-(*#* #stop file *)
-
Intros until 1; XElim H; Intros.
(* case 1: pr0_refl *)
XAuto.
LiftTailRw; XAuto.
(* case 3 : pr0_beta *)
LiftTailRw; XAuto.
-(* case 4: pr0_gamma *)
+(* case 4: pr0_upsilon *)
LiftTailRw; Simpl; Arith0 d; Rewrite lift_d; XAuto.
(* case 5: pr0_delta *)
LiftTailRw; Simpl.
(*#* #start file *)
-(*#* #caption "confluence with substitution" *)
-(*#* #cap #cap t1,t2,v1,v2 #alpha w1 in U1, w2 in U2 *)
+(*#* #caption "confluence with strict substitution" *)
+(*#* #cap #cap t1, t2 #alpha v1 in W1, v2 in W2, w1 in U1, w2 in U2 *)
Theorem pr0_subst0: (t1,t2:?) (pr0 t1 t2) ->
(v1,w1:?; i:?) (subst0 i v1 t1 w1) ->
(* case 3: pr0_beta *)
Repeat Subst0Gen; Rewrite H3; Try Rewrite H5; Try Rewrite H6;
Repeat IH; XEAuto.
-(* case 4: pr0_gamma *)
+(* case 4: pr0_upsilon *)
Repeat Subst0Gen; Rewrite H6; Try Rewrite H8; Try Rewrite H9;
Repeat IH; XDEAuto 7.
(* case 5: pr0_delta *)
LApply (H1 ?4 ?5 ?3); [ Clear H1 H2; Intros H1 | XAuto ];
LApply (H1 ?4); [ Clear H1; Intros H1 | XAuto ];
XElim H1; [ Intros | Intros H1; XElim H1; Intros ]
- | [ H1: (subst0 ?0 ?1 ?2 ?3); H2: (pr0 ?4 ?1) |- ? ] ->
- LApply (pr0_subst0_back ?1 ?2 ?3 ?0); [ Clear H1; Intros H1 | XAuto ];
- LApply (H1 ?4); [ Clear H1 H2; Intros H1 | XAuto ];
- XElim H1; Intros
+ | [ _: (subst0 ?0 ?1 ?2 ?3); _: (pr0 ?4 ?1) |- ? ] ->
+ LApply (pr0_subst0_back ?1 ?2 ?3 ?0); [ Intros H_x | XAuto ];
+ LApply (H_x ?4); [ Clear H_x; Intros H_x | XAuto ];
+ XElim H_x; Intros
| [ H1: (subst0 ?0 ?1 ?2 ?3); H2: (pr0 ?1 ?4) |- ? ] ->
LApply (pr0_subst0_fwd ?1 ?2 ?3 ?0); [ Clear H1; Intros H1 | XAuto ];
LApply (H1 ?4); [ Clear H1 H2; Intros H1 | XAuto ];
+(*#* #stop file *)
+
Require pr0_confluence.
Require pr1_defs.
Theorem pr1_strip : (t0,t1:?) (pr1 t0 t1) -> (t2:?) (pr0 t0 t2) ->
(EX t | (pr1 t1 t) & (pr1 t2 t)).
-
-(*#* #stop proof *)
-
Intros until 1; XElim H; Intros.
(* case 1 : pr1_r *)
XEAuto.
XElim H1; Intros; XEAuto.
Qed.
-(*#* #start proof *)
-
(*#* #caption "confluence with itself: Church-Rosser property" *)
(*#* #cap #cap t0, t1, t2, t *)
Theorem pr1_confluence : (t0,t1:?) (pr1 t0 t1) -> (t2:?) (pr1 t0 t2) ->
(EX t | (pr1 t1 t) & (pr1 t2 t)).
-
-(*#* #stop file *)
-
Intros until 1; XElim H; Intros.
(* case 1 : pr1_r *)
XEAuto.
XElim H1; Intros
| _ -> Pr0Confluence.
-(*#* #start file *)
-
(*#* #single *)
-(*#* #stop file *)
-
Require Export lift_defs.
+(*#* #caption "axioms for strict substitution in terms",
+ "substituted local reference",
+ "substituted tail item: first operand",
+ "substituted tail item: second operand",
+ "substituted tail item: both operands"
+*)
+(*#* #cap #cap t, t1, t2 #alpha v in W, u in V, u1 in V1, u2 in V2, k in z, s in p *)
+
Inductive subst0 : nat -> T -> T -> T -> Prop :=
- | subst0_bref : (v:?; i:?) (subst0 i v (TBRef i) (lift (S i) (0) v))
- | subst0_fst : (v,w,u:?; i:?) (subst0 i v u w) ->
- (t:?; k:?) (subst0 i v (TTail k u t) (TTail k w t))
- | subst0_snd : (k:?; v,w,t:?; i:?) (subst0 (s k i) v t w) -> (u:?)
- (subst0 i v (TTail k u t) (TTail k u w))
- | subst0_both : (v,u1,u2:?; i:?) (subst0 i v u1 u2) ->
- (k:?; t1,t2:?) (subst0 (s k i) v t1 t2) ->
- (subst0 i v (TTail k u1 t1) (TTail k u2 t2)).
+ | subst0_lref: (v:?; i:?) (subst0 i v (TLRef i) (lift (S i) (0) v))
+ | subst0_fst : (v,u2,u1:?; i:?) (subst0 i v u1 u2) ->
+ (t:?; k:?) (subst0 i v (TTail k u1 t) (TTail k u2 t))
+ | subst0_snd : (k:?; v,t2,t1:?; i:?) (subst0 (s k i) v t1 t2) -> (u:?)
+ (subst0 i v (TTail k u t1) (TTail k u t2))
+ | subst0_both: (v,u1,u2:?; i:?) (subst0 i v u1 u2) ->
+ (k:?; t1,t2:?) (subst0 (s k i) v t1 t2) ->
+ (subst0 i v (TTail k u1 t1) (TTail k u2 t2)).
+
+(*#* #stop file *)
Hint subst0 : ltlc := Constructors subst0.
Intros; Inversion H.
Qed.
- Theorem subst0_gen_bref : (v,x:?; i,n:?) (subst0 i v (TBRef n) x) ->
+ Theorem subst0_gen_lref : (v,x:?; i,n:?) (subst0 i v (TLRef n) x) ->
n = i /\ x = (lift (S n) (0) v).
Intros; Inversion H; XAuto.
Qed.
Match Context With
| [ H: (subst0 ?1 ?2 (TSort ?3) ?4) |- ? ] ->
Apply (subst0_gen_sort ?2 ?4 ?1 ?3); Apply H
- | [ H: (subst0 ?1 ?2 (TBRef ?3) ?4) |- ? ] ->
- LApply (subst0_gen_bref ?2 ?4 ?1 ?3); [ Clear H; Intros H | XAuto ];
+ | [ H: (subst0 ?1 ?2 (TLRef ?3) ?4) |- ? ] ->
+ LApply (subst0_gen_lref ?2 ?4 ?1 ?3); [ Clear H; Intros H | XAuto ];
XElim H; Intros
| [ H: (subst0 ?1 ?2 (TTail ?3 ?4 ?5) ?6) |- ? ] ->
LApply (subst0_gen_tail ?3 ?2 ?4 ?5 ?6 ?1); [ Clear H; Intros H | XAuto ];
XElim H; Intros H; XElim H; Intros.
-
XElim t1; Intros.
(* case 1: TSort *)
Rewrite lift_sort in H; Subst0GenBase.
-(* case 2: TBRef n *)
+(* case 2: TLRef n *)
Apply (lt_le_e n (S (plus i d))); Intros.
(* case 2.1: n < 1 + i + d *)
- Rewrite lift_bref_lt in H; [ Idtac | XAuto ].
+ Rewrite lift_lref_lt in H; [ Idtac | XAuto ].
Subst0GenBase; Rewrite H1; Rewrite H.
Rewrite <- lift_d; Simpl; XEAuto.
(* case 2.2: n >= 1 + i + d *)
- Rewrite lift_bref_ge in H; [ Idtac | XAuto ].
+ Rewrite lift_lref_ge in H; [ Idtac | XAuto ].
Subst0GenBase; Rewrite <- H in H0.
EApply le_false; [ Idtac | Apply H0 ]; XAuto.
(* case 3: TTail k *)
XElim t; Intros.
(* case 1: TSort *)
Rewrite lift_sort in H1; Subst0GenBase.
-(* case 2: TBRef n *)
+(* case 2: TLRef n *)
Apply (lt_le_e n d); Intros.
(* case 2.1: n < d *)
- Rewrite lift_bref_lt in H1; [ Idtac | XAuto ].
+ Rewrite lift_lref_lt in H1; [ Idtac | XAuto ].
Subst0GenBase; Rewrite H1 in H2.
EApply le_false; [ Apply H | XAuto ].
(* case 2.2: n >= d *)
- Rewrite lift_bref_ge in H1; [ Idtac | XAuto ].
+ Rewrite lift_lref_ge in H1; [ Idtac | XAuto ].
Subst0GenBase; Rewrite <- H1 in H0.
EApply le_false; [ Apply H2 | XEAuto ].
(* case 3: TTail k *)
XElim t1; Intros.
(* case 1: TSort *)
Rewrite lift_sort in H; Subst0GenBase.
-(* case 2: TBRef n *)
+(* case 2: TLRef n *)
Apply (lt_le_e n d); Intros.
(* case 2.1: n < d *)
- Rewrite lift_bref_lt in H; [ Idtac | XAuto ].
+ Rewrite lift_lref_lt in H; [ Idtac | XAuto ].
Subst0GenBase; Rewrite H in H1.
EApply le_false; [ Apply H0 | XAuto ].
(* case 2.2: n >= d *)
- Rewrite lift_bref_ge in H; [ Idtac | XAuto ].
+ Rewrite lift_lref_ge in H; [ Idtac | XAuto ].
Subst0GenBase; Rewrite <- H; Rewrite H2.
Rewrite minus_plus_r.
EApply ex2_intro; [ Idtac | XAuto ].
Section subst0_lift. (****************************************************)
- Theorem subst0_lift_lt : (t1,t2,u:?; i:?) (subst0 i u t1 t2) ->
- (d:?) (lt i d) -> (h:?)
- (subst0 i (lift h (minus d (S i)) u) (lift h d t1) (lift h d t2)).
+ Theorem subst0_lift_lt: (t1,t2,u:?; i:?) (subst0 i u t1 t2) ->
+ (d:?) (lt i d) -> (h:?)
+ (subst0 i (lift h (minus d (S i)) u) (lift h d t1) (lift h d t2)).
Intros until 1; XElim H; Intros.
-(* case 1: subst0_bref *)
- Rewrite lift_bref_lt; [ Idtac | XAuto ].
+(* case 1: subst0_lref *)
+ Rewrite lift_lref_lt; [ Idtac | XAuto ].
LetTac w := (minus d (S i0)).
Arith8 d '(S i0); Rewrite lift_d; XAuto.
(* case 2: subst0_fst *)
Apply subst0_both; [ Idtac | Rewrite <- (minus_s_s k) ]; XAuto.
Qed.
- Theorem subst0_lift_ge : (t1,t2,u:?; i,h:?) (subst0 i u t1 t2) ->
- (d:?) (le d i) ->
- (subst0 (plus i h) u (lift h d t1) (lift h d t2)).
+ Theorem subst0_lift_ge: (t1,t2,u:?; i,h:?) (subst0 i u t1 t2) ->
+ (d:?) (le d i) ->
+ (subst0 (plus i h) u (lift h d t1) (lift h d t2)).
Intros until 1; XElim H; Intros.
-(* case 1: subst0_bref *)
- Rewrite lift_bref_ge; [ Idtac | XAuto ].
+(* case 1: subst0_lref *)
+ Rewrite lift_lref_ge; [ Idtac | XAuto ].
Rewrite lift_free; [ Idtac | Simpl; XAuto | XAuto ].
Arith5'c h i0; XAuto.
(* case 2: subst0_fst *)
SRwBackIn H2; LiftTailRw; XAuto.
Qed.
- Theorem subst0_lift_ge_S : (t1,t2,u:?; i:?) (subst0 i u t1 t2) ->
- (d:?) (le d i) -> (b:?)
- (subst0 (s (Bind b) i) u (lift (1) d t1) (lift (1) d t2)).
- Intros; Simpl; Arith7 i; Apply subst0_lift_ge; XAuto.
+ Theorem subst0_lift_ge_S: (t1,t2,u:?; i:?) (subst0 i u t1 t2) ->
+ (d:?) (le d i) ->
+ (subst0 (S i) u (lift (1) d t1) (lift (1) d t2)).
+ Intros; Arith7 i; Apply subst0_lift_ge; XAuto.
Qed.
- End subst0_lift.
+ Theorem subst0_lift_ge_s: (t1,t2,u:?; i:?) (subst0 i u t1 t2) ->
+ (d:?) (le d i) -> (b:?)
+ (subst0 (s (Bind b) i) u (lift (1) d t1) (lift (1) d t2)).
+ Intros; Simpl; Apply subst0_lift_ge_S; XAuto.
+ Qed.
- Hints Resolve subst0_lift_lt subst0_lift_ge subst0_lift_ge_S : ltlc.
+ End subst0_lift.
+
+ Hints Resolve subst0_lift_lt subst0_lift_ge
+ subst0_lift_ge_S subst0_lift_ge_s : ltlc.
(u1,u:?; i:?) (subst0 i u u1 u2) ->
(EX t | (subst0 j u1 t1 t) & (subst0 (S (plus i j)) u t t2)).
Intros until 1; XElim H; Intros.
-(* case 1 : subst0_bref *)
+(* case 1 : subst0_lref *)
Arith5 i0 i; XEAuto.
(* case 2 : subst0_fst *)
IH; XEAuto.
(u1,u:?; i:?) (subst0 i u u2 u1) ->
(EX t | (subst0 j u1 t1 t) & (subst0 (S (plus i j)) u t2 t)).
Intros until 1; XElim H; Intros.
-(* case 1 : subst0_bref *)
+(* case 1 : subst0_lref *)
Arith5 i0 i; XEAuto.
(* case 2 : subst0_fst *)
IH; XEAuto.
(lt (weight_map f (lift (S d) (0) u)) (g d)) ->
(le (weight_map f z) (weight_map g t)).
Intros until 1; XElim H.
-(* case 1: subst0_bref *)
+(* case 1: subst0_lref *)
Intros; XAuto.
(* case 2: subst0_fst *)
XElim k; [ XElim b | Idtac ]; Simpl; [ Auto 7 with ltlc (**) | XAuto | XAuto | XAuto ].
(lt (weight_map f (lift (S d) (0) u)) (g d)) ->
(lt (weight_map f z) (weight_map g t)).
Intros until 1; XElim H.
-(* case 1: subst0_bref *)
+(* case 1: subst0_lref *)
Intros; XAuto.
(* case 2: subst0_fst *)
XElim k; [ XElim b | Idtac ]; Simpl; Intros;
Try Subst0GenBase; XAuto.
Qed.
- Theorem subst1_gen_bref : (v,x:?; i,n:?) (subst1 i v (TBRef n) x) ->
- x = (TBRef n) \/
+ Theorem subst1_gen_lref : (v,x:?; i,n:?) (subst1 i v (TLRef n) x) ->
+ x = (TLRef n) \/
n = i /\ x = (lift (S n) (0) v).
Intros; XElim H; Clear x; Intros;
Try Subst0GenBase; XAuto.
Fixpoint weight_map [f:nat->nat; t:T] : nat := Cases t of
| (TSort n) => (0)
- | (TBRef n) => (f n)
+ | (TLRef n) => (f n)
| (TTail (Bind Abbr) u t) =>
(S (plus (weight_map f u) (weight_map (wadd f (S (weight_map f u))) t)))
| (TTail (Bind _) u t) =>
| 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 (TBRef n) (lift (S n) (0) 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 (TBRef n) (lift (S n) (0) u))
+ (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) ->
(*#* #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_bref: (g:?; c:?; x:?; n:?) (ty0 g c (TBRef n) x) ->
+ 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)
(*#* #stop proof *)
- Intros until 1; InsertEq H '(TBRef n); XElim H; Intros.
+ 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.
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 (TBRef ?3) ?4) |- ? ] ->
- LApply (ty0_gen_bref ?1 ?2 ?4 ?3); [ Clear H; Intros H | 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 ];
Pattern 3 d0; Rewrite (le_plus_minus_sym (S n) d0); [ Idtac | XAuto ].
Pattern 4 d0; Rewrite (le_plus_minus (S n) d0); [ Idtac | XAuto ].
EApply ex3_2_intro;
- [ Rewrite lift_bref_lt | Rewrite lift_d | EApply ty0_abbr ]; XEAuto.
+ [ Rewrite lift_lref_lt | Rewrite lift_d | EApply ty0_abbr ]; XEAuto.
(* case 3.2 : n = d0 *)
Rewrite H7; Rewrite H7 in H0; Clear H2 H7 n.
DropDis; Inversion H0; Rewrite H8 in H4; Clear H0 H7 H8 e u0.
Pattern 1 n; Rewrite (lt_plus_minus (0) n); [ Idtac | XEAuto ].
Arith4c '(0) '(minus n (1)).
EApply ex3_2_intro;
- [ Rewrite lift_bref_ge
+ [ Rewrite lift_lref_ge
| Rewrite lift_free; Simpl
| Pattern 2 n; Rewrite (minus_x_SO n)
]; XEAuto.
Pattern 3 d0; Rewrite (le_plus_minus_sym (S n) d0); [ Idtac | XAuto ].
Pattern 4 d0; Rewrite (le_plus_minus (S n) d0); [ Idtac | XAuto ].
EApply ex3_2_intro;
- [ Rewrite lift_bref_lt | Rewrite lift_d | EApply ty0_abst ]; XEAuto.
+ [ Rewrite lift_lref_lt | Rewrite lift_d | EApply ty0_abst ]; XEAuto.
(* case 4.2 : n = d0 *)
Rewrite H7; Rewrite H7 in H0; DropDis; Inversion H0.
(* case 4.3 : n > d0 *)
Pattern 1 n; Rewrite (lt_plus_minus (0) n); [ Idtac | XEAuto ].
Arith4c '(0) '(minus n (1)).
EApply ex3_2_intro;
- [ Rewrite lift_bref_ge
+ [ Rewrite lift_lref_ge
| Rewrite lift_free; Simpl
| Pattern 2 n; Rewrite (minus_x_SO n)
]; XEAuto.
LiftGen; Rewrite <- H0 in H2; Clear H0 x2.
Rewrite <- lift_d; [ Idtac | XAuto ].
Rewrite <- le_plus_minus; [ Idtac | XAuto ].
- EApply ex3_2_intro; [ Rewrite lift_bref_lt | Idtac | EApply ty0_abbr ]; XEAuto.
+ EApply ex3_2_intro; [ Rewrite lift_lref_lt | Idtac | EApply ty0_abbr ]; XEAuto.
(* case 3.2 : n = d0 *)
Rewrite H6 in H0; DropDis; Inversion H0.
(* case 3.3 : n > d0 *)
Pattern 1 n; Rewrite (lt_plus_minus (0) n); [ Idtac | XEAuto ].
Arith4c '(0) '(minus n (1)).
EApply ex3_2_intro;
- [ Rewrite lift_bref_ge
+ [ Rewrite lift_lref_ge
| Rewrite lift_free; Simpl
| Pattern 2 n; Rewrite (minus_x_SO n)
]; XEAuto.
LiftGen; Rewrite <- H0 in H2; Clear H0 x2.
Rewrite <- lift_d; [ Idtac | XAuto ].
Rewrite <- le_plus_minus; [ Idtac | XAuto ].
- EApply ex3_2_intro; [ Rewrite lift_bref_lt | Idtac | EApply ty0_abst ]; XEAuto.
+ EApply ex3_2_intro; [ Rewrite lift_lref_lt | Idtac | EApply ty0_abst ]; XEAuto.
(* case 4.2 : n = d0 *)
Rewrite H6 in H0; DropDis; Inversion H0.
(* case 4.3 : n > d0 *)
Pattern 1 n; Rewrite (lt_plus_minus (0) n); [ Idtac | XEAuto ].
Arith4c '(0) '(minus n (1)).
EApply ex3_2_intro;
- [ Rewrite lift_bref_ge
+ [ Rewrite lift_lref_ge
| Rewrite lift_free; [ Simpl | Simpl | Idtac ]
| Pattern 2 n; Rewrite (minus_x_SO n)
]; XEAuto.
(* case 3.1 : n < d0 *)
Rewrite minus_x_Sy in H4; [ Idtac | XAuto ].
DropGenBase; Rewrite H4 in H0; Clear H4 x.
- Rewrite lift_bref_lt; [ Idtac | XAuto ].
+ Rewrite lift_lref_lt; [ Idtac | XAuto ].
Arith8 d0 '(S n); Rewrite lift_d; [ Arith8' d0 '(S n) | XAuto ].
EApply ty0_abbr; XEAuto.
(* case 3.2 : n >= d0 *)
- Rewrite lift_bref_ge; [ Idtac | XAuto ].
+ Rewrite lift_lref_ge; [ Idtac | XAuto ].
Arith7' n; Rewrite lift_free; [ Idtac | Simpl; XAuto | XAuto ].
Rewrite (plus_sym h (S n)); Simpl; XEAuto.
(* case 4: ty0_abst *)
(* case 4.1 : n < d0 *)
Rewrite minus_x_Sy in H4; [ Idtac | XAuto ].
DropGenBase; Rewrite H4 in H0; Clear H4 x.
- Rewrite lift_bref_lt; [ Idtac | XAuto ].
+ Rewrite lift_lref_lt; [ Idtac | XAuto ].
Arith8 d0 '(S n); Rewrite lift_d; [ Arith8' d0 '(S n) | XAuto ].
EApply ty0_abst; XEAuto.
(* case 4.2 : n >= d0 *)
- Rewrite lift_bref_ge; [ Idtac | XAuto ].
+ Rewrite lift_lref_ge; [ Idtac | XAuto ].
Arith7' n; Rewrite lift_free; [ Idtac | Simpl; XAuto | XAuto ].
Rewrite (plus_sym h (S n)); Simpl; XEAuto.
(* case 5: ty0_bind *)
Require pr0_lift.
Require pr0_subst1.
Require cpr0_defs.
-Require cpr0_props.
Require pc3_props.
Require pc3_gen.
Require ty0_defs.
(*#* #caption "base case" *)
(*#* #cap #cap c1, c2 #alpha t1 in T, t2 in T1, t in T2 *)
- Theorem ty0_sred_cpr0_pr0 : (g:?; c1:?; t1,t:?) (ty0 g c1 t1 t) ->
- (c2:?) (wf0 g c2) -> (cpr0 c1 c2) ->
- (t2:?) (pr0 t1 t2) -> (ty0 g c2 t2 t).
+ Theorem ty0_sred_cpr0_pr0: (g:?; c1:?; t1,t:?) (ty0 g c1 t1 t) ->
+ (c2:?) (wf0 g c2) -> (cpr0 c1 c2) ->
+ (t2:?) (pr0 t1 t2) -> (ty0 g c2 t2 t).
(*#* #stop file *)
Intros until 1; XElim H; Intros.
-(* case 1 : ty0_conv *)
+(* case 1: ty0_conv *)
IH1c; IH0c; EApply ty0_conv; XEAuto.
-(* case 2 : ty0_sort *)
+(* case 2: ty0_sort *)
Inversion H2; XAuto.
-(* case 3 : ty0_abbr *)
+(* case 3: ty0_abbr *)
Inversion H5; Cpr0Drop; IH1c; XEAuto.
-(* case 4 : ty0_abst *)
+(* case 4: ty0_abst *)
Intros; Inversion H5; Cpr0Drop; IH0; IH1.
EApply ty0_conv;
[ EApply ty0_lift; [ Idtac | XAuto | XEAuto ]
| EApply ty0_abst
| EApply pc3_lift ]; XEAuto.
-(* case 5 : ty0_bind *)
+(* case 5: ty0_bind *)
Intros; Inversion H7; Clear H7.
-(* case 5.1 : pr0_refl *)
+(* case 5.1: pr0_refl *)
IH0c; IH0Bc; IH0Bc.
EApply ty0_bind; XEAuto.
-(* case 5.2 : pr0_cont *)
+(* case 5.2: pr0_cont *)
IH0; IH0B; Ty0Correct; IH3B; Ty0Correct.
EApply ty0_conv; [ EApply ty0_bind | EApply ty0_bind | Idtac ]; XEAuto.
-(* case 5.3 : pr0_delta *)
+(* case 5.3: pr0_delta *)
Rewrite <- H8 in H1; Rewrite <- H8 in H2;
Rewrite <- H8 in H3; Rewrite <- H8 in H4; Clear H8 b.
IH0; IH0B; Ty0Correct; IH3B; Ty0Correct.
EApply ty0_conv; [ EApply ty0_bind | EApply ty0_bind | Idtac ]; XEAuto.
-(* case 5.4 : pr0_zeta *)
+(* case 5.4: pr0_zeta *)
Rewrite <- H11 in H1; Rewrite <- H11 in H2; Clear H8 H9 H10 H11 b0 t2 t7 u0.
IH0; IH1BLc; Move H3 after H8; IH0Bc; Ty0Correct; Move H8 after H4; Clear H H0 H1 H3 H6 c c1 t t1;
NewInduction b.
-(* case 5.4.1 : Abbr *)
+(* case 5.4.1: Abbr *)
Ty0GenContext; Subst1Gen; LiftGen; Rewrite H in H1; Clear H x0.
EApply ty0_conv;
[ EApply ty0_bind; XEAuto | XEAuto
| EApply pc3_pr3_x;
EApply (pr3_t (TTail (Bind Abbr) u (lift (1) (0) x1))); XEAuto ].
-(* case 5.4.2 : Abst *)
+(* case 5.4.2: Abst *)
EqFalse.
-(* case 5.4.3 : Void *)
+(* case 5.4.3: Void *)
Ty0GenContext; Rewrite H0; Rewrite H0 in H2; Clear H0 t3.
LiftGen; Rewrite <- H in H1; Clear H x0.
EApply ty0_conv; [ EApply ty0_bind; XEAuto | XEAuto | XAuto ].
-(* case 6 : ty0_appl *)
+(* case 6: ty0_appl *)
Intros; Inversion H5; Clear H5.
-(* case 6.1 : pr0_refl *)
+(* case 6.1: pr0_refl *)
IH0c; IH0c; EApply ty0_appl; XEAuto.
-(* case 6.2 : pr0_cont *)
+(* case 6.2: pr0_cont *)
Clear H6 H7 H8 H9 c1 k t t1 t2 t3 u1.
IH0; Ty0Correct; Ty0GenBase; IH1c; IH0; IH1c.
EApply ty0_conv;
[ EApply ty0_appl; [ XEAuto | EApply ty0_bind; XEAuto ]
| EApply ty0_appl; XEAuto
| XEAuto ].
-(* case 6.3 : pr0_beta *)
+(* case 6.3: pr0_beta *)
Rewrite <- H7 in H1; Rewrite <- H7 in H2; Clear H6 H7 H9 c1 t t1 t2 v v1.
IH1T; IH0c; Ty0Correct; Ty0GenBase; IH0; IH1c.
Move H5 after H13; Ty0GenBase; Pc3Gen; Repeat CSub0Ty0.
| EApply ty0_bind
| Apply (pc3_t (TTail (Bind Abbr) v2 t0))
]; XEAuto.
-(* case 6.4 : pr0_delta *)
+(* case 6.4: pr0_delta *)
Rewrite <- H7 in H1; Rewrite <- H7 in H2; Clear H6 H7 H11 c1 t t1 t2 v v1.
IH1T2c; Clear H1; Ty0Correct; NonLinear; Ty0GenBase; IH1; IH0c.
Move H5 after H1; Ty0GenBase; Pc3Gen; Rewrite lift_bind in H0.
| 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.
-(* case 7 : ty0_cast *)
+(* case 7: ty0_cast *)
Intros; Inversion H5; Clear H5.
-(* case 7.1 : pr0_refl *)
+(* case 7.1: pr0_refl *)
IH0c; IH0c; EApply ty0_cast; XEAuto.
-(* case 7.2 : pr0_cont *)
+(* case 7.2: pr0_cont *)
Clear H6 H7 H8 H9 c1 k u1 t t1 t4 t5.
IH0; IH1c; IH1c.
EApply ty0_conv;
[ XEAuto
| EApply ty0_cast; [ EApply ty0_conv; XEAuto | XEAuto ]
| XAuto ].
-(* case 7.3 : pr0_eps *)
+(* case 7.3: pr0_epsilon *)
XAuto.
Qed.
Section ty0_sred_pr3. (**********************************************)
- Theorem ty0_sred_pr1 : (c:?; t1,t2:?) (pr1 t1 t2) ->
- (g:?; t:?) (ty0 g c t1 t) ->
- (ty0 g c t2 t).
+ Theorem ty0_sred_pr1: (c:?; t1,t2:?) (pr1 t1 t2) ->
+ (g:?; t:?) (ty0 g c t1 t) ->
+ (ty0 g c t2 t).
Intros until 1; XElim H; Intros.
-(* case 1 : pr1_r *)
+(* case 1: pr1_r *)
XAuto.
-(* case 2 : pr1_u *)
+(* case 2: pr1_u *)
EApply H1; EApply ty0_sred_cpr0_pr0; XEAuto.
Qed.
- Theorem ty0_sred_pr2 : (c:?; t1,t2:?) (pr2 c t1 t2) ->
- (g:?; t:?) (ty0 g c t1 t) ->
- (ty0 g c t2 t).
+ Theorem ty0_sred_pr2: (c:?; t1,t2:?) (pr2 c t1 t2) ->
+ (g:?; t:?) (ty0 g c t1 t) ->
+ (ty0 g c t2 t).
Intros until 1; XElim H; Intros.
-(* case 1 : pr2_pr0 *)
+(* case 1: pr2_free *)
EApply ty0_sred_cpr0_pr0; XEAuto.
-(* case 2 : pr2_u *)
- XEAuto.
+(* case 2: pr2_u *)
+ EApply ty0_subst0; Try EApply ty0_sred_cpr0_pr0; XEAuto.
Qed.
(*#* #start file *)
(*#* #caption "general case" *)
(*#* #cap #cap c #alpha t1 in T, t2 in T1, t in T2 *)
- Theorem ty0_sred_pr3 : (c:?; t1,t2:?) (pr3 c t1 t2) ->
- (g:?; t:?) (ty0 g c t1 t) ->
- (ty0 g c t2 t).
+ Theorem ty0_sred_pr3: (c:?; t1,t2:?) (pr3 c t1 t2) ->
+ (g:?; t:?) (ty0 g c t1 t) ->
+ (ty0 g c t2 t).
(*#* #stop file *)
Intros until 1; XElim H; Intros.
-(* case 1 : pr3_r *)
+(* case 1: pr3_refl *)
XAuto.
-(* case 2 : pr3_u *)
+(* case 2: pr3_sing *)
EApply H1; EApply ty0_sred_pr2; XEAuto.
Qed.
Require drop_props.
Require csubst0_defs.
+Require fsubst0_defs.
Require pc3_props.
Require pc3_subst0.
Require ty0_defs.
Intros until 1; XElim H.
(* case 1: ty0_conv *)
Intros until 6; XElim H4; Intros.
-(* case 1.1: fsubst0_t *)
+(* case 1.1: fsubst0_snd *)
IHT; EApply ty0_conv; XEAuto.
-(* case 1.2: fsubst0_c *)
+(* case 1.2: fsubst0_fst *)
IHC; EApply ty0_conv; Try EApply pc3_fsubst0; XEAuto.
-(* case 1.3: fsubst0_b *)
+(* case 1.3: fsubst0_both *)
IHCT; IHCT; EApply ty0_conv; Try EApply pc3_fsubst0; XEAuto.
(* case 2: ty0_sort *)
Intros until 2; XElim H0; Intros.
-(* case 2.1: fsubst0_t *)
+(* case 2.1: fsubst0_snd *)
Subst0GenBase.
-(* case 2.2: fsubst0_c *)
+(* case 2.2: fsubst0_fst *)
XAuto.
-(* case 2.3: fsubst0_b *)
+(* case 2.3: fsubst0_both *)
Subst0GenBase.
(* case 3: ty0_abbr *)
Intros until 5; XElim H3; Intros; Clear c1 c2 t t1 t2.
-(* case 3.1: fsubst0_t *)
+(* case 3.1: fsubst0_snd *)
Subst0GenBase; Rewrite H6; Rewrite <- H3 in H5; Clear H3 H6 i t3.
DropDis; Inversion H5; Rewrite <- H6 in H0; Rewrite H7 in H1; XEAuto.
-(* case 3.2: fsubst0_c *)
+(* case 3.2: fsubst0_fst *)
Apply (lt_le_e n i); Intros; CSubst0Drop.
(* case 3.2.1: n < i, none *)
EApply ty0_abbr; XEAuto.
-(* case 3.2.2: n < i, csubst0_fst *)
+(* case 3.2.2: n < i, csubst0_snd *)
Inversion H0; CSubst0Drop.
Rewrite <- H10 in H7; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H8;
Clear H0 H10 H11 H12 x0 x1 x2.
DropDis; Rewrite minus_x_Sy in H0; [ DropGenBase | XAuto ].
IHT; EApply ty0_abbr; XEAuto.
-(* case 3.2.3: n < i, csubst0_snd *)
+(* case 3.2.3: n < i, csubst0_fst *)
Inversion H0; CSubst0Drop.
Rewrite <- H10 in H8; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H7;
Clear H0 H10 H11 H12 x0 x1 x3.
IHCT; EApply ty0_abbr; XEAuto.
(* case 3.2.5: n >= i *)
EApply ty0_abbr; XEAuto.
-(* case 3.3: fsubst0_b *)
+(* case 3.3: fsubst0_both *)
Subst0GenBase; Rewrite H7; Rewrite <- H3 in H4; Rewrite <- H3 in H6; Clear H3 H7 i t3.
DropDis; Inversion H6; Rewrite <- H7 in H0; Rewrite H8 in H1.
CSubst0Drop; XEAuto.
(* case 4: ty0_abst *)
Intros until 5; XElim H3; Intros; Clear c1 c2 t t1 t2.
-(* case 4.1: fsubst0_t *)
+(* case 4.1: fsubst0_snd *)
Subst0GenBase; Rewrite H3 in H0; DropDis; Inversion H0.
-(* case 4.2: fsubst0_c *)
+(* case 4.2: fsubst0_fst *)
Apply (lt_le_e n i); Intros; CSubst0Drop.
(* case 4.2.1: n < i, none *)
EApply ty0_abst; XEAuto.
-(* case 4.2.2: n < i, csubst0_fst *)
+(* case 4.2.2: n < i, csubst0_snd *)
Inversion H0; CSubst0Drop.
Rewrite <- H10 in H7; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H8; Rewrite <- H12;
Clear H0 H10 H11 H12 x0 x1 x2.
DropDis; Rewrite minus_x_Sy in H0; [ DropGenBase | XAuto ].
IHT; EApply ty0_conv;
[ EApply ty0_lift | EApply ty0_abst | EApply pc3_lift ]; XEAuto.
-(* case 4.2.3: n < i, csubst0_snd *)
+(* case 4.2.3: n < i, csubst0_fst *)
Inversion H0; CSubst0Drop.
Rewrite <- H10 in H8; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H7; Rewrite <- H12;
Clear H0 H10 H11 H12 x0 x1 x3.
]; XEAuto.
(* case 4.2.4: n >= i *)
EApply ty0_abst; XEAuto.
-(* case 4.3: fsubst0_b *)
+(* case 4.3: fsubst0_both *)
Subst0GenBase; Rewrite H3 in H0; DropDis; Inversion H0.
(* case 5: ty0_bind *)
Intros until 7; XElim H5; Intros; Clear H4.
-(* case 5.1: fsubst0_t *)
+(* case 5.1: fsubst0_snd *)
Subst0GenBase; Rewrite H4; Clear H4 t6.
(* case 5.1.1: subst0 on left argument *)
Ty0Correct; IHT; IHTb1; Ty0Correct.
Ty0Correct; IHT; IHTb1; IHTTb; Ty0Correct.
EApply ty0_conv;
[ EApply ty0_bind | EApply ty0_bind | EApply pc3_fsubst0 ]; XEAuto.
-(* case 5.2: fsubst0_c *)
+(* case 5.2: fsubst0_fst *)
IHC; IHCb; Ty0Correct; EApply ty0_bind; XEAuto.
-(* case 5.3: fsubst0_b *)
+(* case 5.3: fsubst0_both *)
Subst0GenBase; Rewrite H4; Clear H4 t6.
(* case 5.3.1: subst0 on left argument *)
IHC; IHCb; Ty0Correct; Ty0Correct; IHCT; IHCTb1; Ty0Correct.
| EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]; XEAuto.
(* case 6: ty0_appl *)
Intros until 5; XElim H3; Intros.
-(* case 6.1: fsubst0_t *)
+(* case 6.1: fsubst0_snd *)
Subst0GenBase; Rewrite H3; Clear H3 c1 c2 t t1 t2 t3.
(* case 6.1.1: subst0 on left argument *)
Ty0Correct; Ty0GenBase; IHT; Ty0Correct.
Ty0Correct; Ty0GenBase; Move H after H10; Ty0Correct; IHT; Clear H2; IHT.
EApply ty0_conv;
[ EApply ty0_appl | EApply ty0_appl | EApply pc3_fsubst0 ]; XEAuto.
-(* case 6.2: fsubst0_c *)
+(* case 6.2: fsubst0_fst *)
IHC; Clear H2; IHC; EApply ty0_appl; XEAuto.
-(* case 6.3: fsubst0_b *)
+(* case 6.3: fsubst0_both *)
Subst0GenBase; Rewrite H3; Clear H3 c1 c2 t t1 t2 t3.
(* case 6.3.1: subst0 on left argument *)
IHC; Ty0Correct; Ty0GenBase; Clear H2; IHC; IHCT.
| EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]; XEAuto.
(* case 7: ty0_cast *)
Clear c1 t t1; Intros until 5; XElim H3; Intros; Clear c2 t3.
-(* case 7.1: fsubst0_t *)
+(* case 7.1: fsubst0_snd *)
Subst0GenBase; Rewrite H3; Clear H3 t4.
(* case 7.1.1: subst0 on left argument *)
IHT; EApply ty0_conv;
[ EApply ty0_conv; [ Idtac | Idtac | Apply pc3_s; EApply pc3_fsubst0 ]
| Idtac ]
| EApply pc3_fsubst0 ]; XEAuto.
-(* case 7.2: fsubst0_c *)
+(* case 7.2: fsubst0_fst *)
IHC; Clear H2; IHC; EApply ty0_cast; XEAuto.
-(* case 6.3: fsubst0_b *)
+(* case 6.3: fsubst0_both *)
Subst0GenBase; Rewrite H3; Clear H3 t4.
(* case 7.3.1: subst0 on left argument *)
IHC; IHCT; Clear H2; IHC.
End ty0_fsubst0.
Hints Resolve ty0_subst0 : ltlc.
-
projects / helm.git / commitdiff