Some clean up and preperation for the last sorry

Author: SamuelLess

InferenceInLean/Basic.lean

@@ -92,19 +92,6 @@ theorem groundResolution_soundness {A : Atom sig Empty} {C D : Clause sig Empty}
 
 /- ### 3.10 General Resolution -/
 
--- TODO: do we need to add that freeVars ∩ freeVars = ∅?
-@[simp]
-def GeneralResolutionRule [inst : DecidableEq X] (A B : Atom sig X) (C D : Clause sig X)
-    (σ : Substitution sig X) :
-    Inference sig X :=
-  ⟨{.neg A :: C, .pos B :: D}, (C ++ D).substitute σ, MostGeneralUnifier [(A, B)] σ⟩
-
-@[simp]
-def GeneralFactorizationRule [inst : DecidableEq X] (A B : Atom sig X) (C : Clause sig X)
-    (σ : Substitution sig X) :
-    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
@@ -114,6 +101,7 @@ lemma validclosed_of_valid [DecidableEq X] {C: Clause sig X} {I : Interpretation
   have := (@three_three_seven sig X univ _ n C I xs hxsnodup rfl).mpr
   exact fun β => this heval β
 
+/- Direct formalization of Proposition 3.10.14 -/
 theorem generalResolutionRuleSound [DecidableEq X] (A B : Atom sig X) (C D : Clause sig X)
     (σ : Substitution sig X) (hmgu : MostGeneralUnifier [(A, B)] σ) :
     @Entails _ _ univ _
@@ -144,7 +132,8 @@ theorem generalResolutionRuleSound [DecidableEq X] (A B : Atom sig X) (C D : Cla
 
   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 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
@@ -164,14 +153,14 @@ theorem generalResolutionRuleSound [DecidableEq X] (A B : Atom sig X) (C D : Cla
 
   -- 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
+    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
+    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
@@ -228,38 +217,3 @@ theorem generalResolutionRuleSound [DecidableEq X] (A B : Atom sig X) (C D : Cla
       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
-  rw [Soundness]
-  intro rule h_rule_general hcond I
-
-  intro β h_premise_true
-  simp_all only [GeneralResolutionRule, Clause, List.append_eq, GeneralFactorizationRule]
-  rw [List.mem_cons, List.mem_singleton] at h_rule_general
-  cases h_rule_general
-  -- proof of resolution rule
-  next h_res_rule =>
-    subst h_res_rule
-    simp only [GeneralResolutionRule] at h_premise_true
-    simp_all only [Clause, GeneralResolutionRule, List.append_eq, Substitution.eq_1,
-      MostGeneralUnifier, Unifier, Equality.eq_1, EqualityProblem.eq_1, List.mem_singleton,
-      forall_eq, MoreGeneral, Set.mem_insert_iff, Set.mem_singleton_iff,
-      EntailsInterpret, forall_eq_or_imp]
-    rcases hcond with ⟨hunif, hmgu⟩
-    repeat rw [← EntailsInterpret] at h_premise_true
-    clear hmgu
-    rw [eval_append_iff_eval_or_subst, Formula.eval]
-    obtain ⟨first, second⟩ := h_premise_true
-    have hclosed : Formula.closed (Clause.toFormula sig X (Literal.neg A :: C)) := sorry
-    have hclosed₂ : Formula.closed (Clause.toFormula sig X (Literal.pos B :: D)) := sorry
-    have s := validIn_of_entails_closed I _ hclosed (by use β)
-    have t := validIn_of_entails_closed I _ hclosed₂ (by use β)
-    apply valid_sub_of_valid _ σ at s
-    apply valid_sub_of_valid _ σ at t
-    specialize s β
-    specialize t β
-    aesop
-  next h_fact_rule =>
-    sorry

InferenceInLean/Semantics.lean

@@ -159,8 +159,6 @@ lemma Assignment.eval_closed_term {sig : Signature} {X : Variables} {I : Interpr
       rw [ih]
     rw [← hargsareequal]
 
-#check Term.subterms_closed
-
 @[simp]
 lemma Assignment.eval_term_with_one_free {univ : Universes} {sig : Signature} {X : Variables}
     {I : Interpretation sig univ} [DecidableEq X] {t : Term sig X}
@@ -184,27 +182,6 @@ lemma Assignment.eval_term_with_one_free {univ : Universes} {sig : Signature} {X
         · exact a
     rw [hargsareequal]
 
-/- @[simp]
-def Term.eval_without_free {sig : Signature} {X : Variables} [DecidableEq X] (t : Term sig X) :
-    t.freeVars = {} → ∀ (f : sig.funs) (args : List (Term sig X)),
-      t = Term.func f args → args = [] := by
-  intro hclosed f args heq
-  by_contra harg
-  induction' t using Term.induction with x args ih f generalizing args
-  · sorry
-  ·
-    simp_all only [imp_false, not_not, Term.func.injEq]
-    obtain ⟨left, right⟩ := heq
-    subst left right
-    apply harg
-    have hex : ∃ (t : Term sig X), t ∈ args := List.exists_mem_of_ne_nil args harg
-    rcases hex with ⟨arg, harg⟩
-    specialize ih (Term.func f args)
-    have h : ∀ term ∈ args,
-      Term.freeVars sig X term = ∅ → ∀ (args : List (Term sig X)), term = Term.func f args := sorry
-    specialize ih h -/
-
-
 lemma List.reduce_to_empty {α β: Type} {xs : List α} {as : List β}
     (hlen : xs.length = as.length) (hzero : as.length = 0 ∨ xs.length = 0) : xs = [] ∧ as = [] := by
   simp_all only [List.length_eq_zero, or_self, and_true, List.length_nil]
@@ -286,19 +263,6 @@ lemma Assignment.bigModify_add_nondup {X : Variables} {univ : Universes} [Decida
     ((β.bigModify xs as).modify x a) x = a := by
   simp_all only [modify, ↓reduceIte]
 
-#check List.drop
-/- lemma Assignment.bigModify_nodup_erase {X : Variables} {univ : Universes} [DecidableEq X]
-    (β : Assignment X univ) (xs : List X) (_huniq : xs.Nodup) (as : List univ)
-    (_hlen : xs.length = as.length) (x : X) (a : univ) (_hx : x ∈ xs)
-    (i : ℕ) (hiinbounds : i < xs.length) (hi : xs[i] = x) (ha : as[i] = a) :
-    ∀ (y : X), β.bigModify (xs.eraseIdx i) (as.eraseIdx i) y = if x == y then β x -/
-#check List.Nodup.erase
-/- lemma Assignment.bigModify_add_nondup {X : Variables} {univ : Universes} [DecidableEq X]
-    (β : Assignment X univ) (xs : List X) (_huniq : xs.Nodup) (as : List univ)
-    (_hlen : xs.length = as.length) (x : X) (a : univ) (_hx : x ∈ xs) :
-    (i : ℕ) (hi : xs[i] = x) (a' : univ) (ha : as[i] = a')
-    (bigModify (xs.dropIdx i) (as.dropIdx i)).modify x a = β := by sorry -/
-
 -- y ∉ [x1, ..., xn] → β[x1 ↦ a1, ..., xn ↦ an] y = β y
 @[simp]
 lemma Assignment.bigModify_nonmem {X : Variables} {univ : Universes} [DecidableEq X]
@@ -566,7 +530,6 @@ lemma Atom.eval_of_many_free {univ : Universes} {sig : Signature} {X : Variables
     exact heval
   rw [hargsareequal]
 
-#check Term.freeVars
 lemma Formula.eval_of_many_free {univ : Universes} {sig : Signature} {X : Variables}
     [inst : DecidableEq X] (I : Interpretation sig univ) (F : Formula sig X) (xs : List X)
     (as : List univ) (hlen : xs.length = as.length)

InferenceInLean/Syntax.lean

@@ -61,6 +61,21 @@ def Term.freeVars : Term sig X -> Set X
   | .func _ [] => ∅
   | .func f (a :: args) => Term.freeVars a ∪ Term.freeVars (Term.func f args)
 
+lemma Term.arg_subset_of_freeVars {sig : Signature} {X : Variables}
+    [_inst : DecidableEq X] (args : List (Term sig X)) (f : sig.funs) :
+    ∀ (arg : Term sig X) (_harg : arg ∈ args),
+    Term.freeVars sig X arg ⊆ Term.freeVars sig X (Term.func f args) := by
+  intro arg harg
+  induction' args with arg' args ih
+  · simp_all only [List.not_mem_nil]
+  · simp only [List.mem_cons] at harg
+    rcases harg with harg | harg
+    · subst harg
+      simp_all only [Term.freeVars.eq_3, Set.subset_union_left]
+    · specialize ih harg
+      rw [Term.freeVars]
+      exact Set.subset_union_of_subset_right ih (Term.freeVars sig X arg')
+
 inductive Atom where
   | pred (p : sig.preds) (args : List (Term sig X))
 
@@ -145,7 +160,8 @@ instance : Coe (Set <| Clause sig X) (Set <| Formula sig X) :=
 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)))
+  | 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) :
@@ -181,17 +197,16 @@ def Atom.freeVars_sub_freeVarsList [DecidableEq X] (a : Atom sig X) :
     | nil => aesop
     | cons head tail ih =>
       simp only [freeVars, Set.union_subset_iff]
-      constructor
+      unfold freeVarsList
+      constructor <;> intro x hxinfree
       · 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]
+        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]
+      · 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
@@ -399,24 +414,3 @@ theorem idempotent_iff_inter_empty {sig : Signature} {X : Variables} [BEq X] [BE
       rw [Substitution.compose]
       refine Substitution.id_of_free_not_in_domain σ (σ x) ?_
       aesop
-
-/-
-Maybe continue with?
-3.3 LEMMA If a is an idempotent substitution and z is an arbitrary substitution, then a is
-more general than z iff za = z.
--/
-
-lemma Term.arg_subset_of_freeVars {sig : Signature} {X : Variables}
-    [_inst : DecidableEq X] (args : List (Term sig X)) (f : sig.funs) :
-    ∀ (arg : Term sig X) (_harg : arg ∈ args),
-    Term.freeVars sig X arg ⊆ Term.freeVars sig X (Term.func f args) := by
-  intro arg harg
-  induction' args with arg' args ih
-  · simp_all only [List.not_mem_nil]
-  · simp only [List.mem_cons] at harg
-    rcases harg with harg | harg
-    · subst harg
-      simp_all only [Term.freeVars.eq_3, Set.subset_union_left]
-    · specialize ih harg
-      rw [Term.freeVars]
-      exact Set.subset_union_of_subset_right ih (Term.freeVars sig X arg')