Merge branch 'generalresolution'

Author: SamuelLess

InferenceInLean/Basic.lean

@@ -105,6 +105,130 @@ def GeneralFactorizationRule [inst : DecidableEq X] (A B : Atom sig X) (C : Clau
     Inference sig X :=
   ⟨{.pos A :: .pos B :: C}, Clause.substitute σ (.pos A :: C), MostGeneralUnifier [(A, B)] σ⟩
 
+lemma validclosed_of_valid [DecidableEq X] {C: Clause sig X} {I : Interpretation sig univ} :
+    ValidIn C.toFormula I → ValidIn C.toClosedFormula I := by
+  intro heval
+  let xs := C.freeVarsList
+  let n := xs.length
+  have hxsnodup : xs.Nodup := by exact nodup_clauseFreeVarsList sig X _
+  have := (@three_three_seven sig X univ _ n C I xs hxsnodup rfl).mpr
+  exact fun β => this heval β
+
+theorem generalResolutionRuleSound [DecidableEq X] (A B : Atom sig X) (C D : Clause sig X)
+    (σ : Substitution sig X) (hmgu : MostGeneralUnifier [(A, B)] σ) :
+    @Entails _ _ univ _
+      (Formula.and
+        (Clause.toClosedFormula sig X (.pos B :: D))
+        (Clause.toClosedFormula sig X (.neg A :: C)))
+      (((D ++ C).substitute σ).toClosedFormula) := by
+  let leftinner : Clause sig X := (.pos B :: D)
+  let rightinner : Clause sig X := (.neg A :: C)
+  let left := Clause.toClosedFormula sig X (.pos B :: D)
+  let right := Clause.toClosedFormula sig X (.neg A :: C)
+  intro I β h_entails
+  simp [Formula.and] at h_entails
+  obtain ⟨hleft, hright⟩ := h_entails
+  have hleftentails : EntailsInterpret I β left := by exact hleft
+  have hrightentails : EntailsInterpret I β right := by exact hright
+  have hleftclosed : Formula.closed left := by
+    exact Clause.closedClause_closed sig X (Literal.pos B :: D)
+  have hrightclosed : Formula.closed right := by
+    exact Clause.closedClause_closed sig X (Literal.neg A :: C)
+  have hleftvalid : ValidIn left I := validIn_of_entails_closed I _ hleftclosed (by use β)
+  have hrightvalid : ValidIn right I := validIn_of_entails_closed I _ hrightclosed (by use β)
+
+  -- ∀z (D ∨ B)σ
+  let leftxs : List X := leftinner.freeVarsList
+  let leftn : ℕ := leftxs.length
+  have hleftxsnodup : leftxs.Nodup := by exact nodup_clauseFreeVarsList sig X leftinner
+
+  let leftys : List X := (leftinner.substitute σ).freeVarsList
+  let leftm : ℕ := leftys.length
+  have hleftysnodup : leftys.Nodup := by exact nodup_clauseFreeVarsList sig X (Clause.substitute σ leftinner)
+
+  have hleft338 := @three_three_eight univ sig X _
+    leftinner I σ leftn leftm leftxs leftys hleftxsnodup rfl hleftysnodup rfl hleftvalid
+
+  --∀z (C ∨ ¬A)σ
+  let rightxs : List X := rightinner.freeVarsList
+  let rightn : ℕ := rightxs.length
+  have hrightxsnodup : rightxs.Nodup := by exact nodup_clauseFreeVarsList sig X rightinner
+
+  let rightys : List X := (rightinner.substitute σ).freeVarsList
+  let rightm : ℕ := rightys.length
+  have hrightysnodup : rightys.Nodup := by
+    exact nodup_clauseFreeVarsList sig X (Clause.substitute σ rightinner)
+
+  have hright338 := @three_three_eight univ sig X _
+    rightinner I σ rightn rightm rightxs rightys hrightxsnodup rfl hrightysnodup rfl hrightvalid
+
+  -- use 3.3.7
+  have hleftinnersub : @ValidIn _ X _ _ (leftinner.substitute σ) I := by
+    exact (three_three_seven leftys.length (Clause.toFormula sig X (Clause.substitute σ leftinner)) I
+            leftys hleftysnodup rfl).mp
+        hleft338
+
+  have hrightinnersub : @ValidIn _ X _ _ (rightinner.substitute σ) I := by
+    exact (three_three_seven rightys.length (Clause.toFormula sig X (Clause.substitute σ rightinner)) I
+            rightys hrightysnodup rfl).mp
+        hright338
+
+  have hDσ_of_negBσ : ∀ β : Assignment X univ, ¬Atom.eval I β (B.substitute σ) →
+      Formula.eval I β (D.substitute σ) := by
+    intro β' hnegatom
+    simp [*] at hleftinnersub
+    unfold leftinner at hleftinnersub
+    have heval_leftinnersub := hleftinnersub β'
+    simp [List.map_cons] at heval_leftinnersub
+    rcases heval_leftinnersub with hBσ | hDσ
+    · simp_all only [Atom.substitute, Atom.pred.injEq, Atom.eval, List.map_map, not_true_eq_false]
+    · exact hDσ
+
+  have hCσ_of_Aσ : ∀ β : Assignment X univ, Atom.eval I β (A.substitute σ) →
+      Formula.eval I β (C.substitute σ) := by
+    intro β' hatom
+    simp [*] at hrightinnersub
+    unfold rightinner at hrightinnersub
+    have heval_rightinnersub := hrightinnersub β'
+    simp [List.map_cons] at heval_rightinnersub
+    rcases heval_rightinnersub with hnAσ | hCσ
+    · simp only [Atom.eval, Atom.substitute, List.map_map, hnAσ] at hatom
+    · exact hCσ
+
+  have hBσeqAσ: ∀ (β : Assignment X univ), Atom.eval I β (A.substitute σ)
+      = Atom.eval I β (B.substitute σ) := by
+    intro β
+    have hunif : A.substitute σ = B.substitute σ := by
+      obtain ⟨hσunif, _⟩ := hmgu
+      simp only [Unifier, EqualityProblem.eq_1, List.mem_singleton, Atom.substitute,
+        Atom.pred.injEq, forall_eq] at hσunif
+      simp only [Atom.substitute, Atom.pred.injEq]
+      exact hσunif
+    rw [hunif]
+
+  have hCDσ : ∀ β' : Assignment X univ, EntailsInterpret I β' (Clause.substitute σ (D ++ C)) := by
+    intro β'
+    by_cases hBσ : Atom.eval I β' (B.substitute σ)
+    · have hAσ : Atom.eval I β' (A.substitute σ) := by
+        rw [hBσeqAσ]
+        exact hBσ
+      have hCσ := hCσ_of_Aσ β' hAσ
+      unfold Clause.substitute at hCσ
+      simp only [EntailsInterpret, Clause.substitute, Clause, List.map_append]
+      generalize List.map (Literal.substitute σ) D = D'
+      generalize List.map (Literal.substitute σ) C = C' at *
+      apply (@eval_append_iff_eval_or sig X univ _ I β' D' C').mpr
+      aesop
+    · have hDσ := hDσ_of_negBσ β' hBσ
+      unfold Clause.substitute at hDσ
+      simp only [EntailsInterpret, Clause.substitute, Clause, List.map_append]
+      generalize List.map (Literal.substitute σ) D = D' at *
+      generalize List.map (Literal.substitute σ) C = C'
+      apply (@eval_append_iff_eval_or sig X univ _ I β' D' C').mpr
+      aesop
+
+  exact validclosed_of_valid hCDσ β
+
 theorem generalResolution_soundness [inst : DecidableEq X] {A B : Atom sig X} {C D : Clause sig X}
     {σ : Substitution sig X} :
     @Soundness _ _ univ _ ([GeneralResolutionRule A B C D σ, GeneralFactorizationRule A B C σ]):= by
@@ -139,10 +263,3 @@ theorem generalResolution_soundness [inst : DecidableEq X] {A B : Atom sig X} {C
     aesop
   next h_fact_rule =>
     sorry
-
-
-/-
-## Further stuff:
-- Compactness
-
--/

InferenceInLean/Semantics.lean

@@ -79,14 +79,7 @@ def Formula.eval {sig : Signature} {X : Variables} {univ : Universes} [Decidable
 
 @[simp]
 lemma Term.eval_without_free_not_term {sig : Signature} {X : Variables} [DecidableEq X]
-    (t : Term sig X) : t.freeVars = {} → ¬∃ (x : X), t = Term.var x := by
-  intro a
-  simp_all only [not_exists]
-  intro x
-  apply Aesop.BuiltinRules.not_intro
-  intro a_1
-  subst a_1
-  simp_all only [Term.freeVars.eq_1, Set.singleton_ne_empty]
+    (t : Term sig X) : t.freeVars = {} → ¬∃ (x : X), t = Term.var x := by aesop
 
 lemma Set.singleton_of_union_empty {α : Type} {x : α} {A B : Set α}
     (h : ¬A = {x}) (hsingleton : A ∪ B = {x}) : A = ∅ := by

InferenceInLean/Syntax.lean

@@ -67,7 +67,7 @@ inductive Atom where
 @[simp]
 def Atom.freeVars {sig : Signature} {X : Variables} : Atom sig X -> Set X
   | .pred _ [] => ∅
-  | .pred P (a :: args) => a.freeVars  ∪ (Atom.pred P args).freeVars
+  | .pred P (a :: args) => a.freeVars ∪ (Atom.pred P args).freeVars
 
 inductive Literal where
   | pos (a : Atom sig X)
@@ -118,6 +118,7 @@ def Formula.freeVars {sig : Signature} {X : Variables} : Formula sig X -> Set X
 @[simp]
 def Formula.closed {sig : Signature} {X : Variables} (F : Formula sig X) : Prop :=
   Formula.freeVars F = ∅
+
 /--
  Creates formula ∀ x_1 ... x_n, F.
 -/
@@ -131,15 +132,102 @@ def Formula.bigForall [DecidableEq X]
 @[simp]
 def Clause.toFormula : Clause sig X -> Formula sig X
   | [] => Formula.falsum
-  | .pos l :: ls => Formula.or (Formula.atom l) (Clause.toFormula ls)
-  | .neg l :: ls => Formula.or (Formula.neg (Formula.atom l)) (Clause.toFormula ls)
+  | .pos l :: ls => (Formula.atom l).or (Clause.toFormula ls)
+  | .neg l :: ls => Formula.or (Formula.atom l).neg (Clause.toFormula ls)
 
 instance : Coe (Clause sig X) (Formula sig X) :=
   ⟨Clause.toFormula sig X⟩
 
 instance : Coe (Set <| Clause sig X) (Set <| Formula sig X) :=
   ⟨fun N => {↑C | C ∈ N}⟩
 
+@[simp]
+def Term.freeVarsList [DecidableEq X] : Term sig X -> List X
+  | Term.var x => [x]
+  | Term.func _ [] => []
+  | Term.func f (a :: args) => List.dedup ((Term.freeVarsList a).append (Term.freeVarsList (Term.func f args)))
+
+@[simp]
+lemma Term.freeVars_sub_freeVarsList [DecidableEq X] (t : Term sig X) :
+    t.freeVars ⊆ (t.freeVarsList).toFinset := by
+  induction' t using Term.induction with x args ih f
+  · aesop
+  · induction args with
+    | nil => aesop
+    | cons head tail ih' =>
+      simp
+      constructor
+      · specialize ih head (by simp)
+        generalize freeVarsList sig X head = Fl at *
+        generalize freeVars sig X head = Fs at *
+        intro x hxinFs
+        simp only [Set.mem_setOf_eq]
+        left
+        exact List.mem_dedup.mp (ih hxinFs)
+      · simp_all only [List.coe_toFinset]
+        intro x hxinfree
+        aesop
+
+def Atom.freeVarsList [DecidableEq X] : Atom sig X -> List X
+  | .pred _ [] => []
+  | .pred P (t :: ts) => List.dedup ((t.freeVarsList).append (Atom.pred P ts).freeVarsList)
+
+def Atom.freeVars_sub_freeVarsList [DecidableEq X] (a : Atom sig X) :
+    a.freeVars ⊆ (a.freeVarsList).toFinset := by
+  simp_all only [List.coe_toFinset]
+  induction a with
+  | pred p args =>
+    induction args with
+    | nil => aesop
+    | cons head tail ih =>
+      simp only [freeVars, Set.union_subset_iff]
+      constructor
+      · have hfree_subset := Term.freeVars_sub_freeVarsList sig X head
+        unfold freeVarsList
+        intro x hxinfree
+        simp_all only [List.coe_toFinset, List.append_eq, List.mem_dedup, List.mem_append, Set.mem_setOf_eq]
+        apply Or.inl
+        apply hfree_subset
+        simp_all only
+      · unfold freeVarsList
+        intro x hxinfree
+        simp_all only [List.coe_toFinset, List.append_eq, List.mem_dedup, List.mem_append, Set.mem_setOf_eq]
+        apply Or.inr
+        apply ih
+        exact hxinfree
+
+def Clause.freeVarsList [DecidableEq X] : Clause sig X -> List X
+  | [] => []
+  | (.pos l) :: ls => List.dedup (l.freeVarsList ++ freeVarsList ls)
+  | (.neg l) :: ls => List.dedup (l.freeVarsList ++ freeVarsList ls)
+
+@[simp]
+lemma nodup_clauseFreeVarsList [DecidableEq X] (C : Clause sig X) :
+    List.Nodup (C.freeVarsList) := by
+  unfold Clause.freeVarsList
+  simp_all only [Clause]
+  split <;> simp_all only [List.nodup_nil, List.nodup_dedup]
+
+@[simp]
+def Clause.toClosedFormula [DecidableEq X] (C : Clause sig X) : Formula sig X :=
+  Formula.bigForall sig X (C.freeVarsList) C
+
+lemma Clause.closedEmpty_closed [DecidableEq X] :
+    Formula.closed (Clause.toClosedFormula sig X []) := by aesop
+
+lemma Clause.consClosed [DecidableEq X] (L : Literal sig X) (C : Clause sig X) :
+    (Clause.toClosedFormula sig X C).closed → (Clause.toClosedFormula sig X (L :: C)).closed := by
+  intro h
+  sorry
+
+theorem Clause.closedClause_closed [DecidableEq X] (C : Clause sig X) :
+    Formula.closed C.toClosedFormula := by
+  induction C with
+  | nil => aesop
+  | cons head tail ih =>
+    simp_all
+    exact Clause.consClosed sig X head tail ih
+
 @[simp]
 def Substitution := X -> Term sig X