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_2/pull/pull_2.ma".
  16 include "static_2/syntax/sh_props.ma".
  17 include "static_2/syntax/sd.ma".
  18
  19 (* SORT DEGREE **************************************************************)
  20
  21 (* Basic_2A1: includes: deg_SO_pos *)
  22 inductive deg_SO (h) (s) (s0): predicate nat ≝
  23 | deg_SO_succ : ∀n. (next h)^n s0 = s → deg_SO h s s0 (↑n)
  24 | deg_SO_zero: (∀n. (next h)^n s0 = s → ⊥) → deg_SO h s s0 0
  25 .
  26
  27 fact deg_SO_inv_succ_aux (h) (s) (s0):
  28      ∀n0. deg_SO h s s0 n0 → ∀n. n0 = ↑n → (next h)^n s0 = s.
  29 #h #s #s0 #n0 * -n0
  30 [ #n #Hn #x #H destruct //
  31 | #_ #x #H destruct
  32 ]
  33 qed-.
  34
  35 (* Basic_2A1: was: deg_SO_inv_pos *)
  36 lemma deg_SO_inv_succ (h) (s) (s0):
  37       ∀n. deg_SO h s s0 (↑n) → (next h)^n s0 = s.
  38 /2 width=3 by deg_SO_inv_succ_aux/ qed-.
  39
  40 lemma deg_SO_refl (h) (s): deg_SO h s s 1.
  41 #h #s @(deg_SO_succ … 0 ?) //
  42 qed.
  43
  44 definition sd_SO (h) (s): sd ≝ mk_sd (deg_SO h s).
  45
  46 lemma sd_SO_props (h) (s): sh_decidable h → sh_acyclic h →
  47       sd_props h (sd_SO h s).
  48 #h #s #Hhd #Hha
  49 @mk_sd_props
  50 [ #s0
  51   elim (nexts_dec … Hhd s0 s) -Hhd
  52   [ * /3 width=2 by deg_SO_succ, ex_intro/
  53   | /5 width=2 by deg_SO_zero, ex_intro/
  54   ]
  55 | #s0 #d1 #d2 * [ #n1 ] #H1 * [1,3: #n2 ] #H2
  56   [ < H2 in H1; -H2 #H
  57     lapply (nexts_inj … Hha … H) -H #H destruct //
  58   | elim H1 /2 width=2 by ex_intro/
  59   | elim H2 /2 width=2 by ex_intro/
  60   | //
  61   ]
  62 | #s0 #d *
  63   [ #n #H destruct cases n -n normalize
  64     [ @deg_SO_zero #n >iter_n_Sm #H
  65       lapply (nexts_inj … Hha … (↑n) 0 H) -H #H destruct
  66     | #n @deg_SO_succ >iter_n_Sm //
  67     ]
  68   | #H0 @deg_SO_zero #n >iter_n_Sm #H destruct
  69     /2 width=2 by/
  70   ]
  71 ]
  72 qed.
  73
  74 rec definition sd_d (h:?) (s:?) (d:?) on d: sd ≝
  75    match d with
  76    [ O   ⇒ sd_O
  77    | S d ⇒ match d with
  78            [ O ⇒ sd_SO h s
  79            | _ ⇒ sd_d h (next h s) d
  80            ]
  81    ].
  82
  83 lemma sd_d_props (h) (s) (d): sh_decidable h → sh_acyclic h →
  84       sd_props h (sd_d h s d).
  85 #h @pull_2 * [ // ]
  86 #d elim d -d /2 width=1 by sd_SO_props/
  87 qed.
  88
  89 (* Properties with sd_d *****************************************************)
  90
  91 lemma sd_d_SS (h):
  92       ∀s,d. sd_d h s (↑↑d) = sd_d h (⫯[h]s) (↑d).
  93 // qed.
  94
  95 lemma sd_d_correct (h): sh_decidable h → sh_acyclic h →
  96       ∀s,d. deg (sd_d h s d) s d.
  97 #h #Hhd #Hha @pull_2 #d elim d -d [ // ]
  98 #d elim d -d /3 width=3 by deg_inv_pred, sd_d_props/
  99 qed.