From 913070a2e9de2867b57e565c46800437a1c36104 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 26 Mar 2022 21:12:19 +0100 Subject: [PATCH] update in delayed updating + additions to lift --- .../substitution/lift_constructors.ma | 16 ++++++++- .../delayed_updating/substitution/lift_id.ma | 30 +++++++++++++++++ .../substitution/lift_prototerm_id.ma | 33 +++++++++++++++++++ .../delayed_updating/substitution/lift_uni.ma | 28 ++++++++++++++++ 4 files changed, 106 insertions(+), 1 deletion(-) create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_id.ma create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_id.ma create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_uni.ma diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma index 31f4bbc14..772c837fb 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma @@ -12,11 +12,17 @@ (* *) (**************************************************************************) -include "delayed_updating/substitution/lift_prototerm_eq.ma". +include "delayed_updating/substitution/lift_prototerm_id.ma". +include "delayed_updating/substitution/lift_uni.ma". include "delayed_updating/syntax/prototerm_constructors.ma". (* LIFT FOR PROTOTERM *******************************************************) +lemma lift_iref_bi (t1) (t2) (n): + t1 ⇔ t2 → 𝛗n.t1 ⇔ 𝛗n.t2. +/2 width=1 by subset_equivalence_ext_f1_bi/ +qed. + lemma lift_iref_sn (f) (t:prototerm) (n:pnat): (𝛗f@❨n❩.↑[⇂*[n]f]t) ⊆ ↑[f](𝛗n.t). #f #t #n #p * #q * #r #Hr #H1 #H2 destruct @@ -35,3 +41,11 @@ lemma lift_iref (f) (t) (n:pnat): (𝛗f@❨n❩.↑[⇂*[n]f]t) ⇔ ↑[f](𝛗n.t). /3 width=1 by conj, lift_iref_sn, lift_iref_dx/ qed. + +lemma lift_iref_uni (t) (m) (n): + (𝛗(n+m).t) ⇔ ↑[𝐮❨m❩](𝛗n.t). +#t #m #n +@(subset_eq_trans … (lift_iref …)) +nsucc_pnpred (lift_path_id p) +/2 width=1 by in_comp_lift_bi/ +qed-. + +lemma lift_term_id_dx (t): + ↑[𝐢]t ⊆ t. +#t #p * #q #Hq #H destruct // +qed-. + +lemma lift_term_id (t): + t ⇔ ↑[𝐢]t. +/3 width=2 by lift_term_id_dx, lift_term_id_sn, conj/ +qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_uni.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_uni.ma new file mode 100644 index 000000000..cd6c79533 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_uni.ma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lift_id.ma". +include "ground/relocation/tr_uni_pap.ma". +include "ground/relocation/tr_uni_tls.ma". + +(* LIFT FOR PATH ***********************************************************) + +(* Constructions with tr_uni ***********************************************) + +lemma lift_path_d_sn_uni (p) (m) (n): + (𝗱(n+m)◗p) = ↑[𝐮❨m❩](𝗱(n)◗p). +#p #m #n +nsucc_pnpred +