]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambda/pointer_sequence.ma
9f4e63cd6e4f9dd0b6048c2ede1947447c5fcdcf
[helm.git] / matita / matita / contribs / lambda / pointer_sequence.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_order.ma".
16
17 (* POINTER SEQUENCE *********************************************************)
18
19 (* Policy: pointer sequence metavariables: r, s *)
20 definition pseq: Type[0] ≝ list ptr.
21
22 (* Note: a "head" computation contracts just redexes in the head *)
23 definition is_head: predicate pseq ≝ All … in_head.
24
25 (* Note: to us, a "normal" computation contracts redexes in non-decreasing positions *)
26 definition is_le: predicate pseq ≝ Allr … ple.
27
28 lemma is_le_compatible: ∀c,s. is_le s → is_le (c:::s).
29 #c #s elim s -s // #p * //
30 #q #s #IHs * /3 width=1/
31 qed.
32
33 lemma is_le_cons: ∀p,s. is_le s → is_le ((dx::p)::sn:::s).
34 #p #s elim s -s // #q1 * /2 width=1/
35 #q2 #s #IHs * /4 width=1/
36 qed.
37
38 lemma is_le_append: ∀r. is_le r → ∀s. is_le s → is_le ((dx:::r)@sn:::s).
39 #r elim r -r /3 width=1/ #p * /2 width=1/
40 #q #r #IHr * /3 width=1/
41 qed.
42
43 theorem is_head_is_le: ∀s. is_head s → is_le s.
44 #s elim s -s // #p * //
45 #q #s #IHs * /3 width=1/
46 qed.
47
48 lemma is_le_in_head: ∀p. in_head p → ∀s. is_le s → is_le (p::s).
49 #p #Hp * // /3 width=1/
50 qed.
51
52 theorem is_head_is_le_trans: ∀r. is_head r → ∀s. is_le s → is_le (r@s).
53 #r elim r -r // #p *
54 [ #_ * /2 width=1/
55 | #q #r #IHr * /3 width=1/
56 ]
57 qed.
58
59 definition ho_compatible_rc: predicate (pseq→relation term) ≝ λR.
60                              ∀s,A1,A2. R s A1 A2 → R (rc:::s) (𝛌.A1) (𝛌.A2).
61
62 definition ho_compatible_sn: predicate (pseq→relation term) ≝ λR.
63                              ∀s,B1,B2,A. R s B1 B2 → R (sn:::s) (@B1.A) (@B2.A).
64
65 definition ho_compatible_dx: predicate (pseq→relation term) ≝ λR.
66                              ∀s,B,A1,A2. R s A1 A2 → R (dx:::s) (@B.A1) (@B.A2).
67
68 lemma lstar_compatible_rc: ∀R. compatible_rc R → ho_compatible_rc (lstar … R).
69 #R #HR #s #A1 #A2 #H @(lstar_ind_l ????????? H) -s -A1 // /3 width=3/
70 qed.
71
72 lemma lstar_compatible_sn: ∀R. compatible_sn R → ho_compatible_sn (lstar … R).
73 #R #HR #s #B1 #B2 #A #H @(lstar_ind_l ????????? H) -s -B1 // /3 width=3/
74 qed.
75
76 lemma lstar_compatible_dx: ∀R. compatible_dx R → ho_compatible_dx (lstar … R).
77 #R #HR #s #B #A1 #A2 #H @(lstar_ind_l ????????? H) -s -A1 // /3 width=3/
78 qed.