matita/matita/contribs/lambdadelta/basic_2/static/sd.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 "basic_2/static/sh.ma".
  16
  17 (* SORT DEGREE **************************************************************)
  18
  19 (* sort degree specification *)
  20 record sd (h:sh): Type[0] ≝ {
  21    deg      : relation nat;                            (* degree of the sort *)
  22    deg_total: ∀s. ∃d. deg s d;                         (* functional relation axioms *)
  23    deg_mono : ∀s,d1,d2. deg s d1 → deg s d2 → d1 = d2;
  24    deg_next : ∀s,d. deg s d → deg (next h s) (⫰d)      (* compatibility condition *)
  25 }.
  26
  27 (* Notable specifications ***************************************************)
  28
  29 definition deg_O: relation nat ≝ λs,d. d = 0.
  30
  31 definition sd_O: ∀h. sd h ≝ λh. mk_sd h deg_O ….
  32 /2 width=2 by le_n_O_to_eq, le_n, ex_intro/ defined.
  33
  34 (* Basic_2A1: includes: deg_SO_pos *)
  35 inductive deg_SO (h:sh) (s:nat) (s0:nat): predicate nat ≝
  36 | deg_SO_succ : ∀n. (next h)^n s0 = s → deg_SO h s s0 (⫯n)
  37 | deg_SO_zero: ((∃n. (next h)^n s0 = s) → ⊥) → deg_SO h s s0 0
  38 .
  39
  40 fact deg_SO_inv_succ_aux: ∀h,s,s0,n0. deg_SO h s s0 n0 → ∀n. n0 = ⫯n →
  41                           (next h)^n s0 = s.
  42 #h #s #s0 #n0 * -n0
  43 [ #n #Hn #x #H destruct //
  44 | #_ #x #H destruct
  45 ]
  46 qed-.
  47
  48 (* Basic_2A1: was: deg_SO_inv_pos *)
  49 lemma deg_SO_inv_succ: ∀h,s,s0,n. deg_SO h s s0 (⫯n) → (next h)^n s0 = s.
  50 /2 width=3 by deg_SO_inv_succ_aux/ qed-.
  51
  52 lemma deg_SO_refl: ∀h,s. deg_SO h s s 1.
  53 #h #s @(deg_SO_succ … 0 ?) //
  54 qed.
  55
  56 lemma deg_SO_gt: ∀h,s1,s2. s1 < s2 → deg_SO h s1 s2 0.
  57 #h #s1 #s2 #HK12 @deg_SO_zero * #n elim n -n normalize
  58 [ #H destruct
  59   elim (lt_refl_false … HK12)
  60 | #n #_ #H
  61   lapply (next_lt h ((next h)^n s2)) >H -H #H
  62   lapply (transitive_lt … H HK12) -s1 #H1
  63   lapply (nexts_le h s2 n) #H2
  64   lapply (le_to_lt_to_lt … H2 H1) -h -n #H
  65   elim (lt_refl_false … H)
  66 ]
  67 qed.
  68
  69 definition sd_SO: ∀h. nat → sd h ≝ λh,s. mk_sd h (deg_SO h s) ….
  70 [ #s0
  71   lapply (nexts_dec h s0 s) *
  72   [ * /3 width=2 by deg_SO_succ, ex_intro/ | /4 width=2 by deg_SO_zero, ex_intro/ ]
  73 | #K0 #d1 #d2 * [ #n1 ] #H1 * [1,3: #n2 ] #H2 //
  74   [ < H2 in H1; -H2 #H
  75     lapply (nexts_inj … H) -H #H destruct //
  76   | elim H1 /2 width=2 by ex_intro/
  77   | elim H2 /2 width=2 by ex_intro/
  78   ]
  79 | #s0 #n *
  80   [ #d #H destruct elim d -d normalize
  81     /2 width=1 by deg_SO_gt, deg_SO_succ, next_lt/
  82   | #H1 @deg_SO_zero * #d #H2 destruct
  83     @H1 -H1 @(ex_intro … (⫯d)) /2 width=1 by sym_eq/ (**) (* explicit constructor *)
  84   ]
  85 ]
  86 defined.
  87
  88 rec definition sd_d (h:sh) (s:nat) (d:nat) on d : sd h ≝
  89    match d with
  90    [ O   ⇒ sd_O h
  91    | S d ⇒ match d with
  92            [ O ⇒ sd_SO h s
  93            | _ ⇒ sd_d h (next h s) d
  94            ]
  95    ].
  96
  97 (* Basic inversion lemmas ***************************************************)
  98
  99 lemma deg_inv_pred: ∀h,o,s,d. deg h o (next h s) (⫯d) → deg h o s (⫯⫯d).
 100 #h #o #s #d #H1
 101 elim (deg_total h o s) #n #H0
 102 lapply (deg_next … H0) #H2
 103 lapply (deg_mono … H1 H2) -H1 -H2 #H >H >S_pred /2 width=2 by ltn_to_ltO/
 104 qed-.
 105
 106 lemma deg_inv_prec: ∀h,o,s,n,d. deg h o ((next h)^n s) (⫯d) → deg h o s (⫯(d+n)).
 107 #h #o #s #n elim n -n normalize /3 width=1 by deg_inv_pred/
 108 qed-.
 109
 110 (* Basic properties *********************************************************)
 111
 112 lemma deg_iter: ∀h,o,s,d,n. deg h o s d → deg h o ((next h)^n s) (d-n).
 113 #h #o #s #d #n elim n -n normalize /3 width=1 by deg_next/
 114 qed.
 115
 116 lemma deg_next_SO: ∀h,o,s,d. deg h o s (⫯d) → deg h o (next h s) d.
 117 /2 width=1 by deg_next/ qed-.
 118
 119 lemma sd_d_SS: ∀h,s,d. sd_d h s (⫯⫯d) = sd_d h (next h s) (⫯d).
 120 // qed.
 121
 122 lemma sd_d_correct: ∀h,d,s. deg h (sd_d h s d) s d.
 123 #h #d elim d -d // #d elim d -d /3 width=1 by deg_inv_pred/
 124 qed.