From 4a95a7b9a4fca6a8670497526103af8dff5c30c5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Wed, 16 Jul 2025 12:45:22 +0200
Subject: [PATCH 1/3] add skolemization function

---
 Skolem.lp | 287 ++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 287 insertions(+)
 create mode 100644 Skolem.lp

diff --git a/Skolem.lp b/Skolem.lp
new file mode 100644
index 0000000..6d8b979
--- /dev/null
+++ b/Skolem.lp
@@ -0,0 +1,287 @@
+require open Stdlib.Prop Stdlib.FOL Stdlib.Epsilon;
+
+// procedure for skolemizing all existentials
+// /!\ WARNING: this is a sequential symbol
+
+private sequential symbol skolem: Prop → Prop;
+private sequential symbol skolem-: Prop → Prop;
+
+rule skolem (∀ $p) ↪ `∀ x, skolem ($p x)
+with skolem (∃ $p) ↪ skolem ($p (ε $p))
+with skolem ($p ∧ $q) ↪ skolem $p ∧ skolem $q
+with skolem ($p ∨ $q) ↪ skolem $p ∨ skolem $q
+with skolem ($p ⇒ $q) ↪ skolem- $p ⇒ skolem $q
+with skolem $p ↪ $p
+
+with skolem- (∀ $p) ↪ skolem- ($p (ε $p))
+with skolem- (∃ $p) ↪ `∃ x, skolem- ($p x)
+with skolem- ($p ∧ $q) ↪ skolem- $p ∧ skolem- $q
+with skolem- ($p ∨ $q) ↪ skolem- $p ∨ skolem- $q
+with skolem- ($p ⇒ $q) ↪ skolem $p ⇒ skolem- $q
+with skolem- $p ↪ $p;
+
+// example
+
+require open Stdlib.Set Stdlib.Nat;
+
+private symbol P:ℕ → TYPE;
+
+rule P 0 ↪ Prop
+with P ($n +1) ↪ τ ι → P $n;
+
+private symbol p : P 2;
+private symbol q : P 4;
+
+private symbol A ≔ `∀ X1, `∃ X2, p X1 X2 ∧ `∀ X3, `∃ X4, q X1 X2 X3 X4;
+
+private symbol sk1 X1 ≔ ε (λ X2, p X1 X2 ∧ `∀ X3, `∃ X4, q X1 X2 X3 X4);
+
+private symbol B ≔ `∀ X1, p X1 (sk1 X1) ∧ `∀ X3, `∃ X4, q X1 (sk1 X1) X3 X4;
+
+private symbol sk2 X1 X3 ≔ ε (λ X4, q X1 (sk1 X1) X3 X4);
+
+private symbol C ≔ `∀ X1, p X1 (sk1 X1) ∧ `∀ X3, q X1 (sk1 X1) X3 (sk2 X1 X3);
+
+assert ⊢ skolem A ≡ C;
+
+// propositional atoms
+
+symbol at:ℕ → Prop;
+
+// we assume that Prop is inductive
+
+symbol ind_Prop (p:Prop → Prop):
+(Π k, π(p (at k))) →
+(Π a f, π((`∀ x:τ a, p (f x)) ⇒ p (∃ f))) →
+(Π a f, π((`∀ x:τ a, p (f x)) ⇒ p (∀ f))) →
+(Π f g, π(p f ⇒ p g ⇒ p (f ∧ g))) →
+(Π f g, π(p f ⇒ p g ⇒ p (f ∨ g))) →
+(Π f g, π(p f ⇒ p g ⇒ p (f ⇒ g))) →
+Π f:Prop, π(p f);
+
+// positions in a proposition
+
+inductive Pos : TYPE ≔
+| top: Pos
+| all: Pos → Pos
+| ex: Pos → Pos
+| and1: Pos → Pos
+| and2: Pos → Pos
+| or1: Pos → Pos
+| or2: Pos → Pos
+| imp1: Pos → Pos
+| imp2: Pos → Pos;
+
+// valid positions
+
+symbol valid: Pos → Prop → Prop;
+
+rule valid top (at _) ↪ ⊥
+with valid top (∃ _) ↪ ⊤
+with valid top (∀ _) ↪ ⊥
+with valid top (_ ∧ _) ↪ ⊥
+with valid top (_ ∨ _) ↪ ⊥
+with valid top (_ ⇒ _) ↪ ⊥
+
+with valid (all _) (at _) ↪ ⊥
+with valid (all _) (∃ _) ↪ ⊥
+with valid (all $i) (∀ $f) ↪ `∀ x, valid $i ($f x)
+with valid (all _) (_ ∧ _) ↪ ⊥
+with valid (all _) (_ ∨ _) ↪ ⊥
+with valid (all _) (_ ⇒ _) ↪ ⊥
+
+with valid (ex _) (at _) ↪ ⊥
+with valid (ex $i) (∃ $f) ↪ `∀ x, valid $i ($f x)
+with valid (ex _) (∀ _) ↪ ⊥
+with valid (ex _) (_ ∧ _) ↪ ⊥
+with valid (ex _) (_ ∨ _) ↪ ⊥
+with valid (ex _) (_ ⇒ _) ↪ ⊥
+
+with valid (and1 _) (at _) ↪ ⊥
+with valid (and1 _) (∃ _) ↪ ⊥
+with valid (and1 _) (∀ _) ↪ ⊥
+with valid (and1 $i) ($f ∧ _) ↪ valid $i $f
+with valid (and1 _) (_ ∨ _) ↪ ⊥
+with valid (and1 _) (_ ⇒ _) ↪ ⊥
+
+with valid (and2 _) (at _) ↪ ⊥
+with valid (and2 _) (∃ _) ↪ ⊥
+with valid (and2 _) (∀ _) ↪ ⊥
+with valid (and2 $i) (_ ∧ $f) ↪ valid $i $f
+with valid (and2 _) (_ ∨ _) ↪ ⊥
+with valid (and2 _) (_ ⇒ _) ↪ ⊥
+
+with valid (or1 _) (at _) ↪ ⊥
+with valid (or1 _) (∃ _) ↪ ⊥
+with valid (or1 _) (∀ _) ↪ ⊥
+with valid (or1 _) (_ ∧ _) ↪ ⊥
+with valid (or1 $i) ($f ∨ _) ↪ valid $i $f
+with valid (or1 _) (_ ⇒ _) ↪ ⊥
+
+with valid (or2 _) (at _) ↪ ⊥
+with valid (or2 _) (∃ _) ↪ ⊥
+with valid (or2 _) (∀ _) ↪ ⊥
+with valid (or2 _) (_ ∧ _) ↪ ⊥
+with valid (or2 $i) (_ ∨ $f) ↪ valid $i $f
+with valid (or2 _) (_ ⇒ _) ↪ ⊥
+
+with valid (imp1 _) (at _) ↪ ⊥
+with valid (imp1 _) (∃ _) ↪ ⊥
+with valid (imp1 _) (∀ _) ↪ ⊥
+with valid (imp1 _) (_ ∧ _) ↪ ⊥
+with valid (imp1 _) (_ ∨ _) ↪ ⊥
+with valid (imp1 $i) ($f ⇒ _) ↪ valid $i $f
+
+with valid (imp2 _) (at _) ↪ ⊥
+with valid (imp2 _) (∃ _) ↪ ⊥
+with valid (imp2 _) (∀ _) ↪ ⊥
+with valid (imp2 _) (_ ∧ _) ↪ ⊥
+with valid (imp2 _) (_ ∨ _) ↪ ⊥
+with valid (imp2 $i) (_ ⇒ $f) ↪ valid $i $f
+;
+
+// induction principle on valid positions
+
+require open Stdlib.Impred;
+
+opaque symbol ind_valid (p:Pos → Prop → Prop):
+(Π a (f:τ a → Prop), π(p top (∃ f))) →
+(Π i a (f:τ a → Prop),
+  π((`∀ x, valid i (f x)) ⇒ (`∀ x, p i (f x)) ⇒ p (all i) (∀ f))) →
+(Π i a (f:τ a → Prop),
+  π((`∀ x, valid i (f x)) ⇒ (`∀ x, p i (f x)) ⇒ p (ex i) (∃ f))) →
+(Π i f g, π(valid i f ⇒ p i f ⇒ p (and1 i) (f ∧ g))) →
+(Π i f g, π(valid i g ⇒ p i g ⇒ p (and2 i) (f ∧ g))) →
+(Π i f g, π(valid i f ⇒ p i f ⇒ p (or1 i) (f ∨ g))) →
+(Π i f g, π(valid i g ⇒ p i g ⇒ p (or2 i) (f ∨ g))) →
+(Π i f g, π(valid i f ⇒ p i f ⇒ p (imp1 i) (f ⇒ g))) →
+(Π i f g, π(valid i g ⇒ p i g ⇒ p (imp2 i) (f ⇒ g))) →
+Π i f, π(valid i f ⇒ p i f) ≔
+begin
+assume p ptop pall pex pand1 pand2 por1 por2 pimp1 pimp2; induction
+// top
+{ refine ind_Prop _ _ _ _ _ _ _
+  { assume k v; apply ⊥ₑ v }
+  { assume a f hf v; apply ptop }
+  { assume a f hf v; apply ⊥ₑ v }
+  { assume f g hf hg v; apply ⊥ₑ v }
+  { assume f g hf hg v; apply ⊥ₑ v }
+  { assume f g hf hg v; apply ⊥ₑ v }
+}
+// all
+{ assume i hi; refine ind_Prop _ _ _ _ _ _ _
+  { assume k v; apply ⊥ₑ v }
+  { assume a f hf v; apply ⊥ₑ v }
+  { assume a f hf v; apply pall i a f v; assume x; apply hi; refine (v x) }
+  { assume f g hf hg v; apply ⊥ₑ v }
+  { assume f g hf hg v; apply ⊥ₑ v }
+  { assume f g hf hg v; apply ⊥ₑ v }
+}
+// ex
+{ assume i hi; refine ind_Prop _ _ _ _ _ _ _
+  { assume k v; apply ⊥ₑ v }
+  { assume a f hf v; apply pex i a f v; assume x; apply hi; refine (v x) }
+  { assume a f hf v; apply ⊥ₑ v }
+  { assume f g hf hg v; apply ⊥ₑ v }
+  { assume f g hf hg v; apply ⊥ₑ v }
+  { assume f g hf hg v; apply ⊥ₑ v }
+}
+// and1
+{ assume i hi; refine ind_Prop _ _ _ _ _ _ _
+  { assume k v; apply ⊥ₑ v }
+  { assume a f hf v; apply ⊥ₑ v }
+  { assume a f hf v; apply ⊥ₑ v }
+  { assume f g hf hg v; apply pand1 i f g v (hi f v) }
+  { assume f g hf hg v; apply ⊥ₑ v }
+  { assume f g hf hg v; apply ⊥ₑ v }
+}
+// and2
+{ assume i hi; refine ind_Prop _ _ _ _ _ _ _
+  { assume k v; apply ⊥ₑ v }
+  { assume a f hf v; apply ⊥ₑ v }
+  { assume a f hf v; apply ⊥ₑ v }
+  { assume f g hf hg v; apply pand2 i f g v (hi g v) }
+  { assume f g hf hg v; apply ⊥ₑ v }
+  { assume f g hf hg v; apply ⊥ₑ v }
+}
+// or1
+{ assume i hi; refine ind_Prop _ _ _ _ _ _ _
+  { assume k v; apply ⊥ₑ v }
+  { assume a f hf v; apply ⊥ₑ v }
+  { assume a f hf v; apply ⊥ₑ v }
+  { assume f g hf hg v; apply ⊥ₑ v }
+  { assume f g hf hg v; apply por1 i f g v (hi f v) }
+  { assume f g hf hg v; apply ⊥ₑ v }
+}
+// or2
+{ assume i hi; refine ind_Prop _ _ _ _ _ _ _
+  { assume k v; apply ⊥ₑ v }
+  { assume a f hf v; apply ⊥ₑ v }
+  { assume a f hf v; apply ⊥ₑ v }
+  { assume f g hf hg v; apply ⊥ₑ v }
+  { assume f g hf hg v; apply por2 i f g v (hi g v) }
+  { assume f g hf hg v; apply ⊥ₑ v }
+}
+// imp1
+{ assume i hi; refine ind_Prop _ _ _ _ _ _ _
+  { assume k v; apply ⊥ₑ v }
+  { assume a f hf v; apply ⊥ₑ v }
+  { assume a f hf v; apply ⊥ₑ v }
+  { assume f g hf hg v; apply ⊥ₑ v }
+  { assume f g hf hg v; apply ⊥ₑ v }
+  { assume f g hf hg v; apply pimp1 i f g v (hi f v) }
+}
+// imp2
+{ assume i hi; refine ind_Prop _ _ _ _ _ _ _
+  { assume k v; apply ⊥ₑ v }
+  { assume a f hf v; apply ⊥ₑ v }
+  { assume a f hf v; apply ⊥ₑ v }
+  { assume f g hf hg v; apply ⊥ₑ v }
+  { assume f g hf hg v; apply ⊥ₑ v }
+  { assume f g hf hg v; apply pimp2 i f g v (hi g v) }
+}
+end;
+
+// skolemization of a particular existential
+
+// /!\ WARNING: partial function defined on valid positions only
+symbol skolem1: Pos → Prop → Prop;
+symbol skolem1-: Pos → Prop → Prop;
+
+rule skolem1 top (∃ $p) ↪ $p (ε $p)
+with skolem1 (all $i) (∀ $p) ↪ `∀ x, skolem1 $i ($p x)
+with skolem1 (and1 $i) ($p ∧ $q) ↪ skolem1 $i $p ∧ $q
+with skolem1 (and2 $i) ($p ∧ $q) ↪ $p ∧ skolem1 $i $q
+with skolem1 (or1 $i) ($p ∨ $q) ↪ skolem1 $i $p ∨ $q
+with skolem1 (or2 $i) ($p ∨ $q) ↪ $p ∨ skolem1 $i $q
+with skolem1 (imp1 $i) ($p ⇒ $q) ↪ skolem1- $i $p ⇒ $q
+with skolem1 (imp2 $i) ($p ⇒ $q) ↪ $p ⇒ skolem1 $i $q
+
+with skolem1- top (∀ $p) ↪ $p (ε $p)
+with skolem1- (ex $i) (∃ $p) ↪ `∃ x, skolem1- $i ($p x)
+with skolem1- (and1 $i) ($p ∧ $q) ↪ skolem1- $i $p ∧ $q
+with skolem1- (and2 $i) ($p ∧ $q) ↪ $p ∧ skolem1- $i $q
+with skolem1- (or1 $i) ($p ∨ $q) ↪ skolem1- $i $p ∨ $q
+with skolem1- (or2 $i) ($p ∨ $q) ↪ $p ∨ skolem1- $i $q
+with skolem1- (imp1 $i) ($p ⇒ $q) ↪ skolem1 $i $p ⇒ $q
+with skolem1- (imp2 $i) ($p ⇒ $q) ↪ $p ⇒ skolem1- $i $q
+;
+
+assert ⊢ skolem1 (all top) A ≡ B;
+assert ⊢ skolem1 (all(and2(all top))) B ≡ C;
+
+// correctness proof
+
+opaque symbol skolem1_correct i f: π(valid i f) → π f → π(skolem1 i f) ≔
+begin
+refine ind_valid (λ i f, f ⇒ skolem1 i f) _ _ _ _ _ _ _ _ _
+{ assume a f h; apply εᵢ _ h }
+{ assume i a f v IH h x; apply IH x (h x) }
+{ admit }
+{ assume i f g v IH h; apply ∧ᵢ { apply IH (∧ₑ₁ h) } { apply ∧ₑ₂ h } }
+{ assume i f g v IH h; apply ∧ᵢ { apply ∧ₑ₁ h } { apply IH (∧ₑ₂ h) } }
+{ assume i f g v IH h; apply ∨ₑ h { assume hf; apply ∨ᵢ₁ (IH hf) } { assume hg; apply ∨ᵢ₂ hg } }
+{ assume i f g v IH h; apply ∨ₑ h { assume hf; apply ∨ᵢ₁ hf } { assume hg; apply ∨ᵢ₂ (IH hg) } }
+{ assume i f g v IH h; admit }
+{ assume i f g v IH h; admit }
+end;

From a299ad9ae1445659a7e8db7d63a049feb2657327 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Thu, 17 Jul 2025 18:34:45 +0200
Subject: [PATCH 2/3] wip

---
 Skolem.lp | 111 ++++++++++++------------------------------------------
 1 file changed, 24 insertions(+), 87 deletions(-)

diff --git a/Skolem.lp b/Skolem.lp
index 6d8b979..c4c9a5c 100644
--- a/Skolem.lp
+++ b/Skolem.lp
@@ -1,24 +1,16 @@
 require open Stdlib.Prop Stdlib.FOL Stdlib.Epsilon;
 
-// procedure for skolemizing all existentials
+// procedure for skolemizing all existentials (no proof provided)
 // /!\ WARNING: this is a sequential symbol
 
 private sequential symbol skolem: Prop → Prop;
-private sequential symbol skolem-: Prop → Prop;
 
-rule skolem (∀ $p) ↪ `∀ x, skolem ($p x)
-with skolem (∃ $p) ↪ skolem ($p (ε $p))
+rule skolem (∃ $p) ↪ skolem ($p (ε $p))
+with skolem (∀ $p) ↪ `∀ x, skolem ($p x)
 with skolem ($p ∧ $q) ↪ skolem $p ∧ skolem $q
 with skolem ($p ∨ $q) ↪ skolem $p ∨ skolem $q
-with skolem ($p ⇒ $q) ↪ skolem- $p ⇒ skolem $q
 with skolem $p ↪ $p
-
-with skolem- (∀ $p) ↪ skolem- ($p (ε $p))
-with skolem- (∃ $p) ↪ `∃ x, skolem- ($p x)
-with skolem- ($p ∧ $q) ↪ skolem- $p ∧ skolem- $q
-with skolem- ($p ∨ $q) ↪ skolem- $p ∨ skolem- $q
-with skolem- ($p ⇒ $q) ↪ skolem $p ⇒ skolem- $q
-with skolem- $p ↪ $p;
+;
 
 // example
 
@@ -56,7 +48,6 @@ symbol ind_Prop (p:Prop → Prop):
 (Π a f, π((`∀ x:τ a, p (f x)) ⇒ p (∀ f))) →
 (Π f g, π(p f ⇒ p g ⇒ p (f ∧ g))) →
 (Π f g, π(p f ⇒ p g ⇒ p (f ∨ g))) →
-(Π f g, π(p f ⇒ p g ⇒ p (f ⇒ g))) →
 Π f:Prop, π(p f);
 
 // positions in a proposition
@@ -69,8 +60,7 @@ inductive Pos : TYPE ≔
 | and2: Pos → Pos
 | or1: Pos → Pos
 | or2: Pos → Pos
-| imp1: Pos → Pos
-| imp2: Pos → Pos;
+;
 
 // valid positions
 
@@ -124,20 +114,6 @@ with valid (or2 _) (∀ _) ↪ ⊥
 with valid (or2 _) (_ ∧ _) ↪ ⊥
 with valid (or2 $i) (_ ∨ $f) ↪ valid $i $f
 with valid (or2 _) (_ ⇒ _) ↪ ⊥
-
-with valid (imp1 _) (at _) ↪ ⊥
-with valid (imp1 _) (∃ _) ↪ ⊥
-with valid (imp1 _) (∀ _) ↪ ⊥
-with valid (imp1 _) (_ ∧ _) ↪ ⊥
-with valid (imp1 _) (_ ∨ _) ↪ ⊥
-with valid (imp1 $i) ($f ⇒ _) ↪ valid $i $f
-
-with valid (imp2 _) (at _) ↪ ⊥
-with valid (imp2 _) (∃ _) ↪ ⊥
-with valid (imp2 _) (∀ _) ↪ ⊥
-with valid (imp2 _) (_ ∧ _) ↪ ⊥
-with valid (imp2 _) (_ ∨ _) ↪ ⊥
-with valid (imp2 $i) (_ ⇒ $f) ↪ valid $i $f
 ;
 
 // induction principle on valid positions
@@ -154,91 +130,64 @@ opaque symbol ind_valid (p:Pos → Prop → Prop):
 (Π i f g, π(valid i g ⇒ p i g ⇒ p (and2 i) (f ∧ g))) →
 (Π i f g, π(valid i f ⇒ p i f ⇒ p (or1 i) (f ∨ g))) →
 (Π i f g, π(valid i g ⇒ p i g ⇒ p (or2 i) (f ∨ g))) →
-(Π i f g, π(valid i f ⇒ p i f ⇒ p (imp1 i) (f ⇒ g))) →
-(Π i f g, π(valid i g ⇒ p i g ⇒ p (imp2 i) (f ⇒ g))) →
 Π i f, π(valid i f ⇒ p i f) ≔
 begin
-assume p ptop pall pex pand1 pand2 por1 por2 pimp1 pimp2; induction
+assume p ptop pall pex pand1 pand2 por1 por2; induction
 // top
-{ refine ind_Prop _ _ _ _ _ _ _
+{ refine ind_Prop _ _ _ _ _ _
   { assume k v; apply ⊥ₑ v }
   { assume a f hf v; apply ptop }
   { assume a f hf v; apply ⊥ₑ v }
   { assume f g hf hg v; apply ⊥ₑ v }
   { assume f g hf hg v; apply ⊥ₑ v }
-  { assume f g hf hg v; apply ⊥ₑ v }
 }
 // all
-{ assume i hi; refine ind_Prop _ _ _ _ _ _ _
+{ assume i hi; refine ind_Prop _ _ _ _ _ _
   { assume k v; apply ⊥ₑ v }
   { assume a f hf v; apply ⊥ₑ v }
   { assume a f hf v; apply pall i a f v; assume x; apply hi; refine (v x) }
   { assume f g hf hg v; apply ⊥ₑ v }
   { assume f g hf hg v; apply ⊥ₑ v }
-  { assume f g hf hg v; apply ⊥ₑ v }
 }
 // ex
-{ assume i hi; refine ind_Prop _ _ _ _ _ _ _
+{ assume i hi; refine ind_Prop _ _ _ _ _ _
   { assume k v; apply ⊥ₑ v }
   { assume a f hf v; apply pex i a f v; assume x; apply hi; refine (v x) }
   { assume a f hf v; apply ⊥ₑ v }
   { assume f g hf hg v; apply ⊥ₑ v }
   { assume f g hf hg v; apply ⊥ₑ v }
-  { assume f g hf hg v; apply ⊥ₑ v }
 }
 // and1
-{ assume i hi; refine ind_Prop _ _ _ _ _ _ _
+{ assume i hi; refine ind_Prop _ _ _ _ _ _
   { assume k v; apply ⊥ₑ v }
   { assume a f hf v; apply ⊥ₑ v }
   { assume a f hf v; apply ⊥ₑ v }
   { assume f g hf hg v; apply pand1 i f g v (hi f v) }
   { assume f g hf hg v; apply ⊥ₑ v }
-  { assume f g hf hg v; apply ⊥ₑ v }
 }
 // and2
-{ assume i hi; refine ind_Prop _ _ _ _ _ _ _
+{ assume i hi; refine ind_Prop _ _ _ _ _ _
   { assume k v; apply ⊥ₑ v }
   { assume a f hf v; apply ⊥ₑ v }
   { assume a f hf v; apply ⊥ₑ v }
   { assume f g hf hg v; apply pand2 i f g v (hi g v) }
   { assume f g hf hg v; apply ⊥ₑ v }
-  { assume f g hf hg v; apply ⊥ₑ v }
 }
 // or1
-{ assume i hi; refine ind_Prop _ _ _ _ _ _ _
+{ assume i hi; refine ind_Prop _ _ _ _ _ _
   { assume k v; apply ⊥ₑ v }
   { assume a f hf v; apply ⊥ₑ v }
   { assume a f hf v; apply ⊥ₑ v }
   { assume f g hf hg v; apply ⊥ₑ v }
   { assume f g hf hg v; apply por1 i f g v (hi f v) }
-  { assume f g hf hg v; apply ⊥ₑ v }
 }
 // or2
-{ assume i hi; refine ind_Prop _ _ _ _ _ _ _
+{ assume i hi; refine ind_Prop _ _ _ _ _ _
   { assume k v; apply ⊥ₑ v }
   { assume a f hf v; apply ⊥ₑ v }
   { assume a f hf v; apply ⊥ₑ v }
   { assume f g hf hg v; apply ⊥ₑ v }
   { assume f g hf hg v; apply por2 i f g v (hi g v) }
-  { assume f g hf hg v; apply ⊥ₑ v }
-}
-// imp1
-{ assume i hi; refine ind_Prop _ _ _ _ _ _ _
-  { assume k v; apply ⊥ₑ v }
-  { assume a f hf v; apply ⊥ₑ v }
-  { assume a f hf v; apply ⊥ₑ v }
-  { assume f g hf hg v; apply ⊥ₑ v }
-  { assume f g hf hg v; apply ⊥ₑ v }
-  { assume f g hf hg v; apply pimp1 i f g v (hi f v) }
-}
-// imp2
-{ assume i hi; refine ind_Prop _ _ _ _ _ _ _
-  { assume k v; apply ⊥ₑ v }
-  { assume a f hf v; apply ⊥ₑ v }
-  { assume a f hf v; apply ⊥ₑ v }
-  { assume f g hf hg v; apply ⊥ₑ v }
-  { assume f g hf hg v; apply ⊥ₑ v }
-  { assume f g hf hg v; apply pimp2 i f g v (hi g v) }
 }
 end;
 
@@ -246,42 +195,30 @@ end;
 
 // /!\ WARNING: partial function defined on valid positions only
 symbol skolem1: Pos → Prop → Prop;
-symbol skolem1-: Pos → Prop → Prop;
 
 rule skolem1 top (∃ $p) ↪ $p (ε $p)
 with skolem1 (all $i) (∀ $p) ↪ `∀ x, skolem1 $i ($p x)
+with skolem1 (ex $i) (∃ $p) ↪ `∃ x, skolem1 $i ($p x)
 with skolem1 (and1 $i) ($p ∧ $q) ↪ skolem1 $i $p ∧ $q
 with skolem1 (and2 $i) ($p ∧ $q) ↪ $p ∧ skolem1 $i $q
 with skolem1 (or1 $i) ($p ∨ $q) ↪ skolem1 $i $p ∨ $q
 with skolem1 (or2 $i) ($p ∨ $q) ↪ $p ∨ skolem1 $i $q
-with skolem1 (imp1 $i) ($p ⇒ $q) ↪ skolem1- $i $p ⇒ $q
-with skolem1 (imp2 $i) ($p ⇒ $q) ↪ $p ⇒ skolem1 $i $q
-
-with skolem1- top (∀ $p) ↪ $p (ε $p)
-with skolem1- (ex $i) (∃ $p) ↪ `∃ x, skolem1- $i ($p x)
-with skolem1- (and1 $i) ($p ∧ $q) ↪ skolem1- $i $p ∧ $q
-with skolem1- (and2 $i) ($p ∧ $q) ↪ $p ∧ skolem1- $i $q
-with skolem1- (or1 $i) ($p ∨ $q) ↪ skolem1- $i $p ∨ $q
-with skolem1- (or2 $i) ($p ∨ $q) ↪ $p ∨ skolem1- $i $q
-with skolem1- (imp1 $i) ($p ⇒ $q) ↪ skolem1 $i $p ⇒ $q
-with skolem1- (imp2 $i) ($p ⇒ $q) ↪ $p ⇒ skolem1- $i $q
 ;
 
 assert ⊢ skolem1 (all top) A ≡ B;
 assert ⊢ skolem1 (all(and2(all top))) B ≡ C;
 
-// correctness proof
+// skolemization preserves provability
 
-opaque symbol skolem1_correct i f: π(valid i f) → π f → π(skolem1 i f) ≔
+opaque symbol skolem1_preserves_provability i f:
+  π(valid i f) → π f → π(skolem1 i f) ≔
 begin
-refine ind_valid (λ i f, f ⇒ skolem1 i f) _ _ _ _ _ _ _ _ _
-{ assume a f h; apply εᵢ _ h }
+refine ind_valid (λ i f, f ⇒ skolem1 i f) _ _ _ _ _ _ _
+{ assume a f h; simplify; apply εᵢ _ h }
 { assume i a f v IH h x; apply IH x (h x) }
-{ admit }
-{ assume i f g v IH h; apply ∧ᵢ { apply IH (∧ₑ₁ h) } { apply ∧ₑ₂ h } }
-{ assume i f g v IH h; apply ∧ᵢ { apply ∧ₑ₁ h } { apply IH (∧ₑ₂ h) } }
-{ assume i f g v IH h; apply ∨ₑ h { assume hf; apply ∨ᵢ₁ (IH hf) } { assume hg; apply ∨ᵢ₂ hg } }
-{ assume i f g v IH h; apply ∨ₑ h { assume hf; apply ∨ᵢ₁ hf } { assume hg; apply ∨ᵢ₂ (IH hg) } }
-{ assume i f g v IH h; admit }
-{ assume i f g v IH h; admit }
+{ assume i a f v IH h; simplify; apply ∃ₑ h; assume x hx; apply ∃ᵢ x; apply IH x; apply hx }
+{ assume i f g v IH h; simplify; apply ∧ᵢ { apply IH (∧ₑ₁ h) } { apply ∧ₑ₂ h } }
+{ assume i f g v IH h; simplify; apply ∧ᵢ { apply ∧ₑ₁ h } { apply IH (∧ₑ₂ h) } }
+{ assume i f g v IH h; simplify; apply ∨ₑ h { assume hf; apply ∨ᵢ₁ (IH hf) } { assume hg; apply ∨ᵢ₂ hg } }
+{ assume i f g v IH h; simplify; apply ∨ₑ h { assume hf; apply ∨ᵢ₁ hf } { assume hg; apply ∨ᵢ₂ (IH hg) } }
 end;

From 4ce5074688f8504be3fab7893bb4eee8393decbe Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Fri, 18 Jul 2025 18:47:08 +0200
Subject: [PATCH 3/3] wip

---
 Skolem.lp | 27 ++++++++++++++++++++-------
 1 file changed, 20 insertions(+), 7 deletions(-)

diff --git a/Skolem.lp b/Skolem.lp
index c4c9a5c..59deeb8 100644
--- a/Skolem.lp
+++ b/Skolem.lp
@@ -214,11 +214,24 @@ opaque symbol skolem1_preserves_provability i f:
   π(valid i f) → π f → π(skolem1 i f) ≔
 begin
 refine ind_valid (λ i f, f ⇒ skolem1 i f) _ _ _ _ _ _ _
-{ assume a f h; simplify; apply εᵢ _ h }
-{ assume i a f v IH h x; apply IH x (h x) }
-{ assume i a f v IH h; simplify; apply ∃ₑ h; assume x hx; apply ∃ᵢ x; apply IH x; apply hx }
-{ assume i f g v IH h; simplify; apply ∧ᵢ { apply IH (∧ₑ₁ h) } { apply ∧ₑ₂ h } }
-{ assume i f g v IH h; simplify; apply ∧ᵢ { apply ∧ₑ₁ h } { apply IH (∧ₑ₂ h) } }
-{ assume i f g v IH h; simplify; apply ∨ₑ h { assume hf; apply ∨ᵢ₁ (IH hf) } { assume hg; apply ∨ᵢ₂ hg } }
-{ assume i f g v IH h; simplify; apply ∨ₑ h { assume hf; apply ∨ᵢ₁ hf } { assume hg; apply ∨ᵢ₂ (IH hg) } }
+{ simplify; assume a f h; apply εᵢ _ h }
+{ simplify; assume i a f v IH h x; apply IH x (h x) }
+{ simplify; assume i a f v IH h; apply ∃ₑ h; assume x hx; apply ∃ᵢ x; apply IH x; apply hx }
+{ simplify; assume i f g v IH h; apply ∧ᵢ { apply IH (∧ₑ₁ h) } { apply ∧ₑ₂ h } }
+{ simplify; assume i f g v IH h; apply ∧ᵢ { apply ∧ₑ₁ h } { apply IH (∧ₑ₂ h) } }
+{ simplify; assume i f g v IH h; apply ∨ₑ h { assume hf; apply ∨ᵢ₁ (IH hf) } { assume hg; apply ∨ᵢ₂ hg } }
+{ simplify; assume i f g v IH h; apply ∨ₑ h { assume hf; apply ∨ᵢ₁ hf } { assume hg; apply ∨ᵢ₂ (IH hg) } }
+end;
+
+opaque symbol skolem1_reflects_provability i f:
+  π(valid i f) → π(skolem1 i f) → π f ≔
+begin
+refine ind_valid (λ i f, skolem1 i f ⇒ f) _ _ _ _ _ _ _
+{ simplify; assume a f h; apply ∃ᵢ _ h }
+{ simplify; assume i a f v IH h x; apply IH x (h x) }
+{ simplify; assume i a f v IH h; apply ∃ₑ h; assume x hx; apply ∃ᵢ x; apply IH x; apply hx }
+{ simplify; assume i f g v IH h; apply ∧ᵢ { apply IH (∧ₑ₁ h) } { apply ∧ₑ₂ h } }
+{ simplify; assume i f g v IH h; apply ∧ᵢ { apply ∧ₑ₁ h } { apply IH (∧ₑ₂ h) } }
+{ simplify; assume i f g v IH h; apply ∨ₑ h { assume hf; apply ∨ᵢ₁ (IH hf) } { assume hg; apply ∨ᵢ₂ hg } }
+{ simplify; assume i f g v IH h; apply ∨ₑ h { assume hf; apply ∨ᵢ₁ hf } { assume hg; apply ∨ᵢ₂ (IH hg) } }
 end;