]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_path.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / unwind_k / unwind2_path.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 "delayed_updating/unwind_k/unwind2_rmap.ma".
16 include "delayed_updating/syntax/path_structure.ma".
17 include "delayed_updating/notation/functions/black_downtriangle_2.ma".
18
19 (* TAILED UNWIND FOR PATH ***************************************************)
20
21 definition unwind2_path (f) (p): path ≝
22 match p with
23 [ list_empty     ⇒ (𝐞)
24 | list_lcons l q ⇒
25   match l with
26   [ label_d k ⇒ (⊗q)◖𝗱(▶[f]q@⧣❨k❩)
27   | label_m   ⇒ ⊗p
28   | label_L   ⇒ ⊗p
29   | label_A   ⇒ ⊗p
30   | label_S   ⇒ ⊗p
31   ]
32 ].
33
34 interpretation
35   "tailed unwind (path)"
36   'BlackDownTriangle f p = (unwind2_path f p).
37
38 (* Basic constructions ******************************************************)
39
40 lemma unwind2_path_empty (f):
41       (𝐞) = ▼[f]𝐞.
42 // qed.
43
44 lemma unwind2_path_d_dx (f) (p) (k) :
45       (⊗p)◖𝗱((▶[f]p)@⧣❨k❩) = ▼[f](p◖𝗱k).
46 // qed.
47
48 lemma unwind2_path_m_dx (f) (p):
49       ⊗p = ▼[f](p◖𝗺).
50 // qed.
51
52 lemma unwind2_path_L_dx (f) (p):
53       (⊗p)◖𝗟 = ▼[f](p◖𝗟).
54 // qed.
55
56 lemma unwind2_path_A_dx (f) (p):
57       (⊗p)◖𝗔 = ▼[f](p◖𝗔).
58 // qed.
59
60 lemma unwind2_path_S_dx (f) (p):
61       (⊗p)◖𝗦 = ▼[f](p◖𝗦).
62 // qed.
63
64 (* Constructions with structure *********************************************)
65
66 lemma structure_unwind2_path (f) (p):
67       ⊗p = ⊗▼[f]p.
68 #f * // * [ #k ] #p //
69 qed.
70
71 lemma unwind2_path_structure (f) (p):
72       ⊗p = ▼[f]⊗p.
73 #f #p elim p -p // * [ #k ] #p #IH //
74 [ <structure_L_dx <unwind2_path_L_dx //
75 | <structure_A_dx <unwind2_path_A_dx //
76 | <structure_S_dx <unwind2_path_S_dx //
77 ]
78 qed.
79
80 lemma unwind2_path_root (f) (p):
81       ∃∃r. 𝐞 = ⊗r & ⊗p●r = ▼[f]p.
82 #f * [| * [ #k ] #p ]
83 /2 width=3 by ex2_intro/
84 <unwind2_path_d_dx <structure_d_dx
85 /2 width=3 by ex2_intro/
86 qed-.
87
88 (* Destructions with structure **********************************************)
89
90 lemma unwind2_path_des_structure (f) (q) (p):
91       ⊗q = ▼[f]p → ⊗q = ⊗p.
92 // qed-.
93
94 (* Basic inversions *********************************************************)
95
96 lemma eq_inv_d_dx_unwind2_path (f) (q) (p) (h):
97       q◖𝗱h = ▼[f]p →
98       ∃∃r,k. q = ⊗r & h = ▶[f]r@⧣❨k❩ & r◖𝗱k = p.
99 #f #q * [| * [ #k ] #p ] #h
100 [ <unwind2_path_empty #H0 destruct
101 | <unwind2_path_d_dx #H0 destruct
102   /2 width=5 by ex3_2_intro/
103 | <unwind2_path_m_dx #H0
104   elim (eq_inv_d_dx_structure … H0)
105 | <unwind2_path_L_dx #H0 destruct
106 | <unwind2_path_A_dx #H0 destruct
107 | <unwind2_path_S_dx #H0 destruct
108 ]
109 qed-.
110
111 lemma eq_inv_m_dx_unwind2_path (f) (q) (p):
112       q◖𝗺 = ▼[f]p → ⊥.
113 #f #q * [| * [ #k ] #p ]
114 [ <unwind2_path_empty #H0 destruct
115 | <unwind2_path_d_dx #H0 destruct
116 | <unwind2_path_m_dx #H0
117   elim (eq_inv_m_dx_structure … H0)
118 | <unwind2_path_L_dx #H0 destruct
119 | <unwind2_path_A_dx #H0 destruct
120 | <unwind2_path_S_dx #H0 destruct
121 ]
122 qed-.
123
124 lemma eq_inv_L_dx_unwind2_path (f) (q) (p):
125       q◖𝗟 = ▼[f]p →
126       ∃∃r1,r2. q = ⊗r1 & ∀g. 𝐞 = ▼[g]r2 & r1●𝗟◗r2 = p.
127 #f #q * [| * [ #k ] #p ]
128 [ <unwind2_path_empty #H0 destruct
129 | <unwind2_path_d_dx #H0 destruct
130 | <unwind2_path_m_dx #H0
131   elim (eq_inv_L_dx_structure … H0) -H0 #r1 #r2 #H1 #H2 #H3 destruct
132   /2 width=5 by ex3_2_intro/
133 | <unwind2_path_L_dx #H0 destruct
134   /2 width=5 by ex3_2_intro/
135 | <unwind2_path_A_dx #H0 destruct
136 | <unwind2_path_S_dx #H0 destruct
137 ]
138 qed-.
139
140 lemma eq_inv_A_dx_unwind2_path (f) (q) (p):
141       q◖𝗔 = ▼[f]p →
142       ∃∃r1,r2. q = ⊗r1 & ∀g. 𝐞 = ▼[g]r2 & r1●𝗔◗r2 = p.
143 #f #q * [| * [ #k ] #p ]
144 [ <unwind2_path_empty #H0 destruct
145 | <unwind2_path_d_dx #H0 destruct
146 | <unwind2_path_m_dx #H0
147   elim (eq_inv_A_dx_structure … H0) -H0 #r1 #r2 #H1 #H2 #H3 destruct
148   /2 width=5 by ex3_2_intro/
149 | <unwind2_path_L_dx #H0 destruct
150 | <unwind2_path_A_dx #H0 destruct
151   /2 width=5 by ex3_2_intro/
152 | <unwind2_path_S_dx #H0 destruct
153 ]
154 qed-.
155
156 lemma eq_inv_S_dx_unwind2_path (f) (q) (p):
157       q◖𝗦 = ▼[f]p →
158       ∃∃r1,r2. q = ⊗r1 & ∀g. 𝐞 = ▼[g]r2 & r1●𝗦◗r2 = p.
159 #f #q * [| * [ #k ] #p ]
160 [ <unwind2_path_empty #H0 destruct
161 | <unwind2_path_d_dx #H0 destruct
162 | <unwind2_path_m_dx #H0
163   elim (eq_inv_S_dx_structure … H0) -H0 #r1 #r2 #H1 #H2 #H3 destruct
164   /2 width=5 by ex3_2_intro/
165 | <unwind2_path_L_dx #H0 destruct
166 | <unwind2_path_A_dx #H0 destruct
167 | <unwind2_path_S_dx #H0 destruct
168   /2 width=5 by ex3_2_intro/
169 ]
170 qed-.