From a8052b7482d5573eca2776ea11cb7a4b06236fbd Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 15 Jul 2005 18:10:14 +0000 Subject: [PATCH] some reorganization and some corrections --- helm/coq-contribs/LAMBDA-TYPES/.depend | 24 +- .../coq-contribs/LAMBDA-TYPES/contexts_defs.v | 5 + helm/coq-contribs/LAMBDA-TYPES/cpr0_defs.v | 85 +++++- helm/coq-contribs/LAMBDA-TYPES/csub0_defs.v | 2 +- helm/coq-contribs/LAMBDA-TYPES/csubst0_defs.v | 45 ++-- helm/coq-contribs/LAMBDA-TYPES/drop_defs.v | 16 +- helm/coq-contribs/LAMBDA-TYPES/drop_props.v | 35 +-- helm/coq-contribs/LAMBDA-TYPES/pc3_defs.v | 16 +- helm/coq-contribs/LAMBDA-TYPES/pc3_gen.v | 73 +++--- helm/coq-contribs/LAMBDA-TYPES/pc3_props.v | 105 ++++---- helm/coq-contribs/LAMBDA-TYPES/pc3_subst0.v | 104 ++++---- .../LAMBDA-TYPES/pr2_confluence.v | 57 ++--- helm/coq-contribs/LAMBDA-TYPES/pr2_defs.v | 169 ++++++------ helm/coq-contribs/LAMBDA-TYPES/pr2_gen.v | 77 +++--- .../LAMBDA-TYPES/pr2_gen_context.v | 27 +- helm/coq-contribs/LAMBDA-TYPES/pr2_lift.v | 7 +- helm/coq-contribs/LAMBDA-TYPES/pr2_subst1.v | 16 +- .../LAMBDA-TYPES/pr3_confluence.v | 15 +- helm/coq-contribs/LAMBDA-TYPES/pr3_defs.v | 169 ++++++++++-- helm/coq-contribs/LAMBDA-TYPES/pr3_gen.v | 242 +++++++----------- .../LAMBDA-TYPES/pr3_gen_context.v | 4 +- helm/coq-contribs/LAMBDA-TYPES/pr3_subst1.v | 1 - helm/coq-contribs/LAMBDA-TYPES/terms_defs.v | 7 +- 23 files changed, 728 insertions(+), 573 deletions(-) diff --git a/helm/coq-contribs/LAMBDA-TYPES/.depend b/helm/coq-contribs/LAMBDA-TYPES/.depend index 881798e10..4f954d495 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/.depend +++ b/helm/coq-contribs/LAMBDA-TYPES/.depend @@ -1,32 +1,31 @@ -LambdaDelta.vo: LambdaDelta.v terms_defs.vo tlt_defs.vo contexts_defs.vo lift_defs.vo lift_gen.vo lift_props.vo lift_tlt.vo subst0_defs.vo subst0_gen.vo subst0_lift.vo subst0_subst0.vo subst0_confluence.vo subst0_tlt.vo subst1_defs.vo subst1_gen.vo subst1_lift.vo subst1_subst1.vo subst1_confluence.vo drop_defs.vo drop_props.vo csubst0_defs.vo csubst1_defs.vo pr0_defs.vo pr0_lift.vo pr0_gen.vo pr0_subst0.vo pr0_confluence.vo pr0_subst1.vo pr1_defs.vo pr1_confluence.vo pr2_defs.vo pr2_lift.vo pr2_gen.vo pr2_confluence.vo pr2_subst1.vo pr2_gen_context.vo pr3_defs.vo pr3_props.vo pr3_gen.vo pr3_confluence.vo pr3_subst1.vo pr3_gen_context.vo cpr0_defs.vo cpr0_props.vo pc1_defs.vo pc3_defs.vo pc3_props.vo pc3_gen.vo pc3_subst0.vo pc3_gen_context.vo ty0_defs.vo ty0_lift.vo ty0_props.vo ty0_subst0.vo ty0_gen_context.vo csub0_defs.vo ty0_sred.vo ty0_sred_props.vo +LambdaDelta.vo: LambdaDelta.v base_tactics.vo base_hints.vo base_types.vo base_blt.vo base_rewrite.vo Base.vo terms_defs.vo tlt_defs.vo contexts_defs.vo lift_defs.vo lift_gen.vo lift_props.vo lift_tlt.vo drop_defs.vo drop_props.vo subst0_defs.vo subst0_gen.vo subst0_lift.vo subst0_subst0.vo subst0_confluence.vo subst0_tlt.vo subst1_defs.vo subst1_gen.vo subst1_lift.vo subst1_subst1.vo subst1_confluence.vo csubst0_defs.vo csubst1_defs.vo fsubst0_defs.vo pr0_defs.vo pr0_lift.vo pr0_gen.vo pr0_subst0.vo pr0_confluence.vo pr0_subst1.vo pr1_defs.vo pr1_confluence.vo cpr0_defs.vo pr2_defs.vo pr2_lift.vo pr2_gen.vo pr2_confluence.vo pr2_subst1.vo pr2_gen_context.vo pr3_defs.vo pr3_props.vo pr3_gen.vo pr3_confluence.vo pr3_subst1.vo pr3_gen_context.vo pc1_defs.vo pc3_defs.vo pc3_props.vo pc3_gen.vo pc3_subst0.vo pc3_gen_context.vo ty0_defs.vo ty0_lift.vo ty0_props.vo ty0_subst0.vo ty0_gen_context.vo csub0_defs.vo ty0_sred.vo ty0_sred_props.vo ty0_sred_props.vo: ty0_sred_props.v lift_props.vo drop_props.vo pc3_props.vo pc3_gen.vo ty0_defs.vo ty0_props.vo ty0_sred.vo -ty0_sred.vo: ty0_sred.v lift_gen.vo subst1_gen.vo csubst1_defs.vo pr0_lift.vo pr0_subst1.vo cpr0_defs.vo cpr0_props.vo pc3_props.vo pc3_gen.vo ty0_defs.vo ty0_lift.vo ty0_props.vo ty0_subst0.vo ty0_gen_context.vo csub0_defs.vo +ty0_sred.vo: ty0_sred.v lift_gen.vo subst1_gen.vo csubst1_defs.vo pr0_lift.vo pr0_subst1.vo cpr0_defs.vo pc3_props.vo pc3_gen.vo ty0_defs.vo ty0_lift.vo ty0_props.vo ty0_subst0.vo ty0_gen_context.vo csub0_defs.vo csub0_defs.vo: csub0_defs.v ty0_defs.vo ty0_gen_context.vo: ty0_gen_context.v lift_gen.vo lift_props.vo subst1_defs.vo subst1_lift.vo subst1_confluence.vo drop_props.vo csubst1_defs.vo pc3_gen.vo pc3_gen_context.vo ty0_defs.vo ty0_lift.vo -ty0_subst0.vo: ty0_subst0.v drop_props.vo csubst0_defs.vo pc3_props.vo pc3_subst0.vo ty0_defs.vo ty0_lift.vo ty0_props.vo +ty0_subst0.vo: ty0_subst0.v drop_props.vo csubst0_defs.vo fsubst0_defs.vo pc3_props.vo pc3_subst0.vo ty0_defs.vo ty0_lift.vo ty0_props.vo ty0_props.vo: ty0_props.v drop_props.vo pc3_props.vo ty0_defs.vo ty0_lift.vo ty0_lift.vo: ty0_lift.v lift_props.vo drop_props.vo pc3_props.vo ty0_defs.vo ty0_defs.vo: ty0_defs.v pc3_defs.vo pc3_gen_context.vo: pc3_gen_context.v subst1_confluence.vo csubst1_defs.vo pr3_gen_context.vo pc3_defs.vo pc3_props.vo -pc3_subst0.vo: pc3_subst0.v subst0_subst0.vo csubst0_defs.vo pr0_subst0.vo pc3_defs.vo +pc3_subst0.vo: pc3_subst0.v subst0_subst0.vo fsubst0_defs.vo pr0_subst0.vo pc3_defs.vo pc3_gen.vo: pc3_gen.v lift_gen.vo pr3_props.vo pr3_gen.vo pc3_defs.vo pc3_props.vo -pc3_props.vo: pc3_props.v subst0_subst0.vo pr0_subst0.vo pr3_defs.vo pr3_props.vo pr3_confluence.vo cpr0_defs.vo cpr0_props.vo pc3_defs.vo +pc3_props.vo: pc3_props.v subst0_subst0.vo pr0_subst0.vo cpr0_defs.vo pr3_defs.vo pr3_props.vo pr3_confluence.vo pc3_defs.vo pc3_defs.vo: pc3_defs.v pr2_defs.vo pr3_defs.vo pc1_defs.vo pc1_defs.vo: pc1_defs.v pr0_defs.vo -cpr0_props.vo: cpr0_props.v pr0_subst0.vo pr3_defs.vo pr3_props.vo cpr0_defs.vo -cpr0_defs.vo: cpr0_defs.v contexts_defs.vo pr0_defs.vo pr3_gen_context.vo: pr3_gen_context.v csubst1_defs.vo pr2_gen_context.vo pr3_defs.vo pr3_subst1.vo: pr3_subst1.v subst1_defs.vo pr2_subst1.vo pr3_defs.vo pr3_confluence.vo: pr3_confluence.v pr2_confluence.vo pr3_defs.vo pr3_gen.vo: pr3_gen.v pr2_gen.vo pr3_defs.vo pr3_props.vo -pr3_props.vo: pr3_props.v subst0_subst0.vo pr0_subst0.vo pr2_lift.vo pr3_defs.vo +pr3_props.vo: pr3_props.v subst0_subst0.vo pr0_subst0.vo cpr0_defs.vo pr2_lift.vo pr2_gen.vo pr3_defs.vo pr3_defs.vo: pr3_defs.v pr1_defs.vo pr2_defs.vo -pr2_gen_context.vo: pr2_gen_context.v drop_props.vo subst1_gen.vo subst1_subst1.vo subst1_confluence.vo csubst1_defs.vo pr0_gen.vo pr0_subst1.vo pr2_defs.vo pr2_subst1.vo +pr2_gen_context.vo: pr2_gen_context.v drop_props.vo subst1_gen.vo subst1_subst1.vo subst1_confluence.vo csubst1_defs.vo pr0_gen.vo pr0_subst1.vo pr2_defs.vo pr2_gen.vo pr2_subst1.vo pr2_subst1.vo: pr2_subst1.v subst1_defs.vo subst1_confluence.vo drop_props.vo pr0_subst1.vo pr2_defs.vo pr2_confluence.vo: pr2_confluence.v subst0_confluence.vo drop_props.vo pr0_subst0.vo pr0_confluence.vo pr2_defs.vo -pr2_gen.vo: pr2_gen.v subst0_gen.vo drop_props.vo pr0_gen.vo pr2_defs.vo +pr2_gen.vo: pr2_gen.v subst0_gen.vo subst0_lift.vo drop_props.vo pr0_gen.vo pr0_subst0.vo pr2_defs.vo pr2_lift.vo: pr2_lift.v subst0_lift.vo drop_props.vo pr0_lift.vo pr2_defs.vo pr2_defs.vo: pr2_defs.v drop_defs.vo pr0_defs.vo +cpr0_defs.vo: cpr0_defs.v contexts_defs.vo drop_defs.vo pr0_defs.vo pr1_confluence.vo: pr1_confluence.v pr0_confluence.vo pr1_defs.vo pr1_defs.vo: pr1_defs.v pr0_defs.vo pr0_subst1.vo: pr0_subst1.v subst1_defs.vo pr0_defs.vo pr0_subst0.vo @@ -35,10 +34,9 @@ pr0_subst0.vo: pr0_subst0.v subst0_gen.vo subst0_lift.vo subst0_subst0.vo subst0 pr0_gen.vo: pr0_gen.v lift_gen.vo lift_props.vo subst0_gen.vo pr0_defs.vo pr0_lift.vo pr0_lift.vo: pr0_lift.v lift_props.vo subst0_lift.vo pr0_defs.vo pr0_defs.vo: pr0_defs.v subst0_defs.vo +fsubst0_defs.vo: fsubst0_defs.v subst0_defs.vo csubst0_defs.vo csubst1_defs.vo: csubst1_defs.v subst1_defs.vo csubst0_defs.vo csubst0_defs.vo: csubst0_defs.v contexts_defs.vo subst0_defs.vo drop_defs.vo -drop_props.vo: drop_props.v lift_gen.vo drop_defs.vo -drop_defs.vo: drop_defs.v contexts_defs.vo lift_defs.vo subst1_confluence.vo: subst1_confluence.v lift_gen.vo subst0_gen.vo subst0_confluence.vo subst1_defs.vo subst1_gen.vo subst1_subst1.vo: subst1_subst1.v subst0_subst0.vo subst1_defs.vo subst1_lift.vo: subst1_lift.v lift_props.vo subst0_lift.vo subst1_defs.vo @@ -50,6 +48,8 @@ subst0_subst0.vo: subst0_subst0.v subst0_defs.vo subst0_gen.vo subst0_lift.vo subst0_lift.vo: subst0_lift.v lift_props.vo subst0_defs.vo subst0_gen.vo: subst0_gen.v lift_props.vo subst0_defs.vo subst0_defs.vo: subst0_defs.v lift_defs.vo +drop_props.vo: drop_props.v lift_gen.vo drop_defs.vo +drop_defs.vo: drop_defs.v contexts_defs.vo lift_defs.vo lift_tlt.vo: lift_tlt.v tlt_defs.vo lift_defs.vo lift_props.vo: lift_props.v lift_defs.vo lift_gen.vo: lift_gen.v lift_defs.vo diff --git a/helm/coq-contribs/LAMBDA-TYPES/contexts_defs.v b/helm/coq-contribs/LAMBDA-TYPES/contexts_defs.v index ec1f9e758..63373a401 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/contexts_defs.v +++ b/helm/coq-contribs/LAMBDA-TYPES/contexts_defs.v @@ -7,6 +7,11 @@ Require Export terms_defs. Hint f3CKT : ltlc := Resolve (f_equal3 C K T). + Tactic Definition CGenBase := + Match Context With + | [ H: (CTail ? ? ?) = (CTail ? ? ?) |- ? ] -> Inversion H; Clear H + | _ -> TGenBase. + Definition r: K -> nat -> nat := [k;i] Cases k of | (Bind _) => i | (Flat _) => (S i) diff --git a/helm/coq-contribs/LAMBDA-TYPES/cpr0_defs.v b/helm/coq-contribs/LAMBDA-TYPES/cpr0_defs.v index ce6faccba..5434debd4 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/cpr0_defs.v +++ b/helm/coq-contribs/LAMBDA-TYPES/cpr0_defs.v @@ -1,11 +1,90 @@ -(*#* #stop file *) - Require Export contexts_defs. +Require Export drop_defs. Require Export pr0_defs. +(*#* #caption "current axioms for the relation $\\CprZ{}{}$", + "reflexivity", "compaibility" +*) +(*#* #cap #cap c, c1, c2 #alpha u1 in V1, u2 in V2, k in z *) + Inductive cpr0 : C -> C -> Prop := | cpr0_refl : (c:?) (cpr0 c c) - | cpr0_cont : (c1,c2:?) (cpr0 c1 c2) -> (u1,u2:?) (pr0 u1 u2) -> + | cpr0_comp : (c1,c2:?) (cpr0 c1 c2) -> (u1,u2:?) (pr0 u1 u2) -> (k:?) (cpr0 (CTail c1 k u1) (CTail c2 k u2)). +(*#* #stop file *) + Hint cpr0 : ltlc := Constructors cpr0. + + Section cpr0_drop. (******************************************************) + + Theorem cpr0_drop : (c1,c2:?) (cpr0 c1 c2) -> (h:?; e1:?; u1:?; k:?) + (drop h (0) c1 (CTail e1 k u1)) -> + (EX e2 u2 | (drop h (0) c2 (CTail e2 k u2)) & + (cpr0 e1 e2) & (pr0 u1 u2) + ). + Intros until 1; XElim H. +(* case 1 : cpr0_refl *) + XEAuto. +(* case 2 : cpr0_comp *) + XElim h. +(* case 2.1 : h = 0 *) + Intros; DropGenBase. + Inversion H2; Rewrite H6 in H1; Rewrite H4 in H; XEAuto. +(* case 2.2 : h > 0 *) + XElim k; Intros; DropGenBase. +(* case 2.2.1 : Bind *) + LApply (H0 n e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ]. + XElim H0; XEAuto. +(* case 2.2.2 : Flat *) + LApply (H0 (S n) e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ]. + XElim H0; XEAuto. + Qed. + + Theorem cpr0_drop_back : (c1,c2:?) (cpr0 c2 c1) -> (h:?; e1:?; u1:?; k:?) + (drop h (0) c1 (CTail e1 k u1)) -> + (EX e2 u2 | (drop h (0) c2 (CTail e2 k u2)) & + (cpr0 e2 e1) & (pr0 u2 u1) + ). + Intros until 1; XElim H. +(* case 1 : cpr0_refl *) + XEAuto. +(* case 2 : cpr0_comp *) + XElim h. +(* case 2.1 : h = 0 *) + Intros; DropGenBase. + Inversion H2; Rewrite H6 in H1; Rewrite H4 in H; XEAuto. +(* case 2.2 : h > 0 *) + XElim k; Intros; DropGenBase. +(* case 2.2.1 : Bind *) + LApply (H0 n e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ]. + XElim H0; XEAuto. +(* case 2.2.2 : Flat *) + LApply (H0 (S n) e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ]. + XElim H0; XEAuto. + Qed. + + End cpr0_drop. + + Tactic Definition Cpr0Drop := + Match Context With + | [ _: (drop ?1 (0) ?2 (CTail ?3 ?4 ?5)); + _: (cpr0 ?2 ?6) |- ? ] -> + LApply (cpr0_drop ?2 ?6); [ Intros H_x | XAuto ]; + LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ]; + XElim H_x; Intros + | [ _: (drop ?1 (0) ?2 (CTail ?3 ?4 ?5)); + _: (cpr0 ?6 ?2) |- ? ] -> + LApply (cpr0_drop_back ?2 ?6); [ Intros H_x | XAuto ]; + LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ]; + XElim H_x; Intros + | [ _: (drop ?1 (0) (CTail ?2 ?7 ?8) (CTail ?3 ?4 ?5)); + _: (cpr0 ?2 ?6) |- ? ] -> + LApply (cpr0_drop (CTail ?2 ?7 ?8) (CTail ?6 ?7 ?8)); [ Intros H_x | XAuto ]; + LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ]; + XElim H_x; Intros + | [ _: (drop ?1 (0) (CTail ?2 ?7 ?8) (CTail ?3 ?4 ?5)); + _: (cpr0 ?6 ?2) |- ? ] -> + LApply (cpr0_drop_back (CTail ?2 ?7 ?8) (CTail ?6 ?7 ?8)); [ Intros H_x | XAuto ]; + LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ]; + XElim H_x; Intros. diff --git a/helm/coq-contribs/LAMBDA-TYPES/csub0_defs.v b/helm/coq-contribs/LAMBDA-TYPES/csub0_defs.v index 7aa8a2c9b..e96bef4a7 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/csub0_defs.v +++ b/helm/coq-contribs/LAMBDA-TYPES/csub0_defs.v @@ -118,7 +118,7 @@ Require Export ty0_defs. Theorem csub0_pr2 : (g:?; c1:?; t1,t2:?) (pr2 c1 t1 t2) -> (c2:?) (csub0 g c1 c2) -> (pr2 c2 t1 t2). Intros until 1; XElim H; Intros. -(* case 1 : pr2_pr0 *) +(* case 1 : pr2_free *) XAuto. (* case 2 : pr2_delta *) CSub0Drop; XEAuto. diff --git a/helm/coq-contribs/LAMBDA-TYPES/csubst0_defs.v b/helm/coq-contribs/LAMBDA-TYPES/csubst0_defs.v index a452fd3f0..8d1ff31dc 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/csubst0_defs.v +++ b/helm/coq-contribs/LAMBDA-TYPES/csubst0_defs.v @@ -1,27 +1,26 @@ -(*#* #stop file *) - Require Export contexts_defs. Require Export subst0_defs. Require Export drop_defs. +(*#* #caption "current axioms for strict substitution in contexts", + "substituted tail item: second operand", + "substituted tail item: first operand", + "substituted tail item: both operands" +*) +(*#* #cap #cap c, c1, c2 #alpha v in W, u in V, u1 in V1, u2 in V2, k in z, r in q *) + Inductive csubst0 : nat -> T -> C -> C -> Prop := - | csubst0_fst : (k:?; i:?; u,v,w:?) (subst0 (r k i) v u w) -> (c:?) - (csubst0 (S i) v (CTail c k u) (CTail c k w)) - | csubst0_snd : (k:?; i:?; c1,c2:?; v:?) (csubst0 (r k i) v c1 c2) -> + | csubst0_snd : (k:?; i:?; v,u1,u2:?) (subst0 (r k i) v u1 u2) -> (c:?) + (csubst0 (S i) v (CTail c k u1) (CTail c k u2)) + | csubst0_fst : (k:?; i:?; c1,c2:?; v:?) (csubst0 (r k i) v c1 c2) -> (u:?) (csubst0 (S i) v (CTail c1 k u) (CTail c2 k u)) - | csubst0_both : (k:?; i:?; u,v,w:?) (subst0 (r k i) v u w) -> + | csubst0_both : (k:?; i:?; v,u1,u2:?) (subst0 (r k i) v u1 u2) -> (c1,c2:?) (csubst0 (r k i) v c1 c2) -> - (csubst0 (S i) v (CTail c1 k u) (CTail c2 k w)). + (csubst0 (S i) v (CTail c1 k u1) (CTail c2 k u2)). - Hint csubst0 : ltlc := Constructors csubst0. - - Inductive fsubst0 [i:nat; v:T; c1:C; t1:T] : C -> T -> Prop := - | fsubst0_t : (t2:?) (subst0 i v t1 t2) -> (fsubst0 i v c1 t1 c1 t2) - | fsubst0_c : (c2:?) (csubst0 i v c1 c2) -> (fsubst0 i v c1 t1 c2 t1) - | fsubst0_b : (t2:?) (subst0 i v t1 t2) -> - (c2:?) (csubst0 i v c1 c2) -> (fsubst0 i v c1 t1 c2 t2). +(*#* #stop file *) - Hint fsubst0 : ltlc := Constructors fsubst0. + Hint csubst0 : ltlc := Constructors csubst0. Section csubst0_gen_base. (***********************************************) @@ -39,9 +38,9 @@ Require Export drop_defs. )). Intros until 1; InsertEq H '(S i); InsertEq H '(CTail c1 k u1). XCase H; Clear x v y y0; Intros; Inversion H1. -(* case 1: csubst0_fst *) +(* case 1: csubst0_snd *) Inversion H0; Rewrite H3 in H; Rewrite H5 in H; Rewrite H6 in H; XEAuto. -(* case 2: csubst0_snd *) +(* case 2: csubst0_fst *) Inversion H0; Rewrite H3 in H; Rewrite H4 in H; Rewrite H5 in H; XEAuto. (* case 2: csubst0_both *) Inversion H2; Rewrite H5 in H; Rewrite H6 in H; Rewrite H7 in H; @@ -72,9 +71,9 @@ Require Export drop_defs. (* case 2.2: n > 0 *) Intros until 3; Clear H0; InsertEq H2 '(S i); XElim H0; Intros. DropGenBase. -(* case 2.2.1: csubst0_fst *) +(* case 2.2.1: csubst0_snd *) XAuto. -(* case 2.2.2: csubst0_snd *) +(* case 2.2.2: csubst0_fst *) XReplaceIn H0 i0 i; DropGenBase; NewInduction k; XEAuto. (* case 2.2.3: csubst0_both *) XReplaceIn H0 i0 i; XReplaceIn H2 i0 i. @@ -124,9 +123,9 @@ Require Export drop_defs. (* case 2.2: n > 0 *) Intros until 3; Clear H0; InsertEq H2 '(S i); XElim H0; Clear c1 c2 v y; Intros; DropGenBase. -(* case 2.2.1: csubst0_fst *) +(* case 2.2.1: csubst0_snd *) XEAuto. -(* case 2.2.2: csubst0_snd *) +(* case 2.2.2: csubst0_fst *) Replace i0 with i; XAuto; XReplaceIn H0 i0 i; XReplaceIn H2 i0 i; Clear H3 i0. Apply (r_dis k); Intros; Rewrite (H3 i) in H0; Rewrite (H3 n) in H4. (* case 2.2.2.1: bind *) @@ -158,9 +157,9 @@ Require Export drop_defs. (* case 2.2 : n > 0 *) Intros until 3; Clear H0; InsertEq H2 '(S i); XElim H0; Intros; DropGenBase. -(* case 2.2.1 : csubst0_fst *) +(* case 2.2.1 : csubst0_snd *) XAuto. -(* case 2.2.2 : csubst0_snd *) +(* case 2.2.2 : csubst0_fst *) XReplaceIn H0 i0 i; NewInduction k; XEAuto. (* case 2.2.3 : csubst0_both *) XReplaceIn H0 i0 i; XReplaceIn H2 i0 i; NewInduction k; XEAuto. diff --git a/helm/coq-contribs/LAMBDA-TYPES/drop_defs.v b/helm/coq-contribs/LAMBDA-TYPES/drop_defs.v index e1576c504..022c66f65 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/drop_defs.v +++ b/helm/coq-contribs/LAMBDA-TYPES/drop_defs.v @@ -1,17 +1,23 @@ -(*#* #stop file *) - Require Export contexts_defs. Require Export lift_defs. +(*#* #caption "current axioms for dropping", + "base case", "untouched tail item", + "dropped tail item", "updated tail item" +*) +(*#* #cap #alpha c in C1, e in C2, u in V, k in z, n in k, d in i, r in q *) + Inductive drop : nat -> nat -> C -> C -> Prop := | drop_sort : (h,d,n:?) (drop h d (CSort n) (CSort n)) - | drop_tail : (c,e:?) (drop (0) (0) c e) -> + | drop_comp : (c,e:?) (drop (0) (0) c e) -> (k:?; u:?) (drop (0) (0) (CTail c k u) (CTail e k u)) | drop_drop : (k:?; h:?; c,e:?) (drop (r k h) (0) c e) -> (u:?) (drop (S h) (0) (CTail c k u) e) | drop_skip : (k:?; h,d:?; c,e:?) (drop h (r k d) c e) -> (u:?) (drop h (S d) (CTail c k (lift h (r k d) u)) (CTail e k u)). +(*#* #stop file *) + Hint drop : ltlc := Constructors drop. Hint discr : ltlc := Extern 4 (drop ? ? ? ?) Simpl. @@ -28,7 +34,7 @@ Require Export lift_defs. Intros until 1; Repeat InsertEq H '(0); XElim H; Intros. (* case 1 : drop_sort *) XAuto. -(* case 2 : drop_tail *) +(* case 2 : drop_comp *) Rewrite H0; XAuto. (* case 3 : drop_drop *) Inversion H2. @@ -44,7 +50,7 @@ Require Export lift_defs. XElim H; Intros. (* case 1 : drop_sort *) Inversion H1. -(* case 2 : drop_tail *) +(* case 2 : drop_comp *) Inversion H1. (* case 3 : drop_drop *) Inversion H1; Inversion H3. diff --git a/helm/coq-contribs/LAMBDA-TYPES/drop_props.v b/helm/coq-contribs/LAMBDA-TYPES/drop_props.v index c9d3ef294..84c8676fb 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/drop_props.v +++ b/helm/coq-contribs/LAMBDA-TYPES/drop_props.v @@ -1,3 +1,5 @@ +(*#* #stop file *) + Require lift_gen. Require drop_defs. @@ -5,24 +7,17 @@ Require drop_defs. Section confluence. (*****************************************************) -(*#* #stop macro *) - Tactic Definition IH := Match Context With [ H1: (drop ?1 ?2 c ?3); H2: (drop ?1 ?2 c ?4) |- ? ] -> LApply (H ?4 ?2 ?1); [ Clear H H2; Intros H | XAuto ]; LApply (H ?3); [ Clear H H1; Intros | XAuto ]. -(*#* #start macro *) - (*#* #caption "confluence, first case" *) (*#* #cap #alpha c in C, x1 in C1, x2 in C2, d in i *) Theorem drop_mono : (c,x1:?; d,h:?) (drop h d c x1) -> (x2:?) (drop h d c x2) -> x1 = x2. - -(*#* #stop proof *) - XElim c. (* case 1: CSort *) Intros; Repeat DropGenBase; Rewrite H0; XAuto. @@ -35,8 +30,6 @@ Require drop_defs. LiftGen; IH; XAuto. Qed. -(*#* #start proof *) - (*#* #caption "confluence, second case" *) (*#* #cap #alpha c in C1, c0 in E1, e in C2, e0 in E2, u in V1, v in V2, i in k, d in i *) @@ -47,9 +40,6 @@ Require drop_defs. (drop i (0) e (CTail e0 (Bind b) v)) & (drop h d c0 e0) ). - -(*#* #stop proof *) - XElim i. (* case 1 : i = 0 *) Intros until 1. @@ -72,17 +62,12 @@ Require drop_defs. XElim H; XEAuto. Qed. -(*#* #start proof *) - (*#* #caption "confluence, third case" *) (*#* #cap #alpha c in C, a in C1, e in C2, i in k, d in i *) Theorem drop_conf_ge: (i:?; a,c:?) (drop i (0) c a) -> (e:?; h,d:?) (drop h d c e) -> (le (plus d h) i) -> (drop (minus i h) (0) e a). - -(*#* #stop proof *) - XElim i. (* case 1 : i = 0 *) Intros until 1. @@ -119,8 +104,6 @@ Require drop_defs. Rewrite <- minus_Sn_m; XEAuto. Qed. -(*#* #start proof *) - End confluence. Section transitivity. (***************************************************) @@ -132,9 +115,6 @@ Require drop_defs. (c1,c2:?; h:?) (drop h d c1 c2) -> (e2:?) (drop i (0) c2 e2) -> (EX e1 | (drop i (0) c1 e1) & (drop h (minus d i) e1 e2)). - -(*#* #stop proof *) - XElim i. (* case 1 : i = 0 *) Intros. @@ -165,17 +145,12 @@ Require drop_defs. XElim IHc; XEAuto. Qed. -(*#* #start proof *) - (*#* #caption "transitivity, second case" *) (*#* #cap #alpha c1 in C1, c2 in C, e2 in C2, d in i, i in k *) Theorem drop_trans_ge : (i:?; c1,c2:?; d,h:?) (drop h d c1 c2) -> (e2:?) (drop i (0) c2 e2) -> (le d i) -> (drop (plus i h) (0) c1 e2). - -(*#* #stop proof *) - XElim i. (* case 1: i = 0 *) Intros. @@ -203,12 +178,8 @@ Require drop_defs. DropGenBase; Apply drop_drop; NewInduction k; Simpl; XEAuto. (**) (* explicit constructor *) Qed. -(*#* #start proof *) - End transitivity. -(*#* #stop macro *) - Tactic Definition DropDis := Match Context With [ H1: (drop ?1 ?2 ?3 ?4); H2: (drop ?1 ?2 ?3 ?5) |- ? ] -> @@ -254,6 +225,4 @@ Require drop_defs. LApply (H1 ?6); [ Clear H1 H2; Intros H1 | XAuto ]; LApply H1; [ Clear H1; Intros | XAuto ]. -(*#* #start macro *) - (*#* #single *) diff --git a/helm/coq-contribs/LAMBDA-TYPES/pc3_defs.v b/helm/coq-contribs/LAMBDA-TYPES/pc3_defs.v index b2b530d59..ada99cf2c 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/pc3_defs.v +++ b/helm/coq-contribs/LAMBDA-TYPES/pc3_defs.v @@ -1,20 +1,29 @@ -(*#* #stop file *) - Require Export pr2_defs. Require Export pr3_defs. Require Export pc1_defs. +(*#* #stop file *) + Inductive pc2 [c:C; t1,t2:T] : Prop := | pc2_r : (pr2 c t1 t2) -> (pc2 c t1 t2) | pc2_x : (pr2 c t2 t1) -> (pc2 c t1 t2). Hint pc2 : ltlc := Constructors pc2. +(*#* #start file *) + +(*#* #caption "axioms for the relation $\\PcT{}{}{}$", + "reflexivity", "single step transitivity" +*) +(*#* #cap #cap c, t, t1, t2, t3 *) + Inductive pc3 [c:C] : T -> T -> Prop := | pc3_r : (t:?) (pc3 c t t) | pc3_u : (t2,t1:?) (pc2 c t1 t2) -> (t3:?) (pc3 c t2 t3) -> (pc3 c t1 t3). +(*#* #stop file *) + Hint pc3 : ltlc := Constructors pc3. Section pc2_props. (******************************************************) @@ -156,5 +165,8 @@ Require Export pc1_defs. LApply (pc3_t (TTail ?3 ?4 ?5) ?1 ?2); [ Intros H_x | XAuto ]; LApply (H_x (TTail ?3 ?6 ?5)); [ Clear H_x; Intros | Apply pc3_s; XAuto ] | [ _: (pc3 ?1 ?2 ?3); _: (pr3 ?1 ?3 ?4) |- ? ] -> + LApply (pc3_t ?3 ?1 ?2); [ Intros H_x | XAuto ]; + LApply (H_x ?4); [ Clear H_x; Intros | XAuto ] + | [ _: (pc3 ?1 ?2 ?3); _: (pc3 ?1 ?4 ?3) |- ? ] -> LApply (pc3_t ?3 ?1 ?2); [ Intros H_x | XAuto ]; LApply (H_x ?4); [ Clear H_x; Intros | XAuto ]. diff --git a/helm/coq-contribs/LAMBDA-TYPES/pc3_gen.v b/helm/coq-contribs/LAMBDA-TYPES/pc3_gen.v index 4e5dabaaa..af5f2a992 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/pc3_gen.v +++ b/helm/coq-contribs/LAMBDA-TYPES/pc3_gen.v @@ -8,16 +8,22 @@ Require pc3_props. Section pc3_gen. (********************************************************) - Theorem pc3_gen_abst : (c:?; u1,u2,t1,t2:?) - (pc3 c (TTail (Bind Abst) u1 t1) - (TTail (Bind Abst) u2 t2) - ) -> - (pc3 c u1 u2) /\ - (b:?; u:?) (pc3 (CTail c (Bind b) u) t1 t2). + Theorem pc3_gen_sort: (c:?; m,n:?) (pc3 c (TSort m) (TSort n)) -> m = n. + Intros; Pc3Confluence; Repeat Pr3GenBase. + Rewrite H in H0; Clear H x c. + Inversion H0; XAuto. + Qed. + + Theorem pc3_gen_abst: (c:?; u1,u2,t1,t2:?) + (pc3 c (TTail (Bind Abst) u1 t1) + (TTail (Bind Abst) u2 t2) + ) -> + (pc3 c u1 u2) /\ + (b:?; u:?) (pc3 (CTail c (Bind b) u) t1 t2). Intros. - Pc3Confluence; Pr3Gen; Pr3Gen; Rewrite H0 in H; Clear H0 x. - Inversion H; Rewrite H5 in H1; Rewrite H6 in H2. - Split; XEAuto. + Pc3Confluence; Repeat Pr3GenBase; Rewrite H0 in H1; Clear H0 x. + Inversion H1; Rewrite H0 in H4; Rewrite H6 in H5. + XEAuto. Qed. Theorem pc3_gen_lift: (c:?; t1,t2:?; h,d:?) @@ -25,43 +31,44 @@ Require pc3_props. (e:?) (drop h d c e) -> (pc3 e t1 t2). Intros. - Pc3Confluence; Pr3Gen; Pr3Gen; Rewrite H1 in H; Clear H1 x. - LiftGen; Rewrite H in H2; XEAuto. + Pc3Confluence; Repeat Pr3Gen; Rewrite H2 in H1; Clear H2 x. + LiftGen; Rewrite H in H3; XEAuto. Qed. - Theorem pc3_gen_not_abst : (b:?) ~b=Abst -> (c:?; t1,t2,u1,u2:?) - (pc3 c (TTail (Bind b) u1 t1) - (TTail (Bind Abst) u2 t2) - ) -> - (pc3 (CTail c (Bind b) u1) t1 - (lift (1) (0) (TTail (Bind Abst) u2 t2)) - ) - . - Intros b; XElim b; Intros; - Try EqFalse; Pc3Confluence; Pr3Gen; Pr3Gen; - Try (Rewrite H1 in H0; Inversion H0); - Rewrite H1 in H4; Pr3Context; + Theorem pc3_gen_not_abst: (b:?) ~b=Abst -> (c:?; t1,t2,u1,u2:?) + (pc3 c (TTail (Bind b) u1 t1) + (TTail (Bind Abst) u2 t2) + ) -> + (pc3 (CTail c (Bind b) u1) t1 + (lift (1) (0) (TTail (Bind Abst) u2 t2)) + ). + XElim b; Intros; + Try EqFalse; Pc3Confluence; Repeat Pr3Gen; + Try (Rewrite H3 in H0; TGenBase); + Rewrite H0 in H2; Clear H H0 x; EApply pc3_pr3_t; XEAuto. Qed. - Theorem pc3_gen_lift_abst : (c:?; t,t2,u2:?; h,d:?) - (pc3 c (lift h d t) + Theorem pc3_gen_lift_abst: (c:?; t,t2,u2:?; h,d:?) + (pc3 c (lift h d t) (TTail (Bind Abst) u2 t2) - ) -> - (e:?) (drop h d c e) -> - (EX u1 t1 | (pr3 e t (TTail (Bind Abst) u1 t1)) & - (pr3 c u2 (lift h d u1)) & - (b:B; u:T)(pr3 (CTail c (Bind b) u) t2 (lift h (S d) t1)) - ). + ) -> + (e:?) (drop h d c e) -> + (EX u1 t1 | (pr3 e t (TTail (Bind Abst) u1 t1)) & + (pr3 c u2 (lift h d u1)) & + (b:B; u:T)(pr3 (CTail c (Bind b) u) t2 (lift h (S d) t1)) + ). Intros. - Pc3Confluence; Pr3Gen; Pr3Gen; Rewrite H1 in H; Clear H1 x. - LiftGenBase; Rewrite H in H4; Rewrite H1 in H2; Rewrite H5 in H3; XEAuto. + Pc3Confluence; Repeat Pr3Gen; Rewrite H in H2; Clear H x. + LiftGenBase; Rewrite H in H3; Rewrite H1 in H4; Rewrite H2 in H5; XEAuto. Qed. End pc3_gen. Tactic Definition Pc3Gen := Match Context With + | [H: (pc3 ?1 (TSort ?2) (TSort ?3)) |- ? ] -> + LApply (pc3_gen_sort ?1 ?2 ?3); [ Clear H; Intros | XAuto ] | [ _: (pc3 ?1 (lift ?2 ?3 ?4) (lift ?2 ?3 ?5)); _: (drop ?2 ?3 ?1 ?6) |- ? ] -> LApply (pc3_gen_lift ?1 ?4 ?5 ?2 ?3); [ Intros H_x | XAuto ]; diff --git a/helm/coq-contribs/LAMBDA-TYPES/pc3_props.v b/helm/coq-contribs/LAMBDA-TYPES/pc3_props.v index 49d9bc4ec..6f48a27fe 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/pc3_props.v +++ b/helm/coq-contribs/LAMBDA-TYPES/pc3_props.v @@ -2,21 +2,20 @@ Require subst0_subst0. Require pr0_subst0. +Require cpr0_defs. Require pr3_defs. Require pr3_props. Require pr3_confluence. -Require cpr0_defs. -Require cpr0_props. Require pc3_defs. Section pc3_confluence. (*************************************************) - Theorem pc3_confluence : (c:?; t1,t2:?) (pc3 c t1 t2) -> - (EX t0 | (pr3 c t1 t0) & (pr3 c t2 t0)). + Theorem pc3_confluence: (c:?; t1,t2:?) (pc3 c t1 t2) -> + (EX t0 | (pr3 c t1 t0) & (pr3 c t2 t0)). Intros; XElim H; Intros. -(* case 1 : pc3_r *) +(* case 1: pc3_r *) XEAuto. -(* case 2 : pc3_u *) +(* case 2: pc3_u *) Clear H0; XElim H1; Intros. Inversion_clear H; [ XEAuto | Pr3Confluence; XEAuto ]. Qed. @@ -31,58 +30,58 @@ Require pc3_defs. Section pc3_context. (****************************************************) - Theorem pc3_pr0_pr2_t : (u1,u2:?) (pr0 u2 u1) -> - (c:?; t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) -> - (pc3 (CTail c k u1) t1 t2). + Theorem pc3_pr0_pr2_t: (u1,u2:?) (pr0 u2 u1) -> + (c:?; t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) -> + (pc3 (CTail c k u1) t1 t2). Intros. Inversion H0; Clear H0; [ XAuto | NewInduction i ]. -(* case 1 : pr2_delta i = 0 *) - DropGenBase; Inversion H0; Clear H0 H3 H4 c k. - Rewrite H5 in H; Clear H5 u2. - Pr0Subst0; XEAuto. -(* case 2 : pr2_delta i > 0 *) +(* case 1: pr2_delta i = 0 *) + DropGenBase; Inversion H0; Clear H0 H4 H5 H6 c k t. + Rewrite H7 in H; Clear H7 u2. + Pr0Subst0; Apply pc3_pr3_t with t0:=x; XEAuto. +(* case 2: pr2_delta i > 0 *) NewInduction k; DropGenBase; XEAuto. Qed. - Theorem pc3_pr2_pr2_t : (c:?; u1,u2:?) (pr2 c u2 u1) -> - (t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) -> - (pc3 (CTail c k u1) t1 t2). + Theorem pc3_pr2_pr2_t: (c:?; u1,u2:?) (pr2 c u2 u1) -> + (t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) -> + (pc3 (CTail c k u1) t1 t2). Intros until 1; Inversion H; Clear H; Intros. -(* case 1 : pr2_pr0 *) +(* case 1: pr2_free *) EApply pc3_pr0_pr2_t; [ Apply H0 | XAuto ]. -(* case 2 : pr2_delta *) +(* case 2: pr2_delta *) Inversion H; [ XAuto | NewInduction i0 ]. -(* case 2.1 : i0 = 0 *) - DropGenBase; Inversion H2; Clear H2. - Rewrite <- H5; Rewrite H6 in H; Rewrite <- H7 in H3; Clear H5 H6 H7 d0 k u0. - Subst0Subst0; Arith9'In H4 i. +(* case 2.1: i0 = 0 *) + DropGenBase; Inversion H4; Clear H3 H4 H7 t t4. + Rewrite <- H9; Rewrite H10 in H; Rewrite <- H11 in H6; Clear H9 H10 H11 d0 k u0. + Pr0Subst0; Subst0Subst0; Arith9'In H6 i. EApply pc3_pr3_u. EApply pr2_delta; XEAuto. - Apply pc3_pr2_x; EApply pr2_delta; [ Idtac | XEAuto ]; XEAuto. -(* case 2.2 : i0 > 0 *) + Apply pc3_pr2_x; EApply pr2_delta; [ Idtac | XEAuto | XEAuto ]; XEAuto. +(* case 2.2: i0 > 0 *) Clear IHi0; NewInduction k; DropGenBase; XEAuto. Qed. - Theorem pc3_pr2_pr3_t : (c:?; u2,t1,t2:?; k:?) - (pr3 (CTail c k u2) t1 t2) -> - (u1:?) (pr2 c u2 u1) -> - (pc3 (CTail c k u1) t1 t2). + Theorem pc3_pr2_pr3_t: (c:?; u2,t1,t2:?; k:?) + (pr3 (CTail c k u2) t1 t2) -> + (u1:?) (pr2 c u2 u1) -> + (pc3 (CTail c k u1) t1 t2). Intros until 1; XElim H; Intros. -(* case 1 : pr3_r *) +(* case 1: pr3_refl *) XAuto. -(* case 2 : pr3_u *) +(* case 2: pr3_sing *) EApply pc3_t. EApply pc3_pr2_pr2_t; [ Apply H2 | Apply H ]. XAuto. Qed. - Theorem pc3_pr3_pc3_t : (c:?; u1,u2:?) (pr3 c u2 u1) -> - (t1,t2:?; k:?) (pc3 (CTail c k u2) t1 t2) -> - (pc3 (CTail c k u1) t1 t2). + Theorem pc3_pr3_pc3_t: (c:?; u1,u2:?) (pr3 c u2 u1) -> + (t1,t2:?; k:?) (pc3 (CTail c k u2) t1 t2) -> + (pc3 (CTail c k u1) t1 t2). Intros until 1; XElim H; Intros. -(* case 1 : pr3_r *) +(* case 1: pr3_refl *) XAuto. -(* case 2 : pr3_u *) +(* case 2: pr3_sing *) Apply H1; Pc3Confluence. EApply pc3_t; [ Idtac | Apply pc3_s ]; EApply pc3_pr2_pr3_t; XEAuto. Qed. @@ -110,9 +109,9 @@ Require pc3_defs. Section pc3_lift. (*******************************************************) - Theorem pc3_lift : (c,e:?; h,d:?) (drop h d c e) -> - (t1,t2:?) (pc3 e t1 t2) -> - (pc3 c (lift h d t1) (lift h d t2)). + Theorem pc3_lift: (c,e:?; h,d:?) (drop h d c e) -> + (t1,t2:?) (pc3 e t1 t2) -> + (pc3 c (lift h d t1) (lift h d t2)). Intros. Pc3Confluence. @@ -125,35 +124,35 @@ Require pc3_defs. Section pc3_cpr0. (*******************************************************) - Remark pc3_cpr0_t_aux : (c1,c2:?) (cpr0 c1 c2) -> - (k:?; u,t1,t2:?) (pr3 (CTail c1 k u) t1 t2) -> - (pc3 (CTail c2 k u) t1 t2). + Remark pc3_cpr0_t_aux: (c1,c2:?) (cpr0 c1 c2) -> + (k:?; u,t1,t2:?) (pr3 (CTail c1 k u) t1 t2) -> + (pc3 (CTail c2 k u) t1 t2). Intros; XElim H0; Intros. -(* case 1.1 : pr3_r *) +(* case 1.1: pr3_refl *) XAuto. -(* case 1.2 : pr3_u *) +(* case 1.2: pr3_sing *) EApply pc3_t; [ Idtac | XEAuto ]. Clear H2 t1 t2. Inversion_clear H0. -(* case 1.2.1 : pr2_pr0 *) +(* case 1.2.1: pr2_free *) XAuto. -(* case 1.2.2 : pr2_delta *) +(* case 1.2.2: pr2_delta *) Cpr0Drop; Pr0Subst0. EApply pc3_pr3_u; [ EApply pr2_delta; XEAuto | XAuto ]. Qed. - Theorem pc3_cpr0_t : (c1,c2:?) (cpr0 c1 c2) -> - (t1,t2:?) (pr3 c1 t1 t2) -> - (pc3 c2 t1 t2). + Theorem pc3_cpr0_t: (c1,c2:?) (cpr0 c1 c2) -> + (t1,t2:?) (pr3 c1 t1 t2) -> + (pc3 c2 t1 t2). Intros until 1; XElim H; Intros. -(* case 1 : cpr0_refl *) +(* case 1: cpr0_refl *) XAuto. -(* case 2 : cpr0_cont *) +(* case 2: cpr0_comp *) Pc3Context; Pc3Confluence. EApply pc3_t; [ Idtac | Apply pc3_s ]; EApply pc3_cpr0_t_aux; XEAuto. Qed. - Theorem pc3_cpr0 : (c1,c2:?) (cpr0 c1 c2) -> (t1,t2:?) (pc3 c1 t1 t2) -> - (pc3 c2 t1 t2). + Theorem pc3_cpr0: (c1,c2:?) (cpr0 c1 c2) -> (t1,t2:?) (pc3 c1 t1 t2) -> + (pc3 c2 t1 t2). Intros; Pc3Confluence. EApply pc3_t; [ Idtac | Apply pc3_s ]; EApply pc3_cpr0_t; XEAuto. Qed. diff --git a/helm/coq-contribs/LAMBDA-TYPES/pc3_subst0.v b/helm/coq-contribs/LAMBDA-TYPES/pc3_subst0.v index 52505544b..4fd7e138a 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/pc3_subst0.v +++ b/helm/coq-contribs/LAMBDA-TYPES/pc3_subst0.v @@ -1,7 +1,7 @@ (*#* #stop file *) Require subst0_subst0. -Require csubst0_defs. +Require fsubst0_defs. Require pr0_subst0. Require pc3_defs. @@ -12,49 +12,49 @@ Require pc3_defs. (e:?) (drop i (0) c1 (CTail e (Bind Abbr) u)) -> (pc3 c2 t2 t). Intros until 1; XElim H. -(* case 1: pr2_pr0 *) +(* case 1: pr2_free *) Intros until 2; XElim H0; Intros. -(* case 1.1: fsubst0_t *) +(* case 1.1: fsubst0_snd *) Pr0Subst0; [ XAuto | Apply (pc3_pr3_u c1 x); XEAuto ]. -(* case 1.2: fsubst0_c *) +(* case 1.2: fsubst0_fst *) XAuto. -(* case 1.3: fsubst0_b *) +(* case 1.3: fsubst0_both *) Pr0Subst0; CSubst0Drop; [ XAuto | Apply (pc3_pr3_u c0 x); XEAuto ]. (* case 2 : pr2_delta *) - Intros until 3; XElim H1; Intros. -(* case 2.1: fsubst0_t. *) + Intros until 4; XElim H2; Intros. +(* case 2.1: fsubst0_snd. *) Apply (pc3_t t1); [ Apply pc3_s; XEAuto | XEAuto ]. -(* case 2.2: fsubst0_c. *) +(* case 2.2: fsubst0_fst. *) Apply (lt_le_e i i0); Intros; CSubst0Drop. (* case 2.2.1: i < i0, none *) XEAuto. -(* case 2.2.2: i < i0, csubst0_fst *) - Inversion H; Rewrite <- H7 in H4; Rewrite <- H8 in H4; Rewrite <- H8 in H5; Rewrite <- H9 in H5; Clear H H7 H8 H9 c2 t2 x0 x1 x2. - Subst0Subst0; Rewrite <- lt_plus_minus_r in H6; [ CSubst0Drop | XAuto ]. +(* case 2.2.2: i < i0, csubst0_snd *) + CGenBase; Rewrite <- H8 in H5; Rewrite <- H9 in H5; Rewrite <- H9 in H6; Rewrite <- H10 in H6; Clear H8 H9 H10 c2 t3 x0 x1 x2. + Subst0Subst0; Rewrite <- lt_plus_minus_r in H7; [ CSubst0Drop | XAuto ]. Apply (pc3_pr3_u c0 x); XEAuto. -(* case 2.2.3: i < i0, csubst0_snd *) - Inversion H; Rewrite <- H7 in H5; Rewrite <- H8 in H4; Rewrite <- H8 in H5; Rewrite <- H9 in H4; Clear H H7 H8 H9 c2 t2 x0 x1 x3. +(* case 2.2.3: i < i0, csubst0_fst *) + CGenBase; Rewrite <- H8 in H6; Rewrite <- H9 in H5; Rewrite <- H9 in H6; Rewrite <- H10 in H5; Clear H8 H9 H10 c2 t3 x0 x1 x3. Apply pc3_pr2_r; XEAuto. (* case 2.2.4: i < i0, csubst0_both *) - Inversion H; Rewrite <- H8 in H6; Rewrite <- H9 in H4; Rewrite <- H9 in H5; Rewrite <- H9 in H6; Rewrite <- H10 in H5; Clear H H8 H9 H10 c2 t2 x0 x1 x3. - Subst0Subst0; Rewrite <- lt_plus_minus_r in H7; [ CSubst0Drop | XAuto ]. + CGenBase; Rewrite <- H9 in H7; Rewrite <- H10 in H5; Rewrite <- H10 in H6; Rewrite <- H10 in H7; Rewrite <- H11 in H6; Clear H9 H10 H11 c2 t3 x0 x1 x3. + Subst0Subst0; Rewrite <- lt_plus_minus_r in H8; [ CSubst0Drop | XAuto ]. Apply (pc3_pr3_u c0 x); XEAuto. (* case 2.2.5: i >= i0 *) XEAuto. -(* case 2.3: fsubst0_b *) +(* case 2.3: fsubst0_both *) Apply (lt_le_e i i0); Intros; CSubst0Drop. (* case 2.3.1 : i < i0, none *) CSubst0Drop; Apply pc3_pr3_u2 with t0 := t1; XEAuto. -(* case 2.3.2 : i < i0, csubst0_fst *) - Inversion H; Rewrite <- H8 in H5; Rewrite <- H9 in H5; Rewrite <- H9 in H6; Rewrite <- H10 in H6; Clear H H8 H9 H10 c2 t2 x0 x1 x2. - Subst0Subst0; Rewrite <- lt_plus_minus_r in H7; [ CSubst0Drop | XAuto ]. +(* case 2.3.2 : i < i0, csubst0_snd *) + CGenBase; Rewrite <- H9 in H6; Rewrite <- H10 in H6; Rewrite <- H10 in H7; Rewrite <- H11 in H7; Clear H9 H10 H11 c2 t3 x0 x1 x2. + Subst0Subst0; Rewrite <- lt_plus_minus_r in H8; [ CSubst0Drop | XAuto ]. Apply (pc3_pr3_u2 c0 t1); [ Idtac | Apply (pc3_pr3_u c0 x) ]; XEAuto. -(* case 2.3.3: i < i0, csubst0_snd *) - Inversion H; Rewrite <- H8 in H6; Rewrite <- H9 in H5; Rewrite <- H9 in H6; Rewrite <- H10 in H5; Clear H H8 H9 H10 c2 t2 x0 x1 x3. +(* case 2.3.3: i < i0, csubst0_fst *) + CGenBase; Rewrite <- H9 in H7; Rewrite <- H10 in H6; Rewrite <- H10 in H7; Rewrite <- H11 in H6; Clear H9 H10 H11 c2 t3 x0 x1 x3. CSubst0Drop; Apply (pc3_pr3_u2 c0 t1); [ Idtac | Apply pc3_pr2_r ]; XEAuto. (* case 2.3.4: i < i0, csubst0_both *) - Inversion H; Rewrite <- H9 in H7; Rewrite <- H10 in H5; Rewrite <- H10 in H6; Rewrite <- H10 in H7; Rewrite <- H11 in H6; Clear H H9 H10 H11 c2 t2 x0 x1 x3. - Subst0Subst0; Rewrite <- lt_plus_minus_r in H8; [ CSubst0Drop | XAuto ]. + CGenBase; Rewrite <- H10 in H8; Rewrite <- H11 in H6; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H7; Clear H10 H11 H12 c2 t3 x0 x1 x3. + Subst0Subst0; Rewrite <- lt_plus_minus_r in H9; [ CSubst0Drop | XAuto ]. Apply (pc3_pr3_u2 c0 t1); [ Idtac | Apply (pc3_pr3_u c0 x) ]; XEAuto. (* case 2.3.5: i >= i0 *) CSubst0Drop; Apply (pc3_pr3_u2 c0 t1); XEAuto. @@ -65,52 +65,52 @@ Require pc3_defs. (e:?) (drop i (0) c1 (CTail e (Bind Abbr) u)) -> (pc3 c2 t t2). Intros until 1; XElim H. -(* case 1: pr2_pr0 *) +(* case 1: pr2_free *) Intros until 2; XElim H0; Intros. -(* case 1.1: fsubst0_t. *) - Apply (pc3_pr3_u c1 t1); XEAuto. -(* case 1.2: fsubst0_c. *) +(* case 1.1: fsubst0_snd. *) + Apply (pc3_pr3_u c1 t2); XEAuto. +(* case 1.2: fsubst0_fst. *) XAuto. -(* case 1.3: fsubst0_c. *) - CSubst0Drop; Apply (pc3_pr3_u c0 t1); XEAuto. +(* case 1.3: fsubst0_both. *) + CSubst0Drop; Apply (pc3_pr3_u c0 t2); XEAuto. (* case 2: pr2_delta *) - Intros until 3; XElim H1; Intros. -(* case 2.1: fsubst0_t. *) - Apply (pc3_t t1); XEAuto. -(* case 2.2: fsubst0_c. *) + Intros until 4; XElim H2; Intros. +(* case 2.1: fsubst0_snd. *) + Apply (pc3_t t2); Apply pc3_pr3_r; XEAuto. +(* case 2.2: fsubst0_fst. *) Apply (lt_le_e i i0); Intros; CSubst0Drop. (* case 2.2.1: i < i0, none *) XEAuto. (* case 2.2.2: i < i0, csubst0_bind *) - Inversion H; Rewrite <- H7 in H4; Rewrite <- H8 in H4; Rewrite <- H8 in H5; Rewrite <- H9 in H5; Clear H H7 H8 H9 c2 t2 x0 x1 x2. - Subst0Subst0; Rewrite <- lt_plus_minus_r in H6; [ CSubst0Drop | XAuto ]. + CGenBase; Rewrite <- H8 in H5; Rewrite <- H9 in H5; Rewrite <- H9 in H6; Rewrite <- H10 in H6; Clear H8 H9 H10 c2 t3 x0 x1 x2. + Subst0Subst0; Rewrite <- lt_plus_minus_r in H7; [ CSubst0Drop | XAuto ]. Apply (pc3_pr3_u c0 x); XEAuto. -(* case 2.2.3: i < i0, csubst0_snd *) - Inversion H; Rewrite <- H7 in H5; Rewrite <- H8 in H4; Rewrite <- H8 in H5; Rewrite <- H9 in H4; Clear H H7 H8 H9 c2 t2 x0 x1 x3. +(* case 2.2.3: i < i0, csubst0_fst *) + CGenBase; Rewrite <- H8 in H6; Rewrite <- H9 in H5; Rewrite <- H9 in H6; Rewrite <- H10 in H5; Clear H8 H9 H10 c2 t3 x0 x1 x3. Apply pc3_pr2_r; XEAuto. (* case 2.2.4: i < i0, csubst0_both *) - Inversion H; Rewrite <- H8 in H6; Rewrite <- H9 in H4; Rewrite <- H9 in H5; Rewrite <- H9 in H6; Rewrite <- H10 in H5; Clear H H8 H9 H10 c2 t2 x0 x1 x3. - Subst0Subst0; Rewrite <- lt_plus_minus_r in H7; [ CSubst0Drop | XAuto ]. + CGenBase; Rewrite <- H9 in H7; Rewrite <- H10 in H5; Rewrite <- H10 in H6; Rewrite <- H10 in H7; Rewrite <- H11 in H6; Clear H9 H10 H11 c2 t3 x0 x1 x3. + Subst0Subst0; Rewrite <- lt_plus_minus_r in H8; [ CSubst0Drop | XAuto ]. Apply (pc3_pr3_u c0 x); XEAuto. (* case 2.2.5: i >= i0 *) XEAuto. -(* case 2.3: fsubst0_b *) +(* case 2.3: fsubst0_both *) Apply (lt_le_e i i0); Intros; CSubst0Drop. (* case 2.3.1 : i < i0, none *) - CSubst0Drop; Apply pc3_pr3_u with t2 := t1; XEAuto. -(* case 2.3.2 : i < i0, csubst0_fst *) - Inversion H; Rewrite <- H8 in H5; Rewrite <- H9 in H5; Rewrite <- H9 in H6; Rewrite <- H10 in H6; Clear H H8 H9 H10 c2 t2 x0 x1 x2. - Subst0Subst0; Rewrite <- lt_plus_minus_r in H7; [ CSubst0Drop | XAuto ]. - Apply (pc3_pr3_u c0 x); [ Idtac | Apply (pc3_pr3_u2 c0 t1) ]; XEAuto. -(* case 2.3.3: i < i0, csubst0_snd *) - Inversion H; Rewrite <- H8 in H6; Rewrite <- H9 in H5; Rewrite <- H9 in H6; Rewrite <- H10 in H5; Clear H H8 H9 H10 c2 t2 x0 x1 x3. - CSubst0Drop; Apply (pc3_pr3_u c0 t1); [ Idtac | Apply pc3_pr2_r ]; XEAuto. -(* case 2.3.4: i < i0, csubst0_both *) - Inversion H; Rewrite <- H9 in H7; Rewrite <- H10 in H5; Rewrite <- H10 in H6; Rewrite <- H10 in H7; Rewrite <- H11 in H6; Clear H H9 H10 H11 c2 t2 x0 x1 x3. + CSubst0Drop; Apply pc3_pr3_u with t2:=t2; Try Apply pc3_pr3_r; XEAuto. +(* case 2.3.2 : i < i0, csubst0_snd *) + CGenBase; Rewrite <- H9 in H6; Rewrite <- H10 in H6; Rewrite <- H10 in H7; Rewrite <- H11 in H7; Clear H9 H10 H11 c2 t3 x0 x1 x2. Subst0Subst0; Rewrite <- lt_plus_minus_r in H8; [ CSubst0Drop | XAuto ]. - Apply (pc3_pr3_u c0 x); [ Idtac | Apply (pc3_pr3_u2 c0 t1) ]; XEAuto. + Apply (pc3_pr3_u c0 x); [ Idtac | Apply (pc3_pr3_u2 c0 t0) ]; XEAuto. +(* case 2.3.3: i < i0, csubst0_fst *) + CGenBase; Rewrite <- H9 in H7; Rewrite <- H10 in H6; Rewrite <- H10 in H7; Rewrite <- H11 in H6; Clear H9 H10 H11 c2 t3 x0 x1 x3. + CSubst0Drop; Apply (pc3_pr3_u c0 t0); [ Idtac | Apply pc3_pr2_r ]; XEAuto. +(* case 2.3.4: i < i0, csubst0_both *) + CGenBase; Rewrite <- H10 in H8; Rewrite <- H11 in H6; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H7; Clear H10 H11 H12 c2 t3 x0 x1 x3. + Subst0Subst0; Rewrite <- lt_plus_minus_r in H9; [ CSubst0Drop | XAuto ]. + Apply (pc3_pr3_u c0 x); [ Idtac | Apply (pc3_pr3_u2 c0 t0) ]; XEAuto. (* case 2.3.5: i >= i0 *) - CSubst0Drop; Apply (pc3_pr3_u c0 t1); XEAuto. + CSubst0Drop; Apply (pc3_pr3_u c0 t0); XEAuto. Qed. Theorem pc3_pc2_fsubst0: (c1:?; t1,t:?) (pc2 c1 t1 t) -> diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr2_confluence.v b/helm/coq-contribs/LAMBDA-TYPES/pr2_confluence.v index afdab3d52..8b2fd4769 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/pr2_confluence.v +++ b/helm/coq-contribs/LAMBDA-TYPES/pr2_confluence.v @@ -8,58 +8,57 @@ Require pr2_defs. Section pr2_confluence. (*************************************************) -(* case 1.1 : pr2_pr0 pr2_pr0 ***********************************************) +(* case 1.1 : pr2_free pr2_free *********************************************) - Remark pr2_pr0_pr0: (c:?; t0,t1,t2:?) - (pr0 t0 t1) -> (pr0 t0 t2) -> - (EX t:T | (pr2 c t1 t) & (pr2 c t2 t)). + Remark pr2_free_free: (c:?; t0,t1,t2:?) + (pr0 t0 t1) -> (pr0 t0 t2) -> + (EX t:T | (pr2 c t1 t) & (pr2 c t2 t)). Intros; Pr0Confluence; XEAuto. Qed. -(* case 1.2 : pr2_pr0 pr2_delta *********************************************) +(* case 1.2 : pr2_free pr2_delta ********************************************) - Remark pr2_pr0_delta: (c,d:?; t0,t1,t2,u:?; i:?) - (pr0 t0 t1) -> - (drop i (0) c (CTail d (Bind Abbr) u)) -> - (subst0 i u t0 t2) -> - (EX t | (pr2 c t1 t) & (pr2 c t2 t)). - Intros; Pr0Subst0; XEAuto. + Remark pr2_free_delta: (c,d:?; t0,t1,t2,t4,u:?; i:?) + (pr0 t0 t1) -> + (drop i (0) c (CTail d (Bind Abbr) u)) -> + (pr0 t0 t4) -> + (subst0 i u t4 t2) -> + (EX t | (pr2 c t1 t) & (pr2 c t2 t)). + Intros; Pr0Confluence; Pr0Subst0; XEAuto. Qed. (* case 2.2 : pr2_delta pr2_delta *******************************************) - Remark pr2_delta_delta: (c,d,d0:?; t0,t1,t2,u,u0:?; i,i0:?) + Remark pr2_delta_delta: (c,d,d0:?; t0,t1,t2,t3,t4,u,u0:?; i,i0:?) (drop i (0) c (CTail d (Bind Abbr) u)) -> - (subst0 i u t0 t1) -> + (pr0 t0 t3) -> + (subst0 i u t3 t1) -> (drop i0 (0) c (CTail d0 (Bind Abbr) u0)) -> - (subst0 i0 u0 t0 t2) -> + (pr0 t0 t4) -> + (subst0 i0 u0 t4 t2) -> (EX t:T | (pr2 c t1 t) & (pr2 c t2 t)). - Intros. + Intros; Pr0Confluence; Repeat Pr0Subst0; + [ XEAuto | XEAuto | XEAuto | Idtac ]. Apply (neq_eq_e i i0); Intros. (* case 1 : i != i0 *) Subst0Confluence; XEAuto. (* case 2 : i = i0 *) - Rewrite H3 in H; Rewrite H3 in H0; Clear H3 i. - DropDis; Inversion H1; Rewrite H5 in H0; Clear H1 H4 H5 d u. - Subst0Confluence; [ Rewrite H1; XEAuto | XEAuto | XEAuto | XEAuto ]. + Rewrite H5 in H; Rewrite H5 in H3; Clear H5 i. + DropDis; Inversion H2; Rewrite H7 in H3; Clear H2 H6 H7 d u. + Subst0Confluence; [ Rewrite H2 in H0; XEAuto | XEAuto | XEAuto | XEAuto ]. Qed. (* main *********************************************************************) - Hints Resolve pr2_pr0_pr0 pr2_pr0_delta pr2_delta_delta : ltlc. - -(*#* #start file *) + Hints Resolve pr2_free_free pr2_free_delta pr2_delta_delta : ltlc. (*#* #caption "confluence with itself: Church-Rosser property" *) (*#* #cap #cap c, t0, t1, t2, t *) - Theorem pr2_confluence : (c,t0,t1:?) (pr2 c t0 t1) -> - (t2:?) (pr2 c t0 t2) -> - (EX t | (pr2 c t1 t) & (pr2 c t2 t)). - -(*#* #stop file *) - - Intros; Inversion H; Inversion H0; XEAuto. + Theorem pr2_confluence: (c,t0,t1:?) (pr2 c t0 t1) -> + (t2:?) (pr2 c t0 t2) -> + (EX t | (pr2 c t1 t) & (pr2 c t2 t)). + Intros; Inversion H; Inversion H0; XDEAuto 3. Qed. End pr2_confluence. @@ -72,6 +71,4 @@ Require pr2_defs. XElim H1; Intros | _ -> Pr0Confluence. -(*#* #start file *) - (*#* #single *) diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr2_defs.v b/helm/coq-contribs/LAMBDA-TYPES/pr2_defs.v index a650dd26f..9dab9cafe 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/pr2_defs.v +++ b/helm/coq-contribs/LAMBDA-TYPES/pr2_defs.v @@ -1,120 +1,137 @@ -(*#* #stop file *) - Require Export drop_defs. Require Export pr0_defs. - Inductive pr2 [c:C; t1,t2:T] : Prop := +(*#* #caption "current axioms for the relation $\\PrS{}{}{}$", + "context-free case", "context-dependent $\\delta$-expansion" +*) +(*#* #cap #cap c, d, t, t1, t2 #alpha u in V *) + + Inductive pr2 [c:C; t1:T] : T -> Prop := (* structural rules *) - | pr2_pr0 : (pr0 t1 t2) -> (pr2 c t1 t2) + | pr2_free : (t2:?) (pr0 t1 t2) -> (pr2 c t1 t2) (* axiom rules *) - | pr2_delta : (d:?; u:?; i:?) - (drop i (0) c (CTail d (Bind Abbr) u)) -> - (subst0 i u t1 t2) -> (pr2 c t1 t2). + | pr2_delta: (d:?; u:?; i:?) + (drop i (0) c (CTail d (Bind Abbr) u)) -> + (t2:?) (pr0 t1 t2) -> (t:?) (subst0 i u t2 t) -> + (pr2 c t1 t). + +(*#* #stop file *) Hint pr2 : ltlc := Constructors pr2. Section pr2_gen_base. (***************************************************) - Theorem pr2_gen_sort : (c:?; x:?; n:?) (pr2 c (TSort n) x) -> - x = (TSort n). - Intros; Inversion H; - Try Subst0GenBase; XEAuto. + Theorem pr2_gen_sort: (c:?; x:?; n:?) (pr2 c (TSort n) x) -> + x = (TSort n). + Intros; Inversion H; Pr0GenBase; + [ XAuto | Rewrite H1 in H2; Subst0GenBase ]. Qed. - Theorem pr2_gen_bref : (c:?; x:?; n:?) (pr2 c (TBRef n) x) -> - x = (TBRef n) \/ - (EX d u | (drop n (0) c (CTail d (Bind Abbr) u)) & - x = (lift (S n) (0) u) - ). - Intros; Inversion H; - Try Subst0GenBase; Try Rewrite <- H1 in H0; XEAuto. + Theorem pr2_gen_lref: (c:?; x:?; n:?) (pr2 c (TLRef n) x) -> + x = (TLRef n) \/ + (EX d u | (drop n (0) c (CTail d (Bind Abbr) u)) & + x = (lift (S n) (0) u) + ). + Intros; Inversion H; Pr0GenBase; + [ XAuto | Rewrite H1 in H2; Subst0GenBase; Rewrite <- H2 in H0; XEAuto ]. Qed. - Theorem pr2_gen_abst : (c:?; u1,t1,x:?) - (pr2 c (TTail (Bind Abst) u1 t1) x) -> - (EX u2 t2 | x = (TTail (Bind Abst) u2 t2) & - (pr2 c u1 u2) & (b:?; u:?) - (pr2 (CTail c (Bind b) u) t1 t2) - ). - Intros; Inversion H; - Try Pr0GenBase; Try Subst0GenBase; XDEAuto 6. + Theorem pr2_gen_abst: (c:?; u1,t1,x:?) + (pr2 c (TTail (Bind Abst) u1 t1) x) -> + (EX u2 t2 | x = (TTail (Bind Abst) u2 t2) & + (pr2 c u1 u2) & (b:?; u:?) + (pr2 (CTail c (Bind b) u) t1 t2) + ). + Intros; Inversion H; Pr0GenBase; + [ XEAuto | Rewrite H1 in H2; Subst0GenBase; XDEAuto 6 ]. Qed. - Theorem pr2_gen_appl : (c:?; u1,t1,x:?) - (pr2 c (TTail (Flat Appl) u1 t1) x) -> (OR - (EX u2 t2 | x = (TTail (Flat Appl) u2 t2) & - (pr2 c u1 u2) & (pr2 c t1 t2) - ) | - (EX y1 z1 u2 t2 | t1 = (TTail (Bind Abst) y1 z1) & - x = (TTail (Bind Abbr) u2 t2) & - (pr0 u1 u2) & (pr0 z1 t2) - ) | - (EX b y1 z1 u2 v2 t2 | - ~b=Abst & - t1 = (TTail (Bind b) y1 z1) & - x = (TTail (Bind b) v2 (TTail (Flat Appl) (lift (1) (0) u2) t2)) & - (pr0 u1 u2) & (pr0 y1 v2) & (pr0 z1 t2)) - ). - Intros; Inversion H; - Try Pr0GenBase; Try Subst0GenBase; XEAuto. + Theorem pr2_gen_appl: (c:?; u1,t1,x:?) + (pr2 c (TTail (Flat Appl) u1 t1) x) -> (OR + (EX u2 t2 | x = (TTail (Flat Appl) u2 t2) & + (pr2 c u1 u2) & (pr2 c t1 t2) + ) | + (EX y1 z1 u2 t2 | t1 = (TTail (Bind Abst) y1 z1) & + x = (TTail (Bind Abbr) u2 t2) & + (pr2 c u1 u2) & (b:?; u:?) + (pr2 (CTail c (Bind b) u) z1 t2) + ) | + (EX b y1 z1 z2 u2 v2 t2 | + ~b=Abst & + t1 = (TTail (Bind b) y1 z1) & + x = (TTail (Bind b) v2 z2) & + (pr2 c u1 u2) & (pr2 c y1 v2) & (pr0 z1 t2)) + ). + Intros; Inversion H; Pr0GenBase; + Try Rewrite H1 in H2; Try Rewrite H4 in H2; Try Rewrite H5 in H2; + Try Subst0GenBase; XDEAuto 7. Qed. - Theorem pr2_gen_cast : (c:?; u1,t1,x:?) - (pr2 c (TTail (Flat Cast) u1 t1) x) -> - (EX u2 t2 | x = (TTail (Flat Cast) u2 t2) & - (pr2 c u1 u2) & (pr2 c t1 t2) - ) \/ - (pr0 t1 x). - Intros; Inversion H; - Try Pr0GenBase; Try Subst0GenBase; XEAuto. + Theorem pr2_gen_cast: (c:?; u1,t1,x:?) + (pr2 c (TTail (Flat Cast) u1 t1) x) -> + (EX u2 t2 | x = (TTail (Flat Cast) u2 t2) & + (pr2 c u1 u2) & (pr2 c t1 t2) + ) \/ + (pr2 c t1 x). + Intros; Inversion H; Pr0GenBase; + Try Rewrite H1 in H2; Try Subst0GenBase; XEAuto. Qed. End pr2_gen_base. Tactic Definition Pr2GenBase := Match Context With - | [ H: (pr2 ?1 (TTail (Bind Abst) ?2 ?3) ?4) |- ? ] -> + | [ H: (pr2 ?1 (TSort ?2) ?3) |- ? ] -> + LApply (pr2_gen_sort ?1 ?3 ?2); [ Clear H; Intros | XAuto ] + | [ H: (pr2 ?1 (TLRef ?2) ?3) |- ? ] -> + LApply (pr2_gen_lref ?1 ?3 ?2); [ Clear H; Intros H | XAuto ]; + XDecompose H + | [ H: (pr2 ?1 (TTail (Bind Abst) ?2 ?3) ?4) |- ? ] -> LApply (pr2_gen_abst ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ]; - XElim H; Intros. + XDecompose H + | [ H: (pr2 ?1 (TTail (Flat Appl) ?2 ?3) ?4) |- ? ] -> + LApply (pr2_gen_appl ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ]; + XDecompose H + | [ H: (pr2 ?1 (TTail (Flat Cast) ?2 ?3) ?4) |- ? ] -> + LApply (pr2_gen_cast ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ]; + XDecompose H. Section pr2_props. (******************************************************) - Theorem pr2_thin_dx : (c:?; t1,t2:?) (pr2 c t1 t2) -> - (u:?; f:?) (pr2 c (TTail (Flat f) u t1) - (TTail (Flat f) u t2)). - Intros; Inversion H; XEAuto. + Theorem pr2_thin_dx: (c:?; t1,t2:?) (pr2 c t1 t2) -> + (u:?; f:?) (pr2 c (TTail (Flat f) u t1) + (TTail (Flat f) u t2)). + Intros; XElim H; XEAuto. Qed. - Theorem pr2_tail_1 : (c:?; u1,u2:?) (pr2 c u1 u2) -> - (k:?; t:?) (pr2 c (TTail k u1 t) (TTail k u2 t)). - Intros; Inversion H; XEAuto. + Theorem pr2_tail_1: (c:?; u1,u2:?) (pr2 c u1 u2) -> + (k:?; t:?) (pr2 c (TTail k u1 t) (TTail k u2 t)). + Intros; XElim H; XEAuto. Qed. - Theorem pr2_tail_2 : (c:?; u,t1,t2:?; k:?) (pr2 (CTail c k u) t1 t2) -> - (pr2 c (TTail k u t1) (TTail k u t2)). - XElim k; Intros; - (Inversion H; [ XAuto | Clear H ]; - (NewInduction i; DropGenBase; [ Inversion H; XEAuto | XEAuto ])). + Theorem pr2_tail_2: (c:?; u,t1,t2:?; k:?) (pr2 (CTail c k u) t1 t2) -> + (pr2 c (TTail k u t1) (TTail k u t2)). + XElim k; Intros; ( + XElim H; [ XAuto | XElim i; Intros; DropGenBase; CGenBase; XEAuto ]). Qed. - + Hints Resolve pr2_tail_2 : ltlc. - Theorem pr2_shift : (i:?; c,e:?) (drop i (0) c e) -> - (t1,t2:?) (pr2 c t1 t2) -> - (pr2 e (app c i t1) (app c i t2)). + Theorem pr2_shift: (i:?; c,e:?) (drop i (0) c e) -> + (t1,t2:?) (pr2 c t1 t2) -> + (pr2 e (app c i t1) (app c i t2)). XElim i. -(* case 1 : i = 0 *) - Intros. - DropGenBase; Rewrite H in H0. +(* case 1: i = 0 *) + Intros; DropGenBase; Rewrite H in H0. Repeat Rewrite app_O; XAuto. -(* case 2 : i > 0 *) +(* case 2: i > 0 *) XElim c. -(* case 2.1 : CSort *) +(* case 2.1: CSort *) Intros; DropGenBase; Rewrite H0; XAuto. -(* case 2.2 : CTail *) +(* case 2.2: CTail *) XElim k; Intros; Simpl; DropGenBase; XAuto. Qed. - + End pr2_props. Hints Resolve pr2_thin_dx pr2_tail_1 pr2_tail_2 pr2_shift : ltlc. diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr2_gen.v b/helm/coq-contribs/LAMBDA-TYPES/pr2_gen.v index 6fcb00c30..98d128233 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/pr2_gen.v +++ b/helm/coq-contribs/LAMBDA-TYPES/pr2_gen.v @@ -1,61 +1,60 @@ (*#* #stop file *) Require subst0_gen. +Require subst0_lift. Require drop_props. Require pr0_gen. +Require pr0_subst0. Require pr2_defs. Section pr2_gen. (********************************************************) - Theorem pr2_gen_abbr : (c:?; u1,t1,x:?) - (pr2 c (TTail (Bind Abbr) u1 t1) x) -> - (EX u2 t2 | x = (TTail (Bind Abbr) u2 t2) & - (pr2 c u1 u2) & - ((b:?; u:?) (pr2 (CTail c (Bind b) u) t1 t2)) \/ - (EX y | (pr0 t1 y) & (subst0 (0) u2 y t2)) - ) \/ - (pr0 t1 (lift (1) (0) x)). - Intros; Inversion H; - Try Pr0Gen; Try Subst0Gen; XDEAuto 8. + Theorem pr2_gen_abbr: (c:?; u1,t1,x:?) + (pr2 c (TTail (Bind Abbr) u1 t1) x) -> + (EX u2 t2 | x = (TTail (Bind Abbr) u2 t2) & + (pr2 c u1 u2) & (OR + (b:?; u:?) (pr2 (CTail c (Bind b) u) t1 t2) | + (EX u | (pr0 u1 u) & (pr2 (CTail c (Bind Abbr) u) t1 t2)) | + (EX y z | (pr2 (CTail c (Bind Abbr) u1) t1 y) & (pr0 y z) & (pr2 (CTail c (Bind Abbr) u1) z t2)) + )) \/ (b:?; u:?) + (pr2 (CTail c (Bind b) u) t1 (lift (1) (0) x)). + Intros; Inversion H; + Pr0Gen; Try Rewrite H1 in H2; Try Subst0Gen; Try Pr0Subst0; XDEAuto 10. Qed. - Theorem pr2_gen_void : (c:?; u1,t1,x:?) - (pr2 c (TTail (Bind Void) u1 t1) x) -> - (EX u2 t2 | x = (TTail (Bind Void) u2 t2) & - (pr2 c u1 u2) & (b:?; u:?) - (pr2 (CTail c (Bind b) u) t1 t2) - ) \/ - (pr0 t1 (lift (1) (0) x)). - Intros; Inversion H; - Try Pr0Gen; Try Subst0Gen; XDEAuto 7. + Theorem pr2_gen_void: (c:?; u1,t1,x:?) + (pr2 c (TTail (Bind Void) u1 t1) x) -> + (EX u2 t2 | x = (TTail (Bind Void) u2 t2) & + (pr2 c u1 u2) & (b:?; u:?) + (pr2 (CTail c (Bind b) u) t1 t2) + ) \/ (b:?; u:?) + (pr2 (CTail c (Bind b) u) t1 (lift (1) (0) x)). + Intros; Inversion H; + Try Pr0Gen; Try Rewrite H1 in H2; Try Subst0Gen; XDEAuto 7. Qed. -(*#* #start file *) - (*#* #caption "generation lemma for lift" *) (*#* #cap #cap c #alpha e in D, t1 in U1, t2 in U2, x in T, d in i *) - Theorem pr2_gen_lift : (c:?; t1,x:?; h,d:?) (pr2 c (lift h d t1) x) -> - (e:?) (drop h d c e) -> - (EX t2 | x = (lift h d t2) & (pr2 e t1 t2)). - -(*#* #stop file *) - + Theorem pr2_gen_lift: (c:?; t1,x:?; h,d:?) (pr2 c (lift h d t1) x) -> + (e:?) (drop h d c e) -> + (EX t2 | x = (lift h d t2) & (pr2 e t1 t2)). Intros. - Inversion H; Clear H. -(* case 1 : pr2_pr0 *) - Pr0Gen; XEAuto. + Inversion H; Clear H; Pr0Gen. +(* case 1 : pr2_free *) + XEAuto. (* case 2 : pr2_delta *) + Rewrite H in H3; Clear H H4 t t2. Apply (lt_le_e i d); Intros. (* case 2.1 : i < d *) - Rewrite (lt_plus_minus i d) in H0; [ Idtac | XAuto ]. - Rewrite (lt_plus_minus i d) in H2; [ Idtac | XAuto ]. - DropDis; Rewrite H0 in H2; Clear H0 u. + Rewrite (lt_plus_minus i d) in H0; [ Idtac | XAuto ]. + Rewrite (lt_plus_minus i d) in H3; [ Idtac | XAuto ]. + DropDis; Rewrite H0 in H3; Clear H0 u. Subst0Gen; Rewrite <- lt_plus_minus in H0; XEAuto. (* case 2.2 : i >= d *) Apply (lt_le_e i (plus d h)); Intros. (* case 2.2.1 : i < d + h *) - EApply subst0_gen_lift_false; [ Apply H | Apply H3 | XEAuto ]. + EApply subst0_gen_lift_false; [ Apply H | Apply H4 | XEAuto ]. (* case 2.2.2 : i >= d + h *) DropDis; Subst0Gen; XEAuto. Qed. @@ -66,16 +65,14 @@ Require pr2_defs. Match Context With | [ H: (pr2 ?1 (TTail (Bind Abbr) ?2 ?3) ?4) |- ? ] -> LApply (pr2_gen_abbr ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ]; - XElim H; - [ Intros H; XElim H; Do 4 Intro; Intros H_x; XElim H_x; - [ Intros | Intros H_x; XElim H_x; Intros ] - | Intros ] + XDecompose H | [ H: (pr2 ?1 (TTail (Bind Void) ?2 ?3) ?4) |- ? ] -> LApply (pr2_gen_void ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ]; - XElim H; [ Intros H; XElim H; Intros | Intros ] + XDecompose H | [ H0: (pr2 ?1 (lift ?2 ?3 ?4) ?5); H1: (drop ?2 ?3 ?1 ?6) |- ? ] -> LApply (pr2_gen_lift ?1 ?4 ?5 ?2 ?3); [ Clear H0; Intros H0 | XAuto ]; LApply (H0 ?6); [ Clear H0; Intros H0 | XAuto ]; - XElim H0; Intros + XDecompose H0 | _ -> Pr2GenBase. + diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr2_gen_context.v b/helm/coq-contribs/LAMBDA-TYPES/pr2_gen_context.v index b2cfaead1..61d2ffef7 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/pr2_gen_context.v +++ b/helm/coq-contribs/LAMBDA-TYPES/pr2_gen_context.v @@ -8,6 +8,7 @@ Require csubst1_defs. Require pr0_gen. Require pr0_subst1. Require pr2_defs. +Require pr2_gen. Require pr2_subst1. Section pr2_gen_context. (************************************************) @@ -20,27 +21,29 @@ Require pr2_subst1. (EX x2 | (subst1 d u t2 (lift (1) d x2)) & (pr2 a x1 x2) ). - Intros until 1; XElim H; Intros. -(* case 1: pr2_pr0 *) - Pr0Subst1; Pr0Gen; Rewrite H in H3; Clear H x; XEAuto. + Intros until 1; XElim H; Intros; + Pr0Subst1; Pr0Gen. +(* case 1: pr2_free *) + Rewrite H in H3; Clear H x; XEAuto. (* case 2: pr2_delta *) + Rewrite H0 in H5; Clear H0 x. Apply (lt_eq_gt_e i d0); Intros. (* case 2.1: i < d0 *) Subst1Confluence; CSubst1Drop. Rewrite minus_x_Sy in H; [ Idtac | XAuto ]. - CSubst1GenBase; Rewrite H in H6; Clear H x0. - Rewrite (lt_plus_minus i d0) in H3; [ Idtac | XAuto ]. - DropDis; Rewrite H in H7; Clear H x2. + CSubst1GenBase; Rewrite H in H7; Clear H x2. + Rewrite (lt_plus_minus i d0) in H4; [ Idtac | XAuto ]. + DropDis; Rewrite H in H8; Clear H x3. Subst1Subst1; Pattern 2 d0 in H; Rewrite (lt_plus_minus i d0) in H; [ Idtac | XAuto ]. - Subst1Gen; Rewrite H in H9; Simpl in H9; Clear H x2. - Rewrite <- lt_plus_minus in H9; [ Idtac | XAuto ]. - Rewrite <- lt_plus_minus_r in H9; XEAuto. + Subst1Gen; Rewrite H in H10; Simpl in H10; Clear H x3. + Rewrite <- lt_plus_minus in H10; [ Idtac | XAuto ]. + Rewrite <- lt_plus_minus_r in H10; XEAuto. (* case 2.2: i = d0 *) - Rewrite H5 in H; Rewrite H5 in H0; Clear H5 i. - DropDis; Inversion H; Rewrite <- H7 in H0; Rewrite <- H7 in H1; Rewrite <- H7; Clear H H6 H7 e u. + Rewrite H0 in H; Rewrite H0 in H1; Clear H0 i. + DropDis; Inversion H; Rewrite <- H8 in H1; Rewrite <- H8 in H2; Rewrite <- H8; Clear H H7 H8 e u. Subst1Confluence; Subst1Gen; Rewrite H0 in H; Clear H0 x; XEAuto. (* case 2.3: i > d0 *) - Subst1Confluence; Subst1Gen; Rewrite H4 in H0; Clear H1 H4 x. + Subst1Confluence; Subst1Gen; Rewrite H5 in H1; Clear H2 H5 x. CSubst1Drop; DropDis; XEAuto. Qed. diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr2_lift.v b/helm/coq-contribs/LAMBDA-TYPES/pr2_lift.v index 9f828bfa8..3546cb5f2 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/pr2_lift.v +++ b/helm/coq-contribs/LAMBDA-TYPES/pr2_lift.v @@ -1,3 +1,5 @@ +(*#* #stop file *) + Require subst0_lift. Require drop_props. Require pr0_lift. @@ -14,11 +16,8 @@ Require pr2_defs. Theorem pr2_lift : (c,e:?; h,d:?) (drop h d c e) -> (t1,t2:?) (pr2 e t1 t2) -> (pr2 c (lift h d t1) (lift h d t2)). - -(*#* #stop file *) - Intros until 2; XElim H0; Intros. -(* case 1 : pr2_pr0 *) +(* case 1 : pr2_free *) XAuto. (* case 2 : pr2_delta *) Apply (lt_le_e i d); Intros; DropDis. diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr2_subst1.v b/helm/coq-contribs/LAMBDA-TYPES/pr2_subst1.v index 988237fc1..5c7302875 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/pr2_subst1.v +++ b/helm/coq-contribs/LAMBDA-TYPES/pr2_subst1.v @@ -9,8 +9,9 @@ Require pr2_defs. Section pr2_subst1_props. (***********************************************) Theorem pr2_delta1: (c,d:?; u:?; i:?) (drop i (0) c (CTail d (Bind Abbr) u)) -> - (t1,t2:?) (subst1 i u t1 t2) -> (pr2 c t1 t2). - Intros; XElim H0; Clear t2; XEAuto. + (t1,t2:?) (pr0 t1 t2) -> (t:?) (subst1 i u t2 t) -> + (pr2 c t1 t). + Intros; XElim H1; Clear t; XEAuto. Qed. Hints Resolve pr2_delta1 : ltlc. @@ -19,16 +20,17 @@ Require pr2_defs. (t1,t2:?) (pr2 c t1 t2) -> (w1:?) (subst1 i v t1 w1) -> (EX w2 | (pr2 c w1 w2) & (subst1 i v t2 w2)). - Intros until 2; XElim H0; Intros. -(* case 1: pr2_pr0 *) - Pr0Subst1; XEAuto. + Intros until 2; XElim H0; Intros; + Pr0Subst1. +(* case 1: pr2_free *) + XEAuto. (* case 2: pr2_delta *) Apply (neq_eq_e i i0); Intros. (* case 2.1: i <> i0 *) Subst1Confluence; XEAuto. (* case 2.2: i = i0 *) - Rewrite <- H3 in H0; Rewrite <- H3 in H1; Clear H3 i0. - DropDis; Inversion H0; Rewrite H5 in H2; Clear H0 H4 H5 e v. + Rewrite <- H4 in H0; Rewrite <- H4 in H2; Clear H4 i0. + DropDis; Inversion H0; Rewrite H6 in H3; Clear H0 H5 H6 e v. Subst1Confluence; XEAuto. Qed. diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr3_confluence.v b/helm/coq-contribs/LAMBDA-TYPES/pr3_confluence.v index 2267e88ae..6f5019bc9 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/pr3_confluence.v +++ b/helm/coq-contribs/LAMBDA-TYPES/pr3_confluence.v @@ -3,24 +3,23 @@ Require pr3_defs. Section pr3_confluence. (*************************************************) +(*#* #stop theorem *) + (*#* #caption "confluence with single step reduction: strip lemma" *) (*#* #cap #cap c, t0, t1, t2, t *) Theorem pr3_strip : (c:?; t0,t1:?) (pr3 c t0 t1) -> (t2:?) (pr2 c t0 t2) -> (EX t | (pr3 c t1 t) & (pr3 c t2 t)). - -(*#* #stop proof *) - Intros until 1; XElim H; Intros. -(* case 1 : pr3_r *) +(* case 1 : pr3_refl *) XEAuto. -(* case 2 : pr3_u *) +(* case 2 : pr3_sing *) Pr2Confluence. LApply (H1 x); [ Clear H1 H2; Intros H1 | XAuto ]. XElim H1; Intros; XEAuto. Qed. -(*#* #start proof *) +(*#* #start theorem *) (*#* #caption "confluence with itself: Church-Rosser property" *) (*#* #cap #cap c, t0, t1, t2, t *) @@ -31,9 +30,9 @@ Require pr3_defs. (*#* #stop file *) Intros until 1; XElim H; Intros. -(* case 1 : pr3_r *) +(* case 1 : pr3_refl *) XEAuto. -(* case 2 : pr3_u *) +(* case 2 : pr3_sing *) LApply (pr3_strip c t3 t5); [ Clear H2; Intros H2 | XAuto ]. LApply (H2 t2); [ Clear H H2; Intros H | XAuto ]. XElim H; Intros. diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr3_defs.v b/helm/coq-contribs/LAMBDA-TYPES/pr3_defs.v index 1d67abfb1..1e5b04249 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/pr3_defs.v +++ b/helm/coq-contribs/LAMBDA-TYPES/pr3_defs.v @@ -1,67 +1,180 @@ -(*#* #stop file *) - Require Export pr1_defs. Require Export pr2_defs. +(*#* #caption "axioms for the relation $\\PrT{}{}{}$", + "reflexivity", "single step transitivity" +*) +(*#* #cap #cap c, t, t1, t2, t3 *) + Inductive pr3 [c:C] : T -> T -> Prop := - | pr3_r : (t:?) (pr3 c t t) - | pr3_u : (t2,t1:?) (pr2 c t1 t2) -> - (t3:?) (pr3 c t2 t3) -> (pr3 c t1 t3). + | pr3_refl: (t:?) (pr3 c t t) + | pr3_sing: (t2,t1:?) (pr2 c t1 t2) -> + (t3:?) (pr3 c t2 t3) -> (pr3 c t1 t3). + +(*#* #stop file *) Hint pr3: ltlc := Constructors pr3. + Section pr3_gen_base. (***************************************************) + + Theorem pr3_gen_sort: (c:?; x:?; n:?) (pr3 c (TSort n) x) -> + x = (TSort n). + Intros; InsertEq H '(TSort n); XElim H; Clear y x; Intros. +(* case 1: pr3_refl *) + XAuto. +(* case 2: pr3_sing *) + Rewrite H2 in H; Clear H2 t1; Pr2GenBase; XAuto. + Qed. + + Tactic Definition IH := + Match Context With + | [ H: (u,t:T) (TTail (Bind Abst) ?1 ?2) = (TTail (Bind Abst) u t) -> ? |- ? ] -> + LApply (H ?1 ?2); [ Clear H; Intros H | XAuto ]; + XDecompose H + | [ H: (u,t:T) (TTail (Flat Appl) ?1 ?2) = (TTail (Flat Appl) u t) -> ? |- ? ] -> + LApply (H ?1 ?2); [ Clear H; Intros H | XAuto ]; + XDecompose H + | [ H: (u,t:T) (TTail (Flat Cast) ?1 ?2) = (TTail (Flat Cast) u t) -> ? |- ? ] -> + LApply (H ?1 ?2); [ Clear H; Intros H | XAuto ]; + XDecompose H. + + Theorem pr3_gen_abst: (c:?; u1,t1,x:?) + (pr3 c (TTail (Bind Abst) u1 t1) x) -> + (EX u2 t2 | x = (TTail (Bind Abst) u2 t2) & + (pr3 c u1 u2) & (b:?; u:?) + (pr3 (CTail c (Bind b) u) t1 t2) + ). + Intros until 1; InsertEq H '(TTail (Bind Abst) u1 t1); + UnIntro H t1; UnIntro H u1; XElim H; Clear y x; Intros; + Rename x into u0; Rename x0 into t0. +(* case 1 : pr3_refl *) + XEAuto. +(* case 2 : pr3_sing *) + Rewrite H2 in H; Clear H0 H2 t1; Pr2GenBase. + Rewrite H0 in H1; Clear H0 t2; IH; XEAuto. + Qed. + + Theorem pr3_gen_appl: (c:?; u1,t1,x:?) + (pr3 c (TTail (Flat Appl) u1 t1) x) -> (OR + (EX u2 t2 | x = (TTail (Flat Appl) u2 t2) & + (pr3 c u1 u2) & (pr3 c t1 t2) + ) | + (EX y1 z1 u2 t2 | (pr3 c (TTail (Bind Abbr) u2 t2) x) & + (pr3 c u1 u2) & + (pr3 c t1 (TTail (Bind Abst) y1 z1)) & + (b:?; u:?) (pr3 (CTail c (Bind b) u) z1 t2) + ) | + (EX b y1 z1 z2 u2 v2 t2 | + (pr3 c (TTail (Bind b) v2 z2) x) & ~b=Abst & + (pr3 c u1 u2) & + (pr3 c t1 (TTail (Bind b) y1 z1)) & + (pr3 c y1 v2) & (pr0 z1 t2)) + ). + Intros; InsertEq H '(TTail (Flat Appl) u1 t1). + UnIntro t1 H; UnIntro u1 H. + XElim H; Clear y x; Intros; + Rename x into u0; Rename x0 into t0. +(* case 1: pr3_refl *) + XEAuto. +(* case 2: pr3_sing *) + Rewrite H2 in H; Clear H2 t1; Pr2GenBase. +(* case 2.1: short step: compatibility *) + Rewrite H3 in H1; Clear H0 H3 t2. + IH; Try (Rewrite H0; Clear H0 t3); XDEAuto 6. +(* case 2.2: short step: beta *) + Rewrite H4 in H0; Rewrite H3; Clear H1 H3 H4 t0 t2; XEAuto. +(* case 2.3: short step: upsilon *) + Rewrite H5 in H0; Rewrite H4; Clear H1 H4 H5 t0 t2; XEAuto. + Qed. + + Theorem pr3_gen_cast: (c:?; u1,t1,x:?) + (pr3 c (TTail (Flat Cast) u1 t1) x) -> + (EX u2 t2 | x = (TTail (Flat Cast) u2 t2) & + (pr3 c u1 u2) & (pr3 c t1 t2) + ) \/ + (pr3 c t1 x). + Intros; InsertEq H '(TTail (Flat Cast) u1 t1); + UnIntro H t1; UnIntro H u1; XElim H; Clear y x; Intros; + Rename x into u0; Rename x0 into t0. +(* case 1: pr3_refl *) + Rewrite H; Clear H t; XEAuto. +(* case 2: pr3_sing *) + Rewrite H2 in H; Clear H2 t1; Pr2GenBase. +(* case 2.1: short step: compatinility *) + Rewrite H3 in H1; Clear H0 H3 t2; + IH; Try Rewrite H0; XEAuto. +(* case 2.2: short step: epsilon *) + XEAuto. + Qed. + + End pr3_gen_base. + + Tactic Definition Pr3GenBase := + Match Context With + | [ H: (pr3 ?1 (TSort ?2) ?3) |- ? ] -> + LApply (pr3_gen_sort ?1 ?3 ?2); [ Clear H; Intros | XAuto ] + | [ H: (pr3 ?1 (TTail (Bind Abst) ?2 ?3) ?4) |- ? ] -> + LApply (pr3_gen_abst ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ]; + XDecompose H + | [ H: (pr3 ?1 (TTail (Flat Appl) ?2 ?3) ?4) |- ? ] -> + LApply (pr3_gen_appl ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ]; + XDecompose H + | [ H: (pr3 ?1 (TTail (Flat Cast) ?2 ?3) ?4) |- ? ] -> + LApply (pr3_gen_cast ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ]; + XDecompose H. + Section pr3_props. (******************************************************) - Theorem pr3_pr2 : (c,t1,t2:?) (pr2 c t1 t2) -> (pr3 c t1 t2). + Theorem pr3_pr2: (c,t1,t2:?) (pr2 c t1 t2) -> (pr3 c t1 t2). XEAuto. Qed. - Theorem pr3_t : (t2,t1,c:?) (pr3 c t1 t2) -> + Theorem pr3_t: (t2,t1,c:?) (pr3 c t1 t2) -> (t3:?) (pr3 c t2 t3) -> (pr3 c t1 t3). Intros until 1; XElim H; XEAuto. Qed. - Theorem pr3_tail_1 : (c:?; u1,u2:?) (pr3 c u1 u2) -> - (k:?; t:?) (pr3 c (TTail k u1 t) (TTail k u2 t)). + Theorem pr3_tail_1: (c:?; u1,u2:?) (pr3 c u1 u2) -> + (k:?; t:?) (pr3 c (TTail k u1 t) (TTail k u2 t)). Intros until 1; XElim H; Intros. -(* case 1 : pr3_r *) +(* case 1: pr3_refl *) XAuto. -(* case 2 : pr3_u *) - EApply pr3_u; [ Apply pr2_tail_1; Apply H | XAuto ]. +(* case 2: pr3_sing *) + EApply pr3_sing; [ Apply pr2_tail_1; Apply H | XAuto ]. Qed. - Theorem pr3_tail_2 : (c:?; u,t1,t2:?; k:?) (pr3 (CTail c k u) t1 t2) -> - (pr3 c (TTail k u t1) (TTail k u t2)). + Theorem pr3_tail_2: (c:?; u,t1,t2:?; k:?) (pr3 (CTail c k u) t1 t2) -> + (pr3 c (TTail k u t1) (TTail k u t2)). Intros until 1; XElim H; Intros. -(* case 1 : pr3_r *) +(* case 1: pr3_refl *) XAuto. -(* case 2 : pr3_u *) - EApply pr3_u; [ Apply pr2_tail_2; Apply H | XAuto ]. +(* case 2: pr3_sing *) + EApply pr3_sing; [ Apply pr2_tail_2; Apply H | XAuto ]. Qed. Hints Resolve pr3_tail_1 pr3_tail_2 : ltlc. - Theorem pr3_tail_21 : (c:?; u1,u2:?) (pr3 c u1 u2) -> - (k:?; t1,t2:?) (pr3 (CTail c k u1) t1 t2) -> - (pr3 c (TTail k u1 t1) (TTail k u2 t2)). + Theorem pr3_tail_21: (c:?; u1,u2:?) (pr3 c u1 u2) -> + (k:?; t1,t2:?) (pr3 (CTail c k u1) t1 t2) -> + (pr3 c (TTail k u1 t1) (TTail k u2 t2)). Intros. EApply pr3_t; [ Apply pr3_tail_2 | Apply pr3_tail_1 ]; XAuto. Qed. - Theorem pr3_tail_12 : (c:?; u1,u2:?) (pr3 c u1 u2) -> - (k:?; t1,t2:?) (pr3 (CTail c k u2) t1 t2) -> - (pr3 c (TTail k u1 t1) (TTail k u2 t2)). + Theorem pr3_tail_12: (c:?; u1,u2:?) (pr3 c u1 u2) -> + (k:?; t1,t2:?) (pr3 (CTail c k u2) t1 t2) -> + (pr3 c (TTail k u1 t1) (TTail k u2 t2)). Intros. EApply pr3_t; [ Apply pr3_tail_1 | Apply pr3_tail_2 ]; XAuto. Qed. - Theorem pr3_shift : (h:?; c,e:?) (drop h (0) c e) -> - (t1,t2:?) (pr3 c t1 t2) -> - (pr3 e (app c h t1) (app c h t2)). + Theorem pr3_shift: (h:?; c,e:?) (drop h (0) c e) -> + (t1,t2:?) (pr3 c t1 t2) -> + (pr3 e (app c h t1) (app c h t2)). Intros until 2; XElim H0; Clear t1 t2; Intros. -(* case 1 : pr3_r *) +(* case 1: pr3_refl *) XAuto. -(* case 2 : pr3_u *) +(* case 2: pr3_sing *) XEAuto. Qed. diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr3_gen.v b/helm/coq-contribs/LAMBDA-TYPES/pr3_gen.v index 855c4deab..e96f49fc3 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/pr3_gen.v +++ b/helm/coq-contribs/LAMBDA-TYPES/pr3_gen.v @@ -4,181 +4,129 @@ Require pr2_gen. Require pr3_defs. Require pr3_props. - Section pr3_gen_void. (***************************************************) + Section pr3_gen_lift. (***************************************************) + +(*#* #caption "generation lemma for lift" *) +(*#* #cap #cap c #alpha e in D, t1 in U1, t2 in U2, x in T, d in i *) + + Theorem pr3_gen_lift: (c:?; t1,x:?; h,d:?) (pr3 c (lift h d t1) x) -> + (e:?) (drop h d c e) -> + (EX t2 | x = (lift h d t2) & (pr3 e t1 t2)). + Intros until 1; InsertEq H '(lift h d t1); + UnIntro H t1; XElim H; Clear y x; Intros; Rename x into t4. +(* case 1 : pr3_refl *) + XEAuto. +(* case 2 : pr3_sing *) + Rewrite H2 in H; Pr2Gen. + LApply (H1 x); [ Clear H1; Intros H1 | XAuto ]. + LApply (H1 e); [ Clear H1; Intros H1 | XAuto ]. + XElim H1; XEAuto. + Qed. + + End pr3_gen_lift. + + Section pr3_gen_lref. (***************************************************) + + Theorem pr3_gen_lref: (c:?; x:?; n:?) (pr3 c (TLRef n) x) -> + x = (TLRef n) \/ + (EX d u v | (drop n (0) c (CTail d (Bind Abbr) u)) & + (pr3 d u v) & + x = (lift (S n) (0) v) + ). + Intros; InsertEq H '(TLRef n); XElim H; Clear y x; Intros. +(* case 1: pr3_refl *) + XAuto. +(* case 2: pr3_sing *) + Rewrite H2 in H; Clear H2 t1; Pr2GenBase. +(* case 2.1: pr2_free *) + XAuto. +(* case 2.2: pr2_delta *) + Rewrite H4 in H0; Clear H1 H4 t2. + LApply (pr3_gen_lift c x1 t3 (S n) (0)); [ Clear H0; Intros | XAuto ]. + LApply (H x0); [ Clear H; Intros | XEAuto ]. + XElim H; XEAuto. + Qed. + + End pr3_gen_lref. + + Section pr3_gen_bind. (***************************************************) Tactic Definition IH := Match Context With - [ H: (u,t:T) (TTail (Bind Void) ?1 ?2) = (TTail (Bind Void) u t) -> ? |- ? ] -> + | [ H: (u,t:T) (TTail (Bind Void) ?1 ?2) = (TTail (Bind Void) u t) -> ? |- ? ] -> LApply (H ?1 ?2); [ Clear H; Intros H | XAuto ]; - XElim H1; Intros H1; XElim H1; Intros. - - Theorem pr3_gen_void : (c:?; u1,t1,x:?) (pr3 c (TTail (Bind Void) u1 t1) x) -> - (EX u2 t2 | x = (TTail (Bind Void) u2 t2) & - (pr3 c u1 u2) & (b:?; u:?) - (pr3 (CTail c (Bind b) u) t1 t2) - ) \/ - (EX u | (pr3 c u1 u) & - (pr3 (CTail c (Bind Void) u) t1 (lift (1) (0) x)) - ). + XDecompose H + | [ H: (u,t:T) (TTail (Bind Abbr) ?1 ?2) = (TTail (Bind Abbr) u t) -> ? |- ? ] -> + LApply (H ?1 ?2); [ Clear H; Intros H | XAuto ]; + XDecompose H. + + Theorem pr3_gen_void: (c:?; u1,t1,x:?) (pr3 c (TTail (Bind Void) u1 t1) x) -> + (EX u2 t2 | x = (TTail (Bind Void) u2 t2) & + (pr3 c u1 u2) & (b:?; u:?) + (pr3 (CTail c (Bind b) u) t1 t2) + ) \/ + (pr3 (CTail c (Bind Void) u1) t1 (lift (1) (0) x)). Intros until 1; InsertEq H '(TTail (Bind Void) u1 t1); UnIntro t1 H; UnIntro u1 H; XElim H; Intros. -(* case 1 : pr3_r *) +(* case 1 : pr3_refl *) Rewrite H; XEAuto. -(* case 2 : pr3_u *) +(* case 2 : pr3_sing *) Rewrite H2 in H; Clear H2 t0; Pr2Gen. (* case 2.1 : short step: compatibility *) - Rewrite H in H0; Rewrite H in H1; Clear H t2; IH. -(* case 2.1.1 : long step: compatibility *) - Rewrite H; Rewrite H in H0; XEAuto. -(* case 2.1.2 : long step: zeta *) - XEAuto. + Rewrite H3 in H1; Clear H0 H3 t2. + IH; Try Pr3Context; Try Rewrite H2; XEAuto. (* case 2.2 : short step: zeta *) - Clear H1; Right. - EApply ex2_intro; [ XAuto | Idtac ]. - EApply pr3_u; [ Idtac | EApply pr3_lift ]. - XEAuto. XAuto. XAuto. + XEAuto. Qed. - End pr3_gen_void. - - Section pr3_gen_abbr. (***************************************************) - - Tactic Definition IH := - LApply (H1 x0 x1); [ Clear H1; Intros H1 | XAuto ]; - XElim H1; - [ Intros H1; XElim H1; - Do 4 Intro; Intros H_x; XElim H_x; - [ Intros | Intros H_x; XElim H_x; Intros ] - | Intros H1; XElim H1; Intros ]. - - Theorem pr3_gen_abbr : (c:?; u1,t1,x:?) (pr3 c (TTail (Bind Abbr) u1 t1) x) -> - (EX u2 t2 | x = (TTail (Bind Abbr) u2 t2) & - (pr3 c u1 u2) & - ((b:?; u:?) (pr3 (CTail c (Bind b) u) t1 t2)) \/ - (EX u3 t3 y | (pr3 c (TTail (Bind Abbr) u3 t3) x) & - (pr3 c u1 u3) & - (b:?; u:?) (pr3 (CTail c (Bind b) u) t1 y) & - (subst0 (0) u3 y t3) - ) - ) \/ - (EX u | (pr3 c u1 u) & - (pr3 (CTail c (Bind Abbr) u) t1 (lift (1) (0) x)) - ). + Theorem pr3_gen_abbr: (c:?; u1,t1,x:?) (pr3 c (TTail (Bind Abbr) u1 t1) x) -> + (EX u2 t2 | x = (TTail (Bind Abbr) u2 t2) & + (pr3 c u1 u2) & + (pr3 (CTail c (Bind Abbr) u1) t1 t2) + ) \/ + (pr3 (CTail c (Bind Abbr) u1) t1 (lift (1) (0) x)). Intros until 1; InsertEq H '(TTail (Bind Abbr) u1 t1); UnIntro H t1; UnIntro H u1; XElim H; Clear y x; Intros; Rename x into u1; Rename x0 into t4. -(* case 1 : pr3_r *) +(* case 1: pr3_refl *) Rewrite H; XEAuto. -(* case 2 : pr3_u *) +(* case 2: pr3_sing *) Rewrite H2 in H; Clear H2 t1; Pr2Gen. -(* case 2.1 : short step: compatibility *) - Rewrite H in H0; Rewrite H in H1; Clear H t2; IH. -(* case 2.1.1 : long step: compatibility *) - Rewrite H; Rewrite H in H0; Clear H t3. - Left; EApply ex3_2_intro; XEAuto. -(* case 2.1.2 : long step: delta *) - Rewrite H; Rewrite H in H0; Rewrite H in H4; Clear H t3. - Left; EApply ex3_2_intro; - [ XEAuto | XEAuto - | Right; EApply ex4_3_intro; - [ EApply pr3_t; [ XAuto | Apply H4 ] | XEAuto | Idtac | Apply H7 ] ]. +(* case 2.1: short step: compatibility *) + Rewrite H3 in H1; Clear H0 H3 t2. + IH; Repeat Pr3Context; + Try (Rewrite H0; Clear H0 t3; Left; EApply ex3_2_intro); XEAuto. -(* case 2.1.3 : long step: zeta *) +(* case 2.2: short step: beta *) + Rewrite H3 in H1; Clear H0 H3 t1. + IH; Repeat Pr3Context; + Try (Rewrite H0; Clear H0 t3; Left; EApply ex3_2_intro); XEAuto. -(* case 2.2 : short step: delta *) - Rewrite H in H0; Rewrite H in H1; Clear H t2; IH. -(* case 2.2.1 : long step: compatibility *) - Left; EApply ex3_2_intro; - [ XEAuto | XEAuto - | Right; EApply ex4_3_intro; [ Rewrite H | Idtac | Idtac | Apply H4 ] ]. - XAuto. XAuto. XAuto. -(* case 2.2.2 : long step: delta *) - Left; EApply ex3_2_intro; - [ XEAuto | XEAuto - | Right; EApply ex4_3_intro; - [ EApply pr3_t; [ Apply pr3_tail_12 | Apply H5 ] - | Idtac | Idtac | Apply H4 ] ]. - XAuto. EApply pr3_t; [ Apply H7 | XEAuto ]. XAuto. XAuto. -(* case 2.2.3 : long step: zeta *) - Right; Apply ex2_intro with x := x0; [ XAuto | Idtac ]. - Apply pr3_u with t2 := x; [ XAuto | Idtac ]. - Apply pr3_u with t2 := x1; [ XEAuto | Idtac ]. - Pr3Context; XAuto. -(* case 2.3 : short step: zeta *) - Clear H1; Right. - EApply ex2_intro; [ XAuto | Idtac ]. - EApply pr3_u; [ Idtac | EApply pr3_lift ]. - XEAuto. XAuto. XAuto. - Qed. - - End pr3_gen_abbr. - - Section pr3_gen_abst. (***************************************************) - - Theorem pr3_gen_abst : (c:?; u1,t1,x:?) - (pr3 c (TTail (Bind Abst) u1 t1) x) -> - (EX u2 t2 | x = (TTail (Bind Abst) u2 t2) & - (pr3 c u1 u2) & (b:?; u:?) - (pr3 (CTail c (Bind b) u) t1 t2) - ). - Intros until 1; InsertEq H '(TTail (Bind Abst) u1 t1); - UnIntro H t1; UnIntro H u1; XElim H; Clear y x; Intros; - Rename x into u1; Rename x0 into t4. -(* case 1 : pr3_r *) - Rewrite H; XEAuto. -(* case 2 : pr3_u *) - Rewrite H2 in H; Clear H2 t1. - Pr2GenBase. - LApply (H1 x0 x1); [ Clear H H1; Intros | XAuto ]. - XElim H; XEAuto. - Qed. - - End pr3_gen_abst. - - Section pr3_gen_lift. (***************************************************) - -(*#* #start file *) - -(*#* #caption "generation lemma for lift" *) -(*#* #cap #cap c #alpha e in D, t1 in U1, t2 in U2, x in T, d in i *) - - Theorem pr3_gen_lift : (c:?; t1,x:?; h,d:?) (pr3 c (lift h d t1) x) -> - (e:?) (drop h d c e) -> - (EX t2 | x = (lift h d t2) & (pr3 e t1 t2)). - -(*#* #stop file *) - - Intros until 1; InsertEq H '(lift h d t1); - UnIntro H t1; XElim H; Clear y x; Intros; Rename x into t4. -(* case 1 : pr3_r *) +(* case 2.3: short step: delta *) + Rewrite H3 in H1; Clear H0 H3 t2. + IH; Repeat Pr3Context; + Try (Rewrite H0; Clear H0 t3; Left; EApply ex3_2_intro); + XDEAuto 7. +(* case 2.4: short step: zeta *) XEAuto. -(* case 2 : pr3_u *) - Rewrite H2 in H; Pr2Gen. - LApply (H1 x); [ Clear H1; Intros H1 | XAuto ]. - LApply (H1 e); [ Clear H1; Intros H1 | XAuto ]. - XElim H1; XEAuto. Qed. - End pr3_gen_lift. + End pr3_gen_bind. Tactic Definition Pr3Gen := Match Context With - | [ H: (pr3 ?1 (TTail (Bind Abst) ?2 ?3) ?4) |- ? ] -> - LApply (pr3_gen_abst ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ]; - XElim H; Intros - | [ H: (pr3 ?1 (TTail (Bind Abbr) ?2 ?3) ?4) |- ? ] -> - LApply (pr3_gen_abbr ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ]; - XElim H; - [ Intros H; XElim H; - Do 4 Intro; Intros H_x; XElim H_x; - [ Intros | Intros H_x; XElim H_x; Intros ] - | Intros H; XElim H; Intros ] + | [ H: (pr3 ?1 (TLRef ?2) ?3) |- ? ] -> + LApply (pr3_gen_lref ?1 ?3 ?2); [ Clear H; Intros H | XAuto ]; + XDecompose H | [ H: (pr3 ?1 (TTail (Bind Void) ?2 ?3) ?4) |- ? ] -> LApply (pr3_gen_void ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ]; - XElim H; Intros H; XElim H; Intros + XDecompose H + | [ H: (pr3 ?1 (TTail (Bind Abbr) ?2 ?3) ?4) |- ? ] -> + LApply (pr3_gen_abbr ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ]; + XDecompose H | [ H0: (pr3 ?1 (lift ?2 ?3 ?4) ?5); H1: (drop ?2 ?3 ?1 ?6) |- ? ] -> LApply (pr3_gen_lift ?1 ?4 ?5 ?2 ?3); [ Clear H0; Intros H0 | XAuto ]; LApply (H0 ?6); [ Clear H0; Intros H0 | XAuto ]; - XElim H0; Intros - | _ -> Pr2Gen. + XDecompose H0 + | _ -> Pr3GenBase. diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr3_gen_context.v b/helm/coq-contribs/LAMBDA-TYPES/pr3_gen_context.v index f0662babe..a7f3e92be 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/pr3_gen_context.v +++ b/helm/coq-contribs/LAMBDA-TYPES/pr3_gen_context.v @@ -15,9 +15,9 @@ Require pr3_defs. (pr3 a x1 x2) ). Intros until 1; XElim H; Intros. -(* case 1: pr3_r *) +(* case 1: pr3_refl *) XEAuto. -(* case 1: pr3_r *) +(* case 1: pr3_refl *) Pr2GenContext. LApply (H1 e u d); [ Clear H1; Intros H1 | XAuto ]. LApply (H1 a0); [ Clear H1; Intros H1 | XAuto ]. diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr3_subst1.v b/helm/coq-contribs/LAMBDA-TYPES/pr3_subst1.v index 78c9834d5..3db6ce000 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/pr3_subst1.v +++ b/helm/coq-contribs/LAMBDA-TYPES/pr3_subst1.v @@ -30,4 +30,3 @@ Require pr3_defs. LApply (H1 ?7); [ Clear H1; Intros H1 | XAuto ]; XElim H1; Intros | _ -> Pr2Subst1. - diff --git a/helm/coq-contribs/LAMBDA-TYPES/terms_defs.v b/helm/coq-contribs/LAMBDA-TYPES/terms_defs.v index 157cb7456..37d8de88d 100644 --- a/helm/coq-contribs/LAMBDA-TYPES/terms_defs.v +++ b/helm/coq-contribs/LAMBDA-TYPES/terms_defs.v @@ -13,11 +13,16 @@ Require Export Base. | Flat : F -> K. Inductive Set T := TSort : nat -> T - | TBRef : nat -> T + | TLRef : nat -> T | TTail : K -> T -> T -> T. Hint f3KTT : ltlc := Resolve (f_equal3 K T T). + Tactic Definition TGenBase := + Match Context With + | [ H: (TTail ? ? ?) = (TTail ? ? ?) |- ? ] -> Inversion H; Clear H + | _ -> Idtac. + Definition s: K -> nat -> nat := [k;i] Cases k of | (Bind _) => (S i) | (Flat _) => i -- 2.39.2