matita/matita/contribs/lambdadelta/ground/relocation/gr_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/gr_eq.ma".
  16 include "ground/relocation/gr_pat_lt.ma".
  17 include "ground/relocation/gr_pat_pat.ma".
  18 include "ground/relocation/gr_ist.ma".
  19
  20 (* TOTALITY CONDITION FOR GENERIC RELOCATION MAPS ***************************)
  21
  22 (* Advanced constructions with gr_pat ***************************************)
  23
  24 (*** at_dec *)
  25 lemma gr_pat_dec (f) (i1) (i2): 𝐓❪f❫ → Decidable (@❪i1,f❫ ≘ i2).
  26 #f #i1 #i2 #Hf lapply (Hf i1) -Hf *
  27 #j2 #Hf elim (eq_pnat_dec i2 j2)
  28 [ #H destruct /2 width=1 by or_introl/
  29 | /4 width=6 by gr_pat_mono, or_intror/
  30 ]
  31 qed-.
  32
  33 (*** is_at_dec *)
  34 lemma is_gr_pat_dec (f) (i2): 𝐓❪f❫ → Decidable (∃i1. @❪i1,f❫ ≘ i2).
  35 #f #i2 #Hf
  36 lapply (dec_plt (λi1.@❪i1,f❫ ≘ i2) … (↑i2)) [| * ]
  37 [ /2 width=1 by gr_pat_dec/
  38 | * /3 width=2 by ex_intro, or_introl/
  39 | #H @or_intror * #i1 #Hi12
  40   /5 width=3 by gr_pat_increasing, plt_succ_dx, ex2_intro/
  41 ]
  42 qed-.
  43
  44 (* Main destructions with gr_pat ********************************************)
  45
  46 (*** at_ext *)
  47 corec theorem gr_eq_ext_pat (f1) (f2): 𝐓❪f1❫ → 𝐓❪f2❫ →
  48               (∀i,i1,i2. @❪i,f1❫ ≘ i1 → @❪i,f2❫ ≘ i2 → i1 = i2) →
  49               f1 ≡ f2.
  50 cases (gr_map_split_tl f1) #H1
  51 cases (gr_map_split_tl f2) #H2
  52 #Hf1 #Hf2 #Hi
  53 [ @(gr_eq_push … H1 H2) @gr_eq_ext_pat -gr_eq_ext_pat
  54   [3:|*: /2 width=3 by gr_ist_inv_push/ ] -Hf1 -Hf2 #i #i1 #i2 #Hg1 #Hg2
  55   lapply (Hi (↑i) (↑i1) (↑i2) ??) /2 width=7 by gr_pat_push/
  56 | cases (Hf2 (𝟏)) -Hf1 -Hf2 -gr_eq_ext_pat
  57   #j2 #Hf2 cases (gr_pat_increasing_strict … Hf2 … H2) -H2
  58   lapply (Hi (𝟏) (𝟏) j2 … Hf2) /2 width=2 by gr_pat_refl/ -Hi -Hf2 -H1
  59   #H2 #H cases (plt_ge_false … H) -H //
  60 | cases (Hf1 (𝟏)) -Hf1 -Hf2 -gr_eq_ext_pat
  61   #j1 #Hf1 cases (gr_pat_increasing_strict … Hf1 … H1) -H1
  62   lapply (Hi (𝟏) j1 (𝟏) Hf1 ?) /2 width=2 by gr_pat_refl/ -Hi -Hf1 -H2
  63   #H1 #H cases (plt_ge_false … H) -H //
  64 | @(gr_eq_next … H1 H2) @gr_eq_ext_pat -gr_eq_ext_pat
  65   [3:|*: /2 width=3 by gr_ist_inv_next/ ] -Hf1 -Hf2 #i #i1 #i2 #Hg1 #Hg2
  66   lapply (Hi i (↑i1) (↑i2) ??) /2 width=5 by gr_pat_next/
  67 ]
  68 qed-.