matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_pat.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/arith/pnat_lt_pred.ma".
  16 include "ground/relocation/pr_pat.ma".
  17
  18 (* POSITIVE APPLICATION FOR PARTIAL RELOCATION MAPS *************************)
  19
  20 (* Main constructions *******************************************************)
  21
  22 (*** at_monotonic *)
  23 theorem pr_pat_monotonic:
  24         ∀j2,i2,f. @❨i2,f❩ ≘ j2 → ∀j1,i1. @❨i1,f❩ ≘ j1 →
  25         i1 < i2 → j1 < j2.
  26 #j2 elim j2 -j2
  27 [ #i2 #f #H2f elim (pr_pat_inv_unit_dx … H2f) -H2f //
  28   #g #H21 #_ #j1 #i1 #_ #Hi elim (plt_ge_false … Hi) -Hi //
  29 | #j2 #IH #i2 #f #H2f * //
  30   #j1 #i1 #H1f #Hi elim (plt_inv_gen … Hi)
  31   #_ #Hi2 elim (pr_pat_inv_succ_bi … H2f (↓i2)) -H2f [1,3: * |*: // ]
  32   #g #H2g #H
  33   [ elim (pr_pat_inv_push_succ … H1f … H) -f
  34     /4 width=8 by plt_inv_succ_bi, plt_succ_bi/
  35   | /4 width=8 by pr_pat_inv_next_succ, plt_succ_bi/
  36   ]
  37 ]
  38 qed-.
  39
  40 (*** at_inv_monotonic *)
  41 theorem pr_pat_inv_monotonic:
  42         ∀j1,i1,f. @❨i1,f❩ ≘ j1 → ∀j2,i2. @❨i2,f❩ ≘ j2 →
  43         j1 < j2 → i1 < i2.
  44 #j1 elim j1 -j1
  45 [ #i1 #f #H1f elim (pr_pat_inv_unit_dx … H1f) -H1f //
  46   #g * -i1 #H #j2 #i2 #H2f #Hj lapply (plt_des_gen … Hj) -Hj
  47   #H22 elim (pr_pat_inv_push_succ … H2f … (↓j2) H) -f //
  48 | #j1 #IH *
  49   [ #f #H1f elim (pr_pat_inv_unit_succ … H1f) -H1f [ |*: // ]
  50     #g #H1g #H #j2 #i2 #H2f #Hj elim (plt_inv_succ_sn … Hj) -Hj
  51     /3 width=7 by pr_pat_inv_next_succ/
  52   | #i1 #f #H1f #j2 #i2 #H2f #Hj elim (plt_inv_succ_sn … Hj) -Hj
  53     #Hj #H22 elim (pr_pat_inv_succ_bi … H1f) -H1f [1,4: * |*: // ]
  54     #g #Hg #H
  55     [ elim (pr_pat_inv_push_succ … H2f … (↓j2) H) -f
  56       /3 width=7 by plt_succ_bi/
  57     | /3 width=7 by pr_pat_inv_next_succ/
  58     ]
  59   ]
  60 ]
  61 qed-.
  62
  63 (*** at_mono *)
  64 theorem pr_pat_mono (f) (i):
  65         ∀i1. @❨i,f❩ ≘ i1 → ∀i2. @❨i,f❩ ≘ i2 → i2 = i1.
  66 #f #i #i1 #H1 #i2 #H2 elim (pnat_split_lt_eq_gt i2 i1) //
  67 #Hi elim (plt_ge_false i i)
  68 /2 width=6 by pr_pat_inv_monotonic/
  69 qed-.
  70
  71 (*** at_inj *)
  72 theorem pr_pat_inj (f) (i):
  73         ∀i1. @❨i1,f❩ ≘ i → ∀i2. @❨i2,f❩ ≘ i → i1 = i2.
  74 #f #i #i1 #H1 #i2 #H2 elim (pnat_split_lt_eq_gt i2 i1) //
  75 #Hi elim (plt_ge_false i i)
  76 /2 width=6 by pr_pat_monotonic/
  77 qed-.
  78
  79 (*** at_div_comm *)
  80 theorem pr_pat_div_comm (f2) (g2) (f1) (g1):
  81         H_pr_pat_div f2 g2 f1 g1 → H_pr_pat_div g2 f2 g1 f1.
  82 #f2 #g2 #f1 #g1 #IH #jg #jf #j #Hg #Hf
  83 elim (IH … Hf Hg) -IH -j /2 width=3 by ex2_intro/
  84 qed-.
  85
  86 (*** at_div_pp *)
  87 theorem pr_pat_div_push_bi (f2) (g2) (f1) (g1):
  88         H_pr_pat_div f2 g2 f1 g1 → H_pr_pat_div (⫯f2) (⫯g2) (⫯f1) (⫯g1).
  89 #f2 #g2 #f1 #g1 #IH #jf #jg #j #Hf #Hg
  90 elim (pr_pat_inv_push … Hf) -Hf [1,2: * |*: // ]
  91 [ #H1 #H2 destruct -IH
  92   lapply (pr_pat_inv_push_unit … Hg ???) -Hg [4: |*: // ] #H destruct
  93   /3 width=3 by pr_pat_refl, ex2_intro/
  94 | #xf #i #Hf2 #H1 #H2 destruct
  95   lapply (pr_pat_inv_push_succ … Hg ????) -Hg [5: * |*: // ] #xg #Hg2 #H destruct
  96   elim (IH … Hf2 Hg2) -IH -i /3 width=9 by pr_pat_push, ex2_intro/
  97 ]
  98 qed-.
  99
 100 (*** at_div_nn *)
 101 theorem pr_pat_div_next_bi (f2) (g2) (f1) (g1):
 102         H_pr_pat_div f2 g2 f1 g1 → H_pr_pat_div (↑f2) (↑g2) (f1) (g1).
 103 #f2 #g2 #f1 #g1 #IH #jf #jg #j #Hf #Hg
 104 elim (pr_pat_inv_next … Hf) -Hf [ |*: // ] #i #Hf2 #H destruct
 105 lapply (pr_pat_inv_next_succ … Hg ????) -Hg [5: |*: // ] #Hg2
 106 elim (IH … Hf2 Hg2) -IH -i /2 width=3 by ex2_intro/
 107 qed-.
 108
 109 (*** at_div_np *)
 110 theorem pr_pat_div_next_push (f2) (g2) (f1) (g1):
 111         H_pr_pat_div f2 g2 f1 g1 → H_pr_pat_div (↑f2) (⫯g2) (f1) (↑g1).
 112 #f2 #g2 #f1 #g1 #IH #jf #jg #j #Hf #Hg
 113 elim (pr_pat_inv_next … Hf) -Hf [ |*: // ] #i #Hf2 #H destruct
 114 lapply (pr_pat_inv_push_succ … Hg ????) -Hg [5: * |*: // ] #xg #Hg2 #H destruct
 115 elim (IH … Hf2 Hg2) -IH -i /3 width=7 by pr_pat_next, ex2_intro/
 116 qed-.
 117
 118 (*** at_div_pn *)
 119 theorem pr_pat_div_push_next (f2) (g2) (f1) (g1):
 120         H_pr_pat_div f2 g2 f1 g1 → H_pr_pat_div (⫯f2) (↑g2) (↑f1) (g1).
 121 /4 width=6 by pr_pat_div_next_push, pr_pat_div_comm/ qed-.