matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_etc.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 (* Properties on after (specific) *********************************************)
  20
  21 lemma after_O2: ∀f2,f1,f. f2 ⊚ f1 ≘ f →
  22                 ∀p. p⨮f2 ⊚ ⫯f1 ≘ p⨮f.
  23 #f2 #f1 #f #Hf #p elim p -p
  24 /2 width=7 by gr_after_refl, gr_after_next/
  25 qed.
  26
  27 lemma after_S2: ∀f2,f1,f,p1,p. f2 ⊚ p1⨮f1 ≘ p⨮f →
  28                 ∀p2. p2⨮f2 ⊚ ↑p1⨮f1 ≘ (p+p2)⨮f.
  29 #f2 #f1 #f #p1 #p #Hf #p2 elim p2 -p2
  30 /2 width=7 by gr_after_next, gr_after_push/
  31 qed.
  32
  33 lemma after_apply: ∀p1,f2,f1,f.
  34       (⫰*[ninj p1] f2) ⊚ f1 ≘ f → f2 ⊚ p1⨮f1 ≘ f2@❨p1❩⨮f.
  35 #p1 elim p1 -p1
  36 [ * /2 width=1 by after_O2/
  37 | #p1 #IH * #p2 #f2 >nsucc_inj <stream_tls_swap
  38   /3 width=1 by after_S2/
  39 ]
  40 qed-.
  41
  42 corec lemma after_total_aux: ∀f2,f1,f. f2 ∘ f1 = f → f2 ⊚ f1 ≘ f.
  43 * #p2 #f2 * #p1 #f1 * #p #f cases p2 -p2
  44 [ cases p1 -p1
  45   [ #H cases (compose_inv_O2 … H) -H /3 width=7 by gr_after_refl, eq_f2/
  46   | #p1 #H cases (compose_inv_S2 … H) -H * -p /3 width=7 by gr_after_push/
  47   ]
  48 | #p2 >gr_next_unfold #H cases (compose_inv_S1 … H) -H * -p >gr_next_unfold
  49   /3 width=5 by gr_after_next/
  50 ]
  51 qed-.
  52
  53 theorem after_total: ∀f1,f2. f2 ⊚ f1 ≘ f2 ∘ f1.
  54 /2 width=1 by after_total_aux/ qed.
  55
  56 (* Inversion lemmas on after (specific) ***************************************)
  57
  58 lemma after_inv_xpx: ∀f2,g2,f,p2,p. p2⨮f2 ⊚ g2 ≘ p⨮f → ∀f1. ⫯f1 = g2 →
  59                      f2 ⊚ f1 ≘ f ∧ p2 = p.
  60 #f2 #g2 #f #p2 elim p2 -p2
  61 [ #p #Hf #f1 #H2 elim (gr_after_inv_push_bi … Hf … H2) -g2 [|*: // ]
  62   #g #Hf #H elim (push_inv_seq_dx … H) -H destruct /2 width=1 by conj/
  63 | #p2 #IH #p #Hf #f1 #H2 elim (gr_after_inv_next_sn … Hf) -Hf [|*: // ]
  64   #g1 #Hg #H1 elim (next_inv_seq_dx … H1) -H1
  65   #x #Hx #H destruct elim (IH … Hg) [|*: // ] -IH -Hg
  66   #H destruct /2 width=1 by conj/
  67 ]
  68 qed-.
  69
  70 lemma after_inv_xnx: ∀f2,g2,f,p2,p. p2⨮f2 ⊚ g2 ≘ p⨮f → ∀f1. ↑f1 = g2 →
  71                      ∃∃q. f2 ⊚ f1 ≘ q⨮f & q+p2 = p.
  72 #f2 #g2 #f #p2 elim p2 -p2
  73 [ #p #Hf #f1 #H2 elim (gr_after_inv_push_next … Hf … H2) -g2 [|*: // ]
  74   #g #Hf #H elim (next_inv_seq_dx … H) -H
  75   #x #Hx #Hg destruct /2 width=3 by ex2_intro/
  76 | #p2 #IH #p #Hf #f1 #H2 elim (gr_after_inv_next_sn … Hf) -Hf [|*: // ]
  77   #g #Hg #H elim (next_inv_seq_dx … H) -H
  78   #x #Hx #H destruct elim (IH … Hg) -IH -Hg [|*: // ]
  79   #m #Hf #Hm destruct /2 width=3 by ex2_intro/
  80 ]
  81 qed-.
  82
  83 lemma after_inv_const: ∀f2,f1,f,p1,p.
  84       p⨮f2 ⊚ p1⨮f1 ≘ p⨮f → f2 ⊚ f1 ≘ f ∧ 𝟏 = p1.
  85 #f2 #f1 #f #p1 #p elim p -p
  86 [ #H elim (gr_after_inv_push_sn_push … H) -H [|*: // ]
  87   #g2 #Hf #H elim (push_inv_seq_dx … H) -H /2 width=1 by conj/
  88 | #p #IH #H lapply (gr_after_inv_next_sn_next … H ????) -H /2 width=5 by/
  89 ]
  90 qed-.
  91
  92 lemma after_inv_total: ∀f2,f1,f. f2 ⊚ f1 ≘ f → f2 ∘ f1 ≡ f.
  93 /2 width=4 by gr_after_mono/ qed-.
  94
  95 (* Forward lemmas on after (specific) *****************************************)
  96
  97 lemma after_fwd_hd: ∀f2,f1,f,p1,p. f2 ⊚ p1⨮f1 ≘ p⨮f → f2@❨p1❩ = p.
  98 #f2 #f1 #f #p1 #p #H lapply (gr_after_des_pat ? p1 (𝟏) … H) -H [4:|*: // ]
  99 /3 width=2 by at_inv_O1, sym_eq/
 100 qed-.
 101
 102 lemma after_fwd_tls: ∀f,f1,p1,f2,p2,p. p2⨮f2 ⊚ p1⨮f1 ≘ p⨮f →
 103                      (⫰*[↓p1]f2) ⊚ f1 ≘ f.
 104 #f #f1 #p1 elim p1 -p1
 105 [ #f2 #p2 #p #H elim (after_inv_xpx … H) -H //
 106 | #p1 #IH * #q2 #f2 #p2 #p #H elim (after_inv_xnx … H) -H [|*: // ]
 107   #x #Hx #H destruct /2 width=3 by/
 108 ]
 109 qed-.
 110
 111 lemma after_inv_apply: ∀f2,f1,f,p2,p1,p. p2⨮f2 ⊚ p1⨮f1 ≘ p⨮f →
 112                        (p2⨮f2)@❨p1❩ = p ∧ (⫰*[↓p1]f2) ⊚ f1 ≘ f.
 113 /3 width=3 by after_fwd_tls, after_fwd_hd, conj/ qed-.
 114
 115 (* Properties on apply ******************************************************)
 116
 117 lemma compose_apply (f2) (f1) (i): f2@❨f1@❨i❩❩ = (f2∘f1)@❨i❩.
 118 /4 width=6 by gr_after_des_pat, at_inv_total, sym_eq/ qed.