Engine: check a named reading in the kernel, as a table

CLAUDE.md

@@ -141,7 +141,7 @@ back to `sorryAx` — that produces a *successful build*.
 | `Testimony/Bib/` | `Core` types, `Attr` registry attribute, `Works` entries, `Render`, `Registry` guards |
 | `Testimony/Provenance.lean` | `Reference`, `Source`, `Tradition`, `Confidence` |
 | `Testimony/Intertext.lean` | Typed relations between passages |
-| `Testimony/Logic/` | `Basic` formula, `Notation` (`p`/`notP`), `Entail` + countermodels + `Independent`, `Package` arguments + manifests, `Line` lines of reason, `Tactic` (`establish`, Horn-only, and `establish_by_search`/`refute_with`/`satisfied_by`/`leaves_open`/`granted`), `Framework` Dung semantics (grounded, preferred), `Dispute` packages as its nodes, defeat derived from entailment and cited confidence, `Horn` the decision procedure that computes a dispute's defeat table, `Certificate` the search that finds what the kernel checks of it (`horn_certify`), `Solver` the verified solver that computes its verdicts, `Witness` the checked reasons they are stated with, `Verdict` a verdict and its witness as one declaration, rendered from the witness, `Support` one position lending another a premise, `Map` a dispute drawn with its defeats, supports and the attacks support implies, `Because` why one package stands against another, at a checked crux, `Burden` the minimal sets of readings an opponent must reject, complete, `Dilemma` every reading of a rival's ambiguous claim, each answered, `Aif` every dispute as an AIF graph, checked against AIF's Definition 1.1 |
+| `Testimony/Logic/` | `Basic` formula, `Notation` (`p`/`notP`), `Entail` + countermodels + `Independent`, `Package` arguments + manifests, `Line` lines of reason, `Tactic` (`establish`, Horn-only, and `establish_by_search`/`refute_with`/`satisfied_by`/`leaves_open`/`granted`), `ModelCheck` a reading written as a table, checked against every premise by the kernel, `Framework` Dung semantics (grounded, preferred), `Dispute` packages as its nodes, defeat derived from entailment and cited confidence, `Horn` the decision procedure that computes a dispute's defeat table, `Certificate` the search that finds what the kernel checks of it (`horn_certify`), `Solver` the verified solver that computes its verdicts, `Witness` the checked reasons they are stated with, `Verdict` a verdict and its witness as one declaration, rendered from the witness, `Support` one position lending another a premise, `Map` a dispute drawn with its defeats, supports and the attacks support implies, `Because` why one package stands against another, at a checked crux, `Burden` the minimal sets of readings an opponent must reject, complete, `Dilemma` every reading of a rival's ambiguous claim, each answered, `Aif` every dispute as an AIF graph, checked against AIF's Definition 1.1 |
 | `Testimony/Argument.lean` | Criteria, definitions, `Satisfies`, `People` |
 | `Testimony/Semantics/` | `Upper` (DOLCE's categories, each with its BFO counterpart), `Vocabulary`, `Grammar` (a claim's meaning as a term, over concepts, words and particulars), `Ontology` (a meaning taken apart and read under definitions), `Meaning` (`HasMeanings`, `HasJoins`), `Discourse` |
 | `Testimony/Ontology/` | Articles that derive what the vocabulary's words mean — definitions with sources, each shown at work — naming no argument (`Relations`; `Time`, an occurrence lasts one length of time; `Kinds`, each concept's category, or why it has none); `Search`, the generic queries; `Shared`, the definitions every join is read under |

Testimony.lean

@@ -16,6 +16,7 @@ import Testimony.Logic.Notation
 import Testimony.Logic.Entail
 import Testimony.Logic.Package
 import Testimony.Logic.Line
+import Testimony.Logic.ModelCheck
 import Testimony.Logic.Tactic
 import Testimony.Logic.Framework
 import Testimony.Logic.Dispute

Testimony/Logic/ModelCheck.lean

@@ -0,0 +1,180 @@
+import Testimony.Logic.Entail
+
+/-!
+# Testimony.Logic.ModelCheck — a named reading, checked by the kernel
+
+`satisfied_by` and `leaves_open` prove that a premise set has a model by naming
+one: a reading, written as a definition that says of each claim whether it
+holds. They used to prove it by having `simp` unfold the premise list and the
+semantics of every formula in it, which cost a module like the sola fide
+dispute most of its elaboration time.
+
+A reading over an enumeration of claims is a table: each claim is `True` or
+`False`. This module reads the table off the definition at elaboration time, as
+a function to `Bool` (`ModelCheck.tableOf`), with the proof that it agrees with
+the reading claim by claim, built as a term by cases rather than proved goal by
+goal. The kernel then evaluates every premise under the table
+(`holdsB`) with `decide +kernel`. Nothing is trusted that was not before:
+`models_iff_holdsB` proves that a formula holds under the reading exactly when
+it evaluates to `true` under the table, and the kernel checks the table's
+agreement with the reading and every evaluation.
+
+A reading that is not such a table — one defined through another reading, or
+over a type that is not an enumeration — is left to the old recipe, which the
+tactics fall back to.
+-/
+
+namespace Testimony.Logic
+
+variable {α : Type}
+
+/-- Whether a formula holds under a valuation given as a table of `Bool`s. -/
+def holdsB (b : α → Bool) : Formula α → Bool
+  | .atom a => b a
+  | .falsum => false
+  | .and p q => holdsB b p && holdsB b q
+  | .or p q => holdsB b p || holdsB b q
+  | .imp p q => !holdsB b p || holdsB b q
+
+/-- **A formula holds under a reading exactly when it evaluates to `true` under
+the reading's table.** -/
+theorem models_iff_holdsB {w : Valuation α} {b : α → Bool} (hb : ∀ a, w a ↔ b a = true) :
+    ∀ φ : Formula α, w ⊧ φ ↔ holdsB b φ = true
+  | .atom a => by
+    simp only [holdsB, FFL.Propositional.Formula.Boolean.models_atom, hb]
+  | .falsum => by
+    simp only [holdsB, Bool.false_eq_true, iff_false]
+    exact FFL.Semantics.Bot.models_falsum w
+  | .and p q => by
+    have hp := models_iff_holdsB hb p
+    have hq := models_iff_holdsB hb q
+    simp only [holdsB, Bool.and_eq_true, ← hp, ← hq]
+    exact FFL.Semantics.And.models_and
+  | .or p q => by
+    have hp := models_iff_holdsB hb p
+    have hq := models_iff_holdsB hb q
+    simp only [holdsB, Bool.or_eq_true, ← hp, ← hq]
+    exact FFL.Semantics.Or.models_or
+  | .imp p q => by
+    have hp := models_iff_holdsB hb p
+    have hq := models_iff_holdsB hb q
+    refine FFL.Semantics.Imp.models_imply.trans ?_
+    cases e : holdsB b p
+    · simp only [holdsB, e, Bool.not_false, Bool.true_or]
+      exact ⟨fun _ => trivial, fun _ h => absurd (e.symm.trans (hp.mp h)) Bool.false_ne_true⟩
+    · simp only [holdsB, e, Bool.not_true, Bool.false_or]
+      exact ⟨fun h => hq.mp (h (hp.mpr e)), fun h _ => hq.mpr h⟩
+
+/-- Every premise holds under a reading, when each evaluates to `true` under its
+table. -/
+theorem models_all_of_holdsB {w : Valuation α} {b : α → Bool} (hb : ∀ a, w a ↔ b a = true)
+    {prems : List (Formula α)} (h : prems.all (holdsB b) = true) : ∀ φ ∈ prems, w ⊧ φ :=
+  fun φ hφ => (models_iff_holdsB hb φ).mpr (List.all_eq_true.mp h φ hφ)
+
+/-- **Satisfiable, by a reading the kernel checks against every premise.** -/
+theorem satisfiable_of_table {prems : List (Formula α)} (w : Valuation α) (b : α → Bool)
+    (hb : ∀ a, w a ↔ b a = true) (h : prems.all (holdsB b) = true) : Satisfiable prems :=
+  satisfiable_of_model w (models_all_of_holdsB hb h)
+
+/-- **Independent, by two readings the kernel checks**: one satisfying every
+premise and falsifying `φ`, one satisfying every premise and `φ`. -/
+theorem independent_of_tables {prems : List (Formula α)} {φ : Formula α}
+    (wf wt : Valuation α) (bf bt : α → Bool)
+    (hbf : ∀ a, wf a ↔ bf a = true) (hbt : ∀ a, wt a ↔ bt a = true)
+    (h : (prems.all (holdsB bf) && !holdsB bf φ && prems.all (holdsB bt) && holdsB bt φ) = true) :
+    Independent prems φ := by
+  simp only [Bool.and_eq_true, Bool.not_eq_true'] at h
+  obtain ⟨⟨⟨hfs, hff⟩, hts⟩, htt⟩ := h
+  exact independent_of_countermodels wf wt (models_all_of_holdsB hbf hfs)
+    (fun hm => absurd (hff.symm.trans ((models_iff_holdsB hbf φ).mp hm)) Bool.false_ne_true)
+    (models_all_of_holdsB hbt hts) ((models_iff_holdsB hbt φ).mpr htt)
+
+end Testimony.Logic
+
+namespace Testimony.Logic.ModelCheck
+
+open Lean Meta Elab Tactic
+
+/-- **A reading's table**, read off its definition: for a valuation `w` over an
+enumeration, the function to `Bool` that is `true` exactly at the claims where
+`w` reduces to `True`, and the proof, by cases, that the two agree. Fails if the
+atom type is not an enumeration or if the reading does not reduce, at some
+claim, to `True` or `False`. -/
+def tableOf (w : Expr) : MetaM (Expr × Expr) := do
+  let wTy ← whnf (← inferType w)
+  let .forallE _ α _ _ := wTy | throwError "model check: not a valuation"
+  let .const αName [] := α.getAppFn | throwError "model check: the atoms are not an enumeration"
+  let some (.inductInfo ind) := (← getEnv).find? αName
+    | throwError "model check: the atoms are not an inductive type"
+  unless ind.numParams == 0 && ind.numIndices == 0 do
+    throwError "model check: the atoms are not an enumeration"
+  let casesOn := mkConst (αName ++ `casesOn) [Level.one]
+  let casesOnProp := mkConst (αName ++ `casesOn) [Level.zero]
+  let mut bools : Array Expr := #[]
+  let mut proofs : Array Expr := #[]
+  let eqTrue (b : Expr) :=
+    mkApp3 (mkConst ``Eq [Level.one]) (mkConst ``Bool) b (mkConst ``Bool.true)
+  for c in ind.ctors do
+    let some (.ctorInfo ci) := (← getEnv).find? c | throwError "model check: no constructor {c}"
+    unless ci.numFields == 0 do throwError "model check: the atoms are not an enumeration"
+    let v ← whnf (mkApp w (mkConst c))
+    if v.isConstOf ``True then
+      bools := bools.push (mkConst ``Bool.true)
+      proofs := proofs.push <| mkApp4 (mkConst ``iff_of_true) (mkConst ``True)
+        (eqTrue (mkConst ``Bool.true)) (mkConst ``True.intro)
+        (mkApp2 (mkConst ``Eq.refl [Level.one]) (mkConst ``Bool) (mkConst ``Bool.true))
+    else if v.isConstOf ``False then
+      bools := bools.push (mkConst ``Bool.false)
+      proofs := proofs.push <| mkApp4 (mkConst ``iff_of_false) (mkConst ``False)
+        (eqTrue (mkConst ``Bool.false)) (mkConst ``not_false) (mkConst ``Bool.false_ne_true)
+    else
+      throwError "model check: the reading is not a table at {c}"
+  let b := .lam `a α (mkAppN casesOn (#[.lam `_ α (mkConst ``Bool) .default, .bvar 0] ++ bools))
+    .default
+  let motive := .lam `a α (mkApp2 (mkConst ``Iff) (mkApp w (.bvar 0))
+    (eqTrue (mkApp b (.bvar 0)))) .default
+  let hb := .lam `a α (mkAppN casesOnProp (#[motive, .bvar 0] ++ proofs)) .default
+  return (b, hb)
+
+/-- Close the goal with `decide +kernel`, or fail. -/
+def kernelDecide (g : MVarId) : TacticM Unit := do
+  let rest ← Tactic.run g (evalTactic (← `(tactic| decide +kernel)))
+  unless rest.isEmpty do throwError "model check: the kernel did not check the reading"
+
+/-- Apply the theorem `thm` to the goal, its explicit arguments before the last
+given by `given`, in order, and its implicit ones found by unifying its
+conclusion with the goal; the last argument, the evaluation, is checked by the
+kernel. -/
+def applyChecked (thm : Name) (given : Array Expr) : TacticM Unit := do
+  let goal ← getMainGoal
+  let c ← mkConstWithFreshMVarLevels thm
+  let (args, binfos, concl) ← forallMetaTelescopeReducing (← inferType c)
+  let explicit := (args.zip binfos).filter (·.2.isExplicit) |>.map (·.1)
+  unless explicit.size == given.size + 1 do
+    throwError "model check: {thm} takes {explicit.size} arguments"
+  for (m, e) in explicit.zip given do
+    unless ← isDefEq m e do throwError "model check: an argument of {thm} does not fit"
+  unless ← isDefEq concl (← goal.getType) do
+    throwError "model check: {thm} does not prove the goal"
+  let h := explicit[given.size]!
+  goal.assign (mkAppN c args)
+  kernelDecide h.mvarId!
+  replaceMainGoal []
+
+/-- `satisfied_by_table w`: prove `Satisfiable prems` from the reading `w`'s
+table, checked by the kernel against every premise. -/
+elab "satisfied_by_table " v:ident : tactic => do
+  let w ← Term.elabTerm v none
+  let (b, hb) ← tableOf w
+  applyChecked ``satisfiable_of_table #[w, b, hb]
+
+/-- `leaves_open_table wf wt`: prove `Independent prems φ` from the two
+readings' tables, checked by the kernel. -/
+elab "leaves_open_table " vf:ident ppSpace vt:ident : tactic => do
+  let wf ← Term.elabTerm vf none
+  let wt ← Term.elabTerm vt none
+  let (bf, hbf) ← tableOf wf
+  let (bt, hbt) ← tableOf wt
+  applyChecked ``independent_of_tables #[wf, wt, bf, bt, hbf, hbt]
+
+end Testimony.Logic.ModelCheck

Testimony/Logic/Tactic.lean

@@ -1,4 +1,5 @@
 import Testimony.Logic.Line
+import Testimony.Logic.ModelCheck
 import Mathlib.Tactic.Tauto
 
 /-!
@@ -209,19 +210,24 @@ macro_rules
 
 /-- Prove `Satisfiable prems` by naming a valuation that models every premise.
 
-The mirror of `refute_with`: same unfolding recipe, opposite purpose. Where a
-countermodel is the rival's reading written down, a model is the position's
-own — the way things are if it is right. Both are named definitions for the
-same reason, that an inline valuation satisfies the checker and tells a reader
-nothing. -/
+The mirror of `refute_with`, opposite purpose. Where a countermodel is the
+rival's reading written down, a model is the position's own — the way things
+are if it is right. Both are named definitions for the same reason, that an
+inline valuation satisfies the checker and tells a reader nothing.
+
+A reading written as a table — `True` or `False` at each claim — is read off as
+one, and the kernel evaluates every premise under it
+(`Testimony.Logic.ModelCheck`); any other reading is proved by `refute_with`'s
+unfolding recipe, which the bracketed definitions serve. -/
 syntax "satisfied_by" ppSpace ident (ppSpace "[" simpLemma,+ "]")? : tactic
 
 macro_rules
   | `(tactic| satisfied_by $v:ident) =>
     `(tactic| satisfied_by $v [Testimony.Logic.caseOf])
   | `(tactic| satisfied_by $v:ident [$ls,*]) =>
-    `(tactic|
-        (refine Testimony.Logic.satisfiable_of_model $v ?_ <;>
+    `(tactic| first
+      | satisfied_by_table $v
+      | (refine Testimony.Logic.satisfiable_of_model $v ?_ <;>
            simp [$ls,*, $v:ident, Testimony.Logic.caseOf, Testimony.Logic.Line.asPackage,
              Testimony.Logic.Line.premises, Testimony.Logic.Line.onGrounds,
              Testimony.Logic.p, Testimony.Logic.notP,
@@ -245,15 +251,19 @@ one, so they settle nothing either way.*
 
 Two identifiers rather than one, for the same reason `refute_with` takes an
 identifier at all. An independence result is two rival readings of one premise
-set, and both of them are positions someone holds. -/
+set, and both of them are positions someone holds.
+
+Two readings written as tables are checked by the kernel, as `satisfied_by`'s
+are; otherwise the unfolding recipe proves the four halves. -/
 syntax "leaves_open" ppSpace ident ppSpace ident (ppSpace "[" simpLemma,+ "]")? : tactic
 
 macro_rules
   | `(tactic| leaves_open $vf:ident $vt:ident) =>
     `(tactic| leaves_open $vf $vt [Testimony.Logic.caseOf])
   | `(tactic| leaves_open $vf:ident $vt:ident [$ls,*]) =>
-    `(tactic|
-        (refine Testimony.Logic.independent_of_countermodels $vf $vt ?_ ?_ ?_ ?_ <;>
+    `(tactic| first
+      | leaves_open_table $vf $vt
+      | (refine Testimony.Logic.independent_of_countermodels $vf $vt ?_ ?_ ?_ ?_ <;>
            simp [$ls,*, $vf:ident, $vt:ident, Testimony.Logic.caseOf,
              Testimony.Logic.Line.asPackage,
              Testimony.Logic.Line.premises, Testimony.Logic.Line.onGrounds,

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: 2326 definitions, 176 entries
+info: every entry is a tagged definition, and every key names one: 2332 definitions, 176 entries
 -/
 #guard_msgs in
 #check_citations under Testimony

arguments/bench/Engine.lean

@@ -267,6 +267,14 @@ example : ∀ i j, solaFideDispute.partOf i j ↔ partyPartOf i j := by
   refine partOf_iff_of_certified ?_
   cases i <;> cases j <;> horn_certify
 
+#bench "satisfied_by: the Pauline case" in
+example : Satisfiable paulineCase.premises := by
+  satisfied_by criticsReading [solaFideDefs]
+
+#bench "satisfied_by: Trent grants the subjective genitive" in
+example : Grants tridentineCase (notP .pistisChristouObjective) := by
+  satisfied_by trentWithoutDeliveranceReading [Grants, solaFideDefs]
+
 #bench "strengths: James hearing under evidence, 12 parties" in
 example :
     ∀ i, ((jamesRegister.rerated .evidence).node i).strength = ratedStrength .evidence i := by
@@ -304,6 +312,15 @@ example :
 
 end TestimonyArguments.SolaFide
 
+namespace TestimonyArguments.SolaScriptura
+open Testimony Testimony.Logic
+
+#bench "leaves_open: parity leaves the canon open" in
+example : Independent canonUnderParity.premises (p .scriptureIsSoleInfallibleRule) := by
+  leaves_open parityEstablishesNothingReading krugerParityReading [solaScripturaDefs]
+
+end TestimonyArguments.SolaScriptura
+
 /-! ### The checks over every argument -/
 
 #bench (runs := 1) "checks: postulates, every package" in

docs/src/performance.md

@@ -78,6 +78,31 @@ The slowest modules of the arguments' build: `SolaFide.Ratings` (150 s),
 | 6 | Replay a refutation on bitmasks (#180) | the certified defeat tables | 7.21 s, 94 MiB | 5.99 s, 70 MiB | 0.008 | kept |
 | 7 | Find exclusions through shared keys, not every pair | the sola fide joins | 45.4 s, 3.43 GiB | 10.6 s, 1.06 GiB | 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 |
+| 9 | Check a named reading in the kernel, as a table, not by `simp` | `satisfied_by` and `leaves_open` | 1.11 s, 8 MiB | 45 ms, 4 MiB | 0.008 | kept |
+
+Round 9, `scripts/bench-ab.sh` against `main`, five interleaved rounds. A
+profile of the slowest modules after round 6 put most of their elaboration in
+`simp`, and most of that in `satisfied_by`: 46 s of `SolaFide.Dispute`'s,
+serially, and 24 s of `SolaFide.Results`'. Its recipe unfolded the premise list
+and rewrote the semantics of every formula in it, a second for one sola fide
+case. But a reading is a table: each claim `True` or `False`. So the tactic now
+reads the table off the definition, as a function to `Bool` with the proof, by
+cases, that it agrees with the reading, and the kernel evaluates every premise
+under it (`Testimony.Logic.ModelCheck`; `models_iff_holdsB` proves the
+evaluation the semantics). A reading that is not a table falls back to the old
+recipe; none in the arguments or the examples does. A first proof of
+`models_iff_holdsB` used `tauto`, which put `Classical.choice` under every model
+it checked, and the generated pages, which print each theorem's axioms, caught
+it; the proof is now by cases, and the theorems rest on what they did,
+`propext` and `Quot.sound`. The Pauline case's model
+fell from 1.11 s to 45 ms (−96%, p = 0.008), a granted denial of Trent's from
+1.05 s to 46 ms (−96%), and the parity reply's independence from 204 ms to
+15 ms (−93%). Measured by hand, two runs each, the tactic otherwise unchanged:
+`SolaFide.Dispute` elaborates in 35.8 s against 48.4 s, and `SolaFide.Results`
+in 12.6 s against 18.6 s. `refute_with` is left as it is: the refutation check
+counts on its recipe unfolding every definition through the argument's unfold
+set, which is what tells a "not Horn" failure from a definition left folded,
+and a kernel check would unfold them all whether tagged or not.
 
 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