From: Ferruccio Guidi Date: Thu, 22 Sep 2016 13:51:29 +0000 (+0000) Subject: basic_2: stronger supclosure allows better inversion lemmas X-Git-Tag: make_still_working~535 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=325bc2fb36e8f8db99a152037d71332c9ac7eff9;p=helm.git basic_2: stronger supclosure allows better inversion lemmas ground_2: more results on sle and sor (rtmap) --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees_etc.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees_etc.etc deleted file mode 100644 index 3fcd30d9b..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees_etc.etc +++ /dev/null @@ -1,136 +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/drops_weight.ma". -include "basic_2/s_computation/fqup_weight.ma". -include "basic_2/s_computation/fqus_fqup.ma". -include "basic_2/static/frees.ma". - -corec lemma sle_refl: ∀f. f ⊆ f. -#f cases (pn_split f) * #g #H -[ @(sle_push … H H) | @(sle_next … H H) ] -H // -qed. - -lemma sle_inv_tl1: ∀f1,f2. ⫱f1 ⊆ f2 → f1 ⊆ ⫯f2. -#f1 elim (pn_split f1) * #g #H destruct -/2 width=5 by sle_next, sle_weak/ -qed-. - -axiom sor_tls: ∀f1,f2,f. f1 ⋓ f2 ≡ f → - ∀n. ⫱*[n]f1 ⋓ ⫱*[n]f2 ≡ ⫱*[n]f. - -axiom sor_sle1: ∀f1,f2,f. f1 ⋓ f2 ≡ f → - ∀g. g ⊆ f1 → g ⊆ f. - -axiom sor_sle2: ∀f1,f2,f. f1 ⋓ f2 ≡ f → - ∀g. g ⊆ f2 → g ⊆ f. - -lemma fqus_inv_refl_atom3: ∀I,G,L,X. ⦃G, L, ⓪{I}⦄ ⊐* ⦃G, L, X⦄ → ⓪{I} = X. -#I #G #L #X #H elim (fqus_inv_fqup … H) -H [2: * // ] -#H lapply (fqup_fwd_fw … H) -H -#H elim (lt_le_false … H) -H /2 width=1 by monotonic_le_plus_r/ -qed-. - -axiom drops_T_isuni_inv_refl: ∀n,L. ⬇*[n] L ≡ L → n = 0. - -axiom fqus_split_fqu: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → - (∧∧ G1 = G2 & L1 = L2 & T1 = T2) ∨ - ∃∃G,L,T. ⦃G1, L1, T1⦄ ⊐ ⦃G, L, T⦄ & ⦃G, L, T⦄ ⊐* ⦃G2, L2, T2⦄. - -axiom fqus_inv_atom1: ∀I,G1,G2,L2,T2. ⦃G1, ⋆, ⓪{I}⦄ ⊐* ⦃G2, L2, T2⦄ → - ∧∧ G1 = G2 & ⋆ = L2 & ⓪{I} = T2. - -axiom fqus_inv_sort1: ∀G1,G2,L1,L2,T2,s. ⦃G1, L1, ⋆s⦄ ⊐* ⦃G2, L2, T2⦄ → - ∧∧ G1 = G2 & L1 = L2 & ⋆s = T2. - -axiom fqus_inv_zero1: ∀I,G1,G2,L1,L2,V1,T2. ⦃G1, L1.ⓑ{I}V1, #0⦄ ⊐* ⦃G2, L2, T2⦄ → - (∧∧ G1 = G2 & L1.ⓑ{I}V1 = L2 & #0 = T2) ∨ ⦃G1, L1, V1⦄ ⊐* ⦃G2, L2, T2⦄. - -axiom fqus_inv_lref1: ∀I,G1,G2,L1,L2,V1,T2,i. ⦃G1, L1.ⓑ{I}V1, #⫯i⦄ ⊐* ⦃G2, L2, T2⦄ → - (∧∧ G1 = G2 & L1.ⓑ{I}V1 = L2 & #(⫯i) = T2) ∨ ⦃G1, L1, #i⦄ ⊐* ⦃G2, L2, T2⦄. - -axiom fqus_inv_gref1: ∀G1,G2,L1,L2,T2,l. ⦃G1, L1, §l⦄ ⊐* ⦃G2, L2, T2⦄ → - ∧∧ G1 = G2 & L1 = L2 & §l = T2. - -axiom fqus_inv_bind1: ∀p,I,G1,G2,L1,L2,V1,T1,T2. ⦃G1, L1, ⓑ{p,I}V1.T1⦄ ⊐* ⦃G2, L2, T2⦄ → - ∨∨ ∧∧ G1 = G2 & L1 = L2 & ⓑ{p,I}V1.T1 = T2 - | ⦃G1, L1, V1⦄ ⊐* ⦃G2, L2, T2⦄ - | ⦃G1, L1.ⓑ{I}V1, T1⦄ ⊐* ⦃G2, L2, T2⦄. - -axiom fqus_inv_flat1: ∀I,G1,G2,L1,L2,V1,T1,T2. ⦃G1, L1, ⓕ{I}V1.T1⦄ ⊐* ⦃G2, L2, T2⦄ → - ∨∨ ∧∧ G1 = G2 & L1 = L2 & ⓕ{I}V1.T1 = T2 - | ⦃G1, L1, V1⦄ ⊐* ⦃G2, L2, T2⦄ - | ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄. - -(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************) - -lemma frees_drops_sle: ∀f1,G,L1,T1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 → - ∀L2,T2. ⦃G, L1, T1⦄ ⊐* ⦃G, L2, T2⦄ → - ∀I,n. ⬇*[n] L1 ≡ L2.ⓑ{I}T2 → - ∃∃f2. L2 ⊢ 𝐅*⦃T2⦄ ≡ f2 & f2 ⊆ ⫱*[⫯n] f1. -#f1 #G #L1 #T1 #H elim H -f1 -L1 -T1 -[ #f1 #J #Hf1 #L2 #T2 #H12 #I #n #HL12 - elim (fqus_inv_atom1 … H12) -H12 #H1 #H2 #H3 destruct - lapply (drops_fwd_lw … HL12) -HL12 #HL12 - elim (lt_le_false … HL12) -HL12 // -| #f1 #J #L1 #V1 #s #_ #_ #L2 #T2 #H12 #I #n #HL12 - elim (fqus_inv_sort1 … H12) -H12 #H1 #H2 #H3 destruct - lapply (drops_fwd_lw … HL12) -HL12 #HL12 - elim (lt_le_false … HL12) -HL12 // -| #f1 #J #L1 #V1 #Hf1 #IH #L2 #T2 #H12 - elim (fqus_inv_zero1 … H12) -H12 [ * | #H12 #I * ] - [ -IH -Hf1 #H1 #H2 #H3 #I #n #HL12 destruct - lapply (drops_fwd_lw … HL12) -HL12 #HL12 - elim (lt_le_false … HL12) -HL12 // - | -IH -H12 #HL12 lapply (drops_fwd_isid … HL12 ?) -HL12 // - #H destruct /3 width=3 by sle_refl, ex2_intro/ - | -Hf1 #n #HL12 lapply (drops_inv_drop1 … HL12) -HL12 - #HL12 elim (IH … H12 … HL12) -IH -H12 -HL12 /3 width=3 by ex2_intro/ - ] -| #f1 #J #L1 #V1 #i #Hf1 #IH #L2 #T2 #H12 - elim (fqus_inv_lref1 … H12) -H12 [ * | #H12 #I * ] - [ -IH -Hf1 #H1 #H2 #H3 #I #n #HL12 destruct - lapply (drops_fwd_lw … HL12) -HL12 #HL12 - elim (lt_le_false … HL12) -HL12 // - | -IH #HL12 lapply (drops_fwd_isid … HL12 ?) -HL12 // - #H destruct <(fqus_inv_refl_atom3 … H12) -H12 /2 width=3 by sle_refl, ex2_intro/ - | -Hf1 #I #HL12 lapply (drops_inv_drop1 … HL12) -HL12 - #HL12 elim (IH … H12 … HL12) -IH -H12 -HL12 /3 width=3 by ex2_intro/ - ] -| #f1 #J #L1 #V1 #l #_ #_ #L2 #T2 #H12 #I #n #HL12 - elim (fqus_inv_gref1 … H12) -H12 #H1 #H2 #H3 destruct - lapply (drops_fwd_lw … HL12) -HL12 #HL12 - elim (lt_le_false … HL12) -HL12 // -| #f1V #f1T #f1 #p #J #L1 #V #T #_ #_ #Hf1 #IHV #IHT #L2 #T2 #H12 #I #n #HL12 - elim (fqus_inv_bind1 … H12) -H12 [ * |*: #H12 ] - [ -IHV -IHT -Hf1 #H1 #H2 #H3 destruct - lapply (drops_fwd_lw … HL12) -HL12 #HL12 - elim (lt_le_false … HL12) -HL12 // - | -IHT elim (IHV … H12 … HL12) -IHV -H12 -HL12 - /4 width=6 by sor_tls, sor_sle1, ex2_intro/ - | -IHV elim (IHT … H12 I (⫯n)) -IHT -H12 /2 width=1 by drops_drop/ -HL12 -