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 corec definition compose: rtmap → rtmap → rtmap.
  21 #f2 * #n1 #f1 @(seq … (f2@❨n1❩)) @(compose ? f1) -compose -f1
  22 @(⫰*[↑n1] f2)
  23 defined.
  24
  25 interpretation "functional composition (nstream)"
  26    'compose f2 f1 = (compose f2 f1).
  27
  28 (* Basic properies on compose ***********************************************)
  29
  30 lemma compose_rew: ∀f2,f1,n1. f2@❨n1❩⨮(⫰*[↑n1]f2)∘f1 = f2∘(n1⨮f1).
  31 #f2 #f1 #n1 <(stream_rew … (f2∘(n1⨮f1))) normalize //
  32 qed.
  33
  34 lemma compose_next: ∀f2,f1,f. f2∘f1 = f → (↑f2)∘f1 = ↑f.
  35 #f2 * #n1 #f1 #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: ∀f2,f1,f,n1,n. f2∘(n1⨮f1) = n⨮f →
  42                        f2@❨n1❩ = n ∧ (⫰*[↑n1]f2)∘f1 = f.
  43 #f2 #f1 #f #n1 #n <(stream_rew … (f2∘(n1⨮f1))) normalize
  44 #H destruct /2 width=1 by conj/
  45 qed-.
  46
  47 lemma compose_inv_O2: ∀f2,f1,f,n2,n. (n2⨮f2)∘(⫯f1) = n⨮f →
  48                       n2 = n ∧ f2∘f1 = f.
  49 #f2 #f1 #f #n2 #n <compose_rew
  50 #H destruct /2 width=1 by conj/
  51 qed-.
  52
  53 lemma compose_inv_S2: ∀f2,f1,f,n2,n1,n. (n2⨮f2)∘(↑n1⨮f1) = n⨮f →
  54                       ↑(n2+f2@❨n1❩) = n ∧ f2∘(n1⨮f1) = f2@❨n1❩⨮f.
  55 #f2 #f1 #f #n2 #n1 #n <compose_rew
  56 #H destruct <tls_S1 /2 width=1 by conj/
  57 qed-.
  58
  59 lemma compose_inv_S1: ∀f2,f1,f,n1,n. (↑f2)∘(n1⨮f1) = n⨮f →
  60                       ↑(f2@❨n1❩) = n ∧ f2∘(n1⨮f1) = f2@❨n1❩⨮f.
  61 #f2 #f1 #f #n1 #n <compose_rew
  62 #H destruct <tls_S1 /2 width=1 by conj/
  63 qed-.
  64
  65 (* Specific properties on after *********************************************)
  66
  67 lemma after_O2: ∀f2,f1,f. f2 ⊚ f1 ≘ f →
  68                 ∀n. n⨮f2 ⊚ ⫯f1 ≘ n⨮f.
  69 #f2 #f1 #f #Hf #n elim n -n /2 width=7 by after_refl, after_next/
  70 qed.
  71
  72 lemma after_S2: ∀f2,f1,f,n1,n. f2 ⊚ n1⨮f1 ≘ n⨮f →
  73                 ∀n2. n2⨮f2 ⊚ ↑n1⨮f1 ≘ ↑(n2+n)⨮f.
  74 #f2 #f1 #f #n1 #n #Hf #n2 elim n2 -n2 /2 width=7 by after_next, after_push/
  75 qed.
  76
  77 lemma after_apply: ∀n1,f2,f1,f. (⫰*[↑n1] f2) ⊚ f1 ≘ f → f2 ⊚ n1⨮f1 ≘ f2@❨n1❩⨮f.
  78 #n1 elim n1 -n1
  79 [ * /2 width=1 by after_O2/
  80 | #n1 #IH * /3 width=1 by after_S2/
  81 ]
  82 qed-.
  83
  84 corec lemma after_total_aux: ∀f2,f1,f. f2 ∘ f1 = f → f2 ⊚ f1 ≘ f.
  85 * #n2 #f2 * #n1 #f1 * #n #f cases n2 -n2
  86 [ cases n1 -n1
  87   [ #H cases (compose_inv_O2 … H) -H /3 width=7 by after_refl, eq_f2/
  88   | #n1 #H cases (compose_inv_S2 … H) -H * -n /3 width=7 by after_push/
  89   ]
  90 | #n2 >next_rew #H cases (compose_inv_S1 … H) -H * -n /3 width=5 by after_next/
  91 ]
  92 qed-.
  93
  94 theorem after_total: ∀f1,f2. f2 ⊚ f1 ≘ f2 ∘ f1.
  95 /2 width=1 by after_total_aux/ qed.
  96
  97 (* Specific inversion lemmas on after ***************************************)
  98
  99 lemma after_inv_xpx: ∀f2,g2,f,n2,n. n2⨮f2 ⊚ g2 ≘ n⨮f → ∀f1. ⫯f1 = g2 →
 100                      f2 ⊚ f1 ≘ f ∧ n2 = n.
 101 #f2 #g2 #f #n2 elim n2 -n2
 102 [ #n #Hf #f1 #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 | #n2 #IH #n #Hf #f1 #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: ∀f2,g2,f,n2,n. n2⨮f2 ⊚ g2 ≘ n⨮f → ∀f1. ↑f1 = g2 →
 112                      ∃∃m. f2 ⊚ f1 ≘ m⨮f & ↑(n2+m) = n.
 113 #f2 #g2 #f #n2 elim n2 -n2
 114 [ #n #Hf #f1 #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 | #n2 #IH #n #Hf #f1 #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: ∀f2,f1,f,n1,n. n⨮f2 ⊚ n1⨮f1 ≘ n⨮f → f2 ⊚ f1 ≘ f ∧ 0 = n1.
 125 #f2 #f1 #f #n1 #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 lemma after_inv_total: ∀f2,f1,f. f2 ⊚ f1 ≘ f → f2 ∘ f1 ≡ f.
 133 /2 width=4 by after_mono/ qed-.
 134
 135 (* Specific forward lemmas on after *****************************************)
 136
 137 lemma after_fwd_hd: ∀f2,f1,f,n1,n. f2 ⊚ n1⨮f1 ≘ n⨮f → f2@❨n1❩ = n.
 138 #f2 #f1 #f #n1 #n #H lapply (after_fwd_at ? n1 0 … H) -H [1,2,3: // ]
 139 /3 width=2 by at_inv_O1, sym_eq/
 140 qed-.
 141
 142 lemma after_fwd_tls: ∀f,f1,n1,f2,n2,n. n2⨮f2 ⊚ n1⨮f1 ≘ n⨮f →
 143                      (⫰*[n1]f2) ⊚ f1 ≘ f.
 144 #f #f1 #n1 elim n1 -n1
 145 [ #f2 #n2 #n #H elim (after_inv_xpx … H) -H //
 146 | #n1 #IH * #m1 #f2 #n2 #n #H elim (after_inv_xnx … H) -H [2,3: // ]
 147   #m #Hm #H destruct /2 width=3 by/
 148 ]
 149 qed-.
 150
 151 lemma after_inv_apply: ∀f2,f1,f,n2,n1,n. n2⨮f2 ⊚ n1⨮f1 ≘ n⨮f →
 152                        (n2⨮f2)@❨n1❩ = n ∧ (⫰*[n1]f2) ⊚ f1 ≘ f.
 153 /3 width=3 by after_fwd_tls, after_fwd_hd, conj/ qed-.
 154
 155 (* Properties on apply ******************************************************)
 156
 157 lemma compose_apply (f2) (f1) (i): f2@❨f1@❨i❩❩ = (f2∘f1)@❨i❩.
 158 /4 width=6 by after_fwd_at, at_inv_total, sym_eq/ qed.