From: Ferruccio Guidi Date: Mon, 20 Dec 2021 18:08:34 +0000 (+0100) Subject: update in ground X-Git-Tag: make_still_working~123 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=04f2f61dbe017ee5a60fd30ae4b6ef355b6e8be4;p=helm.git update in ground + composition for total relocation maps --- diff --git a/matita/matita/contribs/lambdadelta/ground/etc/relocation/pstream_after.etc b/matita/matita/contribs/lambdadelta/ground/etc/relocation/pstream_after.etc deleted file mode 100644 index 1f5bceffe..000000000 --- a/matita/matita/contribs/lambdadelta/ground/etc/relocation/pstream_after.etc +++ /dev/null @@ -1,166 +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 "ground/relocation/pstream_tls.ma". -include "ground/relocation/pstream_istot.ma". -include "ground/relocation/rtmap_after.ma". - -(* RELOCATION P-STREAM ******************************************************) - -corec definition compose: gr_map → gr_map → gr_map. -#f2 * #p1 #f1 @(stream_cons … (f2@❨p1❩)) @(compose ? f1) -compose -f1 -@(⫰*[p1]f2) -defined. - -interpretation "functional composition (nstream)" - 'compose f2 f1 = (compose f2 f1). - -(* Basic properties on compose ***********************************************) - -lemma compose_rew: ∀f2,f1,p1. f2@❨p1❩⨮(⫰*[p1]f2)∘f1 = f2∘(p1⨮f1). -#f2 #f1 #p1 <(stream_rew … (f2∘(p1⨮f1))) normalize // -qed. - -lemma compose_next: ∀f2,f1,f. f2∘f1 = f → (↑f2)∘f1 = ↑f. -#f2 * #p1 #f1 #f nsucc_inj nsucc_inj gr_next_unfold #H cases (compose_inv_S1 … H) -H * -p >gr_next_unfold - /3 width=5 by gr_after_next/ -] -qed-. - -theorem after_total: ∀f1,f2. f2 ⊚ f1 ≘ f2 ∘ f1. -/2 width=1 by after_total_aux/ qed. - -(* Inversion lemmas on after (specific) ***************************************) - -lemma after_inv_xpx: ∀f2,g2,f,p2,p. p2⨮f2 ⊚ g2 ≘ p⨮f → ∀f1. ⫯f1 = g2 → - f2 ⊚ f1 ≘ f ∧ p2 = p. -#f2 #g2 #f #p2 elim p2 -p2 -[ #p #Hf #f1 #H2 elim (gr_after_inv_push_bi … Hf … H2) -g2 [|*: // ] - #g #Hf #H elim (push_inv_seq_dx … H) -H destruct /2 width=1 by conj/ -| #p2 #IH #p #Hf #f1 #H2 elim (gr_after_inv_next_sn … Hf) -Hf [|*: // ] - #g1 #Hg #H1 elim (next_inv_seq_dx … H1) -H1 - #x #Hx #H destruct elim (IH … Hg) [|*: // ] -IH -Hg - #H destruct /2 width=1 by conj/ -] -qed-. - -lemma after_inv_xnx: ∀f2,g2,f,p2,p. p2⨮f2 ⊚ g2 ≘ p⨮f → ∀f1. ↑f1 = g2 → - ∃∃q. f2 ⊚ f1 ≘ q⨮f & q+p2 = p. -#f2 #g2 #f #p2 elim p2 -p2 -[ #p #Hf #f1 #H2 elim (gr_after_inv_push_next … Hf … H2) -g2 [|*: // ] - #g #Hf #H elim (next_inv_seq_dx … H) -H - #x #Hx #Hg destruct /2 width=3 by ex2_intro/ -| #p2 #IH #p #Hf #f1 #H2 elim (gr_after_inv_next_sn … Hf) -Hf [|*: // ] - #g #Hg #H elim (next_inv_seq_dx … H) -H - #x #Hx #H destruct elim (IH … Hg) -IH -Hg [|*: // ] - #m #Hf #Hm destruct /2 width=3 by ex2_intro/ -] -qed-. - -lemma after_inv_const: ∀f2,f1,f,p1,p. - p⨮f2 ⊚ p1⨮f1 ≘ p⨮f → f2 ⊚ f1 ≘ f ∧ 𝟏 = p1. -#f2 #f1 #f #p1 #p elim p -p -[ #H elim (gr_after_inv_push_sn_push … H) -H [|*: // ] - #g2 #Hf #H elim (push_inv_seq_dx … H) -H /2 width=1 by conj/ -| #p #IH #H lapply (gr_after_inv_next_sn_next … H ????) -H /2 width=5 by/ -] -qed-. - -lemma after_inv_total: ∀f2,f1,f. f2 ⊚ f1 ≘ f → f2 ∘ f1 ≡ f. -/2 width=4 by gr_after_mono/ qed-. - -(* Forward lemmas on after (specific) *****************************************) - -lemma after_fwd_hd: ∀f2,f1,f,p1,p. f2 ⊚ p1⨮f1 ≘ p⨮f → f2@❨p1❩ = p. -#f2 #f1 #f #p1 #p #H lapply (gr_after_des_pat ? p1 (𝟏) … H) -H [4:|*: // ] -/3 width=2 by at_inv_O1, sym_eq/ -qed-. - -lemma after_fwd_tls: ∀f,f1,p1,f2,p2,p. p2⨮f2 ⊚ p1⨮f1 ≘ p⨮f → - (⫰*[↓p1]f2) ⊚ f1 ≘ f. -#f #f1 #p1 elim p1 -p1 -[ #f2 #p2 #p #H elim (after_inv_xpx … H) -H // -| #p1 #IH * #q2 #f2 #p2 #p #H elim (after_inv_xnx … H) -H [|*: // ] - #x #Hx #H destruct /2 width=3 by/ -] -qed-. - -lemma after_inv_apply: ∀f2,f1,f,p2,p1,p. p2⨮f2 ⊚ p1⨮f1 ≘ p⨮f → - (p2⨮f2)@❨p1❩ = p ∧ (⫰*[↓p1]f2) ⊚ f1 ≘ f. -/3 width=3 by after_fwd_tls, after_fwd_hd, conj/ qed-. - -(* Properties on apply ******************************************************) - -lemma compose_apply (f2) (f1) (i): f2@❨f1@❨i❩❩ = (f2∘f1)@❨i❩. -/4 width=6 by gr_after_des_pat, at_inv_total, sym_eq/ qed. diff --git a/matita/matita/contribs/lambdadelta/ground/etc/relocation/pstream_tl.etc b/matita/matita/contribs/lambdadelta/ground/etc/relocation/pstream_tl.etc deleted file mode 100644 index 9fa3b818e..000000000 --- a/matita/matita/contribs/lambdadelta/ground/etc/relocation/pstream_tl.etc +++ /dev/null @@ -1,26 +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 "ground/lib/stream_hdtl.ma". -include "ground/relocation/pstream.ma". - -(* RELOCATION P-STREAM ******************************************************) - -(* Properties with stream_tl *************************************************) - -lemma tl_push: ∀f. f = ⫰⫯f. -// qed. - -lemma tl_next: ∀f. ⫰f = ⫰↑f. -* // qed. diff --git a/matita/matita/contribs/lambdadelta/ground/etc/relocation/pstream_tls.etc b/matita/matita/contribs/lambdadelta/ground/etc/relocation/pstream_tls.etc deleted file mode 100644 index d6837045f..000000000 --- a/matita/matita/contribs/lambdadelta/ground/etc/relocation/pstream_tls.etc +++ /dev/null @@ -1,25 +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 "ground/lib/stream_tls.ma". -include "ground/arith/nat_pred_succ.ma". -include "ground/relocation/pstream_tl.ma". - -(* RELOCATION P-STREAM ******************************************************) - -(* Properties with stream_tls ************************************************) - -lemma tls_next: ∀f. ∀p:pnat. ⫰*[p]f = ⫰*[p]↑f. -#f #p >(npsucc_pred p) nsucc_inj nsucc_inj gr_next_unfold #H cases (compose_inv_S1 … H) -H * -p >gr_next_unfold + /3 width=5 by gr_after_next/ +] +qed-. + +theorem after_total: ∀f1,f2. f2 ⊚ f1 ≘ f2 ∘ f1. +/2 width=1 by after_total_aux/ qed. + +(* Inversion lemmas on after (specific) ***************************************) + +lemma after_inv_xpx: ∀f2,g2,f,p2,p. p2⨮f2 ⊚ g2 ≘ p⨮f → ∀f1. ⫯f1 = g2 → + f2 ⊚ f1 ≘ f ∧ p2 = p. +#f2 #g2 #f #p2 elim p2 -p2 +[ #p #Hf #f1 #H2 elim (gr_after_inv_push_bi … Hf … H2) -g2 [|*: // ] + #g #Hf #H elim (push_inv_seq_dx … H) -H destruct /2 width=1 by conj/ +| #p2 #IH #p #Hf #f1 #H2 elim (gr_after_inv_next_sn … Hf) -Hf [|*: // ] + #g1 #Hg #H1 elim (next_inv_seq_dx … H1) -H1 + #x #Hx #H destruct elim (IH … Hg) [|*: // ] -IH -Hg + #H destruct /2 width=1 by conj/ +] +qed-. + +lemma after_inv_xnx: ∀f2,g2,f,p2,p. p2⨮f2 ⊚ g2 ≘ p⨮f → ∀f1. ↑f1 = g2 → + ∃∃q. f2 ⊚ f1 ≘ q⨮f & q+p2 = p. +#f2 #g2 #f #p2 elim p2 -p2 +[ #p #Hf #f1 #H2 elim (gr_after_inv_push_next … Hf … H2) -g2 [|*: // ] + #g #Hf #H elim (next_inv_seq_dx … H) -H + #x #Hx #Hg destruct /2 width=3 by ex2_intro/ +| #p2 #IH #p #Hf #f1 #H2 elim (gr_after_inv_next_sn … Hf) -Hf [|*: // ] + #g #Hg #H elim (next_inv_seq_dx … H) -H + #x #Hx #H destruct elim (IH … Hg) -IH -Hg [|*: // ] + #m #Hf #Hm destruct /2 width=3 by ex2_intro/ +] +qed-. + +lemma after_inv_const: ∀f2,f1,f,p1,p. + p⨮f2 ⊚ p1⨮f1 ≘ p⨮f → f2 ⊚ f1 ≘ f ∧ 𝟏 = p1. +#f2 #f1 #f #p1 #p elim p -p +[ #H elim (gr_after_inv_push_sn_push … H) -H [|*: // ] + #g2 #Hf #H elim (push_inv_seq_dx … H) -H /2 width=1 by conj/ +| #p #IH #H lapply (gr_after_inv_next_sn_next … H ????) -H /2 width=5 by/ +] +qed-. + +lemma after_inv_total: ∀f2,f1,f. f2 ⊚ f1 ≘ f → f2 ∘ f1 ≡ f. +/2 width=4 by gr_after_mono/ qed-. + +(* Forward lemmas on after (specific) *****************************************) + +lemma after_fwd_hd: ∀f2,f1,f,p1,p. f2 ⊚ p1⨮f1 ≘ p⨮f → f2@❨p1❩ = p. +#f2 #f1 #f #p1 #p #H lapply (gr_after_des_pat ? p1 (𝟏) … H) -H [4:|*: // ] +/3 width=2 by at_inv_O1, sym_eq/ +qed-. + +lemma after_fwd_tls: ∀f,f1,p1,f2,p2,p. p2⨮f2 ⊚ p1⨮f1 ≘ p⨮f → + (⫰*[↓p1]f2) ⊚ f1 ≘ f. +#f #f1 #p1 elim p1 -p1 +[ #f2 #p2 #p #H elim (after_inv_xpx … H) -H // +| #p1 #IH * #q2 #f2 #p2 #p #H elim (after_inv_xnx … H) -H [|*: // ] + #x #Hx #H destruct /2 width=3 by/ +] +qed-. + +lemma after_inv_apply: ∀f2,f1,f,p2,p1,p. p2⨮f2 ⊚ p1⨮f1 ≘ p⨮f → + (p2⨮f2)@❨p1❩ = p ∧ (⫰*[↓p1]f2) ⊚ f1 ≘ f. +/3 width=3 by after_fwd_tls, after_fwd_hd, conj/ qed-. + +(* Properties on apply ******************************************************) + +lemma compose_apply (f2) (f1) (i): f2@❨f1@❨i❩❩ = (f2∘f1)@❨i❩. +/4 width=6 by gr_after_des_pat, at_inv_total, sym_eq/ qed. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_pn.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_pn.ma new file mode 100644 index 000000000..e6e9ae515 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_pn.ma @@ -0,0 +1,50 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "ground/relocation/tr_pn_tls.ma". +include "ground/relocation/tr_pap_pn.ma". +include "ground/relocation/tr_compose.ma". + +(* COMPOSITION FOR PARTIAL RELOCATION MAPS **********************************) + +(* Constructions with tr_push anf tr_next ***********************************) + +(*** compose_next *) +lemma tr_compose_next_sn (f2) (f1): + ∀f. f2∘f1 = f → (↑f2)∘f1 = ↑f. +#f2 * #p1 #f1 #f +(npsucc_pred p)