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 "basic_2/notation/relations/supterm_6.ma".
16 include "basic_2/grammar/lenv.ma".
17 include "basic_2/grammar/genv.ma".
18 include "basic_2/relocation/lifts.ma".
20 (* SUPCLOSURE ***************************************************************)
23 (* Note: frees_total requires fqu_drop for all atoms *)
24 inductive fqu: tri_relation genv lenv term ≝
25 | fqu_lref_O : ∀I,G,L,V. fqu G (L.ⓑ{I}V) (#0) G L V
26 | fqu_pair_sn: ∀I,G,L,V,T. fqu G L (②{I}V.T) G L V
27 | fqu_bind_dx: ∀p,I,G,L,V,T. fqu G L (ⓑ{p,I}V.T) G (L.ⓑ{I}V) T
28 | fqu_flat_dx: ∀I,G,L,V,T. fqu G L (ⓕ{I}V.T) G L T
29 | fqu_drop : ∀I,I1,I2,G,L,V. ⬆*[1] ⓪{I2} ≡ ⓪{I1} →
30 fqu G (L.ⓑ{I}V) (⓪{I1}) G L (⓪{I2})
34 "structural successor (closure)"
35 'SupTerm G1 L1 T1 G2 L2 T2 = (fqu G1 L1 T1 G2 L2 T2).
37 (* Basic properties *********************************************************)
39 lemma fqu_lref_S: ∀I,G,L,V,i. ⦃G, L.ⓑ{I}V, #(⫯i)⦄ ⊐ ⦃G, L, #(i)⦄.
40 /2 width=1 by fqu_drop/ qed.
42 (* Basic inversion lemmas ***************************************************)
44 fact fqu_inv_atom1_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
45 ∀I. L1 = ⋆ → T1 = ⓪{I} → ⊥.
46 #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
47 [ #I #G #L #T #J #H destruct
48 | #I #G #L #V #T #J #_ #H destruct
49 | #p #I #G #L #V #T #J #_ #H destruct
50 | #I #G #L #V #T #J #_ #H destruct
51 | #I #I1 #I2 #G #L #V #_ #J #H destruct
55 lemma fqu_inv_atom1: ∀I,G1,G2,L2,T2. ⦃G1, ⋆, ⓪{I}⦄ ⊐ ⦃G2, L2, T2⦄ → ⊥.
56 /2 width=10 by fqu_inv_atom1_aux/ qed-.
58 fact fqu_inv_sort1_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
59 ∀I,K,V,s. L1 = K.ⓑ{I}V → T1 = ⋆s →
60 ∧∧ G1 = G2 & L2 = K & T2 = ⋆s.
61 #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
62 [ #I #G #L #T #J #K #W #s #_ #H destruct
63 | #I #G #L #V #T #J #K #W #s #_ #H destruct
64 | #p #I #G #L #V #T #J #K #W #s #_ #H destruct
65 | #I #G #L #V #T #J #K #W #s #_ #H destruct
66 | #I #I1 #I2 #G #L #V #HI12 #J #K #W #s #H1 #H2 destruct
67 lapply (lifts_inv_sort2 … HI12) -HI12 /2 width=1 by and3_intro/
71 lemma fqu_inv_sort1: ∀I,G1,G2,K,L2,V,T2,s. ⦃G1, K.ⓑ{I}V, ⋆s⦄ ⊐ ⦃G2, L2, T2⦄ →
72 ∧∧ G1 = G2 & L2 = K & T2 = ⋆s.
73 /2 width=7 by fqu_inv_sort1_aux/ qed-.
75 fact fqu_inv_zero1_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
76 ∀I,K,V. L1 = K.ⓑ{I}V → T1 = #0 →
77 ∧∧ G1 = G2 & L2 = K & T2 = V.
78 #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
79 [ #I #G #L #T #J #K #W #H1 #H2 destruct /2 width=1 by and3_intro/
80 | #I #G #L #V #T #J #K #W #_ #H destruct
81 | #p #I #G #L #V #T #J #K #W #_ #H destruct
82 | #I #G #L #V #T #J #K #W #_ #H destruct
83 | #I #I1 #I2 #G #L #V #HI12 #J #K #W #H1 #H2 destruct
84 elim (lifts_inv_lref2_uni_lt … HI12) -HI12 //
88 lemma fqu_inv_zero1: ∀I,G1,G2,K,L2,V,T2. ⦃G1, K.ⓑ{I}V, #0⦄ ⊐ ⦃G2, L2, T2⦄ →
89 ∧∧ G1 = G2 & L2 = K & T2 = V.
90 /2 width=9 by fqu_inv_zero1_aux/ qed-.
92 fact fqu_inv_lref1_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
93 ∀I,K,V,i. L1 = K.ⓑ{I}V → T1 = #(⫯i) →
94 ∧∧ G1 = G2 & L2 = K & T2 = #i.
95 #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
96 [ #I #G #L #T #J #K #W #i #_ #H destruct
97 | #I #G #L #V #T #J #K #W #i #_ #H destruct
98 | #p #I #G #L #V #T #J #K #W #i #_ #H destruct
99 | #I #G #L #V #T #J #K #W #i #_ #H destruct
100 | #I #I1 #I2 #G #L #V #HI12 #J #K #W #i #H1 #H2 destruct
101 lapply (lifts_inv_lref2_uni_ge … HI12) -HI12 /2 width=1 by and3_intro/
105 lemma fqu_inv_lref1: ∀I,G1,G2,K,L2,V,T2,i. ⦃G1, K.ⓑ{I}V, #(⫯i)⦄ ⊐ ⦃G2, L2, T2⦄ →
106 ∧∧ G1 = G2 & L2 = K & T2 = #i.
107 /2 width=9 by fqu_inv_lref1_aux/ qed-.
109 fact fqu_inv_gref1_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
110 ∀I,K,V,l. L1 = K.ⓑ{I}V → T1 = §l →
111 ∧∧ G1 = G2 & L2 = K & T2 = §l.
112 #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
113 [ #I #G #L #T #J #K #W #l #_ #H destruct
114 | #I #G #L #V #T #J #K #W #l #_ #H destruct
115 | #p #I #G #L #V #T #J #K #W #l #_ #H destruct
116 | #I #G #L #V #T #J #K #W #l #_ #H destruct
117 | #I #I1 #I2 #G #L #V #HI12 #J #K #W #l #H1 #H2 destruct
118 lapply (lifts_inv_gref2 … HI12) -HI12 /2 width=1 by and3_intro/
122 lemma fqu_inv_gref1: ∀I,G1,G2,K,L2,V,T2,l. ⦃G1, K.ⓑ{I}V, §l⦄ ⊐ ⦃G2, L2, T2⦄ →
123 ∧∧ G1 = G2 & L2 = K & T2 = §l.
124 /2 width=7 by fqu_inv_gref1_aux/ qed-.
126 fact fqu_inv_bind1_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
127 ∀p,I,V1,U1. T1 = ⓑ{p,I}V1.U1 →
128 (∧∧ G1 = G2 & L1 = L2 & V1 = T2) ∨
129 (∧∧ G1 = G2 & L1.ⓑ{I}V1 = L2 & U1 = T2).
130 #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
131 [ #I #G #L #T #q #J #W #U #H destruct
132 | #I #G #L #V #T #q #J #W #U #H destruct /3 width=1 by and3_intro, or_introl/
133 | #p #I #G #L #V #T #q #J #W #U #H destruct /3 width=1 by and3_intro, or_intror/
134 | #I #G #L #V #T #q #J #W #U #H destruct
135 | #I #I1 #I2 #G #L #V #_ #q #J #W #U #H destruct
139 lemma fqu_inv_bind1: ∀p,I,G1,G2,L1,L2,V1,U1,T2. ⦃G1, L1, ⓑ{p,I}V1.U1⦄ ⊐ ⦃G2, L2, T2⦄ →
140 (∧∧ G1 = G2 & L1 = L2 & V1 = T2) ∨
141 (∧∧ G1 = G2 & L1.ⓑ{I}V1 = L2 & U1 = T2).
142 /2 width=4 by fqu_inv_bind1_aux/ qed-.
144 fact fqu_inv_flat1_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
145 ∀I,V1,U1. T1 = ⓕ{I}V1.U1 →
146 (∧∧ G1 = G2 & L1 = L2 & V1 = T2) ∨
147 (∧∧ G1 = G2 & L1 = L2 & U1 = T2).
148 #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
149 [ #I #G #L #T #J #W #U #H destruct
150 | #I #G #L #V #T #J #W #U #H destruct /3 width=1 by and3_intro, or_introl/
151 | #p #I #G #L #V #T #J #W #U #H destruct
152 | #I #G #L #V #T #J #W #U #H destruct /3 width=1 by and3_intro, or_intror/
153 | #I #I1 #I2 #G #L #V #_ #J #W #U #H destruct
157 lemma fqu_inv_flat1: ∀I,G1,G2,L1,L2,V1,U1,T2. ⦃G1, L1, ⓕ{I}V1.U1⦄ ⊐ ⦃G2, L2, T2⦄ →
158 (∧∧ G1 = G2 & L1 = L2 & V1 = T2) ∨
159 (∧∧ G1 = G2 & L1 = L2 & U1 = T2).
160 /2 width=4 by fqu_inv_flat1_aux/ qed-.
162 (* Basic_2A1: removed theorems 3:
163 fqu_drop fqu_drop_lt fqu_lref_S_lt