matita/matita/contribs/lambdadelta/ground/relocation/pr_after_pat_uni_tls.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/pr_tls.ma".
  16 include "ground/relocation/pr_pat.ma".
  17 (* * it should not depend on pr_isi *)
  18 include "ground/relocation/pr_isi_uni.ma".
  19 include "ground/relocation/pr_after_isi.ma".
  20
  21 (* RELATIONAL COMPOSITION FOR PARTIAL RELOCATION MAPS ***********************)
  22
  23 (* Constructions with pr_pat and pr_uni and pr_tls **************************)
  24
  25 (*** after_uni_succ_dx *)
  26 lemma pr_after_pat_uni (i2) (i1):
  27       ∀f2. @❪i1, f2❫ ≘ i2 →
  28       ∀f. f2 ⊚ 𝐮❨i1❩ ≘ f → 𝐮❨i2❩ ⊚ ⫰*[i2] f2 ≘ f.
  29 #i2 elim i2 -i2
  30 [ #i1 #f2 #Hf2 #f #Hf
  31   elim (pr_pat_inv_unit_dx … Hf2) -Hf2 // #g2 #H1 #H2 destruct
  32   elim (pr_after_inv_push_next … Hf) -Hf [ |*: // ] #g #Hg #H
  33   lapply (pr_after_isi_inv_dx … Hg ?) -Hg
  34   /4 width=5 by pr_after_isi_sn, pr_after_eq_repl_back, pr_after_next/
  35 | #i2 #IH #i1 #f2 #Hf2 #f #Hf >nsucc_inj
  36   elim (pr_pat_inv_succ_dx … Hf2) -Hf2 [1,3: * |*: // ]
  37   [ #g2 #j1 #Hg2 #H1 #H2 destruct >nsucc_inj in Hf; #Hf
  38     elim (pr_after_inv_push_next … Hf) -Hf [ |*: // ] #g #Hg #H destruct
  39     <pr_tls_swap /3 width=5 by pr_after_next/
  40   | #g2 #Hg2 #H2 destruct
  41     elim (pr_after_inv_next_sn … Hf) -Hf [2,3: // ] #g #Hg #H destruct
  42     <pr_tls_swap /3 width=5 by pr_after_next/
  43   ]
  44 ]
  45 qed.
  46
  47 (*** after_uni_succ_sn *)
  48 lemma pr_pat_after_uni_tls (i2) (i1):
  49       ∀f2. @❪i1, f2❫ ≘ i2 →
  50       ∀f. 𝐮❨i2❩ ⊚ ⫰*[i2] f2 ≘ f → f2 ⊚ 𝐮❨i1❩ ≘ f.
  51 #i2 elim i2 -i2
  52 [ #i1 #f2 #Hf2 #f #Hf
  53   elim (pr_pat_inv_unit_dx … Hf2) -Hf2 // #g2 #H1 #H2 destruct
  54   elim (pr_after_inv_next_sn … Hf) -Hf [ |*: // ] #g #Hg #H destruct
  55   lapply (pr_after_isi_inv_sn … Hg ?) -Hg
  56   /4 width=7 by pr_after_isi_dx, pr_after_eq_repl_back, pr_after_push/
  57 | #i2 #IH #i1 #f2 #Hf2 #f >nsucc_inj #Hf
  58   elim (pr_after_inv_next_sn … Hf) -Hf [2,3: // ] #g #Hg #H destruct
  59   elim (pr_pat_inv_succ_dx … Hf2) -Hf2 [1,3: * |*: // ]
  60   [ #g2 #j1 #Hg2 #H1 #H2 destruct <pr_tls_swap in Hg; /3 width=7 by pr_after_push/
  61   | #g2 #Hg2 #H2 destruct <pr_tls_swap in Hg; /3 width=5 by pr_after_next/
  62   ]
  63 ]
  64 qed-.
  65
  66 (* Advanced constructions with pr_uni ***************************************)
  67
  68 (*** after_uni_one_dx *)
  69 lemma pr_after_push_unit:
  70       ∀f2,f. ⫯f2 ⊚ 𝐮❨𝟏❩ ≘ f → 𝐮❨𝟏❩ ⊚ f2 ≘ f.
  71 #f2 #f #H
  72 @(pr_after_pat_uni … (⫯f2))
  73 /2 width=3 by pr_pat_refl/
  74 qed.
  75
  76 (*** after_uni_one_sn *)
  77 lemma pr_after_unit_sn:
  78       ∀f1,f. 𝐮❨𝟏❩ ⊚ f1 ≘ f → ⫯f1 ⊚ 𝐮❨𝟏❩ ≘ f.
  79 /3 width=3 by pr_pat_after_uni_tls, pr_pat_refl/ qed-.