Skip to content

Commit 4a95a7b

Browse files
fblanquifblanqui
committed
add skolemization function
1 parent 4b7b21d commit 4a95a7b

File tree

1 file changed

+287
-0
lines changed

1 file changed

+287
-0
lines changed

‎Skolem.lp‎

Lines changed: 287 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,287 @@
1+
require open Stdlib.Prop Stdlib.FOL Stdlib.Epsilon;
2+
3+
// procedure for skolemizing all existentials
4+
// /!\ WARNING: this is a sequential symbol
5+
6+
private sequential symbol skolem: Prop → Prop;
7+
private sequential symbol skolem-: Prop → Prop;
8+
9+
rule skolem (∀ $p) ↪ `∀ x, skolem ($p x)
10+
with skolem (∃ $p) ↪ skolem ($p (ε $p))
11+
with skolem ($p ∧ $q) ↪ skolem $p ∧ skolem $q
12+
with skolem ($p ∨ $q) ↪ skolem $p ∨ skolem $q
13+
with skolem ($p ⇒ $q) ↪ skolem- $p ⇒ skolem $q
14+
with skolem $p ↪ $p
15+
16+
with skolem- (∀ $p) ↪ skolem- ($p (ε $p))
17+
with skolem- (∃ $p) ↪ `∃ x, skolem- ($p x)
18+
with skolem- ($p ∧ $q) ↪ skolem- $p ∧ skolem- $q
19+
with skolem- ($p ∨ $q) ↪ skolem- $p ∨ skolem- $q
20+
with skolem- ($p ⇒ $q) ↪ skolem $p ⇒ skolem- $q
21+
with skolem- $p ↪ $p;
22+
23+
// example
24+
25+
require open Stdlib.Set Stdlib.Nat;
26+
27+
private symbol P:ℕ → TYPE;
28+
29+
rule P 0 ↪ Prop
30+
with P ($n +1) ↪ τ ι → P $n;
31+
32+
private symbol p : P 2;
33+
private symbol q : P 4;
34+
35+
private symbol A ≔ `∀ X1, `∃ X2, p X1 X2 ∧ `∀ X3, `∃ X4, q X1 X2 X3 X4;
36+
37+
private symbol sk1 X1 ≔ ε (λ X2, p X1 X2 ∧ `∀ X3, `∃ X4, q X1 X2 X3 X4);
38+
39+
private symbol B ≔ `∀ X1, p X1 (sk1 X1) ∧ `∀ X3, `∃ X4, q X1 (sk1 X1) X3 X4;
40+
41+
private symbol sk2 X1 X3 ≔ ε (λ X4, q X1 (sk1 X1) X3 X4);
42+
43+
private symbol C ≔ `∀ X1, p X1 (sk1 X1) ∧ `∀ X3, q X1 (sk1 X1) X3 (sk2 X1 X3);
44+
45+
assert ⊢ skolem A ≡ C;
46+
47+
// propositional atoms
48+
49+
symbol at:ℕ → Prop;
50+
51+
// we assume that Prop is inductive
52+
53+
symbol ind_Prop (p:Prop → Prop):
54+
(Π k, π(p (at k))) →
55+
(Π a f, π((`∀ x:τ a, p (f x)) ⇒ p (∃ f))) →
56+
(Π a f, π((`∀ x:τ a, p (f x)) ⇒ p (∀ f))) →
57+
(Π f g, π(p f ⇒ p g ⇒ p (f ∧ g))) →
58+
(Π f g, π(p f ⇒ p g ⇒ p (f ∨ g))) →
59+
(Π f g, π(p f ⇒ p g ⇒ p (f ⇒ g))) →
60+
Π f:Prop, π(p f);
61+
62+
// positions in a proposition
63+
64+
inductive Pos : TYPE ≔
65+
| top: Pos
66+
| all: Pos → Pos
67+
| ex: Pos → Pos
68+
| and1: Pos → Pos
69+
| and2: Pos → Pos
70+
| or1: Pos → Pos
71+
| or2: Pos → Pos
72+
| imp1: Pos → Pos
73+
| imp2: Pos → Pos;
74+
75+
// valid positions
76+
77+
symbol valid: Pos → Prop → Prop;
78+
79+
rule valid top (at _) ↪ ⊥
80+
with valid top (∃ _) ↪ ⊤
81+
with valid top (∀ _) ↪ ⊥
82+
with valid top (_ ∧ _) ↪ ⊥
83+
with valid top (_ ∨ _) ↪ ⊥
84+
with valid top (_ ⇒ _) ↪ ⊥
85+
86+
with valid (all _) (at _) ↪ ⊥
87+
with valid (all _) (∃ _) ↪ ⊥
88+
with valid (all $i) (∀ $f) ↪ `∀ x, valid $i ($f x)
89+
with valid (all _) (_ ∧ _) ↪ ⊥
90+
with valid (all _) (_ ∨ _) ↪ ⊥
91+
with valid (all _) (_ ⇒ _) ↪ ⊥
92+
93+
with valid (ex _) (at _) ↪ ⊥
94+
with valid (ex $i) (∃ $f) ↪ `∀ x, valid $i ($f x)
95+
with valid (ex _) (∀ _) ↪ ⊥
96+
with valid (ex _) (_ ∧ _) ↪ ⊥
97+
with valid (ex _) (_ ∨ _) ↪ ⊥
98+
with valid (ex _) (_ ⇒ _) ↪ ⊥
99+
100+
with valid (and1 _) (at _) ↪ ⊥
101+
with valid (and1 _) (∃ _) ↪ ⊥
102+
with valid (and1 _) (∀ _) ↪ ⊥
103+
with valid (and1 $i) ($f ∧ _) ↪ valid $i $f
104+
with valid (and1 _) (_ ∨ _) ↪ ⊥
105+
with valid (and1 _) (_ ⇒ _) ↪ ⊥
106+
107+
with valid (and2 _) (at _) ↪ ⊥
108+
with valid (and2 _) (∃ _) ↪ ⊥
109+
with valid (and2 _) (∀ _) ↪ ⊥
110+
with valid (and2 $i) (_ ∧ $f) ↪ valid $i $f
111+
with valid (and2 _) (_ ∨ _) ↪ ⊥
112+
with valid (and2 _) (_ ⇒ _) ↪ ⊥
113+
114+
with valid (or1 _) (at _) ↪ ⊥
115+
with valid (or1 _) (∃ _) ↪ ⊥
116+
with valid (or1 _) (∀ _) ↪ ⊥
117+
with valid (or1 _) (_ ∧ _) ↪ ⊥
118+
with valid (or1 $i) ($f ∨ _) ↪ valid $i $f
119+
with valid (or1 _) (_ ⇒ _) ↪ ⊥
120+
121+
with valid (or2 _) (at _) ↪ ⊥
122+
with valid (or2 _) (∃ _) ↪ ⊥
123+
with valid (or2 _) (∀ _) ↪ ⊥
124+
with valid (or2 _) (_ ∧ _) ↪ ⊥
125+
with valid (or2 $i) (_ ∨ $f) ↪ valid $i $f
126+
with valid (or2 _) (_ ⇒ _) ↪ ⊥
127+
128+
with valid (imp1 _) (at _) ↪ ⊥
129+
with valid (imp1 _) (∃ _) ↪ ⊥
130+
with valid (imp1 _) (∀ _) ↪ ⊥
131+
with valid (imp1 _) (_ ∧ _) ↪ ⊥
132+
with valid (imp1 _) (_ ∨ _) ↪ ⊥
133+
with valid (imp1 $i) ($f ⇒ _) ↪ valid $i $f
134+
135+
with valid (imp2 _) (at _) ↪ ⊥
136+
with valid (imp2 _) (∃ _) ↪ ⊥
137+
with valid (imp2 _) (∀ _) ↪ ⊥
138+
with valid (imp2 _) (_ ∧ _) ↪ ⊥
139+
with valid (imp2 _) (_ ∨ _) ↪ ⊥
140+
with valid (imp2 $i) (_ ⇒ $f) ↪ valid $i $f
141+
;
142+
143+
// induction principle on valid positions
144+
145+
require open Stdlib.Impred;
146+
147+
opaque symbol ind_valid (p:Pos → Prop → Prop):
148+
(Π a (f:τ a → Prop), π(p top (∃ f))) →
149+
(Π i a (f:τ a → Prop),
150+
π((`∀ x, valid i (f x)) ⇒ (`∀ x, p i (f x)) ⇒ p (all i) (∀ f))) →
151+
(Π i a (f:τ a → Prop),
152+
π((`∀ x, valid i (f x)) ⇒ (`∀ x, p i (f x)) ⇒ p (ex i) (∃ f))) →
153+
(Π i f g, π(valid i f ⇒ p i f ⇒ p (and1 i) (f ∧ g))) →
154+
(Π i f g, π(valid i g ⇒ p i g ⇒ p (and2 i) (f ∧ g))) →
155+
(Π i f g, π(valid i f ⇒ p i f ⇒ p (or1 i) (f ∨ g))) →
156+
(Π i f g, π(valid i g ⇒ p i g ⇒ p (or2 i) (f ∨ g))) →
157+
(Π i f g, π(valid i f ⇒ p i f ⇒ p (imp1 i) (f ⇒ g))) →
158+
(Π i f g, π(valid i g ⇒ p i g ⇒ p (imp2 i) (f ⇒ g))) →
159+
Π i f, π(valid i f ⇒ p i f) ≔
160+
begin
161+
assume p ptop pall pex pand1 pand2 por1 por2 pimp1 pimp2; induction
162+
// top
163+
{ refine ind_Prop _ _ _ _ _ _ _
164+
{ assume k v; apply ⊥ₑ v }
165+
{ assume a f hf v; apply ptop }
166+
{ assume a f hf v; apply ⊥ₑ v }
167+
{ assume f g hf hg v; apply ⊥ₑ v }
168+
{ assume f g hf hg v; apply ⊥ₑ v }
169+
{ assume f g hf hg v; apply ⊥ₑ v }
170+
}
171+
// all
172+
{ assume i hi; refine ind_Prop _ _ _ _ _ _ _
173+
{ assume k v; apply ⊥ₑ v }
174+
{ assume a f hf v; apply ⊥ₑ v }
175+
{ assume a f hf v; apply pall i a f v; assume x; apply hi; refine (v x) }
176+
{ assume f g hf hg v; apply ⊥ₑ v }
177+
{ assume f g hf hg v; apply ⊥ₑ v }
178+
{ assume f g hf hg v; apply ⊥ₑ v }
179+
}
180+
// ex
181+
{ assume i hi; refine ind_Prop _ _ _ _ _ _ _
182+
{ assume k v; apply ⊥ₑ v }
183+
{ assume a f hf v; apply pex i a f v; assume x; apply hi; refine (v x) }
184+
{ assume a f hf v; apply ⊥ₑ v }
185+
{ assume f g hf hg v; apply ⊥ₑ v }
186+
{ assume f g hf hg v; apply ⊥ₑ v }
187+
{ assume f g hf hg v; apply ⊥ₑ v }
188+
}
189+
// and1
190+
{ assume i hi; refine ind_Prop _ _ _ _ _ _ _
191+
{ assume k v; apply ⊥ₑ v }
192+
{ assume a f hf v; apply ⊥ₑ v }
193+
{ assume a f hf v; apply ⊥ₑ v }
194+
{ assume f g hf hg v; apply pand1 i f g v (hi f v) }
195+
{ assume f g hf hg v; apply ⊥ₑ v }
196+
{ assume f g hf hg v; apply ⊥ₑ v }
197+
}
198+
// and2
199+
{ assume i hi; refine ind_Prop _ _ _ _ _ _ _
200+
{ assume k v; apply ⊥ₑ v }
201+
{ assume a f hf v; apply ⊥ₑ v }
202+
{ assume a f hf v; apply ⊥ₑ v }
203+
{ assume f g hf hg v; apply pand2 i f g v (hi g v) }
204+
{ assume f g hf hg v; apply ⊥ₑ v }
205+
{ assume f g hf hg v; apply ⊥ₑ v }
206+
}
207+
// or1
208+
{ assume i hi; refine ind_Prop _ _ _ _ _ _ _
209+
{ assume k v; apply ⊥ₑ v }
210+
{ assume a f hf v; apply ⊥ₑ v }
211+
{ assume a f hf v; apply ⊥ₑ v }
212+
{ assume f g hf hg v; apply ⊥ₑ v }
213+
{ assume f g hf hg v; apply por1 i f g v (hi f v) }
214+
{ assume f g hf hg v; apply ⊥ₑ v }
215+
}
216+
// or2
217+
{ assume i hi; refine ind_Prop _ _ _ _ _ _ _
218+
{ assume k v; apply ⊥ₑ v }
219+
{ assume a f hf v; apply ⊥ₑ v }
220+
{ assume a f hf v; apply ⊥ₑ v }
221+
{ assume f g hf hg v; apply ⊥ₑ v }
222+
{ assume f g hf hg v; apply por2 i f g v (hi g v) }
223+
{ assume f g hf hg v; apply ⊥ₑ v }
224+
}
225+
// imp1
226+
{ assume i hi; refine ind_Prop _ _ _ _ _ _ _
227+
{ assume k v; apply ⊥ₑ v }
228+
{ assume a f hf v; apply ⊥ₑ v }
229+
{ assume a f hf v; apply ⊥ₑ v }
230+
{ assume f g hf hg v; apply ⊥ₑ v }
231+
{ assume f g hf hg v; apply ⊥ₑ v }
232+
{ assume f g hf hg v; apply pimp1 i f g v (hi f v) }
233+
}
234+
// imp2
235+
{ assume i hi; refine ind_Prop _ _ _ _ _ _ _
236+
{ assume k v; apply ⊥ₑ v }
237+
{ assume a f hf v; apply ⊥ₑ v }
238+
{ assume a f hf v; apply ⊥ₑ v }
239+
{ assume f g hf hg v; apply ⊥ₑ v }
240+
{ assume f g hf hg v; apply ⊥ₑ v }
241+
{ assume f g hf hg v; apply pimp2 i f g v (hi g v) }
242+
}
243+
end;
244+
245+
// skolemization of a particular existential
246+
247+
// /!\ WARNING: partial function defined on valid positions only
248+
symbol skolem1: Pos → Prop → Prop;
249+
symbol skolem1-: Pos → Prop → Prop;
250+
251+
rule skolem1 top (∃ $p) ↪ $p (ε $p)
252+
with skolem1 (all $i) (∀ $p) ↪ `∀ x, skolem1 $i ($p x)
253+
with skolem1 (and1 $i) ($p ∧ $q) ↪ skolem1 $i $p ∧ $q
254+
with skolem1 (and2 $i) ($p ∧ $q) ↪ $p ∧ skolem1 $i $q
255+
with skolem1 (or1 $i) ($p ∨ $q) ↪ skolem1 $i $p ∨ $q
256+
with skolem1 (or2 $i) ($p ∨ $q) ↪ $p ∨ skolem1 $i $q
257+
with skolem1 (imp1 $i) ($p ⇒ $q) ↪ skolem1- $i $p ⇒ $q
258+
with skolem1 (imp2 $i) ($p ⇒ $q) ↪ $p ⇒ skolem1 $i $q
259+
260+
with skolem1- top (∀ $p) ↪ $p (ε $p)
261+
with skolem1- (ex $i) (∃ $p) ↪ `∃ x, skolem1- $i ($p x)
262+
with skolem1- (and1 $i) ($p ∧ $q) ↪ skolem1- $i $p ∧ $q
263+
with skolem1- (and2 $i) ($p ∧ $q) ↪ $p ∧ skolem1- $i $q
264+
with skolem1- (or1 $i) ($p ∨ $q) ↪ skolem1- $i $p ∨ $q
265+
with skolem1- (or2 $i) ($p ∨ $q) ↪ $p ∨ skolem1- $i $q
266+
with skolem1- (imp1 $i) ($p ⇒ $q) ↪ skolem1 $i $p ⇒ $q
267+
with skolem1- (imp2 $i) ($p ⇒ $q) ↪ $p ⇒ skolem1- $i $q
268+
;
269+
270+
assert ⊢ skolem1 (all top) A ≡ B;
271+
assert ⊢ skolem1 (all(and2(all top))) B ≡ C;
272+
273+
// correctness proof
274+
275+
opaque symbol skolem1_correct i f: π(valid i f) → π f → π(skolem1 i f) ≔
276+
begin
277+
refine ind_valid (λ i f, f ⇒ skolem1 i f) _ _ _ _ _ _ _ _ _
278+
{ assume a f h; apply εᵢ _ h }
279+
{ assume i a f v IH h x; apply IH x (h x) }
280+
{ admit }
281+
{ assume i f g v IH h; apply ∧ᵢ { apply IH (∧ₑ₁ h) } { apply ∧ₑ₂ h } }
282+
{ assume i f g v IH h; apply ∧ᵢ { apply ∧ₑ₁ h } { apply IH (∧ₑ₂ h) } }
283+
{ assume i f g v IH h; apply ∨ₑ h { assume hf; apply ∨ᵢ₁ (IH hf) } { assume hg; apply ∨ᵢ₂ hg } }
284+
{ assume i f g v IH h; apply ∨ₑ h { assume hf; apply ∨ᵢ₁ hf } { assume hg; apply ∨ᵢ₂ (IH hg) } }
285+
{ assume i f g v IH h; admit }
286+
{ assume i f g v IH h; admit }
287+
end;

0 commit comments

Comments
 (0)