1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "ground/xoa/or_5.ma".
16 include "ground/xoa/ex_3_1.ma".
17 include "ground/xoa/ex_4_2.ma".
18 include "ground/xoa/ex_4_3.ma".
19 include "ground/xoa/ex_5_3.ma".
20 include "delayed_updating/syntax/preterm_equivalence.ma".
21 include "delayed_updating/syntax/preterm_constructors.ma".
22 include "delayed_updating/notation/functions/class_d_phi_0.ma".
24 (* BY-DEPTH DELAYED (BDD) TERM **********************************************)
26 inductive bdd: π«β¨pretermβ© β
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
35 "by-depth delayed (preterm)"
38 (* Basic inversions *********************************************************)
40 lemma bdd_inv_in_comp_gen:
41 βt,p. t Ο΅ ππ β p Ο΅ t β
42 β¨β¨ ββn. #n β t & π±nβπ = p
43 | ββu,q,n. u Ο΅ ππ & q Ο΅ u & πn.u β t & π±nβq = p
44 | ββu,q. u Ο΅ ππ & q Ο΅ u & π.u β t & πβq = p
45 | ββv,u,q. v Ο΅ ππ & u Ο΅ ππ & q Ο΅ u & @v.u β t & πβq = p
46 | ββv,u,q. v Ο΅ ππ & u Ο΅ ππ & q Ο΅ v & @v.u β t & π¦βq = p
49 [ #n * /3 width=3 by or5_intro0, ex2_intro/
50 | #u #n #Hu #_ * #q #Hq #Hp /3 width=7 by ex4_3_intro, or5_intro1/
51 | #u #Hu #_ * #q #Hq #Hp /3 width=6 by or5_intro2, ex4_2_intro/
52 | #v #u #Hv #Hu #_ #_ * * #q #Hq #Hp /3 width=8 by ex5_3_intro, or5_intro3, or5_intro4/
53 | #t1 #t2 #Ht12 #_ #IH #Ht2
54 elim IH -IH [6: /2 width=3 by subset_in_eq_repl_fwd/ ] *
55 [ /4 width=3 by subset_eq_trans, or5_intro0, ex2_intro/
56 | /4 width=7 by subset_eq_trans, ex4_3_intro, or5_intro1/
57 | /4 width=6 by subset_eq_trans, or5_intro2, ex4_2_intro/
58 | /4 width=8 by subset_eq_trans, ex5_3_intro, or5_intro3/
59 | /4 width=8 by subset_eq_trans, ex5_3_intro, or5_intro4/
64 lemma bdd_inv_in_comp_d:
65 βt,q,n. t Ο΅ ππ β π±nβq Ο΅ t β
66 β¨β¨ β§β§ #n β t & π = q
67 | ββu. u Ο΅ ππ & q Ο΅ u & πn.u β t
70 elim (bdd_inv_in_comp_gen β¦ Ht Hq) -Ht -Hq *
71 [ #n0 #H1 #H2 destruct /3 width=1 by or_introl, conj/
72 | #u0 #q0 #n0 #Hu0 #Hq0 #H1 #H2 destruct /3 width=4 by ex3_intro, or_intror/
73 | #u0 #q0 #_ #_ #_ #H0 destruct
74 | #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
75 | #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
79 lemma bdd_inv_in_root_d:
80 βt,q,n. t Ο΅ ππ β π±nβq Ο΅ β΅t β
81 β¨β¨ β§β§ #n β t & π = q
82 | ββu. u Ο΅ ππ & q Ο΅ β΅u & πn.u β t
85 elim (bdd_inv_in_comp_d β¦ Ht Hq) -Ht -Hq *
87 elim (eq_inv_list_empty_append β¦ H2) -H2 #H2 #_ destruct
88 /3 width=1 by or_introl, conj/
89 | #u #Hu #Hq #H0 destruct
90 /4 width=4 by ex3_intro, ex_intro, or_intror/
94 lemma bdd_inv_in_comp_L:
95 βt,q. t Ο΅ ππ β πβq Ο΅ t β
96 ββu. u Ο΅ ππ & q Ο΅ u & π.u β t
99 elim (bdd_inv_in_comp_gen β¦ Ht Hq) -Ht -Hq *
100 [ #n0 #_ #H0 destruct
101 | #u0 #q0 #n0 #_ #_ #_ #H0 destruct
102 | #u0 #q0 #Hu0 #Hq0 #H1 #H2 destruct /2 width=4 by ex3_intro/
103 | #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
104 | #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
108 lemma bdd_inv_in_root_L:
109 βt,q. t Ο΅ ππ β πβq Ο΅ β΅t β
110 ββu. u Ο΅ ππ & q Ο΅ β΅u & π.u β t.
112 elim (bdd_inv_in_comp_L β¦ Ht Hq) -Ht -Hq
113 #u #Hu #Hq #H0 destruct
114 /3 width=4 by ex3_intro, ex_intro/
117 lemma bdd_inv_in_comp_A:
118 βt,q. t Ο΅ ππ β πβq Ο΅ t β
119 ββv,u. v Ο΅ ππ & u Ο΅ ππ & q Ο΅ u & @v.u β t
122 elim (bdd_inv_in_comp_gen β¦ Ht Hq) -Ht -Hq *
123 [ #n0 #_ #H0 destruct
124 | #u0 #q0 #n0 #_ #_ #_ #H0 destruct
125 | #u0 #q0 #_ #_ #_ #H0 destruct
126 | #v0 #u0 #q0 #Hv0 #Hu0 #Hq0 #H1 #H2 destruct /2 width=6 by ex4_2_intro/
127 | #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
131 lemma bdd_inv_in_root_A:
132 βt,q. t Ο΅ ππ β πβq Ο΅ β΅t β
133 ββv,u. v Ο΅ ππ & u Ο΅ ππ & q Ο΅ β΅u & @v.u β t
136 elim (bdd_inv_in_comp_A β¦ Ht Hq) -Ht -Hq
137 #v #u #Hv #Hu #Hq #H0 destruct
138 /3 width=6 by ex4_2_intro, ex_intro/
141 lemma bdd_inv_in_comp_S:
142 βt,q. t Ο΅ ππ β π¦βq Ο΅ t β
143 ββv,u. v Ο΅ ππ & u Ο΅ ππ & q Ο΅ v & @v.u β t
146 elim (bdd_inv_in_comp_gen β¦ Ht Hq) -Ht -Hq *
147 [ #n0 #_ #H0 destruct
148 | #u0 #q0 #n0 #_ #_ #_ #H0 destruct
149 | #u0 #q0 #_ #_ #_ #H0 destruct
150 | #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
151 | #v0 #u0 #q0 #Hv0 #Hu0 #Hq0 #H1 #H2 destruct /2 width=6 by ex4_2_intro/
155 lemma bdd_inv_in_root_S:
156 βt,q. t Ο΅ ππ β π¦βq Ο΅ β΅t β
157 ββv,u. v Ο΅ ππ & u Ο΅ ππ & q Ο΅ β΅v & @v.u β t
160 elim (bdd_inv_in_comp_S β¦ Ht Hq) -Ht -Hq
161 #v #u #Hv #Hu #Hq #H0 destruct
162 /3 width=6 by ex4_2_intro, ex_intro/
165 (* Advanced inversions ******************************************************)
167 lemma bbd_mono_in_root_d:
168 βl,n,p,t. t Ο΅ ππ β pβπ±n Ο΅ β΅t β pβl Ο΅ β΅t β π±n = l.
170 [ #t #Ht <list_cons_comm <list_cons_comm #Hn #Hl
171 elim (bdd_inv_in_root_d β¦ Ht Hn) -Ht -Hn *
173 lapply (preterm_root_eq_repl β¦ H0) -H0 #H0
174 lapply (subset_in_eq_repl_fwd ?? β¦ Hl β¦ H0) -H0 -Hl #Hl
175 elim (preterm_in_root_inv_lcons_oref β¦ Hl) -Hl //
177 lapply (preterm_root_eq_repl β¦ H0) -H0 #H0
178 lapply (subset_in_eq_repl_fwd ?? β¦ Hl β¦ H0) -H0 -Hl #Hl
179 elim (preterm_in_root_inv_lcons_iref β¦ Hl) -Hl //
181 | * [ #m ] #p #IH #t #Ht
182 <list_cons_shift <list_cons_shift #Hn #Hl
183 [ elim (bdd_inv_in_root_d β¦ Ht Hn) -Ht -Hn *
185 elim (eq_inv_list_empty_rcons ??? H0)
187 lapply (preterm_root_eq_repl β¦ H0) -H0 #H0
188 lapply (subset_in_eq_repl_fwd ?? β¦ Hl β¦ H0) -H0 -Hl #Hl
189 elim (preterm_in_root_inv_lcons_iref β¦ Hl) -Hl #_ #Hl
192 | elim (bdd_inv_in_root_L β¦ Ht Hn) -Ht -Hn
194 lapply (preterm_root_eq_repl β¦ H0) -H0 #H0
195 lapply (subset_in_eq_repl_fwd ?? β¦ Hl β¦ H0) -H0 -Hl #Hl
196 elim (preterm_in_root_inv_lcons_abst β¦ Hl) -Hl #_ #Hl
198 | elim (bdd_inv_in_root_A β¦ Ht Hn) -Ht -Hn
200 lapply (preterm_root_eq_repl β¦ H0) -H0 #H0
201 lapply (subset_in_eq_repl_fwd ?? β¦ Hl β¦ H0) -H0 -Hl #Hl
202 elim (preterm_in_root_inv_lcons_appl β¦ Hl) -Hl * #H0 #Hl destruct
204 | elim (bdd_inv_in_root_S β¦ Ht Hn) -Ht -Hn
206 lapply (preterm_root_eq_repl β¦ H0) -H0 #H0
207 lapply (subset_in_eq_repl_fwd ?? β¦ Hl β¦ H0) -H0 -Hl #Hl
208 elim (preterm_in_root_inv_lcons_appl β¦ Hl) -Hl * #H0 #Hl destruct