matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_ist.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_pat_lt.ma".
  17 include "ground/relocation/pr_pat_pat.ma".
  18 include "ground/relocation/pr_nat.ma".
  19 include "ground/relocation/pr_ist.ma".
  20
  21 (* TOTALITY CONDITION FOR PARTIAL RELOCATION MAPS ***************************)
  22
  23 (* Advanced constructions with pr_pat ***************************************)
  24
  25 (*** at_dec *)
  26 lemma pr_pat_dec (f) (i1) (i2): 𝐓❨f❩ → Decidable (@❨i1,f❩ ≘ i2).
  27 #f #i1 #i2 #Hf lapply (Hf i1) -Hf *
  28 #j2 #Hf elim (eq_pnat_dec i2 j2)
  29 [ #H destruct /2 width=1 by or_introl/
  30 | /4 width=6 by pr_pat_mono, or_intror/
  31 ]
  32 qed-.
  33
  34 (*** is_at_dec *)
  35 lemma is_pr_pat_dec (f) (i2): 𝐓❨f❩ → Decidable (∃i1. @❨i1,f❩ ≘ i2).
  36 #f #i2 #Hf
  37 lapply (dec_plt (λi1.@❨i1,f❩ ≘ i2) … (↑i2)) [| * ]
  38 [ /2 width=1 by pr_pat_dec/
  39 | * /3 width=2 by ex_intro, or_introl/
  40 | #H @or_intror * #i1 #Hi12
  41   /5 width=3 by pr_pat_increasing, plt_succ_dx, ex2_intro/
  42 ]
  43 qed-.
  44
  45 (* Main destructions with pr_pat ********************************************)
  46
  47 (*** at_ext *)
  48 corec theorem pr_eq_ext_pat (f1) (f2): 𝐓❨f1❩ → 𝐓❨f2❩ →
  49               (∀i,i1,i2. @❨i,f1❩ ≘ i1 → @❨i,f2❩ ≘ i2 → i1 = i2) →
  50               f1 ≡ f2.
  51 cases (pr_map_split_tl f1) #H1
  52 cases (pr_map_split_tl f2) #H2
  53 #Hf1 #Hf2 #Hi
  54 [ @(pr_eq_push … H1 H2) @pr_eq_ext_pat -pr_eq_ext_pat
  55   [3:|*: /2 width=3 by pr_ist_inv_push/ ] -Hf1 -Hf2 #i #i1 #i2 #Hg1 #Hg2
  56   lapply (Hi (↑i) (↑i1) (↑i2) ??) /2 width=7 by pr_pat_push/
  57 | cases (Hf2 (𝟏)) -Hf1 -Hf2 -pr_eq_ext_pat
  58   #j2 #Hf2 cases (pr_pat_increasing_strict … Hf2 … H2) -H2
  59   lapply (Hi (𝟏) (𝟏) j2 … Hf2) /2 width=2 by pr_pat_refl/ -Hi -Hf2 -H1
  60   #H2 #H cases (plt_ge_false … H) -H //
  61 | cases (Hf1 (𝟏)) -Hf1 -Hf2 -pr_eq_ext_pat
  62   #j1 #Hf1 cases (pr_pat_increasing_strict … Hf1 … H1) -H1
  63   lapply (Hi (𝟏) j1 (𝟏) Hf1 ?) /2 width=2 by pr_pat_refl/ -Hi -Hf1 -H2
  64   #H1 #H cases (plt_ge_false … H) -H //
  65 | @(pr_eq_next … H1 H2) @pr_eq_ext_pat -pr_eq_ext_pat
  66   [3:|*: /2 width=3 by pr_ist_inv_next/ ] -Hf1 -Hf2 #i #i1 #i2 #Hg1 #Hg2
  67   lapply (Hi i (↑i1) (↑i2) ??) /2 width=5 by pr_pat_next/
  68 ]
  69 qed-.
  70
  71 (* Advanced constructions with pr_nat ***************************************)
  72
  73 lemma is_pr_nat_dec (f) (l2): 𝐓❨f❩ → Decidable (∃l1. @↑❨l1,f❩ ≘ l2).
  74 #f #l2 #Hf elim (is_pr_pat_dec … (↑l2) Hf)
  75 [ * /3 width=2 by ex_intro, or_introl/
  76 | #H @or_intror * /3 width=2 by ex_intro/
  77 ]
  78 qed-.