matita/matita/contribs/lambdadelta/static_2/syntax/sd_d.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 "ground/generated/pull_2.ma".
  16 include "ground/arith/pnat_pred.ma".
  17 include "static_2/syntax/sh_props.ma".
  18 include "static_2/syntax/sd.ma".
  19
  20 (* SORT DEGREE **************************************************************)
  21
  22 (* Basic_2A1: includes: deg_SO_pos *)
  23 inductive deg_SO (h) (s) (s0): predicate nat ≝
  24 | deg_SO_succ : ∀n. ⇡*[h,n]s0 = s → deg_SO h s s0 (↑n)
  25 | deg_SO_zero: (∀n. ⇡*[h,n]s0 = s → ⊥) → deg_SO h s s0 𝟎
  26 .
  27
  28 fact deg_SO_inv_succ_aux (h) (s) (s0):
  29      ∀n0. deg_SO h s s0 n0 → ∀n. n0 = ↑n → ⇡*[h,n]s0 = s.
  30 #h #s #s0 #n0 * -n0
  31 [ #n #Hn #x #H destruct //
  32 | #_ #x #H elim (eq_inv_zero_nsucc … H)
  33 ]
  34 qed-.
  35
  36 (* Basic_2A1: was: deg_SO_inv_pos *)
  37 lemma deg_SO_inv_succ (h) (s) (s0):
  38       ∀n. deg_SO h s s0 (↑n) → ⇡*[h,n]s0 = s.
  39 /2 width=3 by deg_SO_inv_succ_aux/ qed-.
  40
  41 lemma deg_SO_refl (h) (s):
  42       deg_SO h s s 𝟏.
  43 #h #s @(deg_SO_succ … 𝟎 ?) //
  44 qed.
  45
  46 definition sd_SO (h) (s):
  47            sd ≝ mk_sd (deg_SO h s).
  48
  49 lemma sd_SO_props (h) (s):
  50       sh_decidable h → sh_acyclic h →
  51       sd_props h (sd_SO h s).
  52 #h #s #Hhd #Hha
  53 @mk_sd_props
  54 [ #s0
  55   elim (sh_nexts_dec … Hhd s0 s) -Hhd
  56   [ * /3 width=2 by deg_SO_succ, ex_intro/
  57   | /5 width=2 by deg_SO_zero, ex_intro/
  58   ]
  59 | #s0 #d1 #d2 * [ #n1 ] #H1 * [1,3: #n2 ] #H2
  60   [ < H2 in H1; -H2 #H
  61     lapply (sh_nexts_inj … Hha … H) -H #H destruct //
  62   | elim H1 /2 width=2 by ex_intro/
  63   | elim H2 /2 width=2 by ex_intro/
  64   | //
  65   ]
  66 | #s0 #d *
  67   [ #n #H destruct
  68     <npred_succ @(nat_ind_succ … n) -n
  69     [ @deg_SO_zero #n >sh_nexts_succ_next #H
  70       lapply (sh_nexts_inj … Hha … H) -H #H
  71       elim (eq_inv_nsucc_zero … H)
  72     | #n #_ /2 width=1 by deg_SO_succ/
  73     ]
  74   | #H0 @deg_SO_zero #n >sh_nexts_succ_next #H destruct
  75     /2 width=2 by/
  76   ]
  77 ]
  78 qed.
  79
  80 rec definition sd_d_pnat (h) (s) (d) on d: sd ≝
  81 match d with
  82 [ punit   ⇒ sd_SO h s
  83 | psucc d ⇒ sd_d_pnat h (⇡[h]s) d
  84 ].
  85
  86 definition sd_d (h) (s) (d): sd ≝
  87 match d with
  88 [ nzero  ⇒ sd_O
  89 | ninj d ⇒ sd_d_pnat h s d
  90 ].
  91
  92 lemma sd_d_props (h) (s) (d):
  93       sh_decidable h → sh_acyclic h →
  94       sd_props h (sd_d h s d).
  95 #h @pull_2 * [ // ]
  96 #d elim d -d /2 width=1 by sd_SO_props/
  97 qed.
  98
  99 (* Properties with sd_d *****************************************************)
 100
 101 lemma sd_d_SS (h):
 102       ∀s,d. sd_d h s (↑↑d) = sd_d h (⇡[h]s) (↑d).
 103 // qed.
 104
 105 lemma sd_d_correct (h):
 106       sh_decidable h → sh_acyclic h →
 107       ∀s,d. deg (sd_d h s d) s d.
 108 #h #Hhd #Hha @pull_2 * [ // ]
 109 #d elim d -d [ // ] #d #IH #s
 110 >(npsucc_pred d) in ⊢ (???%);
 111 @(deg_inv_pred h)
 112 [ /2 width=1 by sd_d_props/
 113 | <nsucc_pnpred //
 114 ]
 115 qed.