matita/matita/contribs/lambdadelta/ground/relocation/pstream_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/relocation/pstream_tls.ma".
  16 include "ground/relocation/pstream_istot.ma".
  17 include "ground/relocation/rtmap_after.ma".
  18
  19 (* RELOCATION N-STREAM ******************************************************)
  20
  21 corec definition compose: rtmap → rtmap → rtmap.
  22 #f2 * #p1 #f1 @(stream_cons … (f2@❨p1❩)) @(compose ? f1) -compose -f1
  23 @(⫰*[p1]f2)
  24 defined.
  25
  26 interpretation "functional composition (nstream)"
  27    'compose f2 f1 = (compose f2 f1).
  28
  29 (* Basic properies on compose ***********************************************)
  30
  31 lemma compose_rew: ∀f2,f1,p1. f2@❨p1❩⨮(⫰*[p1]f2)∘f1 = f2∘(p1⨮f1).
  32 #f2 #f1 #p1 <(stream_rew … (f2∘(p1⨮f1))) normalize //
  33 qed.
  34
  35 lemma compose_next: ∀f2,f1,f. f2∘f1 = f → (↑f2)∘f1 = ↑f.
  36 #f2 * #p1 #f1 #f <compose_rew <compose_rew
  37 * -f /2 width=1 by eq_f2/
  38 qed.
  39
  40 (* Basic inversion lemmas on compose ****************************************)
  41
  42 lemma compose_inv_rew: ∀f2,f1,f,p1,p. f2∘(p1⨮f1) = p⨮f →
  43                        f2@❨p1❩ = p ∧ (⫰*[p1]f2)∘f1 = f.
  44 #f2 #f1 #f #p1 #p <compose_rew
  45 #H destruct /2 width=1 by conj/
  46 qed-.
  47
  48 lemma compose_inv_O2: ∀f2,f1,f,p2,p. (p2⨮f2)∘(⫯f1) = p⨮f →
  49                       p2 = p ∧ f2∘f1 = f.
  50 #f2 #f1 #f #p2 #p <compose_rew
  51 #H destruct /2 width=1 by conj/
  52 qed-.
  53
  54 lemma compose_inv_S2: ∀f2,f1,f,p2,p1,p. (p2⨮f2)∘(↑p1⨮f1) = p⨮f →
  55                       f2@❨p1❩+p2 = p ∧ f2∘(p1⨮f1) = f2@❨p1❩⨮f.
  56 #f2 #f1 #f #p2 #p1 #p <compose_rew
  57 #H destruct >nsucc_inj <stream_tls_swap
  58 /2 width=1 by conj/
  59 qed-.
  60
  61 lemma compose_inv_S1: ∀f2,f1,f,p1,p. (↑f2)∘(p1⨮f1) = p⨮f →
  62                       ↑(f2@❨p1❩) = p ∧ f2∘(p1⨮f1) = f2@❨p1❩⨮f.
  63 #f2 #f1 #f #p1 #p <compose_rew
  64 #H destruct /2 width=1 by conj/
  65 qed-.
  66
  67 (* Specific properties on after *********************************************)
  68
  69 lemma after_O2: ∀f2,f1,f. f2 ⊚ f1 ≘ f →
  70                 ∀p. p⨮f2 ⊚ ⫯f1 ≘ p⨮f.
  71 #f2 #f1 #f #Hf #p elim p -p
  72 /2 width=7 by after_refl, after_next/
  73 qed.
  74
  75 lemma after_S2: ∀f2,f1,f,p1,p. f2 ⊚ p1⨮f1 ≘ p⨮f →
  76                 ∀p2. p2⨮f2 ⊚ ↑p1⨮f1 ≘ (p+p2)⨮f.
  77 #f2 #f1 #f #p1 #p #Hf #p2 elim p2 -p2
  78 /2 width=7 by after_next, after_push/
  79 qed.
  80
  81 lemma after_apply: ∀p1,f2,f1,f.
  82       (⫰*[ninj p1] f2) ⊚ f1 ≘ f → f2 ⊚ p1⨮f1 ≘ f2@❨p1❩⨮f.
  83 #p1 elim p1 -p1
  84 [ * /2 width=1 by after_O2/
  85 | #p1 #IH * #p2 #f2 >nsucc_inj <stream_tls_swap
  86   /3 width=1 by after_S2/
  87 ]
  88 qed-.
  89
  90 corec lemma after_total_aux: ∀f2,f1,f. f2 ∘ f1 = f → f2 ⊚ f1 ≘ f.
  91 * #p2 #f2 * #p1 #f1 * #p #f cases p2 -p2
  92 [ cases p1 -p1
  93   [ #H cases (compose_inv_O2 … H) -H /3 width=7 by after_refl, eq_f2/
  94   | #p1 #H cases (compose_inv_S2 … H) -H * -p /3 width=7 by after_push/
  95   ]
  96 | #p2 >next_rew #H cases (compose_inv_S1 … H) -H * -p >next_rew
  97   /3 width=5 by after_next/
  98 ]
  99 qed-.
 100
 101 theorem after_total: ∀f1,f2. f2 ⊚ f1 ≘ f2 ∘ f1.
 102 /2 width=1 by after_total_aux/ qed.
 103
 104 (* Specific inversion lemmas on after ***************************************)
 105
 106 lemma after_inv_xpx: ∀f2,g2,f,p2,p. p2⨮f2 ⊚ g2 ≘ p⨮f → ∀f1. ⫯f1 = g2 →
 107                      f2 ⊚ f1 ≘ f ∧ p2 = p.
 108 #f2 #g2 #f #p2 elim p2 -p2
 109 [ #p #Hf #f1 #H2 elim (after_inv_ppx … Hf … H2) -g2 [|*: // ]
 110   #g #Hf #H elim (push_inv_seq_dx … H) -H destruct /2 width=1 by conj/
 111 | #p2 #IH #p #Hf #f1 #H2 elim (after_inv_nxx … Hf) -Hf [|*: // ]
 112   #g1 #Hg #H1 elim (next_inv_seq_dx … H1) -H1
 113   #x #Hx #H destruct elim (IH … Hg) [|*: // ] -IH -Hg
 114   #H destruct /2 width=1 by conj/
 115 ]
 116 qed-.
 117
 118 lemma after_inv_xnx: ∀f2,g2,f,p2,p. p2⨮f2 ⊚ g2 ≘ p⨮f → ∀f1. ↑f1 = g2 →
 119                      ∃∃q. f2 ⊚ f1 ≘ q⨮f & q+p2 = p.
 120 #f2 #g2 #f #p2 elim p2 -p2
 121 [ #p #Hf #f1 #H2 elim (after_inv_pnx … Hf … H2) -g2 [|*: // ]
 122   #g #Hf #H elim (next_inv_seq_dx … H) -H
 123   #x #Hx #Hg destruct /2 width=3 by ex2_intro/
 124 | #p2 #IH #p #Hf #f1 #H2 elim (after_inv_nxx … Hf) -Hf [|*: // ]
 125   #g #Hg #H elim (next_inv_seq_dx … H) -H
 126   #x #Hx #H destruct elim (IH … Hg) -IH -Hg [|*: // ]
 127   #m #Hf #Hm destruct /2 width=3 by ex2_intro/
 128 ]
 129 qed-.
 130
 131 lemma after_inv_const: ∀f2,f1,f,p1,p.
 132       p⨮f2 ⊚ p1⨮f1 ≘ p⨮f → f2 ⊚ f1 ≘ f ∧ 𝟏 = p1.
 133 #f2 #f1 #f #p1 #p elim p -p
 134 [ #H elim (after_inv_pxp … H) -H [|*: // ]
 135   #g2 #Hf #H elim (push_inv_seq_dx … H) -H /2 width=1 by conj/
 136 | #p #IH #H lapply (after_inv_nxn … H ????) -H /2 width=5 by/
 137 ]
 138 qed-.
 139
 140 lemma after_inv_total: ∀f2,f1,f. f2 ⊚ f1 ≘ f → f2 ∘ f1 ≡ f.
 141 /2 width=4 by after_mono/ qed-.
 142
 143 (* Specific forward lemmas on after *****************************************)
 144
 145 lemma after_fwd_hd: ∀f2,f1,f,p1,p. f2 ⊚ p1⨮f1 ≘ p⨮f → f2@❨p1❩ = p.
 146 #f2 #f1 #f #p1 #p #H lapply (after_fwd_at ? p1 (𝟏) … H) -H [4:|*: // ]
 147 /3 width=2 by at_inv_O1, sym_eq/
 148 qed-.
 149
 150 lemma after_fwd_tls: ∀f,f1,p1,f2,p2,p. p2⨮f2 ⊚ p1⨮f1 ≘ p⨮f →
 151                      (⫰*[↓p1]f2) ⊚ f1 ≘ f.
 152 #f #f1 #p1 elim p1 -p1
 153 [ #f2 #p2 #p #H elim (after_inv_xpx … H) -H //
 154 | #p1 #IH * #q2 #f2 #p2 #p #H elim (after_inv_xnx … H) -H [|*: // ]
 155   #x #Hx #H destruct /2 width=3 by/
 156 ]
 157 qed-.
 158
 159 lemma after_inv_apply: ∀f2,f1,f,p2,p1,p. p2⨮f2 ⊚ p1⨮f1 ≘ p⨮f →
 160                        (p2⨮f2)@❨p1❩ = p ∧ (⫰*[↓p1]f2) ⊚ f1 ≘ f.
 161 /3 width=3 by after_fwd_tls, after_fwd_hd, conj/ qed-.
 162
 163 (* Properties on apply ******************************************************)
 164
 165 lemma compose_apply (f2) (f1) (i): f2@❨f1@❨i❩❩ = (f2∘f1)@❨i❩.
 166 /4 width=6 by after_fwd_at, at_inv_total, sym_eq/ qed.