From: Ferruccio Guidi Date: Mon, 20 Jun 2022 23:33:06 +0000 (+0200) Subject: update in delayed_updating X-Git-Tag: make_still_working~58 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3bf7a0b4185dbffe5b822c907956acdbe2d1c559;p=helm.git update in delayed_updating + WIP on lift + notation changed for delayed updating (term constructor) + minor corrections --- diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/phi_2.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/phi_2.etc new file mode 100644 index 000000000..127815423 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/phi_2.etc @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR DELAYED UPDATING ********************************************) + +notation "hvbox( 𝛗 break term 76 n. break term 70 t )" + non associative with precedence 70 + for @{ 'Phi $n $t }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_d_phi_0.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_d_phi_0.ma deleted file mode 100644 index d45317626..000000000 --- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_d_phi_0.ma +++ /dev/null @@ -1,19 +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 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR DELAYED UPDATING ********************************************) - -notation "hvbox( 𝐃𝛗 )" - non associative with precedence 70 - for @{ 'ClassDPhi }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_d_tau_0.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_d_tau_0.ma new file mode 100644 index 000000000..8b21ae579 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_d_tau_0.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR DELAYED UPDATING ********************************************) + +notation "hvbox( 𝐃𝛕 )" + non associative with precedence 70 + for @{ 'ClassDTau }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/phi_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/phi_2.ma deleted file mode 100644 index 127815423..000000000 --- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/phi_2.ma +++ /dev/null @@ -1,19 +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 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR DELAYED UPDATING ********************************************) - -notation "hvbox( 𝛗 break term 76 n. break term 70 t )" - non associative with precedence 70 - for @{ 'Phi $n $t }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/tau_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/tau_2.ma new file mode 100644 index 000000000..099360cce --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/tau_2.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR DELAYED UPDATING ********************************************) + +notation "hvbox( 𝛕 break term 76 n. break term 70 t )" + non associative with precedence 70 + for @{ 'Tau $n $t }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma index 738553c7d..193136433 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma @@ -26,7 +26,7 @@ definition dfr (p) (q): relation2 prototerm prototerm ≝ λt1,t2. ∃n:pnat. let r ≝ p●𝗔◗𝗟◗q in ∧∧ (𝗟◗q)ᴿ = ↳[n](rᴿ) & r◖𝗱n ϵ t1 & - t1[⋔r←𝛗n.(t1⋔(p◖𝗦))] ⇔ t2 + t1[⋔r←𝛕n.(t1⋔(p◖𝗦))] ⇔ t2 . interpretation diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_eq.ma index a3a349419..c3f6cfa11 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_eq.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_eq.ma @@ -15,6 +15,8 @@ include "delayed_updating/substitution/fsubst.ma". include "delayed_updating/syntax/prototerm_eq.ma". +(* FOCALIZED SUBSTITUTION ***************************************************) + (* Constructions with subset_equivalence ************************************) lemma subset_inclusion_fsubst_bi (t1) (t2) (u1) (u2) (p): diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_lift.ma new file mode 100644 index 000000000..e1be5ded0 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_lift.ma @@ -0,0 +1,54 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "delayed_updating/substitution/fsubst.ma". +include "delayed_updating/substitution/lift_prototerm_eq.ma". +(* +include "delayed_updating/syntax/preterm.ma". +include "delayed_updating/syntax/prototerm_proper.ma". +*) +(* FOCALIZED SUBSTITUTION ***************************************************) + +(* Constructions with lift for preterm **************************************) + +lemma lift_term_fsubst_sn (f) (t) (u) (p): + (↑[f]t)[⋔(↑[f]p)←↑[↑[p]f]u] ⊆ ↑[f](t[⋔p←u]). +#f #t #u #p #ql * * +[ #rl * #r #Hr #H1 #H2 destruct + >lift_path_append + /4 width=3 by in_comp_lift_path_term, or_introl, ex2_intro/ +| * #q #Hq #H1 #H0 + @(ex2_intro … H1) @or_intror @conj // -Hq #r #H2 destruct + /2 width=2 by/ +] +qed-. + +lemma lift_term_fsubst_dx (f) (t) (u) (p): + ↑[f](t[⋔p←u]) ⊆ (↑[f]t)[⋔(↑[f]p)←↑[↑[p]f]u]. +#f #t #u #p #ql * #q * * +[ #r #Hu #H1 #H2 destruct + @or_introl @ex2_intro + [|| nsucc_pnpred