]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_ist.ma
update in delayed_updating
[helm.git] / 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-.