From: Ferruccio Guidi Date: Sat, 25 Jun 2016 17:52:28 +0000 (+0000) Subject: totality of co-composition ! X-Git-Tag: make_still_working~558 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5b93ea047903b606979705ed25a6df6504fd027c;p=helm.git totality of co-composition ! --- diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/functions/cocompose_2.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/cocompose_2.ma new file mode 100644 index 000000000..32741b07b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/cocompose_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 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation "hvbox(f2 ~ \circ break f1)" + right associative with precedence 60 + for @{ 'CoCompose $f2 $f1 }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma index 25bb3c60b..977a0ca02 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma @@ -18,136 +18,136 @@ include "ground_2/relocation/rtmap_after.ma". (* RELOCATION N-STREAM ******************************************************) corec definition compose: rtmap → rtmap → rtmap. -#f1 * #n2 #f2 @(seq … (f1@❴n2❵)) @(compose ? f2) -compose -f2 -@(↓*[⫯n2] f1) +#f2 * #n1 #f1 @(seq … (f2@❴n1❵)) @(compose ? f1) -compose -f1 +@(↓*[⫯n1] f2) defined. interpretation "functional composition (nstream)" - 'compose f1 f2 = (compose f1 f2). + 'compose f2 f1 = (compose f2 f1). (* Basic properies on compose ***********************************************) -lemma compose_rew: ∀f1,f2,n2. f1@❴n2❵@(↓*[⫯n2]f1)∘f2 = f1∘(n2@f2). -#f1 #f2 #n2 <(stream_rew … (f1∘(n2@f2))) normalize // +lemma compose_rew: ∀f2,f1,n1. f2@❴n1❵@(↓*[⫯n1]f2)∘f1 = f2∘(n1@f1). +#f2 #f1 #n1 <(stream_rew … (f2∘(n1@f1))) normalize // qed. -lemma compose_next: ∀f1,f2,f. f1∘f2 = f → (⫯f1)∘f2 = ⫯f. -#f1 * #n2 #f2 #f next_rew #H cases (compose_inv_S1 … H) -H * -n /3 width=7 by after_next/ +| #n2 >next_rew #H cases (compose_inv_S1 … H) -H * -n /3 width=5 by after_next/ ] qed-. -theorem after_total: ∀f2,f1. f1 ⊚ f2 ≡ f1 ∘ f2. +theorem after_total: ∀f1,f2. f2 ⊚ f1 ≡ f2 ∘ f1. /2 width=1 by after_total_aux/ qed. -(* Specific inversion lemmas ************************************************) +(* Specific inversion lemmas on after ***************************************) -lemma after_inv_xpx: ∀f1,g2,f,n1,n. n1@f1 ⊚ g2 ≡ n@f → ∀f2. ↑f2 = g2 → - f1 ⊚ f2 ≡ f ∧ n1 = n. -#f1 #g2 #f #n1 elim n1 -n1 -[ #n #Hf #f2 #H2 elim (after_inv_ppx … Hf … H2) -g2 [2,3: // ] +lemma after_inv_xpx: ∀f2,g2,f,n2,n. n2@f2 ⊚ g2 ≡ n@f → ∀f1. ↑f1 = g2 → + f2 ⊚ f1 ≡ f ∧ n2 = n. +#f2 #g2 #f #n2 elim n2 -n2 +[ #n #Hf #f1 #H2 elim (after_inv_ppx … Hf … H2) -g2 [2,3: // ] #g #Hf #H elim (push_inv_seq_dx … H) -H destruct /2 width=1 by conj/ -| #n1 #IH #n #Hf #f2 #H2 elim (after_inv_nxx … Hf) -Hf [2,3: // ] +| #n2 #IH #n #Hf #f1 #H2 elim (after_inv_nxx … Hf) -Hf [2,3: // ] #g1 #Hg #H1 elim (next_inv_seq_dx … H1) -H1 #x #Hx #H destruct elim (IH … Hg) [2,3: // ] -IH -Hg #H destruct /2 width=1 by conj/ ] qed-. -lemma after_inv_xnx: ∀f1,g2,f,n1,n. n1@f1 ⊚ g2 ≡ n@f → ∀f2. ⫯f2 = g2 → - ∃∃m. f1 ⊚ f2 ≡ m@f & ⫯(n1+m) = n. -#f1 #g2 #f #n1 elim n1 -n1 -[ #n #Hf #f2 #H2 elim (after_inv_pnx … Hf … H2) -g2 [2,3: // ] +lemma after_inv_xnx: ∀f2,g2,f,n2,n. n2@f2 ⊚ g2 ≡ n@f → ∀f1. ⫯f1 = g2 → + ∃∃m. f2 ⊚ f1 ≡ m@f & ⫯(n2+m) = n. +#f2 #g2 #f #n2 elim n2 -n2 +[ #n #Hf #f1 #H2 elim (after_inv_pnx … Hf … H2) -g2 [2,3: // ] #g #Hf #H elim (next_inv_seq_dx … H) -H #x #Hx #Hg destruct /2 width=3 by ex2_intro/ -| #n1 #IH #n #Hf #f2 #H2 elim (after_inv_nxx … Hf) -Hf [2,3: // ] +| #n2 #IH #n #Hf #f1 #H2 elim (after_inv_nxx … Hf) -Hf [2,3: // ] #g #Hg #H elim (next_inv_seq_dx … H) -H #x #Hx #H destruct elim (IH … Hg) -IH -Hg [2,3: // ] #m #Hf #Hm destruct /2 width=3 by ex2_intro/ ] qed-. -lemma after_inv_const: ∀f1,f2,f,n2,n. n@f1 ⊚ n2@f2 ≡ n@f → f1 ⊚ f2 ≡ f ∧ 0 = n2. -#f1 #f2 #f #n2 #n elim n -n +lemma after_inv_const: ∀f2,f1,f,n1,n. n@f2 ⊚ n1@f1 ≡ n@f → f2 ⊚ f1 ≡ f ∧ 0 = n1. +#f2 #f1 #f #n1 #n elim n -n [ #H elim (after_inv_pxp … H) -H [ |*: // ] #g2 #Hf #H elim (push_inv_seq_dx … H) -H /2 width=1 by conj/ | #n #IH #H lapply (after_inv_nxn … H ????) -H /2 width=5 by/ ] qed-. -lemma after_inv_total: ∀f1,f2,f. f1 ⊚ f2 ≡ f → f1 ∘ f2 ≗ f. +lemma after_inv_total: ∀f2,f1,f. f2 ⊚ f1 ≡ f → f2 ∘ f1 ≗ f. /2 width=4 by after_mono/ qed-. -(* Specific forward lemmas **************************************************) +(* Specific forward lemmas on after *****************************************) -lemma after_fwd_hd: ∀f1,f2,f,n2,n. f1 ⊚ n2@f2 ≡ n@f → f1@❴n2❵ = n. -#f1 #f2 #f #n2 #n #H lapply (after_fwd_at ? n2 0 … H) -H [1,2,3: // ] +lemma after_fwd_hd: ∀f2,f1,f,n1,n. f2 ⊚ n1@f1 ≡ n@f → f2@❴n1❵ = n. +#f2 #f1 #f #n1 #n #H lapply (after_fwd_at ? n1 0 … H) -H [1,2,3: // ] /3 width=2 by at_inv_O1, sym_eq/ qed-. -lemma after_fwd_tls: ∀f,f2,n2,f1,n1,n. n1@f1 ⊚ n2@f2 ≡ n@f → - (↓*[n2]f1) ⊚ f2 ≡ f. -#f #f2 #n2 elim n2 -n2 -[ #f1 #n1 #n #H elim (after_inv_xpx … H) -H // -| #n2 #IH * #m1 #f1 #n1 #n #H elim (after_inv_xnx … H) -H [2,3: // ] +lemma after_fwd_tls: ∀f,f1,n1,f2,n2,n. n2@f2 ⊚ n1@f1 ≡ n@f → + (↓*[n1]f2) ⊚ f1 ≡ f. +#f #f1 #n1 elim n1 -n1 +[ #f2 #n2 #n #H elim (after_inv_xpx … H) -H // +| #n1 #IH * #m1 #f2 #n2 #n #H elim (after_inv_xnx … H) -H [2,3: // ] #m #Hm #H destruct /2 width=3 by/ ] qed-. -lemma after_inv_apply: ∀f1,f2,f,n1,n2,n. n1@f1 ⊚ n2@f2 ≡ n@f → - (n1@f1)@❴n2❵ = n ∧ (↓*[n2]f1) ⊚ f2 ≡ f. +lemma after_inv_apply: ∀f2,f1,f,n2,n1,n. n2@f2 ⊚ n1@f1 ≡ n@f → + (n2@f2)@❴n1❵ = n ∧ (↓*[n1]f2) ⊚ f1 ≡ f. /3 width=3 by after_fwd_tls, after_fwd_hd, conj/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_coafter.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_coafter.ma new file mode 100644 index 000000000..4c141a301 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_coafter.ma @@ -0,0 +1,103 @@ +(**************************************************************************) +(* ___ *) +(* ||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_2/notation/functions/cocompose_2.ma". +include "ground_2/relocation/rtmap_coafter.ma". + +(* RELOCATION N-STREAM ******************************************************) + +rec definition fun0 (n1:nat) on n1: rtmap → nat. +* * [ | #n2 #f2 @0 ] +#f2 cases n1 -n1 [ @0 ] +#n1 @(⫯(fun0 n1 f2)) +defined. + +rec definition fun2 (n1:nat) on n1: rtmap → rtmap. +* * [ | #n2 #f2 @(n2@f2) ] +#f2 cases n1 -n1 [ @f2 ] +#n1 @(fun2 n1 f2) +defined. + +rec definition fun1 (n1:nat) (f1:rtmap) on n1: rtmap → rtmap. +* * [ | #n2 #f2 @(n1@f1) ] +#f2 cases n1 -n1 [ @f1 ] +#n1 @(fun1 n1 f1 f2) +defined. + +corec definition cocompose: rtmap → rtmap → rtmap. +#f2 * #n1 #f1 @(seq … (fun0 n1 f2)) @(cocompose (fun2 n1 f2) (fun1 n1 f1 f2)) +defined. + +interpretation "functional co-composition (nstream)" + 'CoCompose f1 f2 = (cocompose f1 f2). + +(* Basic properties on funs *************************************************) + +(* Note: we need theese since matita blocks recursive δ when ι is blocked *) +lemma fun0_xn: ∀f2,n1. 0 = fun0 n1 (⫯f2). +* #n2 #f2 * // +qed. + +lemma fun2_xn: ∀f2,n1. f2 = fun2 n1 (⫯f2). +* #n2 #f2 * // +qed. + +lemma fun1_xxn: ∀f2,f1,n1. fun1 n1 f1 (⫯f2) = n1@f1. +* #n2 #f2 #f1 * // +qed. + +(* Basic properies on cocompose *********************************************) + +lemma cocompose_rew: ∀f2,f1,n1. (fun0 n1 f2)@(fun2 n1 f2)~∘(fun1 n1 f1 f2) = f2 ~∘ (n1@f1). +#f2 #f1 #n1 <(stream_rew … (f2~∘(n1@f1))) normalize // +qed. + +(* Basic inversion lemmas on compose ****************************************) + +lemma cocompose_inv_ppx: ∀f2,f1,f,x. (↑f2) ~∘ (↑f1) = x@f → + 0 = x ∧ f2 ~∘ f1 = f. +#f2 #f1 #f #x +next_rew #H cases (cocompose_inv_nxx … H) -H /3 width=5 by coafter_next/ +] +qed-. + +theorem coafter_total: ∀f2,f1. f2 ~⊚ f1 ≡ f2 ~∘ f1. +/2 width=1 by coafter_total_aux/ qed. diff --git a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl index 63199cb52..92cec8dc5 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl @@ -21,7 +21,7 @@ table { [ { "multiple relocation" * } { [ { "" * } { [ "rtmap" "rtmap_eq ( ? ≗ ? )" "rtmap_pushs ( ↑*[?]? )" "rtmap_tl ( ⫱? )" "rtmap_tls ( ⫱*[?]? )" "rtmap_isid ( 𝐈⦃?⦄ )" "rtmap_id" "rtmap_fcla ( 𝐂⦃?⦄ ≡ ? )" "rtmap_isfin ( 𝐅⦃?⦄ )" "rtmap_isuni ( 𝐔⦃?⦄ )" "rtmap_uni ( 𝐔❴?❵ )" "rtmap_sle ( ? ⊆ ? )" "rtmap_sand ( ? ⋒ ? ≡ ? )" "rtmap_sor ( ? ⋓ ? ≡ ? )" "rtmap_at ( @⦃?,?⦄ ≡ ? )" "rtmap_istot ( 𝐓⦃?⦄ )" "rtmap_after ( ? ⊚ ? ≡ ? )" "rtmap_coafter ( ? ~⊚ ? ≡ ? )" * ] - [ "nstream ( ↑? ) ( ⫯? )" "nstream_eq" "" "" "" "nstream_isid" "nstream_id ( 𝐈𝐝 )" "" "" "" "" "" "nstream_sand" "" "" "nstream_istot ( ?@❴?❵ )" "nstream_after ( ? ∘ ? )" "" * ] + [ "nstream ( ↑? ) ( ⫯? )" "nstream_eq" "" "" "" "nstream_isid" "nstream_id ( 𝐈𝐝 )" "" "" "" "" "" "nstream_sand" "" "" "nstream_istot ( ?@❴?❵ )" "nstream_after ( ? ∘ ? )" "nstream_coafter ( ? ~∘ ? )" * ] (* [ "trace ( ∥?∥ )" "trace_at ( @⦃?,?⦄ ≡ ? )" "trace_after ( ? ⊚ ? ≡ ? )" "trace_isid ( 𝐈⦃?⦄ )" "trace_isun ( 𝐔⦃?⦄ )" "trace_sle ( ? ⊆ ? )" "trace_sor ( ? ⋓ ? ≡ ? )" "trace_snot ( ∁ ? )" * ]