diff --git a/CLAUDE.md b/CLAUDE.md index 59f4ac5..f98680e 100644 --- a/CLAUDE.md +++ b/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 | diff --git a/Testimony.lean b/Testimony.lean index 345dbce..62d2b71 100644 --- a/Testimony.lean +++ b/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 diff --git a/Testimony/Logic/ModelCheck.lean b/Testimony/Logic/ModelCheck.lean new file mode 100644 index 0000000..7b7f673 --- /dev/null +++ b/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 diff --git a/Testimony/Logic/Tactic.lean b/Testimony/Logic/Tactic.lean index 72b953d..71ef7f0 100644 --- a/Testimony/Logic/Tactic.lean +++ b/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, diff --git a/arguments/TestimonyArguments/Checks.lean b/arguments/TestimonyArguments/Checks.lean index 4a39037..cff3c2c 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: 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 diff --git a/arguments/bench/Engine.lean b/arguments/bench/Engine.lean index 1fddca4..44eb650 100644 --- a/arguments/bench/Engine.lean +++ b/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 diff --git a/docs/src/performance.md b/docs/src/performance.md index 42afca6..24f22b1 100644 --- a/docs/src/performance.md +++ b/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 diff --git a/docs/src/style-guide.md b/docs/src/style-guide.md index 7d1bb3c..73fc753 100644 --- a/docs/src/style-guide.md +++ b/docs/src/style-guide.md @@ -194,6 +194,14 @@ while telling a reader nothing. `leaves_open` takes two, in the order of `Independent`'s two halves: first the reading on which the proposition fails, then the reading on which it holds. +**Write a reading as a table.** A reading that says of each claim, by a `match`, +whether it holds — `True` or `False`, with a wildcard for the rest — or that +holds everywhere (`fun _ => True`), is read off as a table, and `satisfied_by` +and `leaves_open` have the kernel evaluate every premise under it +(`Testimony.Logic.ModelCheck`): some 45 ms for a sola fide case, where unfolding +it with `simp` took a second. A reading written any other way, through another +reading or as an equation, still proves what it did, by the slower recipe. + **Prefer `Independent` to a pair of refutations.** When a reply is recorded as "it blocks the objection" and "it establishes nothing" over the *same* premise set, those are the two halves of one independence claim and should be stated as