From 50cfabb6b8136873a02f8fd1512f0b62f97e2639 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 15 Jul 2005 17:54:06 +0000 Subject: [PATCH] some reorganization and some corrections --- helm/coq-contribs/LAMBDA-TYPES/LambdaDelta.v | 14 ++- helm/coq-contribs/LAMBDA-TYPES/Make | 8 +- helm/coq-contribs/LAMBDA-TYPES/Makefile | 24 ++-- helm/coq-contribs/LAMBDA-TYPES/README | 2 +- helm/coq-contribs/LAMBDA-TYPES/base_types.v | 47 ++++++++ helm/coq-contribs/LAMBDA-TYPES/lift_defs.v | 106 +++++++++--------- helm/coq-contribs/LAMBDA-TYPES/lift_gen.v | 30 ++--- helm/coq-contribs/LAMBDA-TYPES/lift_props.v | 18 +-- helm/coq-contribs/LAMBDA-TYPES/lift_tlt.v | 14 +-- .../LAMBDA-TYPES/pr0_confluence.v | 92 +++++++-------- helm/coq-contribs/LAMBDA-TYPES/pr0_defs.v | 58 ++++++---- helm/coq-contribs/LAMBDA-TYPES/pr0_gen.v | 7 +- helm/coq-contribs/LAMBDA-TYPES/pr0_lift.v | 8 +- helm/coq-contribs/LAMBDA-TYPES/pr0_subst0.v | 14 +-- .../LAMBDA-TYPES/pr1_confluence.v | 12 +- helm/coq-contribs/LAMBDA-TYPES/subst0_defs.v | 35 +++--- helm/coq-contribs/LAMBDA-TYPES/subst0_gen.v | 18 +-- helm/coq-contribs/LAMBDA-TYPES/subst0_lift.v | 39 ++++--- .../coq-contribs/LAMBDA-TYPES/subst0_subst0.v | 4 +- helm/coq-contribs/LAMBDA-TYPES/subst0_tlt.v | 4 +- helm/coq-contribs/LAMBDA-TYPES/subst1_defs.v | 4 +- helm/coq-contribs/LAMBDA-TYPES/tlt_defs.v | 2 +- helm/coq-contribs/LAMBDA-TYPES/ty0_defs.v | 12 +- .../LAMBDA-TYPES/ty0_gen_context.v | 16 +-- helm/coq-contribs/LAMBDA-TYPES/ty0_lift.v | 8 +- helm/coq-contribs/LAMBDA-TYPES/ty0_sred.v | 81 +++++++------ helm/coq-contribs/LAMBDA-TYPES/ty0_subst0.v | 52 ++++----- 27 files changed, 390 insertions(+), 339 deletions(-) diff --git a/helm/coq-contribs/LAMBDA-TYPES/LambdaDelta.v b/helm/coq-contribs/LAMBDA-TYPES/LambdaDelta.v index ef5b4afbc..2af21f922 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/LambdaDelta.v +++ b/helm/coq-contribs/LAMBDA-TYPES/LambdaDelta.v @@ -1,3 +1,9 @@ +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. @@ -5,6 +11,8 @@ Require Export lift_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. @@ -16,10 +24,9 @@ Require Export subst1_gen. 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. @@ -28,6 +35,7 @@ Require Export pr0_confluence. 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. @@ -40,8 +48,6 @@ Require Export pr3_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. diff --git a/helm/coq-contribs/LAMBDA-TYPES/Make b/helm/coq-contribs/LAMBDA-TYPES/Make index 0a3e0514c..6a6d87836 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/Make +++ b/helm/coq-contribs/LAMBDA-TYPES/Make @@ -12,6 +12,8 @@ lift_defs.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 @@ -23,10 +25,9 @@ subst1_gen.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 @@ -35,6 +36,7 @@ pr0_confluence.v pr0_subst1.v pr1_defs.v pr1_confluence.v +cpr0_defs.v pr2_defs.v pr2_lift.v pr2_gen.v @@ -47,8 +49,6 @@ pr3_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 diff --git a/helm/coq-contribs/LAMBDA-TYPES/Makefile b/helm/coq-contribs/LAMBDA-TYPES/Makefile index b3936376b..76c27f9e2 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/Makefile +++ b/helm/coq-contribs/LAMBDA-TYPES/Makefile @@ -75,6 +75,8 @@ VFILES=base_tactics.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\ @@ -86,10 +88,9 @@ VFILES=base_tactics.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\ @@ -98,6 +99,7 @@ VFILES=base_tactics.v\ pr0_subst1.v\ pr1_defs.v\ pr1_confluence.v\ + cpr0_defs.v\ pr2_defs.v\ pr2_lift.v\ pr2_gen.v\ @@ -110,8 +112,6 @@ VFILES=base_tactics.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\ @@ -146,6 +146,8 @@ all: base_tactics.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\ @@ -157,10 +159,9 @@ all: base_tactics.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\ @@ -169,6 +170,7 @@ all: base_tactics.vo\ pr0_subst1.vo\ pr1_defs.vo\ pr1_confluence.vo\ + cpr0_defs.vo\ pr2_defs.vo\ pr2_lift.vo\ pr2_gen.vo\ @@ -181,8 +183,6 @@ all: base_tactics.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\ @@ -227,6 +227,8 @@ xml:: .xml_time_stamp lift_gen.vo\ lift_props.vo\ lift_tlt.vo\ + drop_defs.vo\ + drop_props.vo\ subst0_defs.vo\ subst0_gen.vo\ subst0_lift.vo\ @@ -238,10 +240,9 @@ xml:: .xml_time_stamp 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\ @@ -250,6 +251,7 @@ xml:: .xml_time_stamp pr0_subst1.vo\ pr1_defs.vo\ pr1_confluence.vo\ + cpr0_defs.vo\ pr2_defs.vo\ pr2_lift.vo\ pr2_gen.vo\ @@ -262,8 +264,6 @@ xml:: .xml_time_stamp 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\ diff --git a/helm/coq-contribs/LAMBDA-TYPES/README b/helm/coq-contribs/LAMBDA-TYPES/README index d35c2dd39..6a5bf7e0f 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/README +++ b/helm/coq-contribs/LAMBDA-TYPES/README @@ -58,4 +58,4 @@ Further information on this contribution: The latest version of this development is maintained in the CVS repository of the HELM project 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 diff --git a/helm/coq-contribs/LAMBDA-TYPES/base_types.v b/helm/coq-contribs/LAMBDA-TYPES/base_types.v index 0b1c870f3..f24ef915a 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/base_types.v +++ b/helm/coq-contribs/LAMBDA-TYPES/base_types.v @@ -73,6 +73,20 @@ Grammar constr constr10 := [ "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 := @@ -143,6 +157,20 @@ Grammar constr constr10 := [ "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 := @@ -157,3 +185,22 @@ Grammar constr constr10 := [ "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. + diff --git a/helm/coq-contribs/LAMBDA-TYPES/lift_defs.v b/helm/coq-contribs/LAMBDA-TYPES/lift_defs.v index 3185aad6f..1f61d9fad 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/lift_defs.v +++ b/helm/coq-contribs/LAMBDA-TYPES/lift_defs.v @@ -2,16 +2,16 @@ 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. (********************************************************) @@ -19,14 +19,14 @@ Require Export terms_defs. 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. @@ -52,7 +52,7 @@ Require Export terms_defs. 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). @@ -67,68 +67,68 @@ Require Export terms_defs. 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. @@ -143,12 +143,12 @@ Require Export terms_defs. 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. @@ -163,12 +163,12 @@ Require Export terms_defs. 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. @@ -181,22 +181,22 @@ Require Export terms_defs. | [ 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 ]; @@ -211,20 +211,20 @@ Require Export terms_defs. 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 *) @@ -233,4 +233,4 @@ Require Export terms_defs. End lift_props. - Hints Resolve lift_r lift_bref_gt : ltlc. + Hints Resolve lift_r lift_lref_gt : ltlc. diff --git a/helm/coq-contribs/LAMBDA-TYPES/lift_gen.v b/helm/coq-contribs/LAMBDA-TYPES/lift_gen.v index 14914d4cb..63b74709d 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/lift_gen.v +++ b/helm/coq-contribs/LAMBDA-TYPES/lift_gen.v @@ -11,26 +11,21 @@ Require lift_defs. | [ 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. @@ -51,8 +46,6 @@ Require lift_defs. 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 *) @@ -61,30 +54,27 @@ Require lift_defs. (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 ]. @@ -92,7 +82,7 @@ Require lift_defs. 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 *) diff --git a/helm/coq-contribs/LAMBDA-TYPES/lift_props.v b/helm/coq-contribs/LAMBDA-TYPES/lift_props.v index 5d5d7d0a9..366ad999b 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/lift_props.v +++ b/helm/coq-contribs/LAMBDA-TYPES/lift_props.v @@ -9,12 +9,12 @@ Require lift_defs. 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. @@ -24,18 +24,18 @@ Require lift_defs. 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. diff --git a/helm/coq-contribs/LAMBDA-TYPES/lift_tlt.v b/helm/coq-contribs/LAMBDA-TYPES/lift_tlt.v index 3a9cb3fce..7319f3264 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/lift_tlt.v +++ b/helm/coq-contribs/LAMBDA-TYPES/lift_tlt.v @@ -17,12 +17,12 @@ Require lift_defs. 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. @@ -48,12 +48,12 @@ Require lift_defs. 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 *) @@ -84,6 +84,4 @@ Require lift_defs. Hints Resolve lift_tlt_dx : ltlc. -(*#* #start file *) - (*#* #single *) diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr0_confluence.v b/helm/coq-contribs/LAMBDA-TYPES/pr0_confluence.v index b107ac2a9..c23d6743f 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/pr0_confluence.v +++ b/helm/coq-contribs/LAMBDA-TYPES/pr0_confluence.v @@ -47,39 +47,39 @@ Require pr0_subst0. 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. @@ -87,14 +87,14 @@ Require pr0_subst0. 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. @@ -108,14 +108,14 @@ Require pr0_subst0. 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. @@ -141,25 +141,25 @@ Require pr0_subst0. (* 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. diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr0_defs.v b/helm/coq-contribs/LAMBDA-TYPES/pr0_defs.v index 3c7a96bbe..a2180b9d1 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/pr0_defs.v +++ b/helm/coq-contribs/LAMBDA-TYPES/pr0_defs.v @@ -1,37 +1,43 @@ -(*#* #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. @@ -74,13 +80,17 @@ Require Export subst0_defs. 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) |- ? ] -> diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr0_gen.v b/helm/coq-contribs/LAMBDA-TYPES/pr0_gen.v index 0b634e59c..bfe189586 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/pr0_gen.v +++ b/helm/coq-contribs/LAMBDA-TYPES/pr0_gen.v @@ -44,16 +44,11 @@ Require pr0_lift. 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. @@ -66,7 +61,7 @@ Require pr0_lift. 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. diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr0_lift.v b/helm/coq-contribs/LAMBDA-TYPES/pr0_lift.v index f3dc1c518..b6d9ba247 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/pr0_lift.v +++ b/helm/coq-contribs/LAMBDA-TYPES/pr0_lift.v @@ -2,9 +2,11 @@ Require lift_props. 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" *) @@ -13,8 +15,6 @@ Require pr0_defs. 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. @@ -22,7 +22,7 @@ Require pr0_defs. 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. diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr0_subst0.v b/helm/coq-contribs/LAMBDA-TYPES/pr0_subst0.v index ace613d6e..46a137e18 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/pr0_subst0.v +++ b/helm/coq-contribs/LAMBDA-TYPES/pr0_subst0.v @@ -41,8 +41,8 @@ Require pr0_lift. (*#* #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) -> @@ -60,7 +60,7 @@ Require pr0_lift. (* 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 *) @@ -95,10 +95,10 @@ Require pr0_lift. 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 ]; diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr1_confluence.v b/helm/coq-contribs/LAMBDA-TYPES/pr1_confluence.v index 222a08cea..fac076d31 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/pr1_confluence.v +++ b/helm/coq-contribs/LAMBDA-TYPES/pr1_confluence.v @@ -1,3 +1,5 @@ +(*#* #stop file *) + Require pr0_confluence. Require pr1_defs. @@ -11,9 +13,6 @@ 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. @@ -23,16 +22,11 @@ Require pr1_defs. 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. @@ -58,7 +52,5 @@ Require pr1_defs. XElim H1; Intros | _ -> Pr0Confluence. -(*#* #start file *) - (*#* #single *) diff --git a/helm/coq-contribs/LAMBDA-TYPES/subst0_defs.v b/helm/coq-contribs/LAMBDA-TYPES/subst0_defs.v index 5c9c2e5c8..d99a405db 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/subst0_defs.v +++ b/helm/coq-contribs/LAMBDA-TYPES/subst0_defs.v @@ -1,16 +1,24 @@ -(*#* #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. @@ -21,7 +29,7 @@ Require Export lift_defs. 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. @@ -46,10 +54,9 @@ Require Export lift_defs. 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. - diff --git a/helm/coq-contribs/LAMBDA-TYPES/subst0_gen.v b/helm/coq-contribs/LAMBDA-TYPES/subst0_gen.v index 7a0acfeb6..d46ca3555 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/subst0_gen.v +++ b/helm/coq-contribs/LAMBDA-TYPES/subst0_gen.v @@ -17,14 +17,14 @@ Require subst0_defs. 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 *) @@ -49,14 +49,14 @@ Require subst0_defs. 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 *) @@ -87,14 +87,14 @@ Require subst0_defs. 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 ]. diff --git a/helm/coq-contribs/LAMBDA-TYPES/subst0_lift.v b/helm/coq-contribs/LAMBDA-TYPES/subst0_lift.v index d4ce7412f..caabbe0b7 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/subst0_lift.v +++ b/helm/coq-contribs/LAMBDA-TYPES/subst0_lift.v @@ -5,12 +5,12 @@ Require subst0_defs. 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 *) @@ -22,12 +22,12 @@ Require subst0_defs. 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 *) @@ -38,12 +38,19 @@ Require subst0_defs. 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. diff --git a/helm/coq-contribs/LAMBDA-TYPES/subst0_subst0.v b/helm/coq-contribs/LAMBDA-TYPES/subst0_subst0.v index e092e23e7..9f9b6da86 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/subst0_subst0.v +++ b/helm/coq-contribs/LAMBDA-TYPES/subst0_subst0.v @@ -21,7 +21,7 @@ Require subst0_lift. (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. @@ -35,7 +35,7 @@ Require subst0_lift. (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. diff --git a/helm/coq-contribs/LAMBDA-TYPES/subst0_tlt.v b/helm/coq-contribs/LAMBDA-TYPES/subst0_tlt.v index 87bf9c8c0..b5fef207b 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/subst0_tlt.v +++ b/helm/coq-contribs/LAMBDA-TYPES/subst0_tlt.v @@ -11,7 +11,7 @@ Require subst0_defs. (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 ]. @@ -26,7 +26,7 @@ Require subst0_defs. (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; diff --git a/helm/coq-contribs/LAMBDA-TYPES/subst1_defs.v b/helm/coq-contribs/LAMBDA-TYPES/subst1_defs.v index d1e091348..93e0d2ecf 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/subst1_defs.v +++ b/helm/coq-contribs/LAMBDA-TYPES/subst1_defs.v @@ -32,8 +32,8 @@ Require Export subst0_defs. 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. diff --git a/helm/coq-contribs/LAMBDA-TYPES/tlt_defs.v b/helm/coq-contribs/LAMBDA-TYPES/tlt_defs.v index 689477a39..eb3f6fb27 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/tlt_defs.v +++ b/helm/coq-contribs/LAMBDA-TYPES/tlt_defs.v @@ -7,7 +7,7 @@ Require Export terms_defs. 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) => diff --git a/helm/coq-contribs/LAMBDA-TYPES/ty0_defs.v b/helm/coq-contribs/LAMBDA-TYPES/ty0_defs.v index d9b302aca..e2a787624 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/ty0_defs.v +++ b/helm/coq-contribs/LAMBDA-TYPES/ty0_defs.v @@ -30,11 +30,11 @@ Require Export pc3_defs. | 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) -> @@ -87,7 +87,7 @@ Require Export pc3_defs. (*#* #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) @@ -99,7 +99,7 @@ Require Export pc3_defs. (*#* #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. @@ -218,8 +218,8 @@ Require Export pc3_defs. 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 ]; diff --git a/helm/coq-contribs/LAMBDA-TYPES/ty0_gen_context.v b/helm/coq-contribs/LAMBDA-TYPES/ty0_gen_context.v index bf9217602..f04a6aa5e 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/ty0_gen_context.v +++ b/helm/coq-contribs/LAMBDA-TYPES/ty0_gen_context.v @@ -53,7 +53,7 @@ Require ty0_lift. 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. @@ -67,7 +67,7 @@ Require ty0_lift. 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. @@ -84,7 +84,7 @@ Require ty0_lift. 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 *) @@ -92,7 +92,7 @@ Require ty0_lift. 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. @@ -149,7 +149,7 @@ Require ty0_lift. 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 *) @@ -157,7 +157,7 @@ Require ty0_lift. 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. @@ -171,7 +171,7 @@ Require ty0_lift. 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 *) @@ -179,7 +179,7 @@ Require ty0_lift. 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. diff --git a/helm/coq-contribs/LAMBDA-TYPES/ty0_lift.v b/helm/coq-contribs/LAMBDA-TYPES/ty0_lift.v index 107a4ca89..ebe6bfcc7 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/ty0_lift.v +++ b/helm/coq-contribs/LAMBDA-TYPES/ty0_lift.v @@ -26,11 +26,11 @@ Require ty0_defs. (* 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 *) @@ -38,11 +38,11 @@ Require ty0_defs. (* 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 *) diff --git a/helm/coq-contribs/LAMBDA-TYPES/ty0_sred.v b/helm/coq-contribs/LAMBDA-TYPES/ty0_sred.v index dc185a95a..62aa5c399 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/ty0_sred.v +++ b/helm/coq-contribs/LAMBDA-TYPES/ty0_sred.v @@ -4,7 +4,6 @@ Require csubst1_defs. Require pr0_lift. Require pr0_subst1. Require cpr0_defs. -Require cpr0_props. Require pc3_props. Require pc3_gen. Require ty0_defs. @@ -96,66 +95,66 @@ Require csub0_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. @@ -164,7 +163,7 @@ Require csub0_defs. | 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. @@ -180,18 +179,18 @@ Require csub0_defs. | 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. @@ -199,24 +198,24 @@ Require csub0_defs. 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 *) @@ -224,16 +223,16 @@ Require csub0_defs. (*#* #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. diff --git a/helm/coq-contribs/LAMBDA-TYPES/ty0_subst0.v b/helm/coq-contribs/LAMBDA-TYPES/ty0_subst0.v index 3e4703200..1da24f500 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/ty0_subst0.v +++ b/helm/coq-contribs/LAMBDA-TYPES/ty0_subst0.v @@ -1,5 +1,6 @@ Require drop_props. Require csubst0_defs. +Require fsubst0_defs. Require pc3_props. Require pc3_subst0. Require ty0_defs. @@ -128,36 +129,36 @@ Require ty0_props. 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. @@ -171,26 +172,26 @@ Require ty0_props. 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. @@ -207,11 +208,11 @@ Require ty0_props. ]; 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. @@ -223,9 +224,9 @@ Require ty0_props. 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. @@ -241,7 +242,7 @@ Require ty0_props. | 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. @@ -253,9 +254,9 @@ Require ty0_props. 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. @@ -271,7 +272,7 @@ Require ty0_props. | 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; @@ -290,9 +291,9 @@ Require ty0_props. [ 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. @@ -330,4 +331,3 @@ Require ty0_props. End ty0_fsubst0. Hints Resolve ty0_subst0 : ltlc. - -- 2.39.2