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 "static_2/syntax/sh_props.ma".
17 (* SORT HIERARCHY ***********************************************************)
19 (* strict monotonicity condition *)
20 record sh_lt (h): Prop ≝
22 next_lt: ∀s. s < ⫯[h]s
25 (* Basic properties *********************************************************)
27 lemma nexts_le (h): sh_lt h → ∀s,n. s ≤ (next h)^n s.
28 #h #Hh #s #n elim n -n [ // ] normalize #n #IH
29 lapply (next_lt … Hh ((next h)^n s)) #H
30 lapply (le_to_lt_to_lt … IH H) -IH -H /2 width=2 by lt_to_le/
33 lemma nexts_lt (h): sh_lt h → ∀s,n. s < (next h)^(↑n) s.
34 #h #Hh #s #n normalize
35 lapply (nexts_le … Hh s n) #H
36 @(le_to_lt_to_lt … H) /2 width=1 by next_lt/
39 lemma sh_lt_nexts_inv_lt (h): sh_lt h →
40 ∀s,n1,n2. (next h)^n1 s < (next h)^n2 s → n1 < n2.
45 [ #H elim (lt_refl_false … H)
50 elim (lt_refl_false s)
51 /3 width=3 by nexts_lt, transitive_lt/
52 | #n2 >iter_S >iter_S <(iter_n_Sm … (next h)) <(iter_n_Sm … (next h)) #H
58 lemma sh_lt_acyclic (h): sh_lt h → sh_acyclic h.
63 [ #s * [ // ] #n2 >iter_O #H
64 elim (lt_refl_false s) >H in ⊢ (??%); -H
65 /2 width=1 by nexts_lt/
68 elim (lt_refl_false s) <H in ⊢ (??%); -H
69 /2 width=1 by nexts_lt/
70 | #n2 >iter_S >iter_S <(iter_n_Sm … (next h)) <(iter_n_Sm … (next h)) #H
76 lemma sh_lt_dec (h): sh_lt h → sh_decidable h.
78 @mk_sh_decidable #s1 #s2
79 elim (lt_or_ge s2 s1) #Hs
80 [ @or_intror * #n #H destruct
81 @(lt_le_false … Hs) /2 width=1 by nexts_le/ (**) (* full auto too slow *)
82 | @(nat_elim_le_sn … Hs) -s1 -s2 #s1 #s2 #IH #Hs12
83 elim (lt_or_eq_or_gt s2 (⫯[h]s1)) #Hs21 destruct
84 [ elim (le_to_or_lt_eq … Hs12) -Hs12 #Hs12 destruct
85 [ -IH @or_intror * #n #H destruct
86 generalize in match Hs21; -Hs21
87 <(iter_O … (next h) s1) in ⊢ (??%→?); <(iter_S … (next h)) #H
88 lapply (sh_lt_nexts_inv_lt … Hh … H) -H #H
89 <(le_n_O_to_eq n) in Hs12;
90 /2 width=2 by lt_refl_false, le_S_S_to_le/
91 | /3 width=2 by ex_intro, or_introl/
93 | -IH @or_introl @(ex_intro … 1) // (**) (* auto fails *)
94 | lapply (transitive_lt s1 ??? Hs21) [ /2 width=1 by next_lt/ ] -Hs12 #Hs12
95 elim (IH (s2-⫯[h]s1)) -IH
96 [3: /3 width=1 by next_lt, monotonic_lt_minus_r/ ]
97 >minus_minus_m_m [2,4: /2 width=1 by lt_to_le/ ] -Hs21
99 @or_introl @(ex_intro … (↑n)) >iter_S >iter_n_Sm //
100 | #H1 @or_intror * #n #H2 @H1 -H1 destruct
101 generalize in match Hs12; -Hs12
102 <(iter_O … (next h) s1) in ⊢ (?%?→?); #H
103 lapply (sh_lt_nexts_inv_lt … Hh … H) -H #H
105 @(ex_intro … (↓n)) >(iter_n_Sm … (next h)) >iter_S //