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 (*
  16 include "ground/relocation/pstream_tls.ma".
  17 include "ground/relocation/pstream_istot.ma".
  18 *)
  19 include "ground/arith/pnat_plus.ma".
  20 include "ground/relocation/pr_after.ma".
  21 include "ground/relocation/tr_map.ma".
  22
  23 (* Properties on after (specific) *********************************************)
  24
  25 (*** after_O2 *)
  26 lemma tr_after_push_dx:
  27       ∀f2,f1,f. 𝐭❨f2❩ ⊚ f1 ≘ 𝐭❨f❩ →
  28       ∀p. 𝐭❨p⨮f2❩ ⊚ ⫯f1 ≘ 𝐭❨p⨮f❩.
  29 #f2 #f1 #f #Hf #p elim p -p
  30 /2 width=7 by pr_after_refl, pr_after_next/
  31 qed.
  32
  33 (*** after_S2 *)
  34 lemma tr_after_next_dx:
  35       ∀f2,f1,f,p1,p. 𝐭❨f2❩ ⊚ 𝐭❨p1⨮f1❩ ≘ 𝐭❨p⨮f❩ →
  36       ∀p2. 𝐭❨p2⨮f2❩ ⊚ 𝐭❨↑p1⨮f1❩ ≘ 𝐭❨(p+p2)⨮f❩.
  37 #f2 #f1 #f #p1 #p #Hf #p2 elim p2 -p2
  38 /2 width=7 by pr_after_next, pr_after_push/
  39 qed.
  40
  41 include "ground/lib/stream_tls.ma".
  42 include "ground/relocation/tr_pap.ma".
  43
  44 (*** after_apply *)
  45 lemma tr_after_pap:
  46       ∀p1,f2,f1,f. 𝐭❨⇂*[ninj p1]f2❩ ⊚ 𝐭❨f1❩ ≘ 𝐭❨f❩ →
  47       (𝐭❨f2❩) ⊚ 𝐭❨p1⨮f1❩ ≘ 𝐭❨f2@❨p1❩⨮f❩.
  48 #p1 elim p1 -p1
  49 [ * /2 width=1 by tr_after_push_dx/
  50 | #p1 #IH * #p2 #f2 >nsucc_inj <stream_tls_swap
  51   /3 width=1 by tr_after_next_dx/
  52 ]
  53 qed-.
  54
  55 include "ground/relocation/tr_compose_pn.ma".
  56
  57 (*** after_total_aux *)
  58 corec fact tr_after_total_aux:
  59       ∀f2,f1,f. f2 ∘ f1 = f → 𝐭❨f2❩ ⊚ 𝐭❨f1❩ ≘ 𝐭❨f❩.
  60 * #p2 #f2 * #p1 #f1 * #p #f cases p2 -p2
  61 [ cases p1 -p1
  62   [ #H cases (tr_compose_inv_push_dx … H) -H /3 width=7 by pr_after_refl, eq_f2/
  63   | #p1 #H cases (tr_compose_inv_succ_dx … H) -H * -p /3 width=7 by pr_after_push/
  64   ]
  65 | #p2 >tr_next_unfold #H cases (tr_compose_inv_next_sn … H) -H * -p
  66   /3 width=5 by pr_after_next/
  67 ]
  68 qed-.
  69
  70 (*** after_total *)
  71 theorem tr_after_total:
  72         ∀f1,f2. 𝐭❨f2❩ ⊚ 𝐭❨f1❩ ≘ 𝐭❨f2 ∘ f1❩.
  73 /2 width=1 by tr_after_total_aux/ qed.
  74
  75 (* Inversion lemmas on after (specific) ***************************************)
  76
  77 lemma after_inv_xpx: ∀f2,g2,f,p2,p. p2⨮f2 ⊚ g2 ≘ p⨮f → ∀f1. ⫯f1 = g2 →
  78                      f2 ⊚ f1 ≘ f ∧ p2 = p.
  79 #f2 #g2 #f #p2 elim p2 -p2
  80 [ #p #Hf #f1 #H2 elim (gr_after_inv_push_bi … Hf … H2) -g2 [|*: // ]
  81   #g #Hf #H elim (push_inv_seq_dx … H) -H destruct /2 width=1 by conj/
  82 | #p2 #IH #p #Hf #f1 #H2 elim (gr_after_inv_next_sn … Hf) -Hf [|*: // ]
  83   #g1 #Hg #H1 elim (next_inv_seq_dx … H1) -H1
  84   #x #Hx #H destruct elim (IH … Hg) [|*: // ] -IH -Hg
  85   #H destruct /2 width=1 by conj/
  86 ]
  87 qed-.
  88
  89 lemma after_inv_xnx: ∀f2,g2,f,p2,p. p2⨮f2 ⊚ g2 ≘ p⨮f → ∀f1. ↑f1 = g2 →
  90                      ∃∃q. f2 ⊚ f1 ≘ q⨮f & q+p2 = p.
  91 #f2 #g2 #f #p2 elim p2 -p2
  92 [ #p #Hf #f1 #H2 elim (gr_after_inv_push_next … Hf … H2) -g2 [|*: // ]
  93   #g #Hf #H elim (next_inv_seq_dx … H) -H
  94   #x #Hx #Hg destruct /2 width=3 by ex2_intro/
  95 | #p2 #IH #p #Hf #f1 #H2 elim (gr_after_inv_next_sn … Hf) -Hf [|*: // ]
  96   #g #Hg #H elim (next_inv_seq_dx … H) -H
  97   #x #Hx #H destruct elim (IH … Hg) -IH -Hg [|*: // ]
  98   #m #Hf #Hm destruct /2 width=3 by ex2_intro/
  99 ]
 100 qed-.
 101
 102 lemma after_inv_const: ∀f2,f1,f,p1,p.
 103       p⨮f2 ⊚ p1⨮f1 ≘ p⨮f → f2 ⊚ f1 ≘ f ∧ 𝟏 = p1.
 104 #f2 #f1 #f #p1 #p elim p -p
 105 [ #H elim (gr_after_inv_push_sn_push … H) -H [|*: // ]
 106   #g2 #Hf #H elim (push_inv_seq_dx … H) -H /2 width=1 by conj/
 107 | #p #IH #H lapply (gr_after_inv_next_sn_next … H ????) -H /2 width=5 by/
 108 ]
 109 qed-.
 110
 111 lemma after_inv_total: ∀f2,f1,f. f2 ⊚ f1 ≘ f → f2 ∘ f1 ≐ f.
 112 /2 width=4 by gr_after_mono/ qed-.
 113
 114 (* Forward lemmas on after (specific) *****************************************)
 115
 116 lemma after_fwd_hd: ∀f2,f1,f,p1,p. f2 ⊚ p1⨮f1 ≘ p⨮f → f2@❨p1❩ = p.
 117 #f2 #f1 #f #p1 #p #H lapply (gr_after_des_pat ? p1 (𝟏) … H) -H [4:|*: // ]
 118 /3 width=2 by at_inv_O1, sym_eq/
 119 qed-.
 120
 121 lemma after_fwd_tls: ∀f,f1,p1,f2,p2,p. p2⨮f2 ⊚ p1⨮f1 ≘ p⨮f →
 122                      (⫰*[↓p1]f2) ⊚ f1 ≘ f.
 123 #f #f1 #p1 elim p1 -p1
 124 [ #f2 #p2 #p #H elim (after_inv_xpx … H) -H //
 125 | #p1 #IH * #q2 #f2 #p2 #p #H elim (after_inv_xnx … H) -H [|*: // ]
 126   #x #Hx #H destruct /2 width=3 by/
 127 ]
 128 qed-.
 129
 130 lemma after_inv_apply: ∀f2,f1,f,p2,p1,p. p2⨮f2 ⊚ p1⨮f1 ≘ p⨮f →
 131                        (p2⨮f2)@❨p1❩ = p ∧ (⫰*[↓p1]f2) ⊚ f1 ≘ f.
 132 /3 width=3 by after_fwd_tls, after_fwd_hd, conj/ qed-.
 133