From 5b93ea047903b606979705ed25a6df6504fd027c Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 25 Jun 2016 17:52:28 +0000
Subject: [PATCH] totality of co-composition !

---
 .../notation/functions/cocompose_2.ma         |  19 +++
 .../ground_2/relocation/nstream_after.ma      | 118 +++++++++---------
 .../ground_2/relocation/nstream_coafter.ma    | 103 +++++++++++++++
 .../lambdadelta/ground_2/web/ground_2_src.tbl |   2 +-
 4 files changed, 182 insertions(+), 60 deletions(-)
 create mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/functions/cocompose_2.ma
 create mode 100644 matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_coafter.ma

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 <compose_rew <compose_rew
+lemma compose_next: ∀f2,f1,f. f2∘f1 = f → (⫯f2)∘f1 = ⫯f.
+#f2 * #n1 #f1 #f <compose_rew <compose_rew
 * -f <tls_S1 /2 width=1 by eq_f2/
 qed.
 
 (* Basic inversion lemmas on compose ****************************************)
 
-lemma compose_inv_rew: ∀f1,f2,f,n2,n. f1∘(n2@f2) = n@f →
-                       f1@❴n2❵ = n ∧ (↓*[⫯n2]f1)∘f2 = f.
-#f1 #f2 #f #n2 #n <(stream_rew … (f1∘(n2@f2))) normalize
+lemma compose_inv_rew: ∀f2,f1,f,n1,n. f2∘(n1@f1) = n@f →
+                       f2@❴n1❵ = n ∧ (↓*[⫯n1]f2)∘f1 = f.
+#f2 #f1 #f #n1 #n <(stream_rew … (f2∘(n1@f1))) normalize
 #H destruct /2 width=1 by conj/
 qed-.
 
-lemma compose_inv_O2: ∀f1,f2,f,n1,n. (n1@f1)∘(↑f2) = n@f →
-                      n1 = n ∧ f1∘f2 = f.
-#f1 #f2 #f #n1 #n <compose_rew
+lemma compose_inv_O2: ∀f2,f1,f,n2,n. (n2@f2)∘(↑f1) = n@f →
+                      n2 = n ∧ f2∘f1 = f.
+#f2 #f1 #f #n2 #n <compose_rew
 #H destruct /2 width=1 by conj/
 qed-.
 
-lemma compose_inv_S2: ∀f1,f2,f,n1,n2,n. (n1@f1)∘(⫯n2@f2) = n@f →
-                      ⫯(n1+f1@❴n2❵) = n ∧ f1∘(n2@f2) = f1@❴n2❵@f.
-#f1 #f2 #f #n1 #n2 #n <compose_rew
+lemma compose_inv_S2: ∀f2,f1,f,n2,n1,n. (n2@f2)∘(⫯n1@f1) = n@f →
+                      ⫯(n2+f2@❴n1❵) = n ∧ f2∘(n1@f1) = f2@❴n1❵@f.
+#f2 #f1 #f #n2 #n1 #n <compose_rew
 #H destruct <tls_S1 /2 width=1 by conj/
 qed-.
 
-lemma compose_inv_S1: ∀f1,f2,f,n2,n. (⫯f1)∘(n2@f2) = n@f →
-                      ⫯(f1@❴n2❵) = n ∧ f1∘(n2@f2) = f1@❴n2❵@f.
-#f1 #f2 #f #n2 #n <compose_rew
+lemma compose_inv_S1: ∀f2,f1,f,n1,n. (⫯f2)∘(n1@f1) = n@f →
+                      ⫯(f2@❴n1❵) = n ∧ f2∘(n1@f1) = f2@❴n1❵@f.
+#f2 #f1 #f #n1 #n <compose_rew
 #H destruct <tls_S1 /2 width=1 by conj/
 qed-.
 
-(* Specific properties ******************************************************)
+(* Specific properties on after *********************************************)
 
-lemma after_O2: ∀f1,f2,f. f1 ⊚ f2 ≡ f →
-                ∀n. n@f1 ⊚ ↑f2 ≡ n@f.
-#f1 #f2 #f #Hf #n elim n -n /2 width=7 by after_refl, after_next/
+lemma after_O2: ∀f2,f1,f. f2 ⊚ f1 ≡ f →
+                ∀n. n@f2 ⊚ ↑f1 ≡ n@f.
+#f2 #f1 #f #Hf #n elim n -n /2 width=7 by after_refl, after_next/
 qed.
 
-lemma after_S2: ∀f1,f2,f,n2,n. f1 ⊚ n2@f2 ≡ n@f →
-                ∀n1. n1@f1 ⊚ ⫯n2@f2 ≡ ⫯(n1+n)@f.
-#f1 #f2 #f #n2 #n #Hf #n1 elim n1 -n1 /2 width=7 by after_next, after_push/
+lemma after_S2: ∀f2,f1,f,n1,n. f2 ⊚ n1@f1 ≡ n@f →
+                ∀n2. n2@f2 ⊚ ⫯n1@f1 ≡ ⫯(n2+n)@f.
+#f2 #f1 #f #n1 #n #Hf #n2 elim n2 -n2 /2 width=7 by after_next, after_push/
 qed.
 
-lemma after_apply: ∀n2,f1,f2,f. (↓*[⫯n2] f1) ⊚ f2 ≡ f → f1 ⊚ n2@f2 ≡ f1@❴n2❵@f.
-#n2 elim n2 -n2
+lemma after_apply: ∀n1,f2,f1,f. (↓*[⫯n1] f2) ⊚ f1 ≡ f → f2 ⊚ n1@f1 ≡ f2@❴n1❵@f.
+#n1 elim n1 -n1
 [ * /2 width=1 by after_O2/
-| #n2 #IH * /3 width=1 by after_S2/
+| #n1 #IH * /3 width=1 by after_S2/
 ]
 qed-.
 
-corec lemma after_total_aux: ∀f1,f2,f. f1 ∘ f2 = f → f1 ⊚ f2 ≡ f.
-* #n1 #f1 * #n2 #f2 * #n #f cases n1 -n1
-[ cases n2 -n2
+corec lemma after_total_aux: ∀f2,f1,f. f2 ∘ f1 = f → f2 ⊚ f1 ≡ f.
+* #n2 #f2 * #n1 #f1 * #n #f cases n2 -n2
+[ cases n1 -n1
   [ #H cases (compose_inv_O2 … H) -H /3 width=7 by after_refl, eq_f2/
-  | #n2 #H cases (compose_inv_S2 … H) -H * -n /3 width=7 by after_push/
+  | #n1 #H cases (compose_inv_S2 … H) -H * -n /3 width=7 by after_push/
   ]
-| #n1 >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
+<cocompose_rew #H destruct
+normalize /2 width=1 by conj/
+qed-.
+
+lemma cocompose_inv_pnx: ∀f2,f1,f,n1,x. (↑f2) ~∘ ((⫯n1)@f1) = x@f →
+                         ∃∃n. ⫯n = x & f2 ~∘ (n1@f1) = n@f.
+#f2 #f1 #f #n1 #x
+<cocompose_rew #H destruct
+@(ex2_intro … (fun0 n1 f2)) // <cocompose_rew
+/3 width=1 by eq_f2/
+qed-.
+
+lemma cocompose_inv_nxx: ∀f2,f1,f,n1,x. (⫯f2) ~∘ (n1@f1) = x@f →
+                         0 = x ∧ f2 ~∘ (n1@f1) = f.
+#f2 #f1 #f #n1 #x
+<cocompose_rew #H destruct
+/2 width=1 by conj/
+qed-.
+
+(* Specific properties on coafter *******************************************)
+
+corec lemma coafter_total_aux: ∀f2,f1,f. f2 ~∘ f1 = f → f2 ~⊚ f1 ≡ f.
+* #n2 #f2 * #n1 #f1 * #n #f cases n2 -n2
+[ cases n1 -n1
+  [ #H cases (cocompose_inv_ppx … H) -H /3 width=7 by coafter_refl, eq_f2/
+  | #n1 #H cases (cocompose_inv_pnx … H) -H /3 width=7 by coafter_push/
+  ]
+| #n2 >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 ( ∁ ? )" * ]
-- 
2.39.2