1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
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".
20 (* TOTALITY CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
22 (* Advanced properties on at ************************************************)
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/
34 lemma is_gr_pat_dec (f) (i2): 𝐓❪f❫ → Decidable (∃i1. @❪i1,f❫ ≘ i2).
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/
44 (* Main forward lemmas on at ************************************************)
47 corec theorem gr_eq_ext_pat (f1) (f2): 𝐓❪f1❫ → 𝐓❪f2❫ →
48 (∀i,i1,i2. @❪i,f1❫ ≘ i1 → @❪i,f2❫ ≘ i2 → i1 = i2) →
50 cases (gr_map_split_tl f1) #H1
51 cases (gr_map_split_tl f2) #H2
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/