]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambda/labelled_sequential_computation.ma
a609078fe56494417e19d8b4cc5a1a7673cb1380
[helm.git] / matita / matita / contribs / lambda / labelled_sequential_computation.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 "pointer_sequence.ma".
16 include "labelled_sequential_reduction.ma".
17
18 (* LABELLED SEQUENTIAL COMPUTATION (MULTISTEP) ******************************)
19
20 definition lsreds: pseq → relation term ≝ lstar … lsred.
21
22 interpretation "labelled sequential computation"
23    'SeqRedStar M s N = (lsreds s M N).
24
25 notation "hvbox( M break ⇀* [ term 46 s ] break term 46 N )"
26    non associative with precedence 45
27    for @{ 'SeqRedStar $M $s $N }.
28
29 lemma lsreds_step_rc: ∀p,M1,M2. M1 ⇀[p] M2 → M1 ⇀*[p::◊] M2.
30 /2 width=1/
31 qed.
32
33 lemma lsreds_inv_nil: ∀s,M1,M2. M1 ⇀*[s] M2 → ◊ = s → M1 = M2.
34 /2 width=5 by lstar_inv_nil/
35 qed-.
36
37 lemma lsreds_inv_cons: ∀s,M1,M2. M1 ⇀*[s] M2 → ∀q,r. q::r = s →
38                        ∃∃M. M1 ⇀[q] M & M ⇀*[r] M2.
39 /2 width=3 by lstar_inv_cons/
40 qed-.
41
42 lemma lsreds_inv_step_rc: ∀p,M1,M2. M1 ⇀*[p::◊] M2 → M1 ⇀[p] M2.
43 /2 width=1 by lstar_inv_step/
44 qed-.
45
46 lemma lsreds_inv_pos: ∀s,M1,M2. M1 ⇀*[s] M2 → 0 < |s| →
47                       ∃∃p,r,M. p::r = s & M1 ⇀[p] M & M ⇀*[r] M2.
48 /2 width=1 by lstar_inv_pos/
49 qed-.
50
51 lemma lsred_compatible_rc: ho_compatible_rc lsreds.
52 /3 width=1/
53 qed.
54
55 lemma lsred_compatible_sn: ho_compatible_sn lsreds.
56 /3 width=1/
57 qed.
58
59 lemma lsred_compatible_dx: ho_compatible_dx lsreds.
60 /3 width=1/
61 qed.
62
63 lemma lsreds_lift: ∀s. liftable (lsreds s).
64 /2 width=1/
65 qed.
66
67 lemma lsreds_inv_lift: ∀s. deliftable_sn (lsreds s).
68 /3 width=3 by lstar_deliftable_sn, lsred_inv_lift/
69 qed-.
70
71 lemma lsreds_dsubst: ∀s. dsubstable_dx (lsreds s).
72 /2 width=1/
73 qed.
74
75 theorem lsreds_mono: ∀s. singlevalued … (lsreds s).
76 /3 width=7 by lstar_singlevalued, lsred_mono/
77 qed-.
78
79 theorem lsreds_trans: ltransitive … lsreds.
80 /2 width=3 by lstar_ltransitive/
81 qed-.
82
83 (* Note: "|s|" should be unparetesized *)
84 lemma lsreds_fwd_mult: ∀s,M1,M2. M1 ⇀*[s] M2 → #{M2} ≤ #{M1} ^ (2 ^ (|s|)).
85 #s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 normalize //
86 #p #s #M1 #M #HM1 #_ #IHM2
87 lapply (lsred_fwd_mult … HM1) -p #HM1
88 @(transitive_le … IHM2) -M2
89 /3 width=1 by le_exp1, lt_O_exp, lt_to_le/ (**) (* auto: slow without trace *)
90 qed-.