matita/matita/contribs/lambdadelta/static_2/syntax/sh_lt.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 "static_2/syntax/sh_props.ma".
  16
  17 (* SORT HIERARCHY ***********************************************************)
  18
  19 (* strict monotonicity condition *)
  20 record sh_lt (h): Prop ≝
  21 {
  22   next_lt: ∀s. s < ⫯[h]s
  23 }.
  24
  25 (* Basic properties *********************************************************)
  26
  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/
  31 qed.
  32
  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/
  37 qed.
  38
  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.
  41 #h #Hh
  42 @pull_2 #n1
  43 elim n1 -n1
  44 [ #s *
  45   [ #H elim (lt_refl_false … H)
  46   | #n2 //
  47   ]
  48 | #n1 #IH #s *
  49   [ >iter_O #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
  53     /3 width=2 by lt_S_S/
  54   ]
  55 ]
  56 qed-.
  57
  58 lemma sh_lt_acyclic (h): sh_lt h → sh_acyclic h.
  59 #h #Hh
  60 @mk_sh_acyclic
  61 @pull_2 #n1
  62 elim n1 -n1
  63 [ #s * [ // ] #n2 >iter_O #H
  64   elim (lt_refl_false s) >H in ⊢ (??%); -H
  65   /2 width=1 by nexts_lt/
  66 | #n1 #IH #s *
  67   [ >iter_O #H -IH
  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
  71     /3 width=2 by eq_f/
  72   ]
  73 ]
  74 qed.
  75
  76 lemma sh_lt_dec (h): sh_lt h → sh_decidable h.
  77 #h #Hh
  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/
  92     ]
  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
  98     [ * #n #H destruct
  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
 104       <(S_pred … H) -H
 105       @(ex_intro … (↓n)) >(iter_n_Sm … (next h)) >iter_S //
 106     ]
 107   ]
 108 ]
 109 qed-.