From: Ferruccio Guidi Date: Sun, 30 Jan 2022 17:51:41 +0000 (+0100) Subject: update in delayed_updating X-Git-Tag: make_still_working~97 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f2a1fcef1f05dae5dff517ffc0a8439f6071955b;p=helm.git update in delayed_updating + additions to lift + bugs fixed in ifr --- diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notes.txt b/matita/matita/contribs/lambdadelta/delayed_updating/notes.txt new file mode 100644 index 000000000..d70abbe43 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notes.txt @@ -0,0 +1,3 @@ +1) (⫯f)@(1) = 1 +2) f@❨d-n❩ = k → n <= d → (f∘𝐮❨n❩)@❨d❩ = k +3) f@❨d-1❩ = k-1 → 1 < d → 1 < k → (⫯f)@❨d❩ = k diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma index b188a7730..1371c3a31 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma @@ -26,7 +26,7 @@ include "ground/xoa/and_4.ma". definition ifr (p) (q): relation2 prototerm prototerm ≝ λt1,t2. ∃∃b,n. let r ≝ p●𝗔◗b●𝗟◗q in - ∧∧ ⊗b ϵ 𝐁 & ∀f. ❘𝗟◗q❘ = (↑[q]⫯f)@❨n❩ & r◖𝗱n ϵ t1 & + ∧∧ ⊗b ϵ 𝐁 & ∀f. ↑❘q❘ = (↑[q]f)@❨n❩ & r◖𝗱n ϵ t1 & t1[⋔r←↑[𝐮❨❘b●𝗟◗q❘❩](t1⋔(p◖𝗦))] ⇔ t2 . 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 0202dc926..6825b13aa 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma @@ -12,16 +12,20 @@ (* *) (**************************************************************************) +include "ground/relocation/tr_compose_compose.ma". +include "ground/relocation/tr_compose_pn.ma". include "delayed_updating/substitution/lift_eq.ma". -axiom lift_path_after (p) (f1) (f2): +lemma lift_path_after (p) (f1) (f2): ↑[f2]↑[f1]p = ↑[f2∘f1]p. -(* -#p @(path_ind_lift … p) -p // [ #n | #n #l #p | #p ] #IH #f1 #f2 -[ (lift_path_eq_repl … (tr_compose_assoc …)) // | tr_compose_push_bi // +] +qed. + include "delayed_updating/substitution/lift_prototerm.ma". axiom lift_term_after (t) (f1) (f2): @@ -32,7 +36,7 @@ include "delayed_updating/syntax/prototerm_constructors.ma". (* LIFT FOR PROTOTERM *******************************************************) lemma lift_iref_after_sn (f) (t) (n:pnat): - ↑[f∘𝐮❨n❩]t ⊆ ↑[f](𝛗n.t). + (↑[f∘𝐮❨n❩]t) ⊆ ↑[f](𝛗n.t). #f #t #n #p * #q #Hq #H0 destruct @(ex2_intro … (𝗱n◗𝗺◗q)) /2 width=1 by in_comp_iref/ diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma index 0273a3eb8..9e23b2cb9 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma @@ -13,12 +13,13 @@ (**************************************************************************) include "delayed_updating/substitution/lift.ma". -include "ground/notation/relations/ringeq_3.ma". +include "ground/relocation/tr_compose_eq.ma". +include "ground/relocation/tr_pn_eq.ma". (* LIFT FOR PATH ***********************************************************) definition lift_exteq (A): relation2 (lift_continuation A) (lift_continuation A) ≝ - λk1,k2. ∀f,p. k1 f p = k2 f p. + λk1,k2. ∀f1,f2,p. f1 ≗ f2 → k1 f1 p = k2 f2 p. interpretation "extensional equivalence (lift continuation)" @@ -26,41 +27,57 @@ interpretation (* Constructions with lift_exteq ********************************************) -lemma lift_eq_repl_sn (A) (p) (k1) (k2) (f): - k1 ≗{A} k2 → ↑❨k1, f, p❩ = ↑❨k2, f, p❩. -#A #p @(path_ind_lift … p) -p [| #n | #n #l0 #q ] -[ #k1 #k2 #f #Hk lift_lcons_alt >lift_append_rcons_sn +| lift_lcons_alt // >lift_append_rcons_sn // lift_lcons_alt >lift_append_rcons_sn +| lift_lcons_alt >lift_append_rcons_sn // lift_lcons_alt >lift_append_rcons_sn +| lift_lcons_alt >lift_append_rcons_sn //