]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma
update in ground
[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / syntax / bdd_term.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/syntax/prototerm_constructors.ma".
16 include "delayed_updating/syntax/prototerm_equivalence.ma".
17 include "delayed_updating/notation/functions/class_d_phi_0.ma".
18 include "ground/xoa/or_5.ma".
19 include "ground/xoa/ex_3_1.ma".
20 include "ground/xoa/ex_4_2.ma".
21 include "ground/xoa/ex_4_3.ma".
22 include "ground/xoa/ex_5_3.ma".
23
24 (* BY-DEPTH DELAYED (BDD) TERM **********************************************)
25
26 inductive bdd: π’«β¨prototerm❩ β‰
27 | bdd_oref: βˆ€n. bdd (#n)
28 | bdd_iref: βˆ€t,n. bdd t β†’ bdd (𝛗n.t)
29 | bdd_abst: βˆ€t. bdd t β†’ bdd (π›Œ.t)
30 | bdd_appl: βˆ€u,t. bdd u β†’ bdd t β†’ bdd (@u.t)
31 | bdd_conv: βˆ€t1,t2. t1 β‡” t2 β†’ bdd t1 β†’ bdd t2
32 .
33
34 interpretation
35   "by-depth delayed (prototerm)"
36   'ClassDPhi = (bdd).
37
38 (*
39
40 (* Basic inversions *********************************************************)
41
42 lemma bdd_inv_in_comp_gen:
43       βˆ€t,p. t Ο΅ πƒπ›— β†’ p Ο΅ t β†’
44       βˆ¨βˆ¨ βˆƒβˆƒn. #n β‡” t & π—±nβ——πž = p
45        | βˆƒβˆƒu,q,n. u Ο΅ πƒπ›— & q Ο΅ u & π›—n.u β‡” t & π—±n◗𝗺◗q = p
46        | βˆƒβˆƒu,q. u Ο΅ πƒπ›— & q Ο΅ u & π›Œ.u β‡” t & π—Ÿβ——q = p
47        | βˆƒβˆƒv,u,q. v Ο΅ πƒπ›— & u Ο΅ πƒπ›— & q Ο΅ u & @v.u β‡” t & π—”β——q = p
48        | βˆƒβˆƒv,u,q. v Ο΅ πƒπ›— & u Ο΅ πƒπ›— & q Ο΅ v & @v.u β‡” t & π—¦β——q = p
49 .
50 #t #p #H elim H -H
51 [ #n * /3 width=3 by or5_intro0, ex2_intro/
52 | #u #n #Hu #_ * #q #Hq #Hp /3 width=7 by ex4_3_intro, or5_intro1/
53 | #u #Hu #_ * #q #Hq #Hp /3 width=6 by or5_intro2, ex4_2_intro/
54 | #v #u #Hv #Hu #_ #_ * * #q #Hq #Hp /3 width=8 by ex5_3_intro, or5_intro3, or5_intro4/
55 | #t1 #t2 #Ht12 #_ #IH #Ht2
56   elim IH -IH [6: /2 width=3 by subset_in_eq_repl_fwd/ ] *
57   [ /4 width=3 by subset_eq_trans, or5_intro0, ex2_intro/
58   | /4 width=7 by subset_eq_trans, ex4_3_intro, or5_intro1/
59   | /4 width=6 by subset_eq_trans, or5_intro2, ex4_2_intro/
60   | /4 width=8 by subset_eq_trans, ex5_3_intro, or5_intro3/
61   | /4 width=8 by subset_eq_trans, ex5_3_intro, or5_intro4/
62   ]
63 ]
64 qed-.
65
66 lemma bdd_inv_in_comp_d:
67       βˆ€t,q,n. t Ο΅ πƒπ›— β†’ π—±nβ——q Ο΅ t β†’
68       βˆ¨βˆ¨ βˆ§βˆ§ #n β‡” t & πž = q
69        | βˆƒβˆƒu. u Ο΅ πƒπ›— & q Ο΅ Ι±.u & π›—n.u β‡” t
70 .
71 #t #q #n #Ht #Hq
72 elim (bdd_inv_in_comp_gen β€¦ Ht Hq) -Ht -Hq *
73 [ #n0 #H1 #H2 destruct /3 width=1 by or_introl, conj/
74 | #u0 #q0 #n0 #Hu0 #Hq0 #H1 #H2 destruct
75  /4 width=4 by ex3_intro, ex2_intro, or_intror/
76 | #u0 #q0 #_ #_ #_ #H0 destruct
77 | #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
78 | #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
79 ]
80 qed-.
81
82 lemma bdd_inv_in_root_d:
83       βˆ€t,q,n. t Ο΅ πƒπ›— β†’ π—±nβ——q Ο΅ β–΅t β†’
84       βˆ¨βˆ¨ βˆ§βˆ§ #n β‡” t & πž = q
85        | βˆƒβˆƒu. u Ο΅ πƒπ›— & q Ο΅ β–΅Ι±.u & π›—n.u β‡” t
86 .
87 #t #q #n #Ht * #r #Hq
88 elim (bdd_inv_in_comp_d β€¦ Ht Hq) -Ht -Hq *
89 [ #H1 #H2
90   elim (eq_inv_list_empty_append β€¦ H2) -H2 #H2 #_ destruct
91   /3 width=1 by or_introl, conj/
92 | #u #Hu #Hq #H0 destruct
93   /4 width=4 by ex3_intro, ex_intro, or_intror/
94 ]
95 qed-.
96
97 lemma bdd_inv_in_comp_L:
98       βˆ€t,q. t Ο΅ πƒπ›— β†’ π—Ÿβ——q Ο΅ t β†’
99       βˆƒβˆƒu. u Ο΅ πƒπ›— & q Ο΅ u & π›Œ.u β‡” t
100 .
101 #t #q #Ht #Hq
102 elim (bdd_inv_in_comp_gen β€¦ Ht Hq) -Ht -Hq *
103 [ #n0 #_ #H0 destruct
104 | #u0 #q0 #n0 #_ #_ #_ #H0 destruct
105 | #u0 #q0 #Hu0 #Hq0 #H1 #H2 destruct /2 width=4 by ex3_intro/
106 | #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
107 | #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
108 ]
109 qed-.
110
111 lemma bdd_inv_in_root_L:
112       βˆ€t,q. t Ο΅ πƒπ›— β†’ π—Ÿβ——q Ο΅ β–΅t β†’
113       βˆƒβˆƒu. u Ο΅ πƒπ›— & q Ο΅ β–΅u & π›Œ.u β‡” t.
114 #t #q #Ht * #r #Hq
115 elim (bdd_inv_in_comp_L β€¦ Ht Hq) -Ht -Hq
116 #u #Hu #Hq #H0 destruct
117 /3 width=4 by ex3_intro, ex_intro/
118 qed-.
119
120 lemma bdd_inv_in_comp_A:
121       βˆ€t,q. t Ο΅ πƒπ›— β†’ π—”β——q Ο΅ t β†’
122       βˆƒβˆƒv,u. v Ο΅ πƒπ›— & u Ο΅ πƒπ›— & q Ο΅ u & @v.u β‡” t
123 .
124 #t #q #Ht #Hq
125 elim (bdd_inv_in_comp_gen β€¦ Ht Hq) -Ht -Hq *
126 [ #n0 #_ #H0 destruct
127 | #u0 #q0 #n0 #_ #_ #_ #H0 destruct
128 | #u0 #q0 #_ #_ #_ #H0 destruct
129 | #v0 #u0 #q0 #Hv0 #Hu0 #Hq0 #H1 #H2 destruct /2 width=6 by ex4_2_intro/
130 | #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
131 ]
132 qed-.
133
134 lemma bdd_inv_in_root_A:
135       βˆ€t,q. t Ο΅ πƒπ›— β†’ π—”β——q Ο΅ β–΅t β†’
136       βˆƒβˆƒv,u. v Ο΅ πƒπ›— & u Ο΅ πƒπ›— & q Ο΅ β–΅u & @v.u β‡” t
137 .
138 #t #q #Ht * #r #Hq
139 elim (bdd_inv_in_comp_A β€¦ Ht Hq) -Ht -Hq
140 #v #u #Hv #Hu #Hq #H0 destruct
141 /3 width=6 by ex4_2_intro, ex_intro/
142 qed-.
143
144 lemma bdd_inv_in_comp_S:
145       βˆ€t,q. t Ο΅ πƒπ›— β†’ π—¦β——q Ο΅ t β†’
146       βˆƒβˆƒv,u. v Ο΅ πƒπ›— & u Ο΅ πƒπ›— & q Ο΅ v & @v.u β‡” t
147 .
148 #t #q #Ht #Hq
149 elim (bdd_inv_in_comp_gen β€¦ Ht Hq) -Ht -Hq *
150 [ #n0 #_ #H0 destruct
151 | #u0 #q0 #n0 #_ #_ #_ #H0 destruct
152 | #u0 #q0 #_ #_ #_ #H0 destruct
153 | #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
154 | #v0 #u0 #q0 #Hv0 #Hu0 #Hq0 #H1 #H2 destruct /2 width=6 by ex4_2_intro/
155 ]
156 qed-.
157
158 lemma bdd_inv_in_root_S:
159       βˆ€t,q. t Ο΅ πƒπ›— β†’ π—¦β——q Ο΅ β–΅t β†’
160       βˆƒβˆƒv,u. v Ο΅ πƒπ›— & u Ο΅ πƒπ›— & q Ο΅ β–΅v & @v.u β‡” t
161 .
162 #t #q #Ht * #r #Hq
163 elim (bdd_inv_in_comp_S β€¦ Ht Hq) -Ht -Hq
164 #v #u #Hv #Hu #Hq #H0 destruct
165 /3 width=6 by ex4_2_intro, ex_intro/
166 qed-.
167
168 (* Advanced inversions ******************************************************)
169
170 lemma bbd_mono_in_root_d:
171       βˆ€l,n,p,t. t Ο΅ πƒπ›— β†’ p◖𝗱n Ο΅ β–΅t β†’ pβ—–l Ο΅ β–΅t β†’ π—±n = l.
172 #l #n #p elim p -p
173 [ #t #Ht <list_cons_comm <list_cons_comm #Hn #Hl
174   elim (bdd_inv_in_root_d β€¦ Ht Hn) -Ht -Hn *
175   [ #H0 #_
176     lapply (prototerm_root_eq_repl β€¦ H0) -H0 #H0
177     lapply (subset_in_eq_repl_fwd ?? β€¦ Hl β€¦ H0) -H0 -Hl #Hl
178     elim (prototerm_in_root_inv_lcons_oref β€¦ Hl) -Hl //
179   | #u #_ #_ #H0
180     lapply (prototerm_root_eq_repl β€¦ H0) -H0 #H0
181     lapply (subset_in_eq_repl_fwd ?? β€¦ Hl β€¦ H0) -H0 -Hl #Hl
182     elim (prototerm_in_root_inv_lcons_iref β€¦ Hl) -Hl //
183   ]
184 | * [ #m ] #p #IH #t #Ht
185   <list_cons_shift <list_cons_shift #Hn #Hl
186   [ elim (bdd_inv_in_root_d β€¦ Ht Hn) -Ht -Hn *
187     [ #_ #H0
188       elim (eq_inv_list_empty_rcons ??? H0)
189     | #u #Hu #Hp #H0
190       lapply (prototerm_root_eq_repl β€¦ H0) -H0 #H0
191       lapply (subset_in_eq_repl_fwd ?? β€¦ Hl β€¦ H0) -H0 -Hl #Hl
192       elim (prototerm_in_root_inv_lcons_iref β€¦ Hl) -Hl #_ #Hl
193       /2 width=4 by/
194     ]
195   | elim (bdd_inv_in_root_L β€¦ Ht Hn) -Ht -Hn
196     #u #Hu #Hp #H0
197     lapply (prototerm_root_eq_repl β€¦ H0) -H0 #H0
198     lapply (subset_in_eq_repl_fwd ?? β€¦ Hl β€¦ H0) -H0 -Hl #Hl  
199     elim (prototerm_in_root_inv_lcons_abst β€¦ Hl) -Hl #_ #Hl
200     /2 width=4 by/
201   | elim (bdd_inv_in_root_A β€¦ Ht Hn) -Ht -Hn
202     #v #u #_ #Hu #Hp #H0
203     lapply (prototerm_root_eq_repl β€¦ H0) -H0 #H0
204     lapply (subset_in_eq_repl_fwd ?? β€¦ Hl β€¦ H0) -H0 -Hl #Hl
205     elim (prototerm_in_root_inv_lcons_appl β€¦ Hl) -Hl * #H0 #Hl destruct
206     /2 width=4 by/
207   | elim (bdd_inv_in_root_S β€¦ Ht Hn) -Ht -Hn
208     #v #u #Hv #_ #Hp #H0
209     lapply (prototerm_root_eq_repl β€¦ H0) -H0 #H0
210     lapply (subset_in_eq_repl_fwd ?? β€¦ Hl β€¦ H0) -H0 -Hl #Hl
211     elim (prototerm_in_root_inv_lcons_appl β€¦ Hl) -Hl * #H0 #Hl destruct
212     /2 width=4 by/
213   ]
214 ]
215 qed-.
216 *)