Move seperate examples from exercises

Also added notion of Herbrand Interpretations, looking forward to seeing if they are easy to work with...

Author: SamuelLess

InferenceInLean/Exercises.lean InferenceInLean/Examples.leanInferenceInLean/Exercises.lean renamed to InferenceInLean/Examples.lean

@@ -125,98 +125,3 @@ theorem setEntails_iff_union_not_unsat' [inst : DecidableEq X]
     intro I β hgstrue
     specialize hunsat I β
     aesop
-
-
-/- ## Exercise 4 -/
-
-namespace Exercise4
-
-/- ### Exercise 4-1 -/
-
-inductive fs where | b | c | d | f deriving BEq
-inductive ps where | P
-def F : Formula ⟨fs, ps⟩ String := .and (.and (.and (.atom (.pred .P [.func .b []]))
-  (.atom (.pred .P [.func .c []])))
-  (.neg (.atom (.pred .P [.func .d []]))))
-  (.neg (.ex "x" (.atom (.pred .P [.func .f [.func .f [.var "x"]]]))))
-
-theorem ex_4_1 : ∃ I : Interpretation ⟨fs, ps⟩ (Fin 2), ∃ β : Assignment String (Fin 2),
-    Formula.eval I β F := by
-  let I : Interpretation ⟨fs, ps⟩ (Fin 2) := ⟨
-    fun g a => if g == .f || g == .d then 1 else 0,
-    fun _ u => if u[0]! == 0 then True else False⟩
-  use I
-  use (fun _ => 0)
-  simp [I, F]
-  have : fs.f == fs.f := rfl
-  aesop
-
-
-/-
-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.
--/
-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 Exercise4