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/and_4.ma".
16 include "ground/xoa/ex_4_2.ma".
17 include "ground/xoa/or_4.ma".
18 include "static_2/notation/relations/supterm_6.ma".
19 include "static_2/notation/relations/supterm_7.ma".
20 include "static_2/syntax/lenv.ma".
21 include "static_2/syntax/genv.ma".
22 include "static_2/relocation/lifts.ma".
24 (* SUPCLOSURE ***************************************************************)
27 (* Note: frees_total requires fqu_drop for all atoms
28 fqu_cpx_trans requires fqu_drop for all terms
29 frees_fqus_drops requires fqu_drop restricted on atoms
31 inductive fqu (b:bool): tri_relation genv lenv term ≝
32 | fqu_lref_O : ∀I,G,L,V. fqu b G (L.ⓑ[I]V) (#0) G L V
33 | fqu_pair_sn: ∀I,G,L,V,T. fqu b G L (②[I]V.T) G L V
34 | fqu_bind_dx: ∀p,I,G,L,V,T. b = Ⓣ → fqu b G L (ⓑ[p,I]V.T) G (L.ⓑ[I]V) T
35 | fqu_clear : ∀p,I,G,L,V,T. b = Ⓕ → fqu b G L (ⓑ[p,I]V.T) G (L.ⓧ) T
36 | fqu_flat_dx: ∀I,G,L,V,T. fqu b G L (ⓕ[I]V.T) G L T
37 | fqu_drop : ∀I,G,L,T,U. ⇧[1] T ≘ U → fqu b G (L.ⓘ[I]) U G L T
41 "extended structural successor (closure)"
42 'SupTerm b G1 L1 T1 G2 L2 T2 = (fqu b G1 L1 T1 G2 L2 T2).
45 "structural successor (closure)"
46 'SupTerm G1 L1 T1 G2 L2 T2 = (fqu true G1 L1 T1 G2 L2 T2).
48 (* Basic properties *********************************************************)
50 lemma fqu_sort: ∀b,I,G,L,s. ❨G,L.ⓘ[I],⋆s❩ ⬂[b] ❨G,L,⋆s❩.
51 /2 width=1 by fqu_drop/ qed.
53 lemma fqu_lref_S: ∀b,I,G,L,i. ❨G,L.ⓘ[I],#↑i❩ ⬂[b] ❨G,L,#i❩.
54 /2 width=1 by fqu_drop/ qed.
56 lemma fqu_gref: ∀b,I,G,L,l. ❨G,L.ⓘ[I],§l❩ ⬂[b] ❨G,L,§l❩.
57 /2 width=1 by fqu_drop/ qed.
59 (* Basic inversion lemmas ***************************************************)
61 fact fqu_inv_sort1_aux: ∀b,G1,G2,L1,L2,T1,T2. ❨G1,L1,T1❩ ⬂[b] ❨G2,L2,T2❩ →
63 ∃∃J. G1 = G2 & L1 = L2.ⓘ[J] & T2 = ⋆s.
64 #b #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
65 [ #I #G #L #T #s #H destruct
66 | #I #G #L #V #T #s #H destruct
67 | #p #I #G #L #V #T #_ #s #H destruct
68 | #p #I #G #L #V #T #_ #s #H destruct
69 | #I #G #L #V #T #s #H destruct
70 | #I #G #L #T #U #HI12 #s #H destruct
71 lapply (lifts_inv_sort2 … HI12) -HI12 /2 width=2 by ex3_intro/
75 lemma fqu_inv_sort1: ∀b,G1,G2,L1,L2,T2,s. ❨G1,L1,⋆s❩ ⬂[b] ❨G2,L2,T2❩ →
76 ∃∃J. G1 = G2 & L1 = L2.ⓘ[J] & T2 = ⋆s.
77 /2 width=4 by fqu_inv_sort1_aux/ qed-.
79 fact fqu_inv_lref1_aux: ∀b,G1,G2,L1,L2,T1,T2. ❨G1,L1,T1❩ ⬂[b] ❨G2,L2,T2❩ →
81 (∃∃J,V. G1 = G2 & L1 = L2.ⓑ[J]V & T2 = V & i = 0) ∨
82 ∃∃J,j. G1 = G2 & L1 = L2.ⓘ[J] & T2 = #j & i = ↑j.
83 #b #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
84 [ #I #G #L #T #i #H destruct /3 width=4 by ex4_2_intro, or_introl/
85 | #I #G #L #V #T #i #H destruct
86 | #p #I #G #L #V #T #_ #i #H destruct
87 | #p #I #G #L #V #T #_ #i #H destruct
88 | #I #G #L #V #T #i #H destruct
89 | #I #G #L #T #U #HI12 #i #H destruct
90 elim (lifts_inv_lref2_uni … HI12) -HI12 /3 width=3 by ex4_2_intro, or_intror/
94 lemma fqu_inv_lref1: ∀b,G1,G2,L1,L2,T2,i. ❨G1,L1,#i❩ ⬂[b] ❨G2,L2,T2❩ →
95 (∃∃J,V. G1 = G2 & L1 = L2.ⓑ[J]V & T2 = V & i = 0) ∨
96 ∃∃J,j. G1 = G2 & L1 = L2.ⓘ[J] & T2 = #j & i = ↑j.
97 /2 width=4 by fqu_inv_lref1_aux/ qed-.
99 fact fqu_inv_gref1_aux: ∀b,G1,G2,L1,L2,T1,T2. ❨G1,L1,T1❩ ⬂[b] ❨G2,L2,T2❩ →
101 ∃∃J. G1 = G2 & L1 = L2.ⓘ[J] & T2 = §l.
102 #b #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
103 [ #I #G #L #T #l #H destruct
104 | #I #G #L #V #T #l #H destruct
105 | #p #I #G #L #V #T #_ #l #H destruct
106 | #p #I #G #L #V #T #_ #l #H destruct
107 | #I #G #L #V #T #s #H destruct
108 | #I #G #L #T #U #HI12 #l #H destruct
109 lapply (lifts_inv_gref2 … HI12) -HI12 /2 width=3 by ex3_intro/
113 lemma fqu_inv_gref1: ∀b,G1,G2,L1,L2,T2,l. ❨G1,L1,§l❩ ⬂[b] ❨G2,L2,T2❩ →
114 ∃∃J. G1 = G2 & L1 = L2.ⓘ[J] & T2 = §l.
115 /2 width=4 by fqu_inv_gref1_aux/ qed-.
117 fact fqu_inv_bind1_aux: ∀b,G1,G2,L1,L2,T1,T2. ❨G1,L1,T1❩ ⬂[b] ❨G2,L2,T2❩ →
118 ∀p,I,V1,U1. T1 = ⓑ[p,I]V1.U1 →
119 ∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2
120 | ∧∧ G1 = G2 & L1.ⓑ[I]V1 = L2 & U1 = T2 & b = Ⓣ
121 | ∧∧ G1 = G2 & L1.ⓧ = L2 & U1 = T2 & b = Ⓕ
122 | ∃∃J. G1 = G2 & L1 = L2.ⓘ[J] & ⇧[1] T2 ≘ ⓑ[p,I]V1.U1.
123 #b #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
124 [ #I #G #L #T #q #J #V0 #U0 #H destruct
125 | #I #G #L #V #T #q #J #V0 #U0 #H destruct /3 width=1 by and3_intro, or4_intro0/
126 | #p #I #G #L #V #T #Hb #q #J #V0 #U0 #H destruct /3 width=1 by and4_intro, or4_intro1/
127 | #p #I #G #L #V #T #Hb #q #J #V0 #U0 #H destruct /3 width=1 by and4_intro, or4_intro2/
128 | #I #G #L #V #T #q #J #V0 #U0 #H destruct
129 | #I #G #L #T #U #HTU #q #J #V0 #U0 #H destruct /3 width=2 by or4_intro3, ex3_intro/
133 lemma fqu_inv_bind1: ∀b,p,I,G1,G2,L1,L2,V1,U1,T2. ❨G1,L1,ⓑ[p,I]V1.U1❩ ⬂[b] ❨G2,L2,T2❩ →
134 ∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2
135 | ∧∧ G1 = G2 & L1.ⓑ[I]V1 = L2 & U1 = T2 & b = Ⓣ
136 | ∧∧ G1 = G2 & L1.ⓧ = L2 & U1 = T2 & b = Ⓕ
137 | ∃∃J. G1 = G2 & L1 = L2.ⓘ[J] & ⇧[1] T2 ≘ ⓑ[p,I]V1.U1.
138 /2 width=4 by fqu_inv_bind1_aux/ qed-.
140 lemma fqu_inv_bind1_true: ∀p,I,G1,G2,L1,L2,V1,U1,T2. ❨G1,L1,ⓑ[p,I]V1.U1❩ ⬂ ❨G2,L2,T2❩ →
141 ∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2
142 | ∧∧ G1 = G2 & L1.ⓑ[I]V1 = L2 & U1 = T2
143 | ∃∃J. G1 = G2 & L1 = L2.ⓘ[J] & ⇧[1] T2 ≘ ⓑ[p,I]V1.U1.
144 #p #I #G1 #G2 #L1 #L2 #V1 #U1 #T2 #H elim (fqu_inv_bind1 … H) -H
145 /3 width=1 by or3_intro0, or3_intro2/
146 * #HG #HL #HU #H destruct
147 /3 width=1 by and3_intro, or3_intro1/
150 fact fqu_inv_flat1_aux: ∀b,G1,G2,L1,L2,T1,T2. ❨G1,L1,T1❩ ⬂[b] ❨G2,L2,T2❩ →
151 ∀I,V1,U1. T1 = ⓕ[I]V1.U1 →
152 ∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2
153 | ∧∧ G1 = G2 & L1 = L2 & U1 = T2
154 | ∃∃J. G1 = G2 & L1 = L2.ⓘ[J] & ⇧[1] T2 ≘ ⓕ[I]V1.U1.
155 #b #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
156 [ #I #G #L #T #J #V0 #U0 #H destruct
157 | #I #G #L #V #T #J #V0 #U0 #H destruct /3 width=1 by and3_intro, or3_intro0/
158 | #p #I #G #L #V #T #_ #J #V0 #U0 #H destruct
159 | #p #I #G #L #V #T #_ #J #V0 #U0 #H destruct
160 | #I #G #L #V #T #J #V0 #U0 #H destruct /3 width=1 by and3_intro, or3_intro1/
161 | #I #G #L #T #U #HTU #J #V0 #U0 #H destruct /3 width=2 by or3_intro2, ex3_intro/
165 lemma fqu_inv_flat1: ∀b,I,G1,G2,L1,L2,V1,U1,T2. ❨G1,L1,ⓕ[I]V1.U1❩ ⬂[b] ❨G2,L2,T2❩ →
166 ∨∨ ∧∧ G1 = G2 & L1 = L2 & V1 = T2
167 | ∧∧ G1 = G2 & L1 = L2 & U1 = T2
168 | ∃∃J. G1 = G2 & L1 = L2.ⓘ[J] & ⇧[1] T2 ≘ ⓕ[I]V1.U1.
169 /2 width=4 by fqu_inv_flat1_aux/ qed-.
171 (* Advanced inversion lemmas ************************************************)
173 lemma fqu_inv_atom1: ∀b,I,G1,G2,L2,T2. ❨G1,⋆,⓪[I]❩ ⬂[b] ❨G2,L2,T2❩ → ⊥.
174 #b * #x #G1 #G2 #L2 #T2 #H
175 [ elim (fqu_inv_sort1 … H) | elim (fqu_inv_lref1 … H) * | elim (fqu_inv_gref1 … H) ] -H
176 #I [2: #V |3: #i ] #_ #H destruct
179 lemma fqu_inv_sort1_bind: ∀b,I,G1,G2,K,L2,T2,s. ❨G1,K.ⓘ[I],⋆s❩ ⬂[b] ❨G2,L2,T2❩ →
180 ∧∧ G1 = G2 & L2 = K & T2 = ⋆s.
181 #b #I #G1 #G2 #K #L2 #T2 #s #H elim (fqu_inv_sort1 … H) -H
182 #Z #X #H1 #H2 destruct /2 width=1 by and3_intro/
185 lemma fqu_inv_zero1_pair: ∀b,I,G1,G2,K,L2,V,T2. ❨G1,K.ⓑ[I]V,#0❩ ⬂[b] ❨G2,L2,T2❩ →
186 ∧∧ G1 = G2 & L2 = K & T2 = V.
187 #b #I #G1 #G2 #K #L2 #V #T2 #H elim (fqu_inv_lref1 … H) -H *
188 #Z #X #H1 #H2 #H3 #H4 destruct /2 width=1 by and3_intro/
191 lemma fqu_inv_lref1_bind: ∀b,I,G1,G2,K,L2,T2,i. ❨G1,K.ⓘ[I],#(↑i)❩ ⬂[b] ❨G2,L2,T2❩ →
192 ∧∧ G1 = G2 & L2 = K & T2 = #i.
193 #b #I #G1 #G2 #K #L2 #T2 #i #H elim (fqu_inv_lref1 … H) -H *
194 #Z #X #H1 #H2 #H3 #H4 destruct /2 width=1 by and3_intro/
197 lemma fqu_inv_gref1_bind: ∀b,I,G1,G2,K,L2,T2,l. ❨G1,K.ⓘ[I],§l❩ ⬂[b] ❨G2,L2,T2❩ →
198 ∧∧ G1 = G2 & L2 = K & T2 = §l.
199 #b #I #G1 #G2 #K #L2 #T2 #l #H elim (fqu_inv_gref1 … H) -H
200 #Z #H1 #H2 #H3 destruct /2 width=1 by and3_intro/
203 (* Basic_2A1: removed theorems 3:
204 fqu_drop fqu_drop_lt fqu_lref_S_lt