matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "ground_2/relocation/nstream_istot.ma".
  16 include "ground_2/relocation/rtmap_after.ma".
  17
  18 (* RELOCATION N-STREAM ******************************************************)
  19
  20 let corec compose: rtmap → rtmap → rtmap ≝ ?.
  21 #f1 * #n2 #f2 @(seq … (f1@❴n2❵)) @(compose ? f2) -compose -f2
  22 @(↓*[⫯n2] f1)
  23 defined.
  24
  25 interpretation "functional composition (nstream)"
  26    'compose f1 f2 = (compose f1 f2).
  27
  28 (* Basic properies on compose ***********************************************)
  29
  30 lemma compose_rew: ∀f1,f2,n2. f1@❴n2❵@(↓*[⫯n2]f1)∘f2 = f1∘(n2@f2).
  31 #f1 #f2 #n2 <(stream_rew … (f1∘(n2@f2))) normalize //
  32 qed.
  33
  34 lemma compose_next: ∀f1,f2,f. f1∘f2 = f → (⫯f1)∘f2 = ⫯f.
  35 #f1 * #n2 #f2 #f <compose_rew <compose_rew
  36 * -f <tls_S1 /2 width=1 by eq_f2/
  37 qed.
  38
  39 (* Basic inversion lemmas on compose ****************************************)
  40
  41 lemma compose_inv_rew: ∀f1,f2,f,n2,n. f1∘(n2@f2) = n@f →
  42                        f1@❴n2❵ = n ∧ (↓*[⫯n2]f1)∘f2 = f.
  43 #f1 #f2 #f #n2 #n <(stream_rew … (f1∘(n2@f2))) normalize
  44 #H destruct /2 width=1 by conj/
  45 qed-.
  46
  47 lemma compose_inv_O2: ∀f1,f2,f,n1,n. (n1@f1)∘(↑f2) = n@f →
  48                       n1 = n ∧ f1∘f2 = f.
  49 #f1 #f2 #f #n1 #n <compose_rew
  50 #H destruct /2 width=1 by conj/
  51 qed-.
  52
  53 lemma compose_inv_S2: ∀f1,f2,f,n1,n2,n. (n1@f1)∘(⫯n2@f2) = n@f →
  54                       ⫯(n1+f1@❴n2❵) = n ∧ f1∘(n2@f2) = f1@❴n2❵@f.
  55 #f1 #f2 #f #n1 #n2 #n <compose_rew
  56 #H destruct <tls_S1 /2 width=1 by conj/
  57 qed-.
  58
  59 lemma compose_inv_S1: ∀f1,f2,f,n2,n. (⫯f1)∘(n2@f2) = n@f →
  60                       ⫯(f1@❴n2❵) = n ∧ f1∘(n2@f2) = f1@❴n2❵@f.
  61 #f1 #f2 #f #n2 #n <compose_rew
  62 #H destruct <tls_S1 /2 width=1 by conj/
  63 qed-.
  64
  65 (* Specific properties ******************************************************)
  66
  67 lemma after_O2: ∀f1,f2,f. f1 ⊚ f2 ≡ f →
  68                 ∀n. n@f1 ⊚ ↑f2 ≡ n@f.
  69 #f1 #f2 #f #Hf #n elim n -n /2 width=7 by after_refl, after_next/
  70 qed.
  71
  72 lemma after_S2: ∀f1,f2,f,n2,n. f1 ⊚ n2@f2 ≡ n@f →
  73                 ∀n1. n1@f1 ⊚ ⫯n2@f2 ≡ ⫯(n1+n)@f.
  74 #f1 #f2 #f #n2 #n #Hf #n1 elim n1 -n1 /2 width=7 by after_next, after_push/
  75 qed.
  76
  77 lemma after_apply: ∀n2,f1,f2,f. (↓*[⫯n2] f1) ⊚ f2 ≡ f → f1 ⊚ n2@f2 ≡ f1@❴n2❵@f.
  78 #n2 elim n2 -n2
  79 [ * /2 width=1 by after_O2/
  80 | #n2 #IH * /3 width=1 by after_S2/
  81 ]
  82 qed-.
  83
  84 let corec after_total_aux: ∀f1,f2,f. f1 ∘ f2 = f → f1 ⊚ f2 ≡ f ≝ ?.
  85 * #n1 #f1 * #n2 #f2 * #n #f cases n1 -n1
  86 [ cases n2 -n2
  87   [ #H cases (compose_inv_O2 … H) -H /3 width=7 by after_refl, eq_f2/
  88   | #n2 #H cases (compose_inv_S2 … H) -H * -n /3 width=7 by after_push/
  89   ]
  90 | #n1 >next_rew #H cases (compose_inv_S1 … H) -H * -n /3 width=7 by after_next/
  91 ]
  92 qed-.
  93
  94 theorem after_total: ∀f2,f1. f1 ⊚ f2 ≡ f1 ∘ f2.
  95 /2 width=1 by after_total_aux/ qed.
  96
  97 (* Specific inversion lemmas ************************************************)
  98
  99 lemma after_inv_xpx: ∀f1,g2,f,n1,n. n1@f1 ⊚ g2 ≡ n@f → ∀f2. ↑f2 = g2 →
 100                      f1 ⊚ f2 ≡ f ∧ n1 = n.
 101 #f1 #g2 #f #n1 elim n1 -n1
 102 [ #n #Hf #f2 #H2 elim (after_inv_ppx … Hf … H2) -g2 [2,3: // ]
 103   #g #Hf #H elim (push_inv_seq_dx … H) -H destruct /2 width=1 by conj/
 104 | #n1 #IH #n #Hf #f2 #H2 elim (after_inv_nxx … Hf) -Hf [2,3: // ]
 105   #g1 #Hg #H1 elim (next_inv_seq_dx … H1) -H1
 106   #x #Hx #H destruct elim (IH … Hg) [2,3: // ] -IH -Hg
 107   #H destruct /2 width=1 by conj/
 108 ]
 109 qed-.
 110
 111 lemma after_inv_xnx: ∀f1,g2,f,n1,n. n1@f1 ⊚ g2 ≡ n@f → ∀f2. ⫯f2 = g2 →
 112                      ∃∃m. f1 ⊚ f2 ≡ m@f & ⫯(n1+m) = n.
 113 #f1 #g2 #f #n1 elim n1 -n1
 114 [ #n #Hf #f2 #H2 elim (after_inv_pnx … Hf … H2) -g2 [2,3: // ]
 115   #g #Hf #H elim (next_inv_seq_dx … H) -H
 116   #x #Hx #Hg destruct /2 width=3 by ex2_intro/
 117 | #n1 #IH #n #Hf #f2 #H2 elim (after_inv_nxx … Hf) -Hf [2,3: // ]
 118   #g #Hg #H elim (next_inv_seq_dx … H) -H
 119   #x #Hx #H destruct elim (IH … Hg) -IH -Hg [2,3: // ]
 120   #m #Hf #Hm destruct /2 width=3 by ex2_intro/
 121 ]
 122 qed-.
 123
 124 lemma after_inv_const: ∀f1,f2,f,n2,n. n@f1 ⊚ n2@f2 ≡ n@f → f1 ⊚ f2 ≡ f ∧ 0 = n2.
 125 #f1 #f2 #f #n2 #n elim n -n
 126 [ #H elim (after_inv_pxp … H) -H [ |*: // ]
 127   #g2 #Hf #H elim (push_inv_seq_dx … H) -H /2 width=1 by conj/
 128 | #n #IH #H lapply (after_inv_nxn … H ????) -H /2 width=5 by/
 129 ]
 130 qed-.
 131
 132 (* Specific forward lemmas **************************************************)
 133
 134 lemma after_fwd_hd: ∀f1,f2,f,n2,n. f1 ⊚ n2@f2 ≡ n@f → f1@❴n2❵ = n.
 135 #f1 #f2 #f #n2 #n #H lapply (after_fwd_at ? n2 0 … H) -H [1,2,3: // ]
 136 /3 width=2 by at_inv_O1, sym_eq/
 137 qed-.
 138
 139 lemma after_fwd_tls: ∀f,f2,n2,f1,n1,n. n1@f1 ⊚ n2@f2 ≡ n@f →
 140                      (↓*[n2]f1) ⊚ f2 ≡ f.
 141 #f #f2 #n2 elim n2 -n2
 142 [ #f1 #n1 #n #H elim (after_inv_xpx … H) -H //
 143 | #n2 #IH * #m1 #f1 #n1 #n #H elim (after_inv_xnx … H) -H [2,3: // ]
 144   #m #Hm #H destruct /2 width=3 by/
 145 ]
 146 qed-.
 147
 148 lemma after_inv_apply: ∀f1,f2,f,n1,n2,n. n1@f1 ⊚ n2@f2 ≡ n@f →
 149                        (n1@f1)@❴n2❵ = n ∧ (↓*[n2]f1) ⊚ f2 ≡ f.
 150 /3 width=3 by after_fwd_tls, after_fwd_hd, conj/ qed-.