matita/matita/contribs/lambdadelta/ground/relocation/pr_tl_eq.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_eq.ma".
  16 include "ground/relocation/pr_tl.ma".
  17
  18 (* TAIL FOR PARTIAL RELOCATION MAPS *****************************************)
  19
  20 (* Constructions with pr_eq *************************************************)
  21
  22 (*** eq_refl *)
  23 corec lemma pr_eq_refl: reflexive … pr_eq.
  24 #f cases (pr_map_split_tl f) #Hf
  25 [ @(pr_eq_push … Hf Hf) | @(pr_eq_next … Hf Hf) ] -Hf //
  26 qed.
  27
  28 (*** tl_eq_repl *)
  29 lemma pr_tl_eq_repl:
  30       pr_eq_repl … (λf1,f2. ⫰f1 ≡ ⫰f2).
  31 #f1 #f2 * -f1 -f2 //
  32 qed.
  33
  34 (* Inversions with pr_eq ****************************************************)
  35
  36 (*** eq_inv_gen *)
  37 lemma pr_eq_inv_gen (g1) (g2):
  38       g1 ≡ g2 →
  39       ∨∨ ∧∧ ⫰g1 ≡ ⫰g2 & ⫯⫰g1 = g1 & ⫯⫰g2 = g2
  40        | ∧∧ ⫰g1 ≡ ⫰g2 & ↑⫰g1 = g1 & ↑⫰g2 = g2.
  41 #g1 #g2 * -g1 -g2 #f1 #f2 #g1 #g2 #f * *
  42 /3 width=1 by and3_intro, or_introl, or_intror/
  43 qed-.
  44
  45 (* Advanced inversions with pr_eq *******************************************)
  46
  47 (*** pr_eq_inv_px *)
  48 lemma pr_eq_inv_push_sn (g1) (g2):
  49       g1 ≡ g2 → ∀f1. ⫯f1 = g1 →
  50       ∧∧ f1 ≡ ⫰g2 & ⫯⫰g2 = g2.
  51 #g1 #g2 #H #f1 #Hf1
  52 elim (pr_eq_inv_gen … H) -H * #Hg #Hg1 #Hg2 destruct
  53 [ /2 width=1 by conj/
  54 | elim (eq_inv_pr_next_push … Hg1)
  55 ]
  56 qed-.
  57
  58 (*** pr_eq_inv_nx *)
  59 lemma pr_eq_inv_next_sn (g1) (g2):
  60       g1 ≡ g2 → ∀f1. ↑f1 = g1 →
  61       ∧∧ f1 ≡ ⫰g2 & ↑⫰g2 = g2.
  62 #g1 #g2 #H #f1 #Hf1
  63 elim (pr_eq_inv_gen … H) -H * #Hg #Hg1 #Hg2 destruct
  64 [ elim (eq_inv_pr_push_next … Hg1)
  65 | /2 width=1 by conj/
  66 ]
  67 qed-.
  68
  69 (*** pr_eq_inv_xp *)
  70 lemma pr_eq_inv_push_dx (g1) (g2):
  71       g1 ≡ g2 → ∀f2. ⫯f2 = g2 →
  72       ∧∧ ⫰g1 ≡ f2 & ⫯⫰g1 = g1.
  73 #g1 #g2 #H #f2 #Hf2
  74 elim (pr_eq_inv_gen … H) -H * #Hg #Hg1 #Hg2 destruct
  75 [ /2 width=1 by conj/
  76 | elim (eq_inv_pr_next_push … Hg2)
  77 ]
  78 qed-.
  79
  80 (*** pr_eq_inv_xn *)
  81 lemma pr_eq_inv_next_dx (g1) (g2):
  82       g1 ≡ g2 → ∀f2. ↑f2 = g2 →
  83       ∧∧ ⫰g1 ≡ f2 & ↑⫰g1 = g1.
  84 #g1 #g2 #H #f2 #Hf2
  85 elim (pr_eq_inv_gen … H) -H * #Hg #Hg1 #Hg2 destruct
  86 [ elim (eq_inv_pr_push_next … Hg2)
  87 | /2 width=1 by conj/
  88 ]
  89 qed-.
  90
  91 (*** pr_eq_inv_pp *)
  92 lemma pr_eq_inv_push_bi (g1) (g2):
  93       g1 ≡ g2 → ∀f1,f2. ⫯f1 = g1 → ⫯f2 = g2 → f1 ≡ f2.
  94 #g1 #g2 #H #f1 #f2 #H1
  95 elim (pr_eq_inv_push_sn … H … H1) -g1 #Hx2 * #H
  96 lapply (eq_inv_pr_push_bi … H) -H //
  97 qed-.
  98
  99 (*** pr_eq_inv_nn *)
 100 lemma pr_eq_inv_next_bi (g1) (g2):
 101       g1 ≡ g2 → ∀f1,f2. ↑f1 = g1 → ↑f2 = g2 → f1 ≡ f2.
 102 #g1 #g2 #H #f1 #f2 #H1
 103 elim (pr_eq_inv_next_sn … H … H1) -g1 #Hx2 * #H
 104 lapply (eq_inv_pr_next_bi … H) -H //
 105 qed-.
 106
 107 (*** pr_eq_inv_pn *)
 108 lemma pr_eq_inv_push_next (g1) (g2):
 109       g1 ≡ g2 → ∀f1,f2. ⫯f1 = g1 → ↑f2 = g2 → ⊥.
 110 #g1 #g2 #H #f1 #f2 #H1
 111 elim (pr_eq_inv_push_sn … H … H1) -g1 #Hx2 * #H
 112 elim (eq_inv_pr_next_push … H)
 113 qed-.
 114
 115 (*** pr_eq_inv_np *)
 116 lemma pr_eq_inv_next_push (g1) (g2):
 117       g1 ≡ g2 → ∀f1,f2. ↑f1 = g1 → ⫯f2 = g2 → ⊥.
 118 #g1 #g2 #H #f1 #f2 #H1
 119 elim (pr_eq_inv_next_sn … H … H1) -g1 #Hx2 * #H
 120 elim (eq_inv_pr_push_next … H)
 121 qed-.