]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/static_2/syntax/sd_d.ma
partial commit in static_2
[helm.git] / 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 "static_2/syntax/sh_props.ma".
16 include "static_2/syntax/sd.ma".
17
18 (* SORT DEGREE **************************************************************)
19
20 (* Basic_2A1: includes: deg_SO_pos *)
21 inductive deg_SO (h) (s) (s0): predicate nat ≝
22 | deg_SO_succ : ∀n. ⇡*[h,n]s0 = s → deg_SO h s s0 (↑n)
23 | deg_SO_zero: (∀n. ⇡*[h,n]s0 = s → ⊥) → deg_SO h s s0 𝟎
24 .
25
26 fact deg_SO_inv_succ_aux (h) (s) (s0):
27      ∀n0. deg_SO h s s0 n0 → ∀n. n0 = ↑n → ⇡*[h,n]s0 = s.
28 #h #s #s0 #n0 * -n0
29 [ #n #Hn #x #H destruct //
30 | #_ #x #H elim (eq_inv_zero_nsucc … H)
31 ]
32 qed-.
33
34 (* Basic_2A1: was: deg_SO_inv_pos *)
35 lemma deg_SO_inv_succ (h) (s) (s0):
36       ∀n. deg_SO h s s0 (↑n) → ⇡*[h,n]s0 = s.
37 /2 width=3 by deg_SO_inv_succ_aux/ qed-.
38
39 lemma deg_SO_refl (h) (s): deg_SO h s s 𝟏.
40 #h #s @(deg_SO_succ … 𝟎 ?) //
41 qed.
42
43 definition sd_SO (h) (s): sd ≝ mk_sd (deg_SO h s).
44
45 lemma sd_SO_props (h) (s): sh_decidable h → sh_acyclic h →
46       sd_props h (sd_SO h s).
47 #h #s #Hhd #Hha
48 @mk_sd_props
49 [ #s0
50   elim (sh_nexts_dec … Hhd s0 s) -Hhd
51   [ * /3 width=2 by deg_SO_succ, ex_intro/
52   | /5 width=2 by deg_SO_zero, ex_intro/
53   ]
54 | #s0 #d1 #d2 * [ #n1 ] #H1 * [1,3: #n2 ] #H2
55   [ < H2 in H1; -H2 #H
56     lapply (sh_nexts_inj … Hha … H) -H #H destruct //
57   | elim H1 /2 width=2 by ex_intro/
58   | elim H2 /2 width=2 by ex_intro/
59   | //
60   ]
61 | #s0 #d *
62   [ #n #H destruct
63     <npred_succ @(nat_ind_succ … n) -n
64     [ @deg_SO_zero #n >(sh_nexts_succ_next h n s0) #H 
65       lapply (sh_nexts_inj … Hha ???) -H #H destruct
66     | #n @deg_SO_succ >sh_nexts_swap //
67     ]
68   | #H0 @deg_SO_zero #n >sh_nexts_swap #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 (pr_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.