From b007cc966b249872b6907715a757a357ed611ec7 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 2 Nov 2026 02:27:04 +0000 Subject: [PATCH] Certify the support and part-of tables `supports?` and `partOf?` were decided by a search the kernel ran, and the part-of table converted a party's premises to clauses afresh for every premise it asked about. Each question now takes a hint, as a defeat cell's does: `supportsBy?` and `partOfBy?` ask their questions through `Horn.satisfiableAppend?`, each party's clauses converted once a cell, and `horn_certify` finds the hints (`Horn.supportHints`, `Horn.partHints`). `supports_iff_of_certified` and `partOf_iff_of_certified` take any index that tells atoms apart and any hints that decide the cell. The searched forms are the same decisions with no hints, and keep their theorems. Every dispute's support and part-of tables are certified: the arguments' and the grits example's. On sola fide's, five interleaved rounds, searched against certified: part of 8.01 s to 5.00 s (-38%, p = 0.008), 131 to 102 MiB; supports 3.37 s to 1.99 s (-41%, p = 0.008), 17 to 13 MiB. The searched forms match main. Ledger round 8; the citation check's pin moves to 2305 definitions, the proofs' auxiliary definitions. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01BC49XsbtehCbmJMavF1K5Q --- Testimony/Logic/Certificate.lean | 30 ++- Testimony/Logic/Support.lean | 253 ++++++++++++++---- .../BornOfAVirgin/Dispute.lean | 8 +- .../BornOfAVirgin/Dispute/Genesis.lean | 8 +- .../BornOfAVirgin/Dispute/Septuagint.lean | 8 +- .../BornOfAVirgin/Dispute/Wegner.lean | 8 +- arguments/TestimonyArguments/Checks.lean | 2 +- .../TestimonyArguments/SolaFide/Dispute.lean | 8 +- .../SolaFide/JesusWords.lean | 8 +- .../SolaScriptura/Dispute.lean | 8 +- .../SpiritBaptism/Dispute.lean | 8 +- arguments/bench/Engine.lean | 24 ++ docs/src/logic.md | 9 +- docs/src/performance.md | 15 ++ examples/TestimonyExamples/Grits/Dispute.lean | 8 +- 15 files changed, 300 insertions(+), 105 deletions(-) diff --git a/Testimony/Logic/Certificate.lean b/Testimony/Logic/Certificate.lean index 339fbc4..1f699cf 100644 --- a/Testimony/Logic/Certificate.lean +++ b/Testimony/Logic/Certificate.lean @@ -1,5 +1,6 @@ import Testimony.Logic.Horn import Testimony.Logic.Credibility +import Testimony.Logic.Support /-! # Testimony.Logic.Certificate — finding what the kernel checks @@ -115,6 +116,21 @@ question `Horn.satisfiable_of_certified` asks. -/ def hintsAppend (index : α → ℕ) (Γ Δ : List (Formula α)) : List Hint := [hintOnAll index (base Γ) Δ] +/-- **The hints for a support cell**, in the order `supportsBy?` asks its +questions: for each claim among `b`'s premises, whether `a`'s conclusion can +hold with its negation. -/ +@[nospecialize] +def supportHints (index : α → ℕ) (a b : ArgumentPackage α) : List Hint := + let ba := base [a.conclusion] + (b.premises.filter (Page.Explanation.isLiteral ·)).map fun φ => hintOnAll index ba [∼φ] + +/-- **The hints for a part-of cell**, in the order `partOfBy?` asks its +questions: for each premise of `b`, whether `a`'s premises entail it. -/ +@[nospecialize] +def partHints (index : α → ℕ) (b a : ArgumentPackage α) : List Hint := + let ba := base a.premises + b.premises.map fun φ => hintOnAll index ba (entailsQuestion φ) + variable [HasPostulates α] /-- **The hints for a dissent's findings**, in the order `Dissent.findingsBy?` @@ -176,25 +192,29 @@ def injectiveFor (index : Expr) : MetaM Expr := do /-- The search that finds a decision's hints, from the decision the goal states: a defeat cell (`Horn.defeatsBy?`), a dissent's findings -(`Dissent.findingsBy?`), or one question of satisfiability -(`Horn.satisfiableAppend?`). -/ +(`Dissent.findingsBy?`), a support or part-of cell (`supportsBy?`, +`partOfBy?`), or one question of satisfiability (`Horn.satisfiableAppend?`). -/ def searchFor (index lhs : Expr) : MetaM Expr := do let args := lhs.getAppArgs if lhs.isAppOfArity ``Horn.defeatsBy? 9 then mkAppOptM ``Horn.hintsFor #[args[0]!, args[1]!, args[2]!, index, args[5]!, args[6]!] else if lhs.isAppOfArity ``Dissent.findingsBy? 6 then mkAppOptM ``Horn.findingsHints #[args[0]!, args[1]!, args[2]!, index, args[5]!] + else if lhs.isAppOfArity ``supportsBy? 6 then + mkAppOptM ``Horn.supportHints #[args[0]!, args[1]!, index, args[4]!, args[5]!] + else if lhs.isAppOfArity ``partOfBy? 6 then + mkAppOptM ``Horn.partHints #[args[0]!, args[1]!, index, args[4]!, args[5]!] else if lhs.isAppOfArity ``Horn.satisfiableAppend? 6 then let base := args[4]! unless base.isAppOfArity ``Horn.clausesOf 2 do throwError "horn_certify: expected the clauses of a list, got{indentExpr base}" mkAppOptM ``Horn.hintsAppend #[args[0]!, args[1]!, index, base.appArg!, args[5]!] else - throwError "horn_certify: expected `Horn.defeatsBy? …`, `Dissent.findingsBy? …` or \ - `Horn.satisfiableAppend? …`, got{indentExpr lhs}" + throwError "horn_certify: expected `Horn.defeatsBy? …`, `Dissent.findingsBy? …`, \ + `supportsBy? …`, `partOfBy? …` or `Horn.satisfiableAppend? …`, got{indentExpr lhs}" /-- Prove `∃ index, Function.Injective index ∧ ∃ hints, decision index hints … = v`, -for a defeat cell or a dissent's findings, or `∃ index hints, … = v` for a +for a defeat, support or part-of cell or a dissent's findings, or `∃ index hints, … = v` for a question of satisfiability, by finding the hints and having the kernel check them. -/ elab (name := hornCertify) "horn_certify" : tactic => do diff --git a/Testimony/Logic/Support.lean b/Testimony/Logic/Support.lean index cd4b82f..270704b 100644 --- a/Testimony/Logic/Support.lean +++ b/Testimony/Logic/Support.lean @@ -14,8 +14,10 @@ another; that one is part of another. `Supports a b` is that relation: `a`'s conclusion entails a **claim** `b` rests on — an atom or a denied atom among `b`'s premises. It is decided by the Horn -engine and checked by the kernel, as defeats are (`supports?`, -`supports_iff_of_supports?`). +engine and checked by the kernel, as defeats are: from hints, a model or a +refutation for each question, which `horn_certify` finds and the kernel checks +(`supportsBy?`, `supports_iff_of_certified`), or by a search the kernel runs +itself (`supports?`). ## Why claims and not steps @@ -56,47 +58,107 @@ section Decide variable [DecidableEq α] -/-- For each claim among `b`'s premises, whether `a`'s conclusion can hold with -its negation: `some false` is an entailment. -/ -def supportChecks (a b : ArgumentPackage α) : List (Formula α × Option Bool) := - (b.premises.filter (Page.Explanation.isLiteral ·)).map fun φ => - (φ, satisfiable? [a.conclusion, ∼φ]) - -/-- **Whether `a` supports `b`**, decided by the engine: `none` when some -claim's check is undecided and none succeeded. -/ -def supports? (a b : ArgumentPackage α) : Option Bool := - if (supportChecks a b).any (·.2 == some false) then some true - else if (supportChecks a b).all (·.2 == some true) then some false +/-! #### Checks, each with a hint + +Both relations ask one question of satisfiability per premise of `b`, and each +question can be given a hint, a model or a refutation, which the kernel checks +in place of a search (`Horn.clausesSatisfiableBy?`). `checksBy` hands the +questions their hints in order, and any question without one is searched. -/ + +/-- One check per formula, each asked with the hint at its position, or with +`search` past the end of the hints. -/ +def checksBy (f : Hint → Formula α → Option Bool) : + List Hint → List (Formula α) → List (Option Bool) + | _, [] => [] + | hs, φ :: φs => f (hs.headD .search) φ :: checksBy f hs.tail φs + +omit [DecidableEq α] in +/-- Every check was asked of one of the formulas, with a hint that is `search` +unless the index tells atoms apart. -/ +theorem mem_checksBy {P : Prop} {f : Hint → Formula α → Option Bool} {hs : List Hint} + {φs : List (Formula α)} {x : Option Bool} (hidx : P ∨ hs = []) (hx : x ∈ checksBy f hs φs) : + ∃ φ ∈ φs, ∃ h, (P ∨ h = .search) ∧ f h φ = x := by + induction φs generalizing hs with + | nil => simp [checksBy] at hx + | cons φ φs ih => + rcases List.mem_cons.mp hx with rfl | hx + · refine ⟨φ, List.mem_cons_self, _, hidx.imp id fun h => ?_, rfl⟩ + subst h; rfl + · obtain ⟨ψ, hψ, h, hh, e⟩ := ih (hs := hs.tail) (hidx.imp id fun h => by subst h; rfl) hx + exact ⟨ψ, List.mem_cons_of_mem _ hψ, h, hh, e⟩ + +omit [DecidableEq α] in +/-- Every formula was asked about, with a hint that is `search` unless the index +tells atoms apart. -/ +theorem checksBy_mem {P : Prop} {f : Hint → Formula α → Option Bool} {hs : List Hint} + {φs : List (Formula α)} {φ : Formula α} (hidx : P ∨ hs = []) (hφ : φ ∈ φs) : + ∃ h, (P ∨ h = .search) ∧ f h φ ∈ checksBy f hs φs := by + induction φs generalizing hs with + | nil => simp at hφ + | cons ψ φs ih => + rcases List.mem_cons.mp hφ with rfl | hφ + · refine ⟨_, hidx.imp id fun h => ?_, List.mem_cons_self⟩ + subst h; rfl + · obtain ⟨h, hh, hm⟩ := ih (hs := hs.tail) (hidx.imp id fun h => by subst h; rfl) hφ + exact ⟨h, hh, List.mem_cons_of_mem _ hm⟩ + +/-- For each claim among `b`'s premises, in order, whether `a`'s conclusion can +hold with its negation, from a hint: `some false` is an entailment. `a`'s +conclusion is converted to clauses once. -/ +def supportChecksBy (index : α → ℕ) (hints : List Hint) (a b : ArgumentPackage α) : + List (Option Bool) := + let ca := clausesOf [a.conclusion] + checksBy (fun h φ => satisfiableAppend? index h ca [∼φ]) hints + (b.premises.filter (Page.Explanation.isLiteral ·)) + +/-- **Whether `a` supports `b`**, decided from hints: `none` when some claim's +check is undecided, or its hint did not check, and none succeeded. -/ +def supportsBy? (index : α → ℕ) (hints : List Hint) (a b : ArgumentPackage α) : Option Bool := + let checks := supportChecksBy index hints a b + if checks.any (· == some false) then some true + else if checks.all (· == some true) then some false else none -theorem supports_of_supports? {a b : ArgumentPackage α} (h : supports? a b = some true) : +/-- **Whether `a` supports `b`**, every question searched: `supportsBy?` with +no hints. -/ +def supports? (a b : ArgumentPackage α) : Option Bool := supportsBy? (fun _ => 0) [] a b + +theorem supports_of_supportsBy? {index : α → ℕ} {hints : List Hint} {a b : ArgumentPackage α} + (hidx : Function.Injective index ∨ hints = []) (e : supportsBy? index hints a b = some true) : Supports a b := by - unfold supports? at h - split at h + dsimp only [supportsBy?] at e + split at e · rename_i hany - obtain ⟨⟨φ, r⟩, hmem, hr⟩ := List.any_eq_true.mp hany - simp only [supportChecks, List.mem_map, List.mem_filter, Prod.mk.injEq] at hmem - obtain ⟨ψ, ⟨hψ, hlit⟩, rfl, rfl⟩ := hmem - have hsat : ¬ Satisfiable ([a.conclusion] ++ [∼ψ]) := - not_satisfiable_of_satisfiable? (by simpa using hr) - exact ⟨ψ, hψ, hlit, entails_iff_not_satisfiable.mpr hsat⟩ - · split at h <;> simp at h - -theorem not_supports_of_supports? {a b : ArgumentPackage α} (h : supports? a b = some false) : + obtain ⟨r, hmem, hr⟩ := List.any_eq_true.mp hany + obtain ⟨φ, hφ, h, hh, rfl⟩ := mem_checksBy hidx hmem + obtain ⟨hφ, hlit⟩ := List.mem_filter.mp hφ + exact ⟨φ, hφ, hlit, entails_iff_not_satisfiable.mpr + (not_satisfiable_of_satisfiableAppend? hh (by simpa using hr))⟩ + · split at e <;> simp at e + +theorem not_supports_of_supportsBy? {index : α → ℕ} {hints : List Hint} + {a b : ArgumentPackage α} (e : supportsBy? index hints a b = some false) : ¬ Supports a b := by - unfold supports? at h - split at h - · simp at h - · split at h + dsimp only [supportsBy?] at e + split at e + · simp at e + · split at e · rename_i hall rintro ⟨φ, hφ, hlit, hent⟩ - have hmem : (φ, satisfiable? [a.conclusion, ∼φ]) ∈ supportChecks a b := by - simp only [supportChecks, List.mem_map, List.mem_filter] - exact ⟨φ, ⟨hφ, hlit⟩, rfl⟩ - have hsat : satisfiable? ([a.conclusion] ++ [∼φ]) = some true := by - simpa using List.all_eq_true.mp hall _ hmem - exact entails_iff_not_satisfiable.mp hent (satisfiable_of_satisfiable? hsat) - · simp at h + obtain ⟨h, -, hmem⟩ := checksBy_mem (f := fun h φ => + satisfiableAppend? index h (clausesOf [a.conclusion]) [∼φ]) (P := True) (.inl trivial) + (List.mem_filter.mpr ⟨hφ, hlit⟩) + exact entails_iff_not_satisfiable.mp hent + (satisfiable_of_satisfiableAppend? (by simpa using List.all_eq_true.mp hall _ hmem)) + · simp at e + +theorem supports_of_supports? {a b : ArgumentPackage α} (h : supports? a b = some true) : + Supports a b := + supports_of_supportsBy? (.inr rfl) h + +theorem not_supports_of_supports? {a b : ArgumentPackage α} (h : supports? a b = some false) : + ¬ Supports a b := + not_supports_of_supportsBy? h /-- **A support table cell, from the engine**: whenever it decides, the relation is exactly what it says. -/ @@ -108,6 +170,20 @@ theorem supports_iff_of_supports? {a b : ArgumentPackage α} {P : Prop} [Decidab · simp only [hP, decide_false] at h exact ⟨fun hs => absurd hs (not_supports_of_supports? h), fun h' => absurd h' hP⟩ +/-- **A support table cell, from hints the kernel checks.** Whichever index +that tells atoms apart, and whichever hints, decide the cell, the answer is +sound. `horn_certify` (`Testimony.Logic.Certificate`) finds them. -/ +theorem supports_iff_of_certified {a b : ArgumentPackage α} {P : Prop} [Decidable P] + (h : ∃ (index : α → ℕ), Function.Injective index ∧ + ∃ hints : List Hint, supportsBy? index hints a b = some (decide P)) : + Supports a b ↔ P := by + obtain ⟨_, hinj, _, h⟩ := h + by_cases hP : P + · simp only [hP, decide_true] at h + exact iff_of_true (supports_of_supportsBy? (.inl hinj) h) hP + · simp only [hP, decide_false] at h + exact iff_of_false (not_supports_of_supportsBy? h) hP + end Decide /-! ### One position as part of another @@ -160,37 +236,84 @@ theorem not_entails_of_entailsCheck {Γ : List (Formula α)} {φ : Formula α} | imp p q => exact fun he => entails_imp_iff.mp he (satisfiable_of_satisfiable? h) | _ => exact fun he => entails_iff_not_satisfiable.mp he (satisfiable_of_satisfiable? h) -/-- For each premise of `b`, whether `a`'s premises entail it. -/ -def partChecks (b a : ArgumentPackage α) : List (Option Bool) := - b.premises.map (entailsCheck a.premises) +/-- What is asked of a list of formulas to learn whether it entails `φ`: for a +step `p → q`, `p` and `q`'s negation, and otherwise `φ`'s negation. The list +entails `φ` when it cannot hold with them. -/ +def entailsQuestion : Formula α → List (Formula α) + | .imp p q => [p, ∼q] + | φ => [∼φ] + +/-- Whether the formulas whose clauses are `base` entail `φ`, from a hint: +`some false` is an entailment. -/ +def entailsCheckBy (index : α → ℕ) (h : Hint) (base : Option (List (Clause α))) + (φ : Formula α) : Option Bool := + satisfiableAppend? index h base (entailsQuestion φ) + +theorem entails_of_entailsCheckBy {index : α → ℕ} {h : Hint} {Γ : List (Formula α)} + {φ : Formula α} (hidx : Function.Injective index ∨ h = .search) + (e : entailsCheckBy index h (clausesOf Γ) φ = some false) : Entails Γ φ := by + have hn := not_satisfiable_of_satisfiableAppend? hidx e + cases φ with + | imp p q => exact entails_imp_iff.mpr hn + | _ => exact entails_iff_not_satisfiable.mpr hn -/-- **Whether `b` is part of `a`**, decided by the engine. -/ -def partOf? (b a : ArgumentPackage α) : Option Bool := - if (partChecks b a).all (· == some false) then some true - else if (partChecks b a).any (· == some true) then some false +theorem not_entails_of_entailsCheckBy {index : α → ℕ} {h : Hint} {Γ : List (Formula α)} + {φ : Formula α} (e : entailsCheckBy index h (clausesOf Γ) φ = some true) : + ¬ Entails Γ φ := by + have hs := satisfiable_of_satisfiableAppend? e + cases φ with + | imp p q => exact fun he => entails_imp_iff.mp he hs + | _ => exact fun he => entails_iff_not_satisfiable.mp he hs + +/-- For each premise of `b`, in order, whether `a`'s premises entail it, from a +hint. `a`'s premises are converted to clauses once. -/ +def partChecksBy (index : α → ℕ) (hints : List Hint) (b a : ArgumentPackage α) : + List (Option Bool) := + let ca := clausesOf a.premises + checksBy (fun h φ => entailsCheckBy index h ca φ) hints b.premises + +/-- **Whether `b` is part of `a`**, decided from hints. -/ +def partOfBy? (index : α → ℕ) (hints : List Hint) (b a : ArgumentPackage α) : Option Bool := + let checks := partChecksBy index hints b a + if checks.all (· == some false) then some true + else if checks.any (· == some true) then some false else none -theorem partOf_of_partOf? {b a : ArgumentPackage α} (h : partOf? b a = some true) : +/-- **Whether `b` is part of `a`**, every question searched: `partOfBy?` with +no hints. -/ +def partOf? (b a : ArgumentPackage α) : Option Bool := partOfBy? (fun _ => 0) [] b a + +theorem partOf_of_partOfBy? {index : α → ℕ} {hints : List Hint} {b a : ArgumentPackage α} + (hidx : Function.Injective index ∨ hints = []) (e : partOfBy? index hints b a = some true) : PartOf b a := by - unfold partOf? at h - split at h + dsimp only [partOfBy?] at e + split at e · rename_i hall intro φ hφ - have hmem := List.mem_map_of_mem (f := entailsCheck a.premises) hφ - exact entails_of_entailsCheck (by simpa using List.all_eq_true.mp hall _ hmem) - · split at h <;> simp at h - -theorem not_partOf_of_partOf? {b a : ArgumentPackage α} (h : partOf? b a = some false) : - ¬ PartOf b a := by - unfold partOf? at h - split at h - · simp at h - · split at h + obtain ⟨h, hh, hmem⟩ := checksBy_mem (f := fun h φ => + entailsCheckBy index h (clausesOf a.premises) φ) hidx hφ + exact entails_of_entailsCheckBy hh (by simpa using List.all_eq_true.mp hall _ hmem) + · split at e <;> simp at e + +theorem not_partOf_of_partOfBy? {index : α → ℕ} {hints : List Hint} {b a : ArgumentPackage α} + (e : partOfBy? index hints b a = some false) : ¬ PartOf b a := by + dsimp only [partOfBy?] at e + split at e + · simp at e + · split at e · rename_i _ hany obtain ⟨r, hr, hr'⟩ := List.any_eq_true.mp hany - obtain ⟨φ, hφ, rfl⟩ := List.mem_map.mp (by simpa [partChecks] using hr) - exact fun hp => not_entails_of_entailsCheck (by simpa using hr') (hp φ hφ) - · simp at h + obtain ⟨φ, hφ, h, -, rfl⟩ := mem_checksBy (P := True) (.inl trivial) hr + exact fun hp => not_entails_of_entailsCheckBy (by simpa using hr') (hp φ hφ) + · simp at e + +theorem partOf_of_partOf? {b a : ArgumentPackage α} (h : partOf? b a = some true) : + PartOf b a := + partOf_of_partOfBy? (.inr rfl) h + +theorem not_partOf_of_partOf? {b a : ArgumentPackage α} (h : partOf? b a = some false) : + ¬ PartOf b a := + not_partOf_of_partOfBy? h /-- **A part-of table cell, from the engine.** -/ theorem partOf_iff_of_partOf? {b a : ArgumentPackage α} {P : Prop} [Decidable P] @@ -201,6 +324,18 @@ theorem partOf_iff_of_partOf? {b a : ArgumentPackage α} {P : Prop} [Decidable P · simp only [hP, decide_false] at h exact ⟨fun hs => absurd hs (not_partOf_of_partOf? h), fun h' => absurd h' hP⟩ +/-- **A part-of table cell, from hints the kernel checks.** -/ +theorem partOf_iff_of_certified {b a : ArgumentPackage α} {P : Prop} [Decidable P] + (h : ∃ (index : α → ℕ), Function.Injective index ∧ + ∃ hints : List Hint, partOfBy? index hints b a = some (decide P)) : + PartOf b a ↔ P := by + obtain ⟨_, hinj, _, h⟩ := h + by_cases hP : P + · simp only [hP, decide_true] at h + exact iff_of_true (partOf_of_partOfBy? (.inl hinj) h) hP + · simp only [hP, decide_false] at h + exact iff_of_false (not_partOf_of_partOfBy? h) hP + end DecidePart namespace Dispute diff --git a/arguments/TestimonyArguments/BornOfAVirgin/Dispute.lean b/arguments/TestimonyArguments/BornOfAVirgin/Dispute.lean index 0ae0287..b740f02 100644 --- a/arguments/TestimonyArguments/BornOfAVirgin/Dispute.lean +++ b/arguments/TestimonyArguments/BornOfAVirgin/Dispute.lean @@ -542,15 +542,15 @@ entailment lends a premise (see `Testimony.Logic.Support`). Every cell is computed by `supports?` and checked by the kernel. -/ theorem isaiahDispute_supports : ∀ i j, ¬ isaiahDispute.supports i j := by intro i j - refine (supports_iff_of_supports? (P := False) ?_).not.mpr id - cases i <;> cases j <;> decide +kernel + refine (supports_iff_of_certified (P := False) ?_).not.mpr id + cases i <;> cases j <;> horn_certify /-- **No case is part of another's** here, in all thirty-six pairs, except each party's own. Every cell is computed by `partOf?` and checked by the kernel. -/ theorem isaiahDispute_partOf : ∀ i j, isaiahDispute.partOf i j ↔ i = j := by intro i j - refine partOf_iff_of_partOf? ?_ - cases i <;> cases j <;> decide +kernel + refine partOf_iff_of_certified ?_ + cases i <;> cases j <;> horn_certify /-- The dispute drawn: who defeats whom. -/ def isaiahMap : ArgumentMap isaiahDispute where diff --git a/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Genesis.lean b/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Genesis.lean index 181535c..7aae5fa 100644 --- a/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Genesis.lean +++ b/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Genesis.lean @@ -241,15 +241,15 @@ premise. Every cell is computed by `supports?` and checked by the kernel. -/ theorem genesisDispute_supports : ∀ i j, genesisDispute.supports i j ↔ genesisPartySupports i j := by intro i j - refine supports_iff_of_supports? ?_ - cases i <;> cases j <;> decide +kernel + refine supports_iff_of_certified ?_ + cases i <;> cases j <;> horn_certify /-- **No case is part of another's** here, in all nine pairs, except each party's own. Every cell is computed by `partOf?` and checked by the kernel. -/ theorem genesisDispute_partOf : ∀ i j, genesisDispute.partOf i j ↔ i = j := by intro i j - refine partOf_iff_of_partOf? ?_ - cases i <;> cases j <;> decide +kernel + refine partOf_iff_of_certified ?_ + cases i <;> cases j <;> horn_certify /-- The dispute drawn: who defeats whom, with no support between the parties. -/ def genesisMap : ArgumentMap genesisDispute where diff --git a/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Septuagint.lean b/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Septuagint.lean index 57780f4..7fb96f8 100644 --- a/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Septuagint.lean +++ b/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Septuagint.lean @@ -580,15 +580,15 @@ by `supports?` and checked by the kernel. -/ theorem septuagintDispute_supports : ∀ i j, septuagintDispute.supports i j ↔ septuagintPartySupports i j := by intro i j - refine supports_iff_of_supports? ?_ - cases i <;> cases j <;> decide +kernel + refine supports_iff_of_certified ?_ + cases i <;> cases j <;> horn_certify /-- **No case is part of another's** here, in all thirty-six pairs, except each party's own. Every cell is computed by `partOf?` and checked by the kernel. -/ theorem septuagintDispute_partOf : ∀ i j, septuagintDispute.partOf i j ↔ i = j := by intro i j - refine partOf_iff_of_partOf? ?_ - cases i <;> cases j <;> decide +kernel + refine partOf_iff_of_certified ?_ + cases i <;> cases j <;> horn_certify /-- The dispute drawn: who defeats whom, and the one support. -/ def septuagintMap : ArgumentMap septuagintDispute where diff --git a/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Wegner.lean b/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Wegner.lean index f71e7b2..22bacc7 100644 --- a/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Wegner.lean +++ b/arguments/TestimonyArguments/BornOfAVirgin/Dispute/Wegner.lean @@ -221,15 +221,15 @@ all nine pairs. Every cell is computed by `supports?` and checked by the kernel. -/ theorem wegnerDispute_supports : ∀ i j, ¬ wegnerDispute.supports i j := by intro i j - refine (supports_iff_of_supports? (P := False) ?_).not.mpr id - cases i <;> cases j <;> decide +kernel + refine (supports_iff_of_certified (P := False) ?_).not.mpr id + cases i <;> cases j <;> horn_certify /-- **No case is part of another's** here, in all nine pairs, except each party's own. Every cell is computed by `partOf?` and checked by the kernel. -/ theorem wegnerDispute_partOf : ∀ i j, wegnerDispute.partOf i j ↔ i = j := by intro i j - refine partOf_iff_of_partOf? ?_ - cases i <;> cases j <;> decide +kernel + refine partOf_iff_of_certified ?_ + cases i <;> cases j <;> horn_certify /-- The dispute drawn: who defeats whom. -/ def wegnerMap : ArgumentMap wegnerDispute where diff --git a/arguments/TestimonyArguments/Checks.lean b/arguments/TestimonyArguments/Checks.lean index 3d4c82f..4a86ff8 100644 --- a/arguments/TestimonyArguments/Checks.lean +++ b/arguments/TestimonyArguments/Checks.lean @@ -101,7 +101,7 @@ The canonical witness #check_refutations under TestimonyArguments using unfoldSets /-- -info: every entry is a tagged definition, and every key names one: 2298 definitions, 176 entries +info: every entry is a tagged definition, and every key names one: 2305 definitions, 176 entries -/ #guard_msgs in #check_citations under Testimony diff --git a/arguments/TestimonyArguments/SolaFide/Dispute.lean b/arguments/TestimonyArguments/SolaFide/Dispute.lean index b896256..d20d2f2 100644 --- a/arguments/TestimonyArguments/SolaFide/Dispute.lean +++ b/arguments/TestimonyArguments/SolaFide/Dispute.lean @@ -987,8 +987,8 @@ support (see `Testimony.Logic.Support`). Every cell is computed by `supports?` and checked by the kernel. -/ theorem solaFideDispute_supports : ∀ i j, ¬ solaFideDispute.supports i j := by intro i j - refine (supports_iff_of_supports? (P := False) ?_).not.mpr id - cases i <;> cases j <;> decide +kernel + refine (supports_iff_of_certified (P := False) ?_).not.mpr id + cases i <;> cases j <;> horn_certify /-- Whose case is part of whose, as a table: besides each party's own, two pairs. -/ @@ -1008,8 +1008,8 @@ only adds to it; and every case is part of itself. Nothing else. Every cell is computed by `partOf?` and checked by the kernel. -/ theorem solaFideDispute_partOf : ∀ i j, solaFideDispute.partOf i j ↔ partyPartOf i j := by intro i j - refine partOf_iff_of_partOf? ?_ - cases i <;> cases j <;> decide +kernel + refine partOf_iff_of_certified ?_ + cases i <;> cases j <;> horn_certify /-- The dispute drawn: who defeats whom, and whose case is part of whose. -/ def solaFideMap : ArgumentMap solaFideDispute where diff --git a/arguments/TestimonyArguments/SolaFide/JesusWords.lean b/arguments/TestimonyArguments/SolaFide/JesusWords.lean index 2746786..2e9d0e6 100644 --- a/arguments/TestimonyArguments/SolaFide/JesusWords.lean +++ b/arguments/TestimonyArguments/SolaFide/JesusWords.lean @@ -575,15 +575,15 @@ all 49 pairs. Every cell is computed by `supports?` and checked by the kernel. -/ theorem jesusWordsDispute_supports : ∀ i j, ¬ jesusWordsDispute.supports i j := by intro i j - refine (supports_iff_of_supports? (P := False) ?_).not.mpr id - cases i <;> cases j <;> decide +kernel + refine (supports_iff_of_certified (P := False) ?_).not.mpr id + cases i <;> cases j <;> horn_certify /-- Each party's case is part of its own and of no other's. Every cell is computed by `partOf?` and checked by the kernel. -/ theorem jesusWordsDispute_partOf : ∀ i j, jesusWordsDispute.partOf i j ↔ i = j := by intro i j - refine partOf_iff_of_partOf? ?_ - cases i <;> cases j <;> decide +kernel + refine partOf_iff_of_certified ?_ + cases i <;> cases j <;> horn_certify /-- The dispute over Jesus' words drawn: who defeats whom. -/ def jesusWordsMap : ArgumentMap jesusWordsDispute where diff --git a/arguments/TestimonyArguments/SolaScriptura/Dispute.lean b/arguments/TestimonyArguments/SolaScriptura/Dispute.lean index 77cedaf..fb10de7 100644 --- a/arguments/TestimonyArguments/SolaScriptura/Dispute.lean +++ b/arguments/TestimonyArguments/SolaScriptura/Dispute.lean @@ -208,8 +208,8 @@ is not support. Every cell is computed by `supports?` and checked by the kernel. -/ theorem mark7Dispute_supports : ∀ i j, ¬ mark7Dispute.supports i j := by intro i j - refine (supports_iff_of_supports? (P := False) ?_).not.mpr id - cases i <;> cases j <;> decide +kernel + refine (supports_iff_of_certified (P := False) ?_).not.mpr id + cases i <;> cases j <;> horn_certify /-- Whose case is part of whose, as a table: besides each party's own, Trent's is part of each reading of it. -/ @@ -227,8 +227,8 @@ reading of it, which only adds to it; and every case is part of itself. Every cell is computed by `partOf?` and checked by the kernel. -/ theorem mark7Dispute_partOf : ∀ i j, mark7Dispute.partOf i j ↔ mark7PartyPartOf i j := by intro i j - refine partOf_iff_of_partOf? ?_ - cases i <;> cases j <;> decide +kernel + refine partOf_iff_of_certified ?_ + cases i <;> cases j <;> horn_certify /-- The dispute over Mark 7 drawn: who defeats whom, and whose case is part of whose. -/ diff --git a/arguments/TestimonyArguments/SpiritBaptism/Dispute.lean b/arguments/TestimonyArguments/SpiritBaptism/Dispute.lean index 0ad8ee3..e4d8209 100644 --- a/arguments/TestimonyArguments/SpiritBaptism/Dispute.lean +++ b/arguments/TestimonyArguments/SpiritBaptism/Dispute.lean @@ -177,15 +177,15 @@ def spiritBaptismFinite : Solver.Finite spiritBaptismDispute.defeats where `supports?` and checked by the kernel. -/ theorem spiritBaptismDispute_supports : ∀ i j, ¬ spiritBaptismDispute.supports i j := by intro i j - refine (supports_iff_of_supports? (P := False) ?_).not.mpr id - cases i <;> cases j <;> decide +kernel + refine (supports_iff_of_certified (P := False) ?_).not.mpr id + cases i <;> cases j <;> horn_certify /-- Each view's case is part of its own and of no other's. Every cell is computed by `partOf?` and checked by the kernel. -/ theorem spiritBaptismDispute_partOf : ∀ i j, spiritBaptismDispute.partOf i j ↔ i = j := by intro i j - refine partOf_iff_of_partOf? ?_ - cases i <;> cases j <;> decide +kernel + refine partOf_iff_of_certified ?_ + cases i <;> cases j <;> horn_certify /-- The dispute over Spirit baptism drawn: who defeats whom. -/ def spiritBaptismMap : ArgumentMap spiritBaptismDispute where diff --git a/arguments/bench/Engine.lean b/arguments/bench/Engine.lean index 3fcb072..b2e350f 100644 --- a/arguments/bench/Engine.lean +++ b/arguments/bench/Engine.lean @@ -241,6 +241,30 @@ example (i : Party) simp only [List.mem_cons, List.not_mem_nil, or_false] at hi rcases hi with rfl | rfl | rfl | rfl | rfl | rfl <;> cases j <;> horn_certify +#bench (runs := 1) "supports: sola fide, 144 cells" in +example : ∀ i j, ¬ solaFideDispute.supports i j := by + intro i j + refine (supports_iff_of_supports? (P := False) ?_).not.mpr id + cases i <;> cases j <;> decide +kernel + +#bench (runs := 1) "supports, certified: sola fide, 144 cells" in +example : ∀ i j, ¬ solaFideDispute.supports i j := by + intro i j + refine (supports_iff_of_certified (P := False) ?_).not.mpr id + cases i <;> cases j <;> horn_certify + +#bench (runs := 1) "part of: sola fide, 144 cells" in +example : ∀ i j, solaFideDispute.partOf i j ↔ partyPartOf i j := by + intro i j + refine partOf_iff_of_partOf? ?_ + cases i <;> cases j <;> decide +kernel + +#bench (runs := 1) "part of, certified: sola fide, 144 cells" in +example : ∀ i j, solaFideDispute.partOf i j ↔ partyPartOf i j := by + intro i j + refine partOf_iff_of_certified ?_ + cases i <;> cases j <;> horn_certify + #bench "strengths: James hearing under evidence, 12 parties" in example : ∀ i, ((jamesRegister.rerated .evidence).node i).strength = ratedStrength .evidence i := by diff --git a/docs/src/logic.md b/docs/src/logic.md index 4043a9e..d9c4b19 100644 --- a/docs/src/logic.md +++ b/docs/src/logic.md @@ -759,14 +759,15 @@ tables of how parties stand together (`Testimony.Logic.Support`). of assuming it. So the critics' case is part of Paul's, and Sanders meets Paul on the history of Second Temple Judaism, where the literature has the dispute. -Both tables are proved like the defeat table, cell by cell, by `supports?` or -`partOf?` and `decide +kernel`: +Both tables are proved like the defeat table, cell by cell, from hints the +kernel checks: `horn_certify` finds a model or a refutation for each question +`supportsBy?` or `partOfBy?` asks, and `decide +kernel` checks them. ```lean theorem solaFideDispute_partOf : ∀ i j, solaFideDispute.partOf i j ↔ partyPartOf i j := by intro i j - refine partOf_iff_of_partOf? ?_ - cases i <;> cases j <;> decide +kernel + refine partOf_iff_of_certified ?_ + cases i <;> cases j <;> horn_certify ``` The page draws the graph, lists the parties by number, and tabulates every diff --git a/docs/src/performance.md b/docs/src/performance.md index 83aad5a..941ad3e 100644 --- a/docs/src/performance.md +++ b/docs/src/performance.md @@ -76,6 +76,21 @@ The slowest modules of the arguments' build: `SolaFide.Ratings` (150 s), | 4 | Certify assessments and consistency; in a hearing, weigh a step's rank only once it is attacked (#183) | the hearings and assessments | 3.08 s, 97 MiB | 0.48 s, 16 MiB | 0.008 | kept | | 5 | Compare a citation by its key and locus, a key checked to name one entry | a hearing's rerated strengths | 2.54 s, 83 MiB | 0.86 s, 25 MiB | 0.008 | kept | | 6 | Replay a refutation on bitmasks (#180) | the certified defeat tables | 7.21 s, 94 MiB | 5.99 s, 70 MiB | 0.008 | kept | +| 8 | Certify the support and part-of tables | sola fide's part-of table | 8.01 s, 131 MiB | 5.00 s, 102 MiB | 0.008 | kept | + +Round 8, measured on one side of a `scripts/bench-ab.sh` run against `main`, +five interleaved rounds, as round 3 was: each of sola fide's two tables of how +parties stand together is benchmarked searched, as before, and certified. Both +were still decided by a search the kernel ran, `supports?` and `partOf?`, and +the part-of table converted a party's premises to clauses afresh for every +premise it asked about. Now each question takes a hint, as a defeat cell's +does (`supportsBy?`, `partOfBy?`), `horn_certify` finds them, and each party's +premises are converted once a cell. The part-of table fell from 8.01 s to +5.00 s (−38%, p = 0.008) and from 131 to 102 MiB; the support table from +3.37 s to 1.99 s (−41%, p = 0.008), 17 to 13 MiB. The searched forms, now the +same decisions with no hints, matched `main` (p ≥ 0.55). Measured by hand, +two runs each: `SolaFide.Dispute` elaborates in 41.5 s against 47.6 s with its +two tables searched. Round 6, `scripts/bench-ab.sh` against `main`, five interleaved rounds. A certified refutation was replayed over lists of settled atoms, each membership diff --git a/examples/TestimonyExamples/Grits/Dispute.lean b/examples/TestimonyExamples/Grits/Dispute.lean index d4342bc..b39fe44 100644 --- a/examples/TestimonyExamples/Grits/Dispute.lean +++ b/examples/TestimonyExamples/Grits/Dispute.lean @@ -184,15 +184,15 @@ def gritsFinite : Solver.Finite gritsDispute.defeats where `supports?` and checked by the kernel. -/ theorem gritsDispute_supports : ∀ i j, ¬ gritsDispute.supports i j := by intro i j - refine (supports_iff_of_supports? (P := False) ?_).not.mpr id - cases i <;> cases j <;> decide +kernel + refine (supports_iff_of_certified (P := False) ?_).not.mpr id + cases i <;> cases j <;> horn_certify /-- Each side's case is part of its own and of no other's. Every cell is computed by `partOf?` and checked by the kernel. -/ theorem gritsDispute_partOf : ∀ i j, gritsDispute.partOf i j ↔ i = j := by intro i j - refine partOf_iff_of_partOf? ?_ - cases i <;> cases j <;> decide +kernel + refine partOf_iff_of_certified ?_ + cases i <;> cases j <;> horn_certify /-- The dispute over the five minutes drawn: who defeats whom. -/ def gritsMap : ArgumentMap gritsDispute where