matita/matita/contribs/lambda_delta/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: ∀k. ∃l. deg k l;                              (* functional relation axioms *)
  23    deg_mono : ∀k,l1,l2. deg k l1 → deg k l2 → l1 = l2;
  24    deg_next : ∀k,l. deg k l → deg (next h k) (l - 1);       (* compatibility condition *)
  25    deg_prev : ∀k,l. deg (next h k) (l + 1) → deg k (l + 2)
  26 }.
  27
  28 (* Notable specifications ***************************************************)
  29
  30 definition deg_O: relation nat ≝ λk,l. l = 0.
  31
  32 definition sd_O: ∀h. sd h ≝ λh. mk_sd h deg_O ….
  33 // /2 width=1/ /2 width=2/ qed.
  34
  35 inductive deg_SO (h:sh) (k:nat) (k0:nat): predicate nat ≝
  36 | deg_SO_pos : ∀l0. (next h)^l0 k0 = k → deg_SO h k k0 (l0 + 1)
  37 | deg_SO_zero: ((∃l0. (next h)^l0 k0 = k) → ⊥) → deg_SO h k k0 0
  38 .
  39
  40 fact deg_SO_inv_pos_aux: ∀h,k,k0,l0. deg_SO h k k0 l0 → ∀l. l0 = l + 1 →
  41                          (next h)^l k0 = k.
  42 #h #k #k0 #l0 * -l0
  43 [ #l0 #Hl0 #l #H
  44   lapply (injective_plus_l … H) -H #H destruct //
  45 | #_ #l0 <plus_n_Sm #H destruct
  46 ]
  47 qed.
  48
  49 lemma deg_SO_inv_pos: ∀h,k,k0,l0. deg_SO h k k0 (l0 + 1) → (next h)^l0 k0 = k.
  50 /2 width=3/ qed-.
  51
  52 lemma deg_SO_refl: ∀h,k. deg_SO h k k 1.
  53 #h #k @(deg_SO_pos … 0 ?) //
  54 qed.
  55
  56 lemma deg_SO_gt: ∀h,k1,k2. k1 < k2 → deg_SO h k1 k2 0.
  57 #h #k1 #k2 #HK12 @deg_SO_zero * #l elim l -l normalize
  58 [ #H destruct
  59   elim (lt_refl_false … HK12)
  60 | #l #_ #H
  61   lapply (next_lt h ((next h)^l k2)) >H -H #H
  62   lapply (transitive_lt … H HK12) -k1 #H1
  63   lapply (nexts_le h k2 l) #H2
  64   lapply (le_to_lt_to_lt … H2 H1) -h -l #H
  65   elim (lt_refl_false … H)
  66 qed.
  67
  68 definition sd_SO: ∀h. nat → sd h ≝ λh,k. mk_sd h (deg_SO h k) ….
  69 [ #k0
  70   lapply (nexts_dec h k0 k) * [ * /3 width=2/ | /4 width=2/ ]
  71 | #K0 #l1 #l2 * [ #l01 ] #H1 * [1,3: #l02 ] #H2 //
  72   [ < H2 in H1; -H2 #H
  73     lapply (nexts_inj … H) -H #H destruct //
  74   | elim (H1 ?) /2 width=2/
  75   | elim (H2 ?) /2 width=2/
  76   ]
  77 | #k0 #l0 *
  78   [ #l #H destruct elim l -l normalize /2 width=1/
  79   | #H1 @deg_SO_zero * #l #H2 destruct
  80     @H1 -H1 @(ex_intro … (S l)) /2 width=1/ (**) (* explicit constructor *)
  81   ]
  82 | #K0 #l0 #H
  83   <(deg_SO_inv_pos … H) -H >plus_n_2
  84   @deg_SO_pos >iter_SO /2 width=1/ (**) (* explicit constructor: iter_SO is needed *)
  85 ]
  86 qed.
  87
  88 let rec sd_l (h:sh) (k:nat) (l:nat) on l : sd h ≝
  89    match l with
  90    [ O   ⇒ sd_O h
  91    | S l ⇒ match l with
  92            [ O ⇒ sd_SO h k
  93            | _ ⇒ sd_l h (next h k) l
  94            ]
  95    ].
  96
  97 (* Basic properties *********************************************************)
  98
  99 lemma sd_l_SS: ∀h,k,l. sd_l h k (l + 2) = sd_l h (next h k) (l + 1).
 100 #h #k #l <plus_n_Sm <plus_n_Sm //
 101 qed.
 102
 103 lemma sd_l_correct: ∀h,l,k. deg h (sd_l h k l) k l.
 104 #h #l @(nat_ind_plus … l) -l // #l @(nat_ind_plus … l) -l // /3 width=1/
 105 qed.