From 37d40349c3c82a62a8cbced18545bfd526ebe7ff Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 29 Aug 2011 15:21:40 +0000 Subject: [PATCH] - we shared the atomic term constructions - we fixed the notation of the binary term construction - we inverted the dependences of cl_shift and cl_weight --- .../lambda-delta/Basic-2/grammar/cl_shift.ma | 12 +- .../lambda-delta/Basic-2/grammar/cl_weight.ma | 15 +- .../lambda-delta/Basic-2/grammar/item.ma | 20 ++- .../lambda-delta/Basic-2/grammar/term.ma | 11 +- .../Basic-2/grammar/term_simple.ma | 6 +- .../Basic-2/grammar/term_weight.ma | 3 +- .../lambda-delta/Basic-2/grammar/thom.ma | 7 +- .../contribs/lambda-delta/Basic-2/notation.ma | 12 +- .../lambda-delta/Basic-2/reduction/cpr.ma | 2 +- .../lambda-delta/Basic-2/reduction/tpr.ma | 153 +++++++----------- .../Basic-2/reduction/tpr_lift.ma | 30 ++-- .../lambda-delta/Basic-2/reduction/tpr_tpr.ma | 61 ++++--- .../lambda-delta/Basic-2/substitution/drop.ma | 2 +- .../lambda-delta/Basic-2/substitution/lift.ma | 8 +- .../lambda-delta/Basic-2/substitution/tps.ma | 13 +- .../Basic-2/substitution/tps_lift.ma | 26 ++- .../Basic-2/substitution/tps_tps.ma | 2 - 17 files changed, 166 insertions(+), 217 deletions(-) diff --git a/matita/matita/contribs/lambda-delta/Basic-2/grammar/cl_shift.ma b/matita/matita/contribs/lambda-delta/Basic-2/grammar/cl_shift.ma index df96372be..50898bbef 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/grammar/cl_shift.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/grammar/cl_shift.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic-2/grammar/cl_weight.ma". +include "Basic-2/grammar/lenv.ma". (* SHIFT OF A CLOSURE *******************************************************) @@ -22,13 +22,3 @@ let rec shift L T on L ≝ match L with ]. interpretation "shift (closure)" 'Append L T = (shift L T). - -(* Basic properties *********************************************************) - -lemma tw_shift: ∀L,T. #[L, T] ≤ #[L @ T]. -#L elim L // -#K #I #V #IHL #T -@transitive_le [3: @IHL |2: /2/ | skip ] -qed. - - diff --git a/matita/matita/contribs/lambda-delta/Basic-2/grammar/cl_weight.ma b/matita/matita/contribs/lambda-delta/Basic-2/grammar/cl_weight.ma index b501ef3e5..899da0720 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/grammar/cl_weight.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/grammar/cl_weight.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "Basic-2/grammar/lenv_weight.ma". +include "Basic-2/grammar/cl_shift.ma". (* WEIGHT OF A CLOSURE ******************************************************) @@ -22,10 +23,16 @@ interpretation "weight (closure)" 'Weight L T = (cw L T). (* Basic properties *********************************************************) -lemma cw_shift: ∀K,I,V,T. #[K. 𝕓{I} V, T] < #[K, 𝕓{I} V. T]. -normalize // -qed. - axiom cw_wf_ind: ∀R:lenv→term→Prop. (∀L2,T2. (∀L1,T1. #[L1,T1] < #[L2,T2] → R L1 T1) → R L2 T2) → ∀L,T. R L T. + +lemma cw_shift: ∀K,I,V,T. #[K. 𝕓{I} V, T] < #[K, 𝕔{I} V. T]. +normalize // +qed. + +lemma tw_shift: ∀L,T. #[L, T] ≤ #[L @ T]. +#L elim L // +#K #I #V #IHL #T +@transitive_le [3: @IHL |2: /2/ | skip ] +qed. diff --git a/matita/matita/contribs/lambda-delta/Basic-2/grammar/item.ma b/matita/matita/contribs/lambda-delta/Basic-2/grammar/item.ma index 37b5d18af..b594c5a12 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/grammar/item.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/grammar/item.ma @@ -21,24 +21,30 @@ include "Ground-2/list.ma". include "Basic-2/notation.ma". -(* BINARY ITEMS *************************************************************) +(* ITEMS ********************************************************************) + +(* atomic items *) +inductive item0: Type[0] ≝ + | Sort: nat → item0 (* sort: starting at 0 *) + | LRef: nat → item0 (* reference by index: starting at 0 *) +. (* binary binding items *) inductive bind2: Type[0] ≝ -| Abbr: bind2 (* abbreviation *) -| Abst: bind2 (* abstraction *) + | Abbr: bind2 (* abbreviation *) + | Abst: bind2 (* abstraction *) . (* binary non-binding items *) inductive flat2: Type[0] ≝ -| Appl: flat2 (* application *) -| Cast: flat2 (* explicit type annotation *) + | Appl: flat2 (* application *) + | Cast: flat2 (* explicit type annotation *) . (* binary items *) inductive item2: Type[0] ≝ -| Bind: bind2 → item2 (* binding item *) -| Flat: flat2 → item2 (* non-binding item *) + | Bind: bind2 → item2 (* binding item *) + | Flat: flat2 → item2 (* non-binding item *) . coercion item2_of_bind2: ∀I:bind2.item2 ≝ Bind on _I:bind2 to item2. diff --git a/matita/matita/contribs/lambda-delta/Basic-2/grammar/term.ma b/matita/matita/contribs/lambda-delta/Basic-2/grammar/term.ma index 309df0b3f..3b6614361 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/grammar/term.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/grammar/term.ma @@ -18,14 +18,15 @@ include "Basic-2/grammar/item.ma". (* terms *) inductive term: Type[0] ≝ -| TSort: nat → term (* sort: starting at 0 *) -| TLRef: nat → term (* reference by index: starting at 0 *) -| TPair: item2 → term → term → term (* binary item construction *) + | TAtom: item0 → term (* atomic item construction *) + | TPair: item2 → term → term → term (* binary item construction *) . -interpretation "sort (term)" 'Star k = (TSort k). +interpretation "sort (term)" 'Star k = (TAtom (Sort k)). -interpretation "local reference (term)" 'LRef i = (TLRef i). +interpretation "local reference (term)" 'LRef i = (TAtom (LRef i)). + +interpretation "term construction (atomic)" 'SItem I = (TAtom I). interpretation "term construction (binary)" 'SItem I T1 T2 = (TPair I T1 T2). diff --git a/matita/matita/contribs/lambda-delta/Basic-2/grammar/term_simple.ma b/matita/matita/contribs/lambda-delta/Basic-2/grammar/term_simple.ma index 4b4958e00..c182ba360 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/grammar/term_simple.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/grammar/term_simple.ma @@ -17,8 +17,7 @@ include "Basic-2/grammar/term.ma". (* SIMPLE (NEUTRAL) TERMS ***************************************************) inductive simple: term → Prop ≝ - | simple_sort: ∀k. simple (⋆k) - | simple_lref: ∀i. simple (#i) + | simple_atom: ∀I. simple (𝕒{I}) | simple_flat: ∀I,V,T. simple (𝕗{I} V. T) . @@ -28,8 +27,7 @@ interpretation "simple (term)" 'Simple T = (simple T). fact simple_inv_bind_aux: ∀T. 𝕊[T] → ∀J,W,U. T = 𝕓{J} W. U → False. #T * -T -[ #k #J #W #U #H destruct -| #k #J #W #U #H destruct +[ #I #J #W #U #H destruct | #I #V #T #J #W #U #H destruct ] qed. diff --git a/matita/matita/contribs/lambda-delta/Basic-2/grammar/term_weight.ma b/matita/matita/contribs/lambda-delta/Basic-2/grammar/term_weight.ma index 3e7063507..a960e48d1 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/grammar/term_weight.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/grammar/term_weight.ma @@ -17,8 +17,7 @@ include "Basic-2/grammar/term.ma". (* WEIGHT OF A TERM *********************************************************) let rec tw T ≝ match T with -[ TSort _ ⇒ 1 -| TLRef _ ⇒ 1 +[ TAtom _ ⇒ 1 | TPair _ V T ⇒ tw V + tw T + 1 ]. diff --git a/matita/matita/contribs/lambda-delta/Basic-2/grammar/thom.ma b/matita/matita/contribs/lambda-delta/Basic-2/grammar/thom.ma index 660fff5bf..34af6f9f4 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/grammar/thom.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/grammar/thom.ma @@ -17,11 +17,10 @@ include "Basic-2/grammar/term_simple.ma". (* HOMOMORPHIC TERMS ********************************************************) inductive thom: term → term → Prop ≝ - | thom_sort: ∀k. thom (⋆k) (⋆k) - | thom_lref: ∀i. thom (#i) (#i) - | thom_abst: ∀V1,V2,T1,T2. thom (𝕚{Abst} V1. T1) (𝕚{Abst} V2. T2) + | thom_atom: ∀I. thom (𝕒{I}) (𝕒{I}) + | thom_abst: ∀V1,V2,T1,T2. thom (𝕔{Abst} V1. T1) (𝕔{Abst} V2. T2) | thom_appl: ∀V1,V2,T1,T2. thom T1 T2 → 𝕊[T1] → 𝕊[T2] → - thom (𝕚{Appl} V1. T1) (𝕚{Appl} V2. T2) + thom (𝕔{Appl} V1. T1) (𝕔{Appl} V2. T2) . interpretation "homomorphic (term)" 'napart T1 T2 = (thom T1 T2). diff --git a/matita/matita/contribs/lambda-delta/Basic-2/notation.ma b/matita/matita/contribs/lambda-delta/Basic-2/notation.ma index 653365be8..8f068effd 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/notation.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/notation.ma @@ -28,7 +28,11 @@ notation "hvbox( # term 90 k )" non associative with precedence 90 for @{ 'LRef $k }. -notation "hvbox( 𝕚 { I } break term 90 T1 . break term 90 T )" +notation "hvbox( 𝕒 { I } )" + non associative with precedence 90 + for @{ 'SItem $I }. + +notation "hvbox( 𝕔 { I } break term 90 T1 . break term 90 T )" non associative with precedence 90 for @{ 'SItem $I $T1 $T }. @@ -43,7 +47,11 @@ notation "hvbox( 𝕗 { I } break term 90 T1 . break term 90 T )" notation "hvbox( T . break 𝕓 { I } break term 90 T1 )" non associative with precedence 89 for @{ 'DBind $T $I $T1 }. - +(* +notation > "hvbox( T . break 𝕔 { I } break term 90 T1 )" + non associative with precedence 89 + for @{ 'DBind $T $I $T1 }. +*) (**) (* this breaks all parsing *) notation "hvbox( # [ x ] )" non associative with precedence 90 for @{ 'Weight $x }. diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma index e06b8fa6d..de7daa04b 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma @@ -59,7 +59,7 @@ lemma cpr_delta: ∀L,K,V,W,i. qed. lemma cpr_cast: ∀L,V,T1,T2. - L ⊢ T1 ⇒ T2 → L ⊢ 𝕗{Cast} V. T1 ⇒ T2. + L ⊢ T1 ⇒ T2 → L ⊢ 𝕔{Cast} V. T1 ⇒ T2. #L #V #T1 #T2 * /3/ qed. diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma index e6dfc2c1d..3d441c931 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma @@ -17,22 +17,21 @@ include "Basic-2/substitution/tps.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) inductive tpr: term → term → Prop ≝ -| tpr_sort : ∀k. tpr (⋆k) (⋆k) -| tpr_lref : ∀i. tpr (#i) (#i) +| tpr_atom : ∀I. tpr (𝕒{I}) (𝕒{I}) | tpr_flat : ∀I,V1,V2,T1,T2. tpr V1 V2 → tpr T1 T2 → tpr (𝕗{I} V1. T1) (𝕗{I} V2. T2) | tpr_beta : ∀V1,V2,W,T1,T2. tpr V1 V2 → tpr T1 T2 → - tpr (𝕚{Appl} V1. 𝕚{Abst} W. T1) (𝕚{Abbr} V2. T2) + tpr (𝕔{Appl} V1. 𝕔{Abst} W. T1) (𝕔{Abbr} V2. T2) | tpr_delta: ∀I,V1,V2,T1,T2,T. tpr V1 V2 → tpr T1 T2 → ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ T → - tpr (𝕚{I} V1. T1) (𝕚{I} V2. T) + tpr (𝕓{I} V1. T1) (𝕓{I} V2. T) | tpr_theta: ∀V,V1,V2,W1,W2,T1,T2. tpr V1 V2 → ↑[0,1] V2 ≡ V → tpr W1 W2 → tpr T1 T2 → - tpr (𝕚{Appl} V1. 𝕚{Abbr} W1. T1) (𝕚{Abbr} W2. 𝕚{Appl} V. T2) + tpr (𝕔{Appl} V1. 𝕔{Abbr} W1. T1) (𝕔{Abbr} W2. 𝕔{Appl} V. T2) | tpr_zeta : ∀V,T,T1,T2. ↑[0,1] T1 ≡ T → tpr T1 T2 → - tpr (𝕚{Abbr} V. T) T2 -| tpr_tau : ∀V,T1,T2. tpr T1 T2 → tpr (𝕚{Cast} V. T1) T2 + tpr (𝕔{Abbr} V. T) T2 +| tpr_tau : ∀V,T1,T2. tpr T1 T2 → tpr (𝕔{Cast} V. T1) T2 . interpretation @@ -42,7 +41,7 @@ interpretation (* Basic properties *********************************************************) lemma tpr_bind: ∀I,V1,V2,T1,T2. V1 ⇒ V2 → T1 ⇒ T2 → - 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2. + 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2. /2/ qed. lemma tpr_refl: ∀T. T ⇒ T. @@ -52,10 +51,9 @@ qed. (* Basic inversion lemmas ***************************************************) -fact tpr_inv_sort1_aux: ∀U1,U2. U1 ⇒ U2 → ∀k. U1 = ⋆k → U2 = ⋆k. +fact tpr_inv_atom1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I. U1 = 𝕒{I} → U2 = 𝕒{I}. #U1 #U2 * -U1 U2 -[ #k0 #k #H destruct -k0 // -| #i #k #H destruct +[ // | #I #V1 #V2 #T1 #T2 #_ #_ #k #H destruct | #V1 #V2 #W #T1 #T2 #_ #_ #k #H destruct | #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #k #H destruct @@ -65,34 +63,17 @@ fact tpr_inv_sort1_aux: ∀U1,U2. U1 ⇒ U2 → ∀k. U1 = ⋆k → U2 = ⋆k. ] qed. -lemma tpr_inv_sort1: ∀k,U2. ⋆k ⇒ U2 → U2 = ⋆k. -/2/ qed. - -fact tpr_inv_lref1_aux: ∀U1,U2. U1 ⇒ U2 → ∀i. U1 = #i → U2 = #i. -#U1 #U2 * -U1 U2 -[ #k #i #H destruct -| #j #i #H destruct -j // -| #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct -| #V1 #V2 #W #T1 #T2 #_ #_ #i #H destruct -| #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #i #H destruct -| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #i #H destruct -| #V #T #T1 #T2 #_ #_ #i #H destruct -| #V #T1 #T2 #_ #i #H destruct -] -qed. - -lemma tpr_inv_lref1: ∀i,U2. #i ⇒ U2 → U2 = #i. +lemma tpr_inv_atom1: ∀I,U2. 𝕒{I} ⇒ U2 → U2 = 𝕒{I}. /2/ qed. fact tpr_inv_bind1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I,V1,T1. U1 = 𝕓{I} V1. T1 → (∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 & ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ T & - U2 = 𝕚{I} V2. T + U2 = 𝕓{I} V2. T ) ∨ ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2 & I = Abbr. #U1 #U2 * -U1 U2 -[ #k #I #V #T #H destruct -| #i #I #V #T #H destruct +[ #J #I #V #T #H destruct | #I1 #V1 #V2 #T1 #T2 #_ #_ #I #V #T #H destruct | #V1 #V2 #W #T1 #T2 #_ #_ #I #V #T #H destruct | #I1 #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #I0 #V0 #T0 #H destruct -I1 V1 T1 /3 width=7/ @@ -105,102 +86,90 @@ qed. lemma tpr_inv_bind1: ∀V1,T1,U2,I. 𝕓{I} V1. T1 ⇒ U2 → (∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 & ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ T & - U2 = 𝕚{I} V2. T + U2 = 𝕓{I} V2. T ) ∨ ∃∃T. ↑[0,1] T ≡ T1 & tpr T U2 & I = Abbr. /2/ qed. -lemma tpr_inv_abbr1: ∀V1,T1,U2. 𝕚{Abbr} V1. T1 ⇒ U2 → +lemma tpr_inv_abbr1: ∀V1,T1,U2. 𝕓{Abbr} V1. T1 ⇒ U2 → (∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 & ⋆. 𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T & - U2 = 𝕚{Abbr} V2. T + U2 = 𝕓{Abbr} V2. T ) ∨ ∃∃T. ↑[0,1] T ≡ T1 & tpr T U2. #V1 #T1 #U2 #H elim (tpr_inv_bind1 … H) -H * /3 width=7/ qed. -fact tpr_inv_appl1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,U0. U1 = 𝕚{Appl} V1. U0 → +fact tpr_inv_flat1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I,V1,U0. U1 = 𝕗{I} V1. U0 → ∨∨ ∃∃V2,T2. V1 ⇒ V2 & U0 ⇒ T2 & - U2 = 𝕚{Appl} V2. T2 + U2 = 𝕗{I} V2. T2 | ∃∃V2,W,T1,T2. V1 ⇒ V2 & T1 ⇒ T2 & - U0 = 𝕚{Abst} W. T1 & - U2 = 𝕓{Abbr} V2. T2 + U0 = 𝕔{Abst} W. T1 & + U2 = 𝕔{Abbr} V2. T2 & I = Appl | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 & ↑[0,1] V2 ≡ V & - U0 = 𝕚{Abbr} W1. T1 & - U2 = 𝕚{Abbr} W2. 𝕚{Appl} V. T2. + U0 = 𝕔{Abbr} W1. T1 & + U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2 & + I = Appl + | (U0 ⇒ U2 ∧ I = Cast). #U1 #U2 * -U1 U2 -[ #k #V #T #H destruct -| #i #V #T #H destruct -| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #V #T #H destruct -I V1 T1 /3 width=5/ -| #V1 #V2 #W #T1 #T2 #HV12 #HT12 #V #T #H destruct -V1 T /3 width=8/ -| #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #V0 #T0 #H destruct -| #V #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #V0 #T0 #H - destruct -V1 T0 /3 width=12/ -| #V #T #T1 #T2 #_ #_ #V0 #T0 #H destruct -| #V #T1 #T2 #_ #V0 #T0 #H destruct +[ #I #J #V #T #H destruct +| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #J #V #T #H destruct -I V1 T1 /3 width=5/ +| #V1 #V2 #W #T1 #T2 #HV12 #HT12 #J #V #T #H destruct -J V1 T /3 width=8/ +| #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #J #V0 #T0 #H destruct +| #V #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #J #V0 #T0 #H + destruct -J V1 T0 /3 width=12/ +| #V #T #T1 #T2 #_ #_ #J #V0 #T0 #H destruct +| #V #T1 #T2 #HT12 #J #V0 #T0 #H destruct -J V T1 /3/ ] qed. -lemma tpr_inv_appl1: ∀V1,U0,U2. 𝕚{Appl} V1. U0 ⇒ U2 → +lemma tpr_inv_flat1: ∀V1,U0,U2,I. 𝕗{I} V1. U0 ⇒ U2 → ∨∨ ∃∃V2,T2. V1 ⇒ V2 & U0 ⇒ T2 & - U2 = 𝕚{Appl} V2. T2 + U2 = 𝕗{I} V2. T2 | ∃∃V2,W,T1,T2. V1 ⇒ V2 & T1 ⇒ T2 & - U0 = 𝕚{Abst} W. T1 & - U2 = 𝕓{Abbr} V2. T2 + U0 = 𝕔{Abst} W. T1 & + U2 = 𝕔{Abbr} V2. T2 & I = Appl | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 & ↑[0,1] V2 ≡ V & - U0 = 𝕚{Abbr} W1. T1 & - U2 = 𝕚{Abbr} W2. 𝕚{Appl} V. T2. -/2/ qed. - -fact tpr_inv_cast1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕚{Cast} V1. T1 → - (∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Cast} V2. T2) - ∨ T1 ⇒ U2. -#U1 #U2 * -U1 U2 -[ #k #V #T #H destruct -| #i #V #T #H destruct -| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #V #T #H destruct -I V1 T1 /3 width=5/ -| #V1 #V2 #W #T1 #T2 #_ #_ #V #T #H destruct -| #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #V0 #T0 #H destruct -| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #V0 #T0 #H destruct -| #V #T #T1 #T2 #_ #_ #V0 #T0 #H destruct -| #V #T1 #T2 #HT12 #V0 #T0 #H destruct -V T1 /2/ -] -qed. - -lemma tpr_inv_cast1: ∀V1,T1,U2. 𝕚{Cast} V1. T1 ⇒ U2 → - (∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Cast} V2. T2) - ∨ T1 ⇒ U2. + U0 = 𝕔{Abbr} W1. T1 & + U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2 & + I = Appl + | (U0 ⇒ U2 ∧ I = Cast). /2/ qed. -lemma tpr_inv_flat1: ∀V1,U0,U2,I. 𝕗{I} V1. U0 ⇒ U2 → +lemma tpr_inv_appl1: ∀V1,U0,U2. 𝕔{Appl} V1. U0 ⇒ U2 → ∨∨ ∃∃V2,T2. V1 ⇒ V2 & U0 ⇒ T2 & - U2 = 𝕗{I} V2. T2 + U2 = 𝕔{Appl} V2. T2 | ∃∃V2,W,T1,T2. V1 ⇒ V2 & T1 ⇒ T2 & - U0 = 𝕚{Abst} W. T1 & - U2 = 𝕓{Abbr} V2. T2 & I = Appl + U0 = 𝕔{Abst} W. T1 & + U2 = 𝕔{Abbr} V2. T2 | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 & ↑[0,1] V2 ≡ V & - U0 = 𝕚{Abbr} W1. T1 & - U2 = 𝕚{Abbr} W2. 𝕚{Appl} V. T2 & - I = Appl - | (U0 ⇒ U2 ∧ I = Cast). -#V1 #U0 #U2 * #H -[ elim (tpr_inv_appl1 … H) -H * /3 width=12/ -| elim (tpr_inv_cast1 … H) -H [1: *] /3 width=5/ + U0 = 𝕔{Abbr} W1. T1 & + U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2. +#V1 #U0 #U2 #H +elim (tpr_inv_flat1 … H) -H * /3 width=12/ #_ #H destruct +qed. + +lemma tpr_inv_cast1: ∀V1,T1,U2. 𝕔{Cast} V1. T1 ⇒ U2 → + (∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Cast} V2. T2) + ∨ T1 ⇒ U2. +#V1 #T1 #U2 #H +elim (tpr_inv_flat1 … H) -H * /3 width=5/ +[ #V2 #W #W1 #W2 #_ #_ #_ #_ #H destruct +| #V2 #W #W1 #W2 #T2 #U1 #_ #_ #_ #_ #_ #_ #H destruct ] qed. fact tpr_inv_lref2_aux: ∀T1,T2. T1 ⇒ T2 → ∀i. T2 = #i → ∨∨ T1 = #i | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i & - T1 = 𝕚{Abbr} V. T - | ∃∃V,T. T ⇒ #i & T1 = 𝕚{Cast} V. T. + T1 = 𝕔{Abbr} V. T + | ∃∃V,T. T ⇒ #i & T1 = 𝕔{Cast} V. T. #T1 #T2 * -T1 T2 -[ #k #i #H destruct -| #j #i /2/ +[ #I #i #H destruct /2/ | #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct | #V1 #V2 #W #T1 #T2 #_ #_ #i #H destruct | #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #i #H destruct @@ -213,6 +182,6 @@ qed. lemma tpr_inv_lref2: ∀T1,i. T1 ⇒ #i → ∨∨ T1 = #i | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i & - T1 = 𝕓{Abbr} V. T - | ∃∃V,T. T ⇒ #i & T1 = 𝕗{Cast} V. T. + T1 = 𝕔{Abbr} V. T + | ∃∃V,T. T ⇒ #i & T1 = 𝕔{Cast} V. T. /2/ qed. diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_lift.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_lift.ma index a748416f0..66e872eae 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_lift.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_lift.ma @@ -20,12 +20,11 @@ include "Basic-2/reduction/tpr.ma". lemma tpr_lift: ∀T1,T2. T1 ⇒ T2 → ∀d,e,U1. ↑[d, e] T1 ≡ U1 → ∀U2. ↑[d, e] T2 ≡ U2 → U1 ⇒ U2. #T1 #T2 #H elim H -H T1 T2 -[ #k #d #e #U1 #HU1 #U2 #HU2 - lapply (lift_mono … HU1 … HU2) -HU1 #H destruct -U1; - lapply (lift_inv_sort1 … HU2) -HU2 #H destruct -U2 // -| #i #d #e #U1 #HU1 #U2 #HU2 - lapply (lift_mono … HU1 … HU2) -HU1 #H destruct -U1; - lapply (lift_inv_lref1 … HU2) * * #Hid #H destruct -U2 // +[ * #i #d #e #U1 #HU1 #U2 #HU2 + lapply (lift_mono … HU1 … HU2) -HU1 #H destruct -U1 + [ lapply (lift_inv_sort1 … HU2) -HU2 #H destruct -U2 // + | lapply (lift_inv_lref1 … HU2) * * #Hid #H destruct -U2 // + ] | #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X1 #HX1 #X2 #HX2 elim (lift_inv_flat1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct -X1; elim (lift_inv_flat1 … HX2) -HX2 #W2 #U2 #HVW2 #HTU2 #HX2 destruct -X2 /3/ @@ -57,10 +56,10 @@ lemma tpr_inv_lift: ∀T1,T2. T1 ⇒ T2 → ∀d,e,U1. ↑[d, e] U1 ≡ T1 → ∃∃U2. ↑[d, e] U2 ≡ T2 & U1 ⇒ U2. #T1 #T2 #H elim H -H T1 T2 -[ #k #d #e #U1 #HU1 - lapply (lift_inv_sort2 … HU1) -HU1 #H destruct -U1 /2/ -| #i #d #e #U1 #HU1 - lapply (lift_inv_lref2 … HU1) -HU1 * * #Hid #H destruct -U1 /3/ +[ * #i #d #e #U1 #HU1 + [ lapply (lift_inv_sort2 … HU1) -HU1 #H destruct -U1 /2/ + | lapply (lift_inv_lref2 … HU1) -HU1 * * #Hid #H destruct -U1 /3/ + ] | #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X #HX elim (lift_inv_flat2 … HX) -HX #V0 #T0 #HV01 #HT01 #HX destruct -X; elim (IHV12 … HV01) -IHV12 HV01; @@ -96,11 +95,10 @@ qed. (* Advanced inversion lemmas ************************************************) -fact tpr_inv_abst1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕚{Abst} V1. T1 → - ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Abst} V2. T2. +fact tpr_inv_abst1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕔{Abst} V1. T1 → + ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Abst} V2. T2. #U1 #U2 * -U1 U2 -[ #k #V #T #H destruct -| #i #V #T #H destruct +[ #I #V #T #H destruct | #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct | #V1 #V2 #W #T1 #T2 #_ #_ #V #T #H destruct | #I #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #V0 #T0 #H destruct -I V1 T1; @@ -111,6 +109,6 @@ fact tpr_inv_abst1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕚{Abst} V1. T1 ] qed. -lemma tpr_inv_abst1: ∀V1,T1,U2. 𝕚{Abst} V1. T1 ⇒ U2 → - ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Abst} V2. T2. +lemma tpr_inv_abst1: ∀V1,T1,U2. 𝕔{Abst} V1. T1 ⇒ U2 → + ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Abst} V2. T2. /2/ qed. diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tpr.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tpr.ma index aa55eb8b5..27f09e20a 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tpr.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tpr.ma @@ -20,10 +20,7 @@ include "Basic-2/reduction/tpr_tps.ma". (* Confluence lemmas ********************************************************) -fact tpr_conf_sort_sort: ∀k. ∃∃X. ⋆k ⇒ X & ⋆k ⇒ X. -/2/ qed. - -fact tpr_conf_lref_lref: ∀i. ∃∃X. #i ⇒ X & #i ⇒ X. +fact tpr_conf_atom_atom: ∀I. ∃∃X. 𝕒{I} ⇒ X & 𝕒{I} ⇒ X. /2/ qed. fact tpr_conf_flat_flat: @@ -46,8 +43,8 @@ fact tpr_conf_flat_beta: ∃∃X. X1 ⇒ X & X2 ⇒ X ) → V0 ⇒ V1 → V0 ⇒ V2 → - U0 ⇒ T2 → 𝕓{Abst} W0. U0 ⇒ T1 → - ∃∃X. 𝕗{Appl} V1. T1 ⇒ X & 𝕓{Abbr} V2. T2 ⇒ X. + U0 ⇒ T2 → 𝕔{Abst} W0. U0 ⇒ T1 → + ∃∃X. 𝕔{Appl} V1. T1 ⇒ X & 𝕔{Abbr} V2. T2 ⇒ X. #V0 #V1 #T1 #V2 #W0 #U0 #T2 #IH #HV01 #HV02 #HT02 #H elim (tpr_inv_abst1 … H) -H #W1 #U1 #HW01 #HU01 #H destruct -T1; elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2 @@ -61,8 +58,8 @@ fact tpr_conf_flat_theta: ∃∃X. X1 ⇒ X & X2 ⇒ X ) → V0 ⇒ V1 → V0 ⇒ V2 → ↑[O,1] V2 ≡ V → - W0 ⇒ W2 → U0 ⇒ U2 → 𝕓{Abbr} W0. U0 ⇒ T1 → - ∃∃X. 𝕗{Appl} V1. T1 ⇒ X & 𝕓{Abbr} W2. 𝕗{Appl} V. U2 ⇒ X. + W0 ⇒ W2 → U0 ⇒ U2 → 𝕔{Abbr} W0. U0 ⇒ T1 → + ∃∃X. 𝕔{Appl} V1. T1 ⇒ X & 𝕔{Abbr} W2. 𝕔{Appl} V. U2 ⇒ X. #V0 #V1 #T1 #V2 #V #W0 #W2 #U0 #U2 #IH #HV01 #HV02 #HV2 #HW02 #HU02 #H elim (IH … HV01 … HV02) -HV01 HV02 // #VV #HVV1 #HVV2 elim (lift_total VV 0 1) #VVV #HVV @@ -98,7 +95,7 @@ fact tpr_conf_flat_cast: ∃∃X. X1 ⇒ X & X2 ⇒ X ) → V0 ⇒ V1 → T0 ⇒ T1 → T0 ⇒ X2 → - ∃∃X. 𝕗{Cast} V1. T1 ⇒ X & X2 ⇒ X. + ∃∃X. 𝕔{Cast} V1. T1 ⇒ X & X2 ⇒ X. #X2 #V0 #V1 #T0 #T1 #IH #_ #HT01 #HT02 elim (IH … HT01 … HT02) -HT01 HT02 IH /3/ qed. @@ -110,7 +107,7 @@ fact tpr_conf_beta_beta: ∃∃X. X1 ⇒ X & X2 ⇒ X ) → V0 ⇒ V1 → V0 ⇒ V2 → T0 ⇒ T1 → T0 ⇒ T2 → - ∃∃X. 𝕓{Abbr} V1. T1 ⇒X & 𝕓{Abbr} V2. T2 ⇒ X. + ∃∃X. 𝕔{Abbr} V1. T1 ⇒X & 𝕔{Abbr} V2. T2 ⇒ X. #W0 #V0 #V1 #T0 #T1 #V2 #T2 #IH #HV01 #HV02 #HT01 #HT02 elim (IH … HV01 … HV02) -HV01 HV02 // elim (IH … HT01 … HT02) -HT01 HT02 IH /3 width=5/ @@ -159,7 +156,7 @@ fact tpr_conf_theta_theta: ) → V0 ⇒ V1 → V0 ⇒ V2 → W0 ⇒ W1 → W0 ⇒ W2 → T0 ⇒ T1 → T0 ⇒ T2 → ↑[O, 1] V1 ≡ VV1 → ↑[O, 1] V2 ≡ VV2 → - ∃∃X. 𝕓{Abbr} W1. 𝕗{Appl} VV1. T1 ⇒ X & 𝕓{Abbr} W2. 𝕗{Appl} VV2. T2 ⇒ X. + ∃∃X. 𝕔{Abbr} W1. 𝕔{Appl} VV1. T1 ⇒ X & 𝕔{Abbr} W2. 𝕔{Appl} VV2. T2 ⇒ X. #VV1 #V0 #V1 #W0 #W1 #T0 #T1 #V2 #VV2 #W2 #T2 #IH #HV01 #HV02 #HW01 #HW02 #HT01 #HT02 #HVV1 #HVV2 elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2 elim (IH … HW01 … HW02) -HW01 HW02 // #W #HW1 #HW2 @@ -208,75 +205,71 @@ fact tpr_conf_aux: ∀X0,X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → X0 = Y0 → ∃∃X. X1 ⇒ X & X2 ⇒ X. #Y0 #IH #X0 #X1 #X2 * -X0 X1 -[ #k1 #H1 #H2 destruct -Y0; - lapply (tpr_inv_sort1 … H1) -H1 -(* case 1: sort, sort *) - #H1 destruct -X2 // -| #i1 #H1 #H2 destruct -Y0; - lapply (tpr_inv_lref1 … H1) -H1 -(* case 2: lref, lref *) +[ #I1 #H1 #H2 destruct -Y0; + lapply (tpr_inv_atom1 … H1) -H1 +(* case 1: atom, atom *) #H1 destruct -X2 // | #I #V0 #V1 #T0 #T1 #HV01 #HT01 #H1 #H2 destruct -Y0; elim (tpr_inv_flat1 … H1) -H1 * -(* case 3: flat, flat *) +(* case 2: flat, flat *) [ #V2 #T2 #HV02 #HT02 #H destruct -X2 /3 width=7 by tpr_conf_flat_flat/ (**) (* /3 width=7/ is too slow *) -(* case 4: flat, beta *) +(* case 3: flat, beta *) | #V2 #W #U0 #T2 #HV02 #HT02 #H1 #H2 #H3 destruct -T0 X2 I /3 width=8 by tpr_conf_flat_beta/ (**) (* /3 width=8/ is too slow *) -(* case 5: flat, theta *) +(* case 4: flat, theta *) | #V2 #V #W0 #W2 #U0 #U2 #HV02 #HW02 #HT02 #HV2 #H1 #H2 #H3 destruct -T0 X2 I /3 width=11 by tpr_conf_flat_theta/ (**) (* /3 width=11/ is too slow *) -(* case 6: flat, tau *) +(* case 5: flat, tau *) | #HT02 #H destruct -I /3 width=6 by tpr_conf_flat_cast/ (**) (* /3 width=6/ is too slow *) ] | #V0 #V1 #W0 #T0 #T1 #HV01 #HT01 #H1 #H2 destruct -Y0; elim (tpr_inv_appl1 … H1) -H1 * -(* case 7: beta, flat (repeated) *) +(* case 6: beta, flat (repeated) *) [ #V2 #T2 #HV02 #HT02 #H destruct -X2 @ex2_1_comm /3 width=8 by tpr_conf_flat_beta/ -(* case 8: beta, beta *) +(* case 7: beta, beta *) | #V2 #WW0 #TT0 #T2 #HV02 #HT02 #H1 #H2 destruct -W0 T0 X2 /3 width=8 by tpr_conf_beta_beta/ (**) (* /3 width=8/ is too slow *) -(* case 9, beta, theta (excluded) *) +(* case 8, beta, theta (excluded) *) | #V2 #VV2 #WW0 #W2 #TT0 #T2 #_ #_ #_ #_ #H destruct ] | #I1 #V0 #V1 #T0 #T1 #TT1 #HV01 #HT01 #HTT1 #H1 #H2 destruct -Y0; elim (tpr_inv_bind1 … H1) -H1 * -(* case 10: delta, delta *) +(* case 9: delta, delta *) [ #V2 #T2 #TT2 #HV02 #HT02 #HTT2 #H destruct -X2 /3 width=11 by tpr_conf_delta_delta/ (**) (* /3 width=11/ is too slow *) -(* case 11: delta, zata *) +(* case 10: delta, zata *) | #T2 #HT20 #HTX2 #H destruct -I1; /3 width=10 by tpr_conf_delta_zeta/ (**) (* /3 width=10/ is too slow *) ] | #VV1 #V0 #V1 #W0 #W1 #T0 #T1 #HV01 #HVV1 #HW01 #HT01 #H1 #H2 destruct -Y0; elim (tpr_inv_appl1 … H1) -H1 * -(* case 12: theta, flat (repeated) *) +(* case 11: theta, flat (repeated) *) [ #V2 #T2 #HV02 #HT02 #H destruct -X2 @ex2_1_comm /3 width=11 by tpr_conf_flat_theta/ -(* case 13: theta, beta (repeated) *) +(* case 12: theta, beta (repeated) *) | #V2 #WW0 #TT0 #T2 #_ #_ #H destruct -(* case 14: theta, theta *) +(* case 13: theta, theta *) | #V2 #VV2 #WW0 #W2 #TT0 #T2 #V02 #HW02 #HT02 #HVV2 #H1 #H2 destruct -W0 T0 X2 /3 width=14 by tpr_conf_theta_theta/ (**) (* /3 width=14/ is too slow *) ] | #V0 #TT0 #T0 #T1 #HTT0 #HT01 #H1 #H2 destruct -Y0; elim (tpr_inv_abbr1 … H1) -H1 * -(* case 15: zeta, delta (repeated) *) +(* case 14: zeta, delta (repeated) *) [ #V2 #T2 #TT2 #HV02 #HT02 #HTT2 #H destruct -X2 @ex2_1_comm /3 width=10 by tpr_conf_delta_zeta/ -(* case 16: zeta, zeta *) +(* case 15: zeta, zeta *) | #T2 #HTT20 #HTX2 /3 width=9 by tpr_conf_zeta_zeta/ (**) (* /3 width=9/ is too slow *) ] | #V0 #T0 #T1 #HT01 #H1 #H2 destruct -Y0; elim (tpr_inv_cast1 … H1) -H1 -(* case 17: tau, flat (repeated) *) +(* case 16: tau, flat (repeated) *) [ * #V2 #T2 #HV02 #HT02 #H destruct -X2 @ex2_1_comm /3 width=6 by tpr_conf_flat_cast/ -(* case 18: tau, tau *) +(* case 17: tau, tau *) | #HT02 /2 by tpr_conf_tau_tau/ ] diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/drop.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/drop.ma index 149fabde3..65aaf3d4e 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/drop.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/drop.ma @@ -205,7 +205,7 @@ qed. (* Basic-1: removed theorems 18: drop_skip_flat - cimp_flat_sx cimp_flat_dx cimp_bind cimp_getl_conf + cimp_flat_sx cimp_flat_dx cimp_bind cimp_getl_conf drop_clear drop_clear_O drop_clear_S clear_gen_sort clear_gen_bind clear_gen_flat clear_gen_flat_r clear_gen_all clear_clear clear_mono clear_trans clear_ctail diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/lift.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/lift.ma index 3f9eadf43..0a4e1715a 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/lift.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/lift.ma @@ -38,16 +38,14 @@ qed. lemma lift_refl: ∀T,d. ↑[d, 0] T ≡ T. #T elim T -T -[ // -| #i #d elim (lt_or_ge i d) /2/ -| #I elim I -I /2/ +[ * #i // #d elim (lt_or_ge i d) /2/ +| * /2/ ] qed. lemma lift_total: ∀T1,d,e. ∃T2. ↑[d,e] T1 ≡ T2. #T1 elim T1 -T1 -[ /2/ -| #i #d #e elim (lt_or_ge i d) /3/ +[ * #i /2/ #d #e elim (lt_or_ge i d) /3/ | * #I #V1 #T1 #IHV1 #IHT1 #d #e elim (IHV1 d e) -IHV1 #V2 #HV12 [ elim (IHT1 (d+1) e) -IHT1 /3/ diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps.ma index d2e71ed7d..2c61e3363 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps.ma @@ -17,8 +17,7 @@ include "Basic-2/substitution/drop.ma". (* PARALLEL SUBSTITUTION ON TERMS *******************************************) inductive tps: lenv → term → nat → nat → term → Prop ≝ -| tps_sort : ∀L,k,d,e. tps L (⋆k) d e (⋆k) -| tps_lref : ∀L,i,d,e. tps L (#i) d e (#i) +| tps_atom : ∀L,I,d,e. tps L (𝕒{I}) d e (𝕒{I}) | tps_subst: ∀L,K,V,W,i,d,e. d ≤ i → i < d + e → ↓[0, i] L ≡ K. 𝕓{Abbr} V → ↑[0, i + 1] V ≡ W → tps L (#i) d e W | tps_bind : ∀L,I,V1,V2,T1,T2,d,e. @@ -38,7 +37,6 @@ lemma tps_leq_repl: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≫ T2 → ∀L2. L1 [d, e] ≈ L2 → L2 ⊢ T1 [d, e] ≫ T2. #L1 #T1 #T2 #d #e #H elim H -H L1 T1 T2 d e [ // -| // | #L1 #K1 #V #W #i #d #e #Hdi #Hide #HLK1 #HVW #L2 #HL12 elim (drop_leq_drop1 … HL12 … HLK1 ? ?) -HL12 HLK1 // /2/ | /4/ @@ -56,7 +54,6 @@ lemma tps_weak: ∀L,T1,T2,d1,e1. L ⊢ T1 [d1, e1] ≫ T2 → L ⊢ T1 [d2, e2] ≫ T2. #L #T1 #T #d1 #e1 #H elim H -L T1 T d1 e1 [ // -| // | #L #K #V #W #i #d1 #e1 #Hid1 #Hide1 #HLK #HVW #d2 #e2 #Hd12 #Hde12 lapply (transitive_le … Hd12 … Hid1) -Hd12 Hid1 #Hid2 lapply (lt_to_le_to_lt … Hide1 … Hde12) -Hide1 /2/ @@ -69,7 +66,6 @@ lemma tps_weak_top: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → L ⊢ T1 [d, |L| - d] ≫ T2. #L #T1 #T #d #e #H elim H -L T1 T d e [ // -| // | #L #K #V #W #i #d #e #Hdi #_ #HLK #HVW lapply (drop_fwd_drop2_length … HLK) #Hi lapply (le_to_lt_to_lt … Hdi Hi) #Hd @@ -90,7 +86,6 @@ lemma tps_split_up: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → ∀i. d ≤ i → ∃∃T. L ⊢ T1 [d, i - d] ≫ T & L ⊢ T [i, d + e - i] ≫ T2. #L #T1 #T2 #d #e #H elim H -L T1 T2 d e [ /2/ -| /2/ | #L #K #V #W #i #d #e #Hdi #Hide #HLK #HVW #j #Hdj #Hjde elim (lt_or_ge i j) [ -Hide Hjde; @@ -119,8 +114,7 @@ fact tps_inv_lref1_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → ∀i. T1 = #i ↓[O, i] L ≡ K. 𝕓{Abbr} V & ↑[O, i + 1] V ≡ T2. #L #T1 #T2 #d #e * -L T1 T2 d e -[ #L #k #d #e #i #H destruct -| /2/ +[ #L #I #d #e #i #H destruct -I /2/ | #L #K #V #T2 #i #d #e #Hdi #Hide #HLK #HVT2 #j #H destruct -i /3/ | #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #i #H destruct | #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #i #H destruct @@ -141,7 +135,6 @@ fact tps_inv_bind1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ≫ U2 → U2 = 𝕓{I} V2. T2. #d #e #L #U1 #U2 * -d e L U1 U2 [ #L #k #d #e #I #V1 #T1 #H destruct -| #L #i #d #e #I #V1 #T1 #H destruct | #L #K #V #W #i #d #e #_ #_ #_ #_ #I #V1 #T1 #H destruct | #L #J #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #I #V #T #H destruct /2 width=5/ | #L #J #V1 #V2 #T1 #T2 #d #e #_ #_ #I #V #T #H destruct @@ -160,7 +153,6 @@ fact tps_inv_flat1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ≫ U2 → U2 = 𝕗{I} V2. T2. #d #e #L #U1 #U2 * -d e L U1 U2 [ #L #k #d #e #I #V1 #T1 #H destruct -| #L #i #d #e #I #V1 #T1 #H destruct | #L #K #V #W #i #d #e #_ #_ #_ #_ #I #V1 #T1 #H destruct | #L #J #V1 #V2 #T1 #T2 #d #e #_ #_ #I #V #T #H destruct | #L #J #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #I #V #T #H destruct /2 width=5/ @@ -175,7 +167,6 @@ lemma tps_inv_flat1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕗{I} V1. T1 [d, e] ≫ U2 → fact tps_inv_refl0_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → e = 0 → T1 = T2. #L #T1 #T2 #d #e #H elim H -H L T1 T2 d e [ // -| // | #L #K #V #W #i #d #e #Hdi #Hide #_ #_ #H destruct -e; lapply (le_to_lt_to_lt … Hdi … Hide) -Hdi Hide (lift_mono … H1 … H2) -H1 H2 // -| #K #i #dt #et #L #U1 #U2 #d #e #_ #H1 #H2 #_ +[ #K #I #dt #et #L #U1 #U2 #d #e #_ #H1 #H2 #_ >(lift_mono … H1 … H2) -H1 H2 // | #K #KV #V #W #i #dt #et #Hdti #Hidet #HKV #HVW #L #U1 #U2 #d #e #HLK #H #HVU2 #Hdetd lapply (lt_to_le_to_lt … Hidet … Hdetd) -Hdetd #Hid @@ -53,9 +51,7 @@ lemma tps_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫ T2 → d ≤ dt → L ⊢ U1 [dt + e, et] ≫ U2. #K #T1 #T2 #dt #et #H elim H -H K T1 T2 dt et -[ #K #k #dt #et #L #U1 #U2 #d #e #_ #H1 #H2 #_ - >(lift_mono … H1 … H2) -H1 H2 // -| #K #i #dt #et #L #U1 #U2 #d #e #_ #H1 #H2 #_ +[ #K #I #dt #et #L #U1 #U2 #d #e #_ #H1 #H2 #_ >(lift_mono … H1 … H2) -H1 H2 // | #K #KV #V #W #i #dt #et #Hdti #Hidet #HKV #HVW #L #U1 #U2 #d #e #HLK #H #HWU2 #Hddt lapply (transitive_le … Hddt … Hdti) -Hddt #Hid @@ -78,10 +74,10 @@ lemma tps_inv_lift1_le: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 → dt + et ≤ d → ∃∃T2. K ⊢ T1 [dt, et] ≫ T2 & ↑[d, e] T2 ≡ U2. #L #U1 #U2 #dt #et #H elim H -H L U1 U2 dt et -[ #L #k #dt #et #K #d #e #_ #T1 #H #_ - lapply (lift_inv_sort2 … H) -H #H destruct -T1 /2/ -| #L #i #dt #et #K #d #e #_ #T1 #H #_ - elim (lift_inv_lref2 … H) -H * #Hid #H destruct -T1 /3/ +[ #L * #i #dt #et #K #d #e #_ #T1 #H #_ + [ lapply (lift_inv_sort2 … H) -H #H destruct -T1 /2/ + | elim (lift_inv_lref2 … H) -H * #Hid #H destruct -T1 /3/ + ] | #L #KV #V #W #i #dt #et #Hdti #Hidet #HLKV #HVW #K #d #e #HLK #T1 #H #Hdetd lapply (lt_to_le_to_lt … Hidet … Hdetd) -Hdetd #Hid lapply (lift_inv_lref2_lt … H … Hid) -H #H destruct -T1; @@ -103,10 +99,10 @@ lemma tps_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 → d + e ≤ dt → ∃∃T2. K ⊢ T1 [dt - e, et] ≫ T2 & ↑[d, e] T2 ≡ U2. #L #U1 #U2 #dt #et #H elim H -H L U1 U2 dt et -[ #L #k #dt #et #K #d #e #_ #T1 #H #_ - lapply (lift_inv_sort2 … H) -H #H destruct -T1 /2/ -| #L #i #dt #et #K #d #e #_ #T1 #H #_ - elim (lift_inv_lref2 … H) -H * #Hid #H destruct -T1 /3/ +[ #L * #i #dt #et #K #d #e #_ #T1 #H #_ + [ lapply (lift_inv_sort2 … H) -H #H destruct -T1 /2/ + | elim (lift_inv_lref2 … H) -H * #Hid #H destruct -T1 /3/ + ] | #L #KV #V #W #i #dt #et #Hdti #Hidet #HLKV #HVW #K #d #e #HLK #T1 #H #Hdedt lapply (transitive_le … Hdedt … Hdti) #Hdei lapply (plus_le_weak … Hdedt) -Hdedt #Hedt @@ -136,7 +132,6 @@ lemma tps_inv_lift1_eq: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ≫ U2 → ∀T1. ↑[d, e] T1 ≡ U1 → U1 = U2. #L #U1 #U2 #d #e #H elim H -H L U1 U2 d e [ // -| // | #L #K #V #W #i #d #e #Hdi #Hide #_ #_ #T1 #H elim (lift_inv_lref2 … H) -H * #H [ lapply (le_to_lt_to_lt … Hdi … H) -Hdi H #H @@ -188,7 +183,6 @@ fact tps_inv_refl1_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → e = 1 → ∀K,V. ↓[0, d] L ≡ K. 𝕓{Abst} V → T1 = T2. #L #T1 #T2 #d #e #H elim H -H L T1 T2 d e [ // -| // | #L #K0 #V0 #W #i #d #e #Hdi #Hide #HLK0 #_ #H destruct -e; >(le_to_le_to_eq … Hdi ?) /2/ -d #K #V #HLK lapply (drop_mono … HLK0 … HLK) #H destruct diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_tps.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_tps.ma index 83316ac30..65b1b86d4 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_tps.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_tps.ma @@ -22,7 +22,6 @@ theorem tps_conf: ∀L,T0,T1,d,e. L ⊢ T0 [d, e] ≫ T1 → ∀T2. L ⊢ T0 [d, ∃∃T. L ⊢ T1 [d, e] ≫ T & L ⊢ T2 [d, e] ≫ T. #L #T0 #T1 #d #e #H elim H -H L T0 T1 d e [ /2/ -| /2/ | #L #K1 #V1 #T1 #i1 #d #e #Hdi1 #Hi1de #HLK1 #HVT1 #T2 #H elim (tps_inv_lref1 … H) -H [ #HX destruct -T2 /4/ @@ -51,7 +50,6 @@ theorem tps_trans_down: ∀L,T1,T0,d1,e1. L ⊢ T1 [d1, e1] ≫ T0 → ∃∃T. L ⊢ T1 [d2, e2] ≫ T & L ⊢ T [d1, e1] ≫ T2. #L #T1 #T0 #d1 #e1 #H elim H -L T1 T0 d1 e1 [ /2/ -| /2/ | #L #K #V #W #i1 #d1 #e1 #Hdi1 #Hide1 #HLK #HVW #T2 #d2 #e2 #HWT2 #Hde2d1 lapply (transitive_le … Hde2d1 Hdi1) -Hde2d1 #Hde2i1 lapply (tps_weak … HWT2 0 (i1 + 1) ? ?) -HWT2; normalize /2/ -Hde2i1 #HWT2 -- 2.39.2