From: Ferruccio Guidi Date: Wed, 9 May 2018 18:10:36 +0000 (+0200) Subject: update in groud_2 and models X-Git-Tag: make_still_working~327 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc update in groud_2 and models + denotation is preserved by r-transition + minor additions --- diff --git a/matita/matita/contribs/lambdadelta/apps_2/etc/models/model_cpr.etc b/matita/matita/contribs/lambdadelta/apps_2/etc/models/model_cpr.etc deleted file mode 100644 index cc96e9954..000000000 --- a/matita/matita/contribs/lambdadelta/apps_2/etc/models/model_cpr.etc +++ /dev/null @@ -1,54 +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/reduction/cpr.ma". -include "apps_2/models/model_drop.ma". - -(* MODEL ********************************************************************) - -(* Forward lemmas on context-sensitive parallel reduction for terms *********) - -lemma sound_fwd_cpr: ∀M. sound M → extensional M → - ∀sv,gv,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → - ∀lv. lv ∈ 〚L〛⦋M⦌{sv, gv} → 〚T1〛{sv, gv, lv} = 〚T2〛{sv, gv, lv}. -#M #H1M #H2M #sv #gv #G #L #T1 #T2 #H elim H -G -L -T1 -T2 // -[ #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #lv #Hlv >(m2 … H1M) - <(sound_fwd_lift … H1M H2M … HVW2) -HVW2 - lapply (sound_drop … HLK … Hlv) // -L -H2M #H - elim (li_inv_ldef … H) -H #v #HK #H - elim (lower_inv_raise_be … H) -H #H >H -H #Hlv - (m4 … H1M) >(m4 … H1M) -H1M (m6 … H1M) >(m6 … H1M) -H1M /3 width=1 by eq_f2/ - | -IHV12 >(m7 … H1M) >(m7 … H1M) -H1M /2 width=1 by/ - ] -| #G #L #V #U1 #U2 #T2 #_ #HTU2 #IHU12 #lv #Hlv >(m4 … H1M) - >IHU12 -IHU12 /2 width=1 by li_ldef/ - <(sound_fwd_lift … H1M H2M … HTU2) -H2M -HTU2 - /2 width=1 by sound_ti_eq_l/ -| #G #L #V #T1 #T2 #_ #IHT12 #lv #Hlv >(m7 … H1M) -H1M /2 width=1 by/ -| #a #G #L #V1 #V2 #W1 #w2 #T1 #T2 #_ #_ #_ #IHV12 #_ #IHT12 #lv #Hlv - >(m6 … H1M) >(m8 … H1M) >(m4 … H1M) >(m7 … H1M) -H1M - >IHV12 -IHV12 /3 width=1 by li_ldec/ -| #a #G #L #V1 #V2 #W2 #U1 #U2 #T1 #T2 #_ #HVW2 #_ #_ #IHV12 #IHU12 #IHT12 #lv #Hlv - >(m6 … H1M) >(m4 … H1M) >(m4 … H1M) >(m6 … H1M) - >IHV12 -IHV12 // vlift_eq /2 width=1 by mq/ +qed. + +lemma ti_lref_vlift_gt (M): is_model M → + ∀gv,lv,d,i. ⟦#(↑i)⟧[gv,⫯[d]lv] ≗{M} ⟦#i⟧[gv,lv]. +#M #HM #gv #lv #d #i +@(mr … HM) [4,5: @(seq_sym … HM) @(ml … HM) |1,2: skip ] +>vlift_gt /2 width=1 by mq/ +qed. diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma b/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma index 87a0800e7..e784d3b7a 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/veq.ma @@ -32,10 +32,22 @@ lemma veq_repl (M): is_model M → replace_2 … (veq M) (veq M) (veq M). /2 width=5 by mr/ qed-. +lemma veq_sym (M): is_model M → symmetric … (veq M). +/3 width=5 by veq_repl, veq_refl/ qed-. + +lemma veq_trans (M): is_model M → Transitive … (veq M). +/3 width=5 by veq_repl, veq_refl/ qed-. + +(* Properties with extebsional equivalence **********************************) + lemma ext_veq (M): is_model M → ∀lv1,lv2. lv1 ≐ lv2 → lv1 ≗{M} lv2. /2 width=1 by mq/ qed. +lemma veq_repl_exteq (M): is_model M → + replace_2 … (veq M) (exteq …) (exteq …). +/2 width=5 by mr/ qed-. + lemma exteq_veq_trans (M): ∀lv1,lv. lv1 ≐ lv → ∀lv2. lv ≗{M} lv2 → lv1 ≗ lv2. // qed-. diff --git a/matita/matita/contribs/lambdadelta/apps_2/notation/models/ringeq_4.ma b/matita/matita/contribs/lambdadelta/apps_2/notation/models/ringeq_4.ma deleted file mode 100644 index bb6c30068..000000000 --- a/matita/matita/contribs/lambdadelta/apps_2/notation/models/ringeq_4.ma +++ /dev/null @@ -1,27 +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 *) -(* *) -(**************************************************************************) - -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) - -notation < "hvbox( L ⊢ break term 46 T1 ≗ break term 46 T2 )" - non associative with precedence 45 - for @{ 'RingEq $M $L $T1 $T2 }. - -notation > "hvbox( L ⊢ break term 46 T1 ≗ break term 46 T2 )" - non associative with precedence 45 - for @{ 'RingEq ? $L $T1 $T2 }. - -notation > "hvbox( L ⊢ break term 46 T1 ≗{ break term 46 M } break term 46 T2 )" - non associative with precedence 45 - for @{ 'RingEq $M $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/apps_2/notation/models/ringeq_5.ma b/matita/matita/contribs/lambdadelta/apps_2/notation/models/ringeq_5.ma new file mode 100644 index 000000000..94e36c02d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/notation/models/ringeq_5.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation < "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ≗ break term 46 T2 )" + non associative with precedence 45 + for @{ 'RingEq $M $G $L $T1 $T2 }. + +notation > "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ≗ break term 46 T2 )" + non associative with precedence 45 + for @{ 'RingEq ? $G $L $T1 $T2 }. + +notation > "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ≗{ break term 46 M } break term 46 T2 )" + non associative with precedence 45 + for @{ 'RingEq $M $G $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl index b68727314..6f9d8a2e7 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl @@ -12,7 +12,7 @@ table { class "orange" [ { "models" * } { [ { "denotational equivalence" * } { - [ "deq" + "( ? ⊢ ? ≗{?} ? )" * ] + [ "deq" + "( ? ⊢ ? ≗{?} ? )" "deq_cpr" * ] } ] [ { "evaluation equivalence" * } { @@ -28,6 +28,7 @@ table { "model_vlift" + "( ⫯{?}[?]? )" + "( ⫯{?}[?←?]? )" "model_props" "model_li" + "( ? ϵ ⟦?⟧{?}[?] )" + "model_gi" * ] } ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma index 042e814cd..6411f701c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma @@ -98,6 +98,66 @@ lemma cpr_inv_flat1: ∀h,I,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓕ{I}V1.U1 ➡[h] U2 ] qed-. +(* Basic eliminators ********************************************************) + +lemma cpr_ind (h): ∀R:relation4 genv lenv term term. + (∀I,G,L. R G L (⓪{I}) (⓪{I})) → + (∀G,K,V1,V2,W2. ⦃G, K⦄ ⊢ V1 ➡[h] V2 → R G K V1 V2 → + ⬆*[1] V2 ≘ W2 → R G (K.ⓓV1) (#0) W2 + ) → (∀I,G,K,T,U,i. ⦃G, K⦄ ⊢ #i ➡[h] T → R G K (#i) T → + ⬆*[1] T ≘ U → R G (K.ⓘ{I}) (#↑i) (U) + ) → (∀p,I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ➡[h] T2 → + R G L V1 V2 → R G (L.ⓑ{I}V1) T1 T2 → R G L (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2) + ) → (∀I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L⦄ ⊢ T1 ➡[h] T2 → + R G L V1 V2 → R G L T1 T2 → R G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2) + ) → (∀G,L,V,T1,T,T2. ⦃G, L.ⓓV⦄ ⊢ T1 ➡[h] T → R G (L.ⓓV) T1 T → + ⬆*[1] T2 ≘ T → R G L (+ⓓV.T1) T2 + ) → (∀G,L,V,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 → R G L T1 T2 → + R G L (ⓝV.T1) T2 + ) → (∀p,G,L,V1,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L⦄ ⊢ W1 ➡[h] W2 → ⦃G, L.ⓛW1⦄ ⊢ T1 ➡[h] T2 → + R G L V1 V2 → R G L W1 W2 → R G (L.ⓛW1) T1 T2 → + R G L (ⓐV1.ⓛ{p}W1.T1) (ⓓ{p}ⓝW2.V2.T2) + ) → (∀p,G,L,V1,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V → ⦃G, L⦄ ⊢ W1 ➡[h] W2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ➡[h] T2 → + R G L V1 V → R G L W1 W2 → R G (L.ⓓW1) T1 T2 → + ⬆*[1] V ≘ V2 → R G L (ⓐV1.ⓓ{p}W1.T1) (ⓓ{p}W2.ⓐV2.T2) + ) → + ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 → R G L T1 T2. +#h #R #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #G #L #T1 #T2 +* #c #HC #H generalize in match HC; -HC +elim H -c -G -L -T1 -T2 +[ /2 width=3 by ex2_intro/ +| #G #L #s #H + lapply (isrt_inv_01 … H) -H #H destruct +| /3 width=4 by ex2_intro/ +| #c #G #L #V1 #V2 #W2 #_ #_ #_ #H + elim (isrt_inv_plus_SO_dx … H) -H // #n #_ #H destruct +| /3 width=4 by ex2_intro/ +| #cV #cT #p #I #G #L #V1 #V2 #T1 #T2 #HV12 #HT12 #IHV #IHT #H + elim (isrt_O_inv_max … H) -H #HcV #HcT + /4 width=3 by isr_inv_shift, ex2_intro/ +| #cV #cT #G #L #V1 #V2 #T1 #T2 #HV12 #HT12 #IHV #IHT #H + elim (isrt_O_inv_max … H) -H #HcV #HcT + /4 width=3 by isr_inv_shift, ex2_intro/ +| #cU #cT #G #L #U1 #U2 #T1 #T2 #HUT #HU12 #HT12 #IHU #IHT #H + elim (isrt_O_inv_max … H) -H #HcV #HcT + /3 width=3 by ex2_intro/ +| /4 width=4 by isrt_inv_plus_O_dx, ex2_intro/ +| /4 width=4 by isrt_inv_plus_O_dx, ex2_intro/ +| #c #G #L #U1 #U2 #T #_ #_ #H + elim (isrt_inv_plus_SO_dx … H) -H // #n #_ #H destruct +| #cV #cW #cT #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12 #IHV #IHW #IHT #H + lapply (isrt_inv_plus_O_dx … H ?) -H // #H + elim (isrt_O_inv_max … H) -H #H #HcT + elim (isrt_O_inv_max … H) -H #HcV #HcW + /4 width=3 by isr_inv_shift, ex2_intro/ +| #cV #cW #cT #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HW12 #HT12 #IHV #IHW #IHT #H + lapply (isrt_inv_plus_O_dx … H ?) -H // #H + elim (isrt_O_inv_max … H) -H #H #HcT + elim (isrt_O_inv_max … H) -H #HcV #HcW + /4 width=4 by isr_inv_shift, ex2_intro/ +] +qed-. + (* Basic_1: removed theorems 12: pr0_subst0_back pr0_subst0_fwd pr0_subst0 pr0_delta1 diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma index ffe968f54..97636d5d8 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma @@ -1,4 +1,3 @@ - (**************************************************************************) (* ___ *) (* ||M|| *) diff --git a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_max.ma b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_max.ma index cfd1be7e5..058b1a3c0 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_max.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_max.ma @@ -84,6 +84,13 @@ elim (max_inv_dx … H) -H #ri1 #rs1 #ti1 #ts1 #ri2 #rs2 #ti2 #ts2 #_ #_ #H1 #H2 elim (max_inv_O3 … H1) -H1 /3 width=5 by ex3_2_intro, ex1_2_intro/ qed-. +lemma isrt_O_inv_max: ∀c1,c2. 𝐑𝐓⦃0, c1 ∨ c2⦄ → ∧∧ 𝐑𝐓⦃0, c1⦄ & 𝐑𝐓⦃0, c2⦄. +#c1 #c2 #H +elim (isrt_inv_max … H) -H #n1 #n2 #Hn1 #Hn2 #H +elim (max_inv_O3 … H) -H #H1 #H2 destruct +/2 width=1 by conj/ +qed-. + lemma isrt_inv_max_O_dx: ∀n,c1,c2. 𝐑𝐓⦃n, c1 ∨ c2⦄ → 𝐑𝐓⦃0, c2⦄ → 𝐑𝐓⦃n, c1⦄. #n #c1 #c2 #H #H2 elim (isrt_inv_max … H) -H #n1 #n2 #Hn1 #Hn2 #H destruct