Rename basic to Resolution

Also add abbrev GroundTerm and remove unfinished exercises

Author: SamuelLess

InferenceInLean.lean

@@ -1,3 +1,3 @@
 -- This module serves as the root of the `InferenceInLean` library.
 -- Import modules here that should be built as part of the library.
-import «InferenceInLean».Basic
+import «InferenceInLean».Resolution

InferenceInLean/Exercises/Exercise4.lean

@@ -1,4 +1,4 @@
-import InferenceInLean.Basic
+import InferenceInLean.Resolution
 import Mathlib.Data.Finset.Defs
 
 set_option autoImplicit false
@@ -163,150 +163,4 @@ theorem ex_4_2b : ∃ I : Interpretation sig42 (Fin 2), ∃ β : Assignment Stri
 end Task2
 
 
-/- ### Exercise 4.6
-  Let Σ = (Ω, Π) be a signature. For every Σ-formula F without equality,
-  let neg(F) be the formula that one obtains from F by replacing every atom P(t1,...,tn)
-  in F by its negation ¬P(t1,...,tn) for every P/n ∈ Π.
-  Prove: If F is valid, then neg(F) is valid. -/
-
-namespace Task6
-
-/- ! Rather large chunks of this namespace were generated by Claude 3.7 Sonnet (free version) !
-  Let's see if I want to fix this... -/
-
--- Define the neg function that negates all atoms in a formula
-@[simp]
-def negFormula {sig : Signature} {X : Variables} : Formula sig X → Formula sig X
-  | Formula.falsum => Formula.falsum
-  | Formula.verum => Formula.verum
-  | Formula.atom a => Formula.neg (Formula.atom a)  -- replace atom with its negation
-  | Formula.neg (Formula.atom a) => Formula.atom a  -- special case: double negation of atom
-  | Formula.neg f => Formula.neg (negFormula f)
-  | Formula.and f g => Formula.and (negFormula f) (negFormula g)
-  | Formula.or f g => Formula.or (negFormula f) (negFormula g)
-  | Formula.imp f g => Formula.imp (negFormula f) (negFormula g)
-  | Formula.iff f g => Formula.iff (negFormula f) (negFormula g)
-  | Formula.all x f => Formula.all x (negFormula f)
-  | Formula.ex x f => Formula.ex x (negFormula f)
-
--- Define a "dual" interpretation that flips the truth value of all predicates
-@[simp]
-def dualInterpretation {sig : Signature} {univ : Universes}
-    (I : Interpretation sig univ) : Interpretation sig univ :=
-  ⟨I.functions, fun p args => ¬(I.predicates p args)⟩
-
-theorem dualInterpretation.funs_eq {sig : Signature} {X : Variables} {univ : Universes}
-    [DecidableEq X] (I : Interpretation sig univ) :
-    I.functions = (dualInterpretation I).functions := rfl
-
--- Lemma: For any term t, eval(t) in the original interpretation is the same as in the dual
-@[simp]
-theorem term_eval_invariant {sig : Signature} {X : Variables} {univ : Universes}
-    [DecidableEq X] (I : Interpretation sig univ) (β : Assignment X univ) (t : Term sig X) :
-    Term.eval I β t = Term.eval (dualInterpretation I) β t := by
-  induction' t using Term.induction with x args ih f <;> aesop
-
--- Lemma: For any atom a, eval(¬a) in the original interpretation equals eval(a) in the dual
-@[simp]
-theorem atom_eval_dual {sig : Signature} {X : Variables} {univ : Universes}
-    [DecidableEq X] (I : Interpretation sig univ) (β : Assignment X univ) (a : Atom sig X) :
-    ¬(Atom.eval I β a) ↔ Atom.eval (dualInterpretation I) β a := by
-  simp [term_eval_invariant]
-  induction a.2 with
-  | nil => simp
-  | cons head tail ih =>
-    induction' head using Term.induction with x args ih f
-    sorry
-    sorry
-
--- Main theorem: The key equivalence - F evaluates to true in I iff neg(F) evaluates to true in dual(I)
-theorem negFormula_eval_iff {sig : Signature} {X : Variables} {univ : Universes}
-    [DecidableEq X] (I : Interpretation sig univ) (β : Assignment X univ) (F : Formula sig X) :
-    Formula.eval I β F ↔ Formula.eval (dualInterpretation I) β (negFormula F) := by
-  sorry
-
- -- Final theorem: If F is valid, then neg(F) is valid
-theorem valid_negFormula {sig : Signature} {X : Variables} {univ : Universes}
-    [DecidableEq X] (F : Formula sig X) :
-    @Valid sig X univ _ F → @Valid sig X univ _ (negFormula F) := by
-  intro h_valid I β
-  simp_all only [Valid]
-  have := h_valid I β
-  have := (negFormula_eval_iff I β F).mp this
-  sorry
-
-end Task6
-
-
-/- ### Exercise 4.7 (*)
-  Let Π be a set of propositional variables. Let N and N' be sets
-  of clauses over Π. Let S be a set of literals that does not contain any complementary
-  literals. Prove: If every clause in N contains at least one literal L with L ∈ S and if no
-  clause in N' contains a literal L with L ∈ S, then N ∪ N' is satisfiable if and only if N'
-  is satisfiable.  -/
-
-namespace Task7
-
-def Interpretation.add (I : Interpretation ⟨Empty, String⟩ String)
-    (β : Assignment Empty String) (L : Literal ⟨Empty, String⟩ Empty) :
-    Interpretation ⟨Empty, String⟩ String :=
-  -- add something to I such that Formula.eval L is true
-  Interpretation.mk I.functions (match L with
-    | Literal.pos a => match a with
-      | Atom.pred p args =>
-        have argsinter := args.map (Term.eval I β)
-        (fun p' args' => if p' == p && args' == argsinter
-          then True
-          else I.predicates p' args')
-    | Literal.neg a => match a with
-      | Atom.pred p args =>
-        have argsinter := args.map (Term.eval I β)
-        (fun p' args' => if p' == p && args' == argsinter
-          then False
-          else I.predicates p' args')
-  )
-
-lemma tmp (I : Interpretation ⟨Empty, String⟩ String) (β : Assignment Empty String)
-    (C : Clause ⟨Empty, String⟩ Empty)
-    (hCsat : EntailsInterpret I β C) (L : Literal ⟨Empty, String⟩ Empty) (h : L.comp ∉ C) :
-    EntailsInterpret (Interpretation.add I β L) β C := by
-  sorry
-
-theorem ex_4_7
-    (N N' : Set <| Clause ⟨Empty, String⟩ Empty) (S : Set <| Literal ⟨Empty, String⟩ Empty)
-    (hSnoCompl : ∀ L ∈ S, L.comp ∉ S)
-    (hNsatByS : ∀ C ∈ N, ∃ L ∈ C, L ∈ S) (hN'noComplS : ∀ C ∈ N', ¬∃ L ∈ C, L.comp ∈ S) :
-    (@ClauseSetSatisfiable _ _ univ _ (N ∪ N') ↔ @ClauseSetSatisfiable _ _ univ _ N') := by
-  simp only [not_exists, not_and] at hN'noComplS
-  apply Iff.intro
-  · simp [ClauseSetSatisfiable]
-    intro I β h
-    apply Exists.intro
-    · apply Exists.intro
-      · intro C a
-        apply h
-        simp_all only [or_true]
-  · simp [ClauseSetSatisfiable]
-    intro I_N' β_N' hN'sat
-    use I_N'
-    use β_N' -- delay instanciation of assignment
-    intro C hC
-    cases hC
-    next hCinN =>
-      /- This is the actual hard case of this exercise. On paper it might look like this:
-          - Show that I_N' and β_N' do not contradict (SAT N) (this is due to hN'noComplS)
-          - Expand β_N' by the assignments implied by S to β_N'andS
-          - then β_N'andS satisfies N using hNsatByS
-      -/
-      obtain ⟨L, ⟨hLinC, hLinS⟩⟩ := hNsatByS C hCinN
-      have hLcompninS : L.comp ∉ S := by exact hSnoCompl L hLinS
-      --let ?β := β_N'
-      --let β_N'andS := β.modify L
-      sorry
-
-    next hCinN' => exact hN'sat C hCinN'
-
-end Task7
-
-
 end Exercise4

InferenceInLean/Exercises/Exercise5.lean

@@ -1,4 +1,4 @@
-import InferenceInLean.Basic
+import InferenceInLean.Resolution
 import Mathlib.Data.Finset.Defs
 import Mathlib.Data.Set.Card
 import Mathlib.SetTheory.Cardinal.Finite
@@ -33,11 +33,11 @@ def f : List (Term sig5_1 String) -> Term sig5_1 String := .func .f
 def P : List (Term sig5_1 String) -> Formula sig5_1 String := fun args =>.atom <| .pred .P args
 
 /- Force the interpretation of P to be false for every list of arguments with the wrong arity. -/
-def ArityP : (preds -> List (Term sig5_1 Empty) -> Prop) -> Prop
-| ps => ∀ (args : List (Term sig5_1 Empty)), (args.length ≠ 1) → ¬(ps .P args)
+def ArityP (ps : preds -> List (GroundTerm sig5_1) -> Prop) : Prop :=
+  ∀ (args : List (GroundTerm sig5_1)), (args.length ≠ 1) → ¬(ps .P args)
 
 -- (1) There is a Σ-model A of P (b) ∧ ¬P (f (b)) such that UA = {7, 8, 9}.
-def F₁ : Formula sig5_1 String := .and (P [b]) (.neg (P [f [b]]))
+def F₁ : Formula sig5_1 String := (P [b]).and (.neg (P [f [b]]))
 theorem task5_1_1 : ∃ (I : Interpretation sig5_1 (Fin 3)), ∀ β : Assignment String (Fin 3),
     EntailsInterpret I β F₁ := by
   -- Define the interpretation I for universe {0, 1, 2} (representing {7, 8, 9})
@@ -58,7 +58,7 @@ theorem task5_1_1 : ∃ (I : Interpretation sig5_1 (Fin 3)), ∀ β : Assignment
   simp [F₁, EntailsInterpret, I, P, b, f]
 
 -- (2) There is no Σ-model A of P (b) ∧ ¬P (f (f (b))) such that fA (a) = a for every a ∈ UA.
-def F₂ : Formula sig5_1 String := .and (P [b]) (.neg (P [f [f [b]]]))
+def F₂ : Formula sig5_1 String := (P [b]).and (.neg (P [f [f [b]]]))
 theorem task5_1_2 : ¬∃ (univ : Universes) (I : Interpretation sig5_1 univ),
     ∀ β : Assignment String univ, EntailsInterpret I β F₂ ∧
     (∀ a, (I.functions .f) [a] = a):= by
@@ -85,7 +85,7 @@ theorem task5_1_2 : ¬∃ (univ : Universes) (I : Interpretation sig5_1 univ),
 theorem task5_1_3 : ∃ preds, ∀ β, EntailsInterpret (HerbrandInterpretation sig5_1 preds) β F₁ := by
   -- First, let's define our Herbrand interpretation
   -- We need to define how predicates behave on ground terms
-  let preds : sig5_1.preds → List (Term sig5_1 Empty) → Prop := fun p args =>
+  let preds : sig5_1.preds → List (GroundTerm sig5_1) → Prop := fun p args =>
     match p, args with
     | .P, [.func .b []] => True
     | .P, [.func .f [.func .b []]] => False
@@ -100,16 +100,16 @@ theorem task5_1_3 : ∃ preds, ∀ β, EntailsInterpret (HerbrandInterpretation
 -- (4) P(b) ∧ ∀x ¬P(x) has no Herbrand model.
 def F₄ : Formula sig5_1 String := .and (P [b]) (.all "x" (.neg (P [.var "x"])))
 theorem task5_1_4 : ¬∃ preds, ∀ β, EntailsInterpret (HerbrandInterpretation sig5_1 preds) β F₄ := by
-  let b' : Term sig5_1 Empty := Term.func .b []
+  let b' : GroundTerm sig5_1 := Term.func .b []
   intro h
   rcases h with ⟨preds, h⟩
-  let β₀ : Assignment String (Term sig5_1 Empty) := fun _ => b'
+  let β₀ : Assignment String (GroundTerm sig5_1) := fun _ => b'
   have h₀ := h β₀
   have hPb : preds .P [b'] := by
     simp [F₄, P, b] at h₀
     exact h₀.1
   obtain ⟨_, h_forall⟩ := h₀
-  let β₁ : Assignment String (Term sig5_1 Empty) := β₀.modify "x" b'
+  let β₁ : Assignment String (GroundTerm sig5_1) := β₀.modify "x" b'
   have hNotPb : ¬preds .P [b'] := by
     simp [Formula.eval, HerbrandInterpretation, Atom.eval, Term.eval,
           Assignment.modify, Formula.all, β₁] at h_forall
@@ -120,13 +120,13 @@ theorem task5_1_4 : ¬∃ preds, ∀ β, EntailsInterpret (HerbrandInterpretatio
 
 -- (5) ∀x P (f (x)) does not have a Herbrand model with a two-element universe.
 def F₅ : Formula sig5_1 String := .all "x" (P [f [.var "x"]])
-theorem task5_1_5  (S : Set <| Term sig5_1 Empty) (hall : ∀ t : Term sig5_1 Empty, t ∈ S) :
+theorem task5_1_5  (S : Set <| GroundTerm sig5_1) (hall : ∀ t : GroundTerm sig5_1, t ∈ S) :
     Set.encard S ≠ 2 := by
-  let t₀ : Term sig5_1 Empty := .func .b []
-  let t₁ : Term sig5_1 Empty := .func .f [t₀]
-  let t₂ : Term sig5_1 Empty := .func .f [t₁]
-  let t₃ : Term sig5_1 Empty := .func .f [t₂]
-  let S' : Set (Term sig5_1 Empty) := {t₀, t₁, t₂}
+  let t₀ : GroundTerm sig5_1 := .func .b []
+  let t₁ : GroundTerm sig5_1 := .func .f [t₀]
+  let t₂ : GroundTerm sig5_1 := .func .f [t₁]
+  let t₃ : GroundTerm sig5_1 := .func .f [t₂]
+  let S' : Set (GroundTerm sig5_1) := {t₀, t₁, t₂}
   have ht₀ := hall t₀
   have ht₁ := hall t₁
   have ht₂ := hall t₂
@@ -158,10 +158,10 @@ theorem task5_1_6 : ∃! ps,
     ext p args
     cases p
     -- Let's prove that P must be true for all args for preds'
-    have h : ∀ (t : Term sig5_1 Empty), preds' .P [t] := by
+    have h : ∀ (t : GroundTerm sig5_1), preds' .P [t] := by
       intro t
       -- Create an assignment that maps x to t
-      let β : Assignment String (Term sig5_1 Empty) := fun v => Term.func .b []
+      let β : Assignment String (GroundTerm sig5_1) := fun v => Term.func .b []
       -- Use the entailment hypothesis
       have h_entails_β := h_entails β
       -- Extract the universal quantifier's meaning

InferenceInLean/Basic.lean renamed to InferenceInLean/Resolution.lean

@@ -20,8 +20,8 @@ structure Interpretation where
   predicates : sig.preds -> (List univ -> Prop)
 
 @[simp]
-def HerbrandInterpretation (sig : Signature) (preds : sig.preds -> List (Term sig Empty) -> Prop) :
-    Interpretation sig (Term sig Empty) := ⟨fun f args => Term.func f args, preds⟩
+def HerbrandInterpretation (sig : Signature) (preds : sig.preds -> List (GroundTerm sig) -> Prop) :
+    Interpretation sig (GroundTerm sig) := ⟨fun f args => Term.func f args, preds⟩
 
 /- ### Assigments
 > β : X → univ

InferenceInLean/Semantics.lean

@@ -22,6 +22,8 @@ inductive Term where
   | var (x : X)
   | func (f : sig.funs) (args: List Term)
 
+abbrev GroundTerm (sig : Signature) := Term sig Empty
+
 lemma Term.induction {P : (Term sig X) → Prop}
     (base : ∀ x : X, P (var x)) (step : ∀ (args : List (Term sig X)),
       (ih : ∀ term ∈ args, P term) → ∀ (f : sig.funs), P (func f args)) :

InferenceInLean/Syntax.lean

@@ -49,10 +49,6 @@ def MostGeneralUnifier {sig : Signature} {X : Variables} [DecidableEq X]
     (E : EqualityProblem sig X) (σ : Substitution sig X) : Prop :=
   Unifier E σ ∧ (∀ τ : Substitution sig X, Unifier E τ → σ ≤ τ)
 
-/-
-TODO: Add example proof for a mgu.
--/
-
 lemma mgu_imp_unifier {sig : Signature} {X : Variables} [DecidableEq X] (E : EqualityProblem sig X)
     (σ : Substitution sig X) : MostGeneralUnifier E σ → Unifier E σ := fun ⟨h, _⟩ => h