From: Ferruccio Guidi Date: Mon, 26 May 2014 17:08:40 +0000 (+0000) Subject: new definition of llor gives a long awaited lemma :), X-Git-Tag: make_still_working~917 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=44927f6b05adef73df12ff1b85f79f99698709d3;p=helm.git new definition of llor gives a long awaited lemma :), but introduces an axiom :( --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/llor/lleq_llor.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llor/lleq_llor.etc deleted file mode 100644 index a180d1124..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/llor/lleq_llor.etc +++ /dev/null @@ -1,35 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/relocation/llor.ma". -include "basic_2/substitution/lleq_alt.ma". - -(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************) - -(* Properties on poinwise union for local environments **********************) - -lemma llor_lleq_O: ∀T,L1,L2,L. L1 ⩖[T] L2 ≡ L → |L1| ≤ |L2| → |L2| = |L| → L2 ⋕[T, yinj 0] L. -#T #L1 @(f2_ind … rfw … L1 T) -L1 -T -#n #IH #L1 #T #Hn #L2 #L #H #HL12 #HL2 elim (llor_inv_alt … H) // destruct -#HL1 #IHT @lleq_intro_alt // -#I2 #I #K2 #K #V2 #V #i #_ #HnT #HLK2 #HLK lapply (ldrop_fwd_length_lt2 … HLK) -#Hi elim (ldrop_O1_lt L1 i) // -#I1 #K1 #V1 #HLK1 elim (IHT … HLK1 HLK) >HL1 >HL2 Hi -Hi +elim (IH … HLK1 HLK) -IH #HI1 * +/4 width=5 by or_introl, or_intror, and3_intro, ex4_3_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_llor.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_llor.ma new file mode 100644 index 000000000..80bc596f2 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_llor.ma @@ -0,0 +1,36 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/substitution/llor.ma". +include "basic_2/substitution/lleq_alt.ma". + +(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************) + +(* Properties on poinwise union for local environments **********************) +(* +lemma llor_lleq_O: ∀R,L1,L2,T. llpx_sn R 0 T L1 L2 → + ∀L. L1 ⩖[T] L2 ≡ L → L2 ≡[T, 0] L. +#R #L1 #L2 #T #H1 #L #H2 +elim (llpx_sn_llpx_sn_alt … H1) -H1 #HL12 #IH1 +elim H2 -H2 #_ #HL1 #IH2 +@lleq_intro_alt // #I2 #I #K2 #K #V2 #V #i #Hi #HnT #HLK2 #HLK +lapply (ldrop_fwd_length_lt2 … HLK) #HiL +elim (ldrop_O1_lt (Ⓕ) L1 i) // -HiL #I1 #K1 #V1 #HLK1 +elim (IH1 … HLK1 HLK2) // -IH1 +[ #H #_ destruct + elim (IH2 … HLK1 HLK2 HLK) * /2 width=1 by conj/ + #H elim HnT -HnT +| #H @HnT -HnT +] +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/llor.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/llor.ma deleted file mode 100644 index 9d0122cca..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/llor.ma +++ /dev/null @@ -1,56 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/notation/relations/lazyor_4.ma". -include "basic_2/relocation/lpx_sn.ma". -include "basic_2/substitution/cofrees.ma". - -(* POINTWISE UNION FOR LOCAL ENVIRONMENTS ***********************************) - -inductive clor (T) (L2) (K1) (V1): predicate term ≝ -| clor_sn: |K1| < |L2| → K1 ⊢ |L2|-|K1|-1 ~ϵ 𝐅*[yinj 0]⦃T⦄ → clor T L2 K1 V1 V1 -| clor_dx: ∀I,K2,V2. |K1| < |L2| → (K1 ⊢ |L2|-|K1|-1 ~ϵ 𝐅*[yinj 0]⦃T⦄ → ⊥) → - ⇩[|L2|-|K1|-1] L2 ≡ K2.ⓑ{I}V2 → clor T L2 K1 V1 V2 -. - -definition llor: relation4 term lenv lenv lenv ≝ - λT,L2. lpx_sn (clor T L2). - -interpretation - "lazy union (local environment)" - 'LazyOr L1 T L2 L = (llor T L2 L1 L). - -(* Basic properties *********************************************************) - -lemma llor_pair_sn: ∀I,L1,L2,L,V,T. L1 ⩖[T] L2 ≡ L → - |L1| < |L2| → L1 ⊢ |L2|-|L1|-1 ~ϵ 𝐅*[yinj 0]⦃T⦄ → - L1.ⓑ{I}V ⩖[T] L2 ≡ L.ⓑ{I}V. -/3 width=2 by clor_sn, lpx_sn_pair/ qed. - -lemma llor_pair_dx: ∀I,J,L1,L2,L,K2,V1,V2,T. L1 ⩖[T] L2 ≡ L → - |L1| < |L2| → (L1 ⊢ |L2|-|L1|-1 ~ϵ 𝐅*[yinj 0]⦃T⦄ → ⊥) → - ⇩[|L2|-|L1|-1] L2 ≡ K2.ⓑ{J}V2 → - L1.ⓑ{I}V1 ⩖[T] L2 ≡ L.ⓑ{I}V2. -/4 width=3 by clor_dx, lpx_sn_pair/ qed. - -lemma llor_total: ∀T,L2,L1. |L1| ≤ |L2| → ∃L. L1 ⩖[T] L2 ≡ L. -#T #L2 #L1 elim L1 -L1 /2 width=2 by ex_intro/ -#L1 #I1 #V1 #IHL1 normalize -#H elim IHL1 -IHL1 /2 width=3 by transitive_le/ -#L #HT elim (cofrees_dec L1 T 0 (|L2|-|L1|-1)) -[ /3 width=2 by llor_pair_sn, ex_intro/ -| elim (ldrop_O1_lt (Ⓕ) L2 (|L2|-|L1|-1)) - /5 width=4 by llor_pair_dx, monotonic_lt_minus_l, ex_intro/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/llor_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/llor_alt.ma deleted file mode 100644 index b62a00263..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/llor_alt.ma +++ /dev/null @@ -1,66 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/relocation/lpx_sn_alt.ma". -include "basic_2/substitution/llor.ma". - -(* POINTWISE UNION FOR LOCAL ENVIRONMENTS ***********************************) - -(* Alternative definition ***************************************************) - -theorem llor_intro_alt: ∀T,L2,L1,L. |L1| ≤ |L2| → |L1| = |L| → - (∀I1,I,K1,K,V1,V,i. ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L ≡ K.ⓑ{I}V → - (K1 ⊢ |L2|-|L1|+i ~ϵ 𝐅*[yinj 0]⦃T⦄ → I1 = I ∧ V1 = V) ∧ - (∀I2,K2,V2. (K1 ⊢ |L2|-|L1|+i ~ϵ 𝐅*[yinj 0]⦃T⦄ → ⊥) → - ⇩[|L2|-|L1|+i] L2 ≡ K2.ⓑ{I2}V2 → I1 = I ∧ V2 = V - ) - ) → L1 ⩖[T] L2 ≡ L. -#T #L2 #L1 #L #HL12 #HL1 #IH @lpx_sn_intro_alt // -HL1 -#I1 #I #K1 #K #V1 #V #i #HLK1 #HLK -lapply (ldrop_fwd_length_minus4 … HLK1) -lapply (ldrop_fwd_length_le4 … HLK1) -normalize in ⊢ (%→%→?); #HKL1 #Hi -lapply (plus_minus_minus_be_aux … HL12 Hi) // -Hi Hi -Hi -elim (IH … HLK1 HLK) -IH #HI1 * -/4 width=5 by or_introl, or_intror, and3_intro, ex4_3_intro/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_llor.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_llor.ma new file mode 100644 index 000000000..a22618f1c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_llor.ma @@ -0,0 +1,34 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/relocation/lpx_sn_alt.ma". +include "basic_2/substitution/llor.ma". +include "basic_2/substitution/lleq_alt.ma". + +(* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****) + +(* Inversion lemmas on poinwise union for local environments ****************) + +lemma llpx_sn_llor_fwd_sn: ∀R. (∀L. reflexive … (R L)) → + ∀L1,L2,T. llpx_sn R 0 T L1 L2 → + ∀L. L1 ⩖[T] L2 ≡ L → lpx_sn R L1 L. +#R #HR #L1 #L2 #T #H1 #L #H2 +elim (llpx_sn_llpx_sn_alt … H1) -H1 #HL12 #IH1 +elim H2 -H2 #_ #HL1 #IH2 +@lpx_sn_intro_alt // #I1 #I #K1 #K #V1 #V #i #HLK1 #HLK +lapply (ldrop_fwd_length_lt2 … HLK) #HiL +elim (ldrop_O1_lt (Ⓕ) L2 i) // -HiL -HL1 -HL12 #I2 #K2 #V2 #HLK2 +elim (IH2 … HLK1 HLK2 HLK) -IH2 -HLK * [ /2 width=1 by conj/ ] +#HnT #H1 #H2 elim (IH1 … HnT … HLK1 HLK2) -IH1 -HnT -HLK1 -HLK2 /2 width=1 by conj/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index 54cb06e9f..b97ddd853 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -211,15 +211,15 @@ table { [ { "substitution" * } { [ { "lazy equivalence" * } { [ "fleq ( ⦃?,?,?⦄ ⋕[?] ⦃?,?,?⦄ )" "fleq_fleq" * ] - [ "lleq ( ? ⋕[?,?] ? )" "lleq_alt" + "lleq_alt_rec" + "lleq_leq" + "lleq_ldrop" + "lleq_fqus" + "lleq_lleq" * ] + [ "lleq ( ? ⋕[?,?] ? )" "lleq_alt" + "lleq_alt_rec" + "lleq_leq" + "lleq_ldrop" + "lleq_fqus" + "lleq_llor" + "lleq_lleq" * ] } ] [ { "lazy pointwise extension of a relation" * } { - [ "llpx_sn" "llpx_sn_alt" + "llpx_sn_alt_rec" + "llpx_sn_tc" + "llpx_sn_leq" + "llpx_sn_ldrop" + "llpx_sn_lpx_sn" * ] + [ "llpx_sn" "llpx_sn_alt" + "llpx_sn_alt_rec" + "llpx_sn_tc" + "llpx_sn_leq" + "llpx_sn_ldrop" + "llpx_sn_lpx_sn" + "llpx_sn_llor" * ] } ] [ { "pointwise union for local environments" * } { - [ "llor ( ? ⩖[?] ? ≡ ? )" "llor_alt" * ] + [ "llor ( ? ⩖[?] ? ≡ ? )" * ] } ] [ { "context-sensitive exclusion from free variables" * } {