Engine: convert each party's position to clauses once per 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`), `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/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`), and each party's position converted once per table (`prepare_clauses`), `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/Checks/Citations.lean

@@ -84,7 +84,7 @@ syntax (name := checkCitationsCmd) "#check_citations" " under " ident : command
 elab_rules : command
   | `(#check_citations under $root) => checkCitations [root.getId]
 
-/-- info: every entry is a tagged definition, and every key names one: 48 definitions, 15 entries -/
+/-- info: every entry is a tagged definition, and every key names one: 49 definitions, 15 entries -/
 #guard_msgs in
 #check_citations under Testimony.Checks.Fixture
 

Testimony/Checks/Fixture.lean

@@ -216,10 +216,13 @@ theorem node_strength : ∀ i, (node i).strength = strength i
   | .minutes => by decide
   | .clock => by decide
 
+prepare_clauses disputeClauses for dispute
+
 /-- Who defeats whom, computed and checked by the kernel. -/
 theorem dispute_defeats : ∀ i j, dispute.defeats i j ↔ defeats i j := by
   intro i j
-  refine Horn.defeats_iff_of_certified (node_strength i) (node_strength j) ?_
+  refine Horn.defeats_iff_of_prepared (node_strength i) (node_strength j)
+    (disputeClauses.spec i) (disputeClauses.spec j) ?_
   cases i <;> cases j <;> horn_certify
 
 /-- The dispute, in the form the solver and the AIF check read. -/

Testimony/Logic/Certificate.lean

@@ -116,6 +116,23 @@ question `Horn.satisfiable_of_certified` asks. -/
 def hintsAppend (index : α → ℕ) (Γ Δ : List (Formula α)) : List Hint :=
   [hintOnAll index (base Γ) Δ]
 
+/-- The base of a list of clauses, already converted: what propagation settled
+from them, and the clauses that fired. -/
+def baseOfClauses (cs : List (Clause α)) : Base α :=
+  let (s, trace) := chainTrace cs (cs.length + 1) ⟨[], []⟩ []
+  ⟨cs, s, trace⟩
+
+/-- **The hints for a cell whose positions are given as clauses**
+(`Horn.defeatsWith?`), in the order `Horn.defeatChecks` asks its questions, as
+`hintsFor` finds them from the packages. -/
+@[nospecialize]
+def hintsWith (index : α → ℕ) (ca cb : Option (List (Clause α))) (b : ArgumentPackage α) :
+    List Hint :=
+  let ba := ca.map baseOfClauses
+  let bb := cb.map baseOfClauses
+  (hintOn index ba b.conclusion :: b.premises.map (hintOn index ba)) ++
+    (stepsOf b.premises).flatMap fun q => [hintOn index bb (∼q.2), hintOn index ba q.2]
+
 /-- **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. -/
@@ -198,6 +215,8 @@ 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 ``Horn.defeatsWith? 9 then
+    mkAppOptM ``Horn.hintsWith #[args[0]!, args[1]!, index, args[4]!, 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
@@ -210,8 +229,9 @@ def searchFor (index lhs : Expr) : MetaM Expr := 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? …`, \
-      `supportsBy? …`, `partOfBy? …` or `Horn.satisfiableAppend? …`, got{indentExpr lhs}"
+    throwError "horn_certify: expected `Horn.defeatsBy? …`, `Horn.defeatsWith? …`, \
+      `Dissent.findingsBy? …`, `supportsBy? …`, `partOfBy? …` or \
+      `Horn.satisfiableAppend? …`, got{indentExpr lhs}"
 
 /-- Prove `∃ index, Function.Injective index ∧ ∃ hints, decision index hints … = v`,
 for a defeat, support or part-of cell or a dissent's findings, or `∃ index hints, … = v` for a
@@ -248,4 +268,95 @@ elab (name := hornCertify) "horn_certify" : tactic => do
   goal.assign <| mkApp4 (.const ``Exists.intro us) indexTy p index body
   replaceMainGoal []
 
+/-! ### Each party's clauses, once
+
+A defeat table asks every cell about two parties' positions as clauses, and
+converting a position is most of what a cell costs the kernel. `prepare_clauses`
+converts each party's position once, at elaboration time, writes the result as a
+literal, and proves for each party that the literal is what the conversion
+gives: the kernel evaluates the conversion once per party, and every cell reads
+the literal. -/
+
+/-- A list of clauses as a term, each atom the constructor at its index. -/
+def clausesExpr (α : Expr) (ctors : Array Name) (cs : List (List ℕ × List ℕ)) :
+    MetaM Expr := do
+  let atom (k : ℕ) : MetaM Expr := do
+    let some c := ctors[k]? | throwError "prepare_clauses: no constructor {k}"
+    return mkConst c
+  let clauseTy := mkApp (mkConst ``Horn.Clause) α
+  let mut out : Array Expr := #[]
+  for (body, heads) in cs do
+    let b ← body.mapM atom
+    let h ← heads.mapM atom
+    out := out.push (mkApp3 (mkConst ``Horn.Clause.mk) α (← mkListLit α b) (← mkListLit α h))
+  mkListLit clauseTy out.toList
+
+/-- `prepare_clauses name for d`: define `name : ι → Option (List (Clause α))`,
+each party's position as clauses, written out, and prove `name_spec : ∀ i,
+clausesOf (d.node i).held = name i`, which the kernel checks once per party. -/
+elab "prepare_clauses " name:ident " for " d:term : command => Command.liftTermElabM do
+  let d ← Term.elabTerm d none
+  Term.synthesizeSyntheticMVarsNoPostponing
+  let d ← instantiateMVars d
+  let dTy ← whnfR (← inferType d)
+  let #[α, inst, ι] := dTy.getAppArgs | throwError "prepare_clauses: not a dispute"
+  let enumCtors (ty : Expr) : MetaM (Name × Array Name) := do
+    let .const n [] := ty | throwError "prepare_clauses: {ty} is not an enumeration"
+    let some (.inductInfo i) := (← getEnv).find? n | throwError "prepare_clauses: {n}?"
+    return (n, i.ctors.toArray)
+  let (ιName, parties) ← enumCtors ι
+  let (_, atoms) ← enumCtors α
+  let αName := α.constName!
+  let optTy := mkApp (mkConst ``Option [Level.zero]) (mkApp (mkConst ``List [Level.zero])
+    (mkApp (mkConst ``Horn.Clause) α))
+  let mut lits : Array Expr := #[]
+  for c in parties do
+    let held := mkApp3 (mkConst ``ArgumentPackage.held) α inst
+      (mkApp (mkApp4 (mkConst ``Dispute.node) α inst ι d) (mkConst c))
+    let cl := mkApp2 (mkConst ``Horn.clausesOf) α held
+    -- Evaluated as constructor indices, a type the evaluator knows.
+    let idx := mkConst (αName ++ `ctorIdx)
+    let toIdx ← withLocalDeclD `c (mkApp (mkConst ``Horn.Clause) α) fun c => do
+      let body ← mkAppM ``List.map #[idx, ← mkAppM ``Horn.Clause.body #[c]]
+      let heads ← mkAppM ``List.map #[idx, ← mkAppM ``Horn.Clause.heads #[c]]
+      mkLambdaFVars #[c] (← mkAppM ``Prod.mk #[body, heads])
+    let mapClauses ← mkAppM ``List.map #[toIdx]
+    let asIdx ← mkAppM ``Option.map #[mapClauses, cl]
+    let v ← unsafe evalExpr (Option (List (List ℕ × List ℕ)))
+      (← inferType asIdx) asIdx
+    let lit ← match v with
+      | some cs => pure (mkApp2 (mkConst ``Option.some [Level.zero])
+          (mkApp (mkConst ``List [Level.zero]) (mkApp (mkConst ``Horn.Clause) α))
+          (← clausesExpr α atoms cs))
+      | none => pure (mkApp (mkConst ``Option.none [Level.zero])
+          (mkApp (mkConst ``List [Level.zero]) (mkApp (mkConst ``Horn.Clause) α)))
+    lits := lits.push lit
+  let defName := (← getCurrNamespace) ++ name.getId
+  let casesOn (motive : Expr) (minors : Array Expr) (i : Expr) (lvl : Level) : Expr :=
+    mkAppN (mkConst (ιName ++ `casesOn) [lvl]) (#[motive, i] ++ minors)
+  let body := Expr.lam `i ι (casesOn (.lam `_ ι optTy .default) lits (.bvar 0) Level.one) .default
+  addAndCompile <| .defnDecl {
+    name := defName, levelParams := [], type := .forallE `i ι optTy .default, value := body,
+    hints := .abbrev, safety := .safe }
+  addDocStringCore defName s!"Each party's position in `{d}`, as clauses, written out once \
+    so that every cell of its defeat table reads them rather than converting the position \
+    again. Generated by `prepare_clauses`; `{defName ++ `spec}` proves it."
+  -- For each party, the conversion reduces to its literal: `Eq.refl`, checked by the kernel.
+  let specTy ← withLocalDeclD `i ι fun i => do
+    let held := mkApp3 (mkConst ``ArgumentPackage.held) α inst
+      (mkApp (mkApp4 (mkConst ``Dispute.node) α inst ι d) i)
+    mkForallFVars #[i] (← mkEq (mkApp2 (mkConst ``Horn.clausesOf) α held)
+      (mkApp (mkConst defName) i))
+  let motive ← withLocalDeclD `i ι fun i => do
+    let held := mkApp3 (mkConst ``ArgumentPackage.held) α inst
+      (mkApp (mkApp4 (mkConst ``Dispute.node) α inst ι d) i)
+    mkLambdaFVars #[i] (← mkEq (mkApp2 (mkConst ``Horn.clausesOf) α held)
+      (mkApp (mkConst defName) i))
+  let proofs ← lits.mapM fun lit => mkEqRefl lit
+  let specVal := Expr.lam `i ι (casesOn motive proofs (.bvar 0) Level.zero) .default
+  addDecl <| .thmDecl {
+    name := defName ++ `spec, levelParams := [], type := specTy, value := specVal }
+  addDocStringCore (defName ++ `spec) s!"Each party's clauses in `{defName}` are what \
+    converting its position gives, checked by the kernel once for each party."
+
 end Testimony.Logic.Certificate

Testimony/Logic/Horn.lean

@@ -887,29 +887,36 @@ def stepRebuts? (index : α → ℕ) (hb ha : Hint) (ca cb : Option (List (Claus
     else none
 
 /-- Every way `a` could defeat `b`: the rebuttal, each premise of `b`, and each
-claim `b`'s steps deliver, each with its hint. -/
-def defeatChecks (index : α → ℕ) (hints : List Hint) (a b : ArgumentPackage α) (s t : ℕ) :
-    List (Option Bool) :=
-  let ca := clausesOf a.held
-  let cb := clausesOf b.held
+claim `b`'s steps deliver, each with its hint, given the clauses of what each
+holds, `ca` and `cb`. -/
+def defeatChecks (index : α → ℕ) (hints : List Hint) (ca cb : Option (List (Clause α)))
+    (b : ArgumentPackage α) (s t : ℕ) : List (Option Bool) :=
   let n := b.premises.length
   (rebuts? index (hintAt hints 0) b ca s t ::
     b.premises.zipIdx.map fun (φ, i) => undermines? index (hintAt hints (i + 1)) b ca s φ) ++
     (stepsOf b.premises).zipIdx.map fun (q, i) =>
       stepRebuts? index (hintAt hints (n + 1 + 2 * i)) (hintAt hints (n + 2 + 2 * i)) ca cb s t
         q.2
 
-/-- Whether `a`, of strength `s`, defeats `b`, of strength `t`, from hints:
-`some true` if any way succeeds, `some false` if every way is shown to fail,
-`none` if some check was on a formula without clauses, or its hint did not
-check, and none succeeded. The checks are made once. -/
-def defeatsBy? (index : α → ℕ) (hints : List Hint) (a b : ArgumentPackage α) (s t : ℕ) :
-    Option Bool :=
-  let checks := defeatChecks index hints a b s t
+/-- Whether `a`, of strength `s`, defeats `b`, of strength `t`, from hints, given
+the clauses of what each holds: `some true` if any way succeeds, `some false` if
+every way is shown to fail, `none` if some check was on a formula without
+clauses, or its hint did not check, and none succeeded. The checks are made
+once. A table converts each party's position once, not once for every cell it
+appears in (`defeats_iff_of_prepared`). -/
+def defeatsWith? (index : α → ℕ) (hints : List Hint) (ca cb : Option (List (Clause α)))
+    (b : ArgumentPackage α) (s t : ℕ) : Option Bool :=
+  let checks := defeatChecks index hints ca cb b s t
   if checks.any (· == some true) then some true
   else if checks.all (· == some false) then some false
   else none
 
+/-- Whether `a`, of strength `s`, defeats `b`, of strength `t`, from hints, each
+position converted to clauses here. -/
+def defeatsBy? (index : α → ℕ) (hints : List Hint) (a b : ArgumentPackage α) (s t : ℕ) :
+    Option Bool :=
+  defeatsWith? index hints (clausesOf a.held) (clausesOf b.held) b s t
+
 /-- Whether `a`, of strength `s`, defeats `b`, of strength `t`, every question
 searched: `defeatsBy?` with no hints. -/
 def defeats? (a b : ArgumentPackage α) (s t : ℕ) : Option Bool :=
@@ -1028,8 +1035,9 @@ theorem defeats_of_defeatsBy? {index : α → ℕ} {hints : List Hint} {a b : Ar
     {s t : ℕ} (hidx : Function.Injective index ∨ hints = []) (hs : a.strength = s)
     (ht : b.strength = t) (h : defeatsBy? index hints a b s t = some true) : Defeats a b := by
   subst hs ht
-  dsimp only [defeatsBy?] at h
-  generalize hc : defeatChecks index hints a b a.strength b.strength = checks at h
+  dsimp only [defeatsBy?, defeatsWith?] at h
+  generalize hc : defeatChecks index hints (clausesOf a.held) (clausesOf b.held) b a.strength
+    b.strength = checks at h
   split at h
   · rename_i hany
     obtain ⟨x, hx, hxt⟩ := List.any_eq_true.mp hany
@@ -1055,8 +1063,9 @@ theorem not_defeats_of_defeatsBy? {index : α → ℕ} {hints : List Hint}
     {a b : ArgumentPackage α} {s t : ℕ} (hs : a.strength = s) (ht : b.strength = t)
     (h : defeatsBy? index hints a b s t = some false) : ¬ Defeats a b := by
   subst hs ht
-  dsimp only [defeatsBy?] at h
-  generalize hc : defeatChecks index hints a b a.strength b.strength = checks at h
+  dsimp only [defeatsBy?, defeatsWith?] at h
+  generalize hc : defeatChecks index hints (clausesOf a.held) (clausesOf b.held) b a.strength
+    b.strength = checks at h
   split at h
   · simp at h
   · split at h
@@ -1138,6 +1147,19 @@ theorem defeats_iff_of_certified {a b : ArgumentPackage α} {s t : ℕ} {P : Pro
   · simp only [hP, decide_false] at h
     exact iff_of_false (not_defeats_of_defeatsBy? hs ht h) hP
 
+/-- **A cell of a defeat table, from hints the kernel checks and each position's
+clauses given.** The clauses are proved once for each party
+(`prepare_clauses`), so a table converts each position once rather than in every
+cell. -/
+theorem defeats_iff_of_prepared {a b : ArgumentPackage α} {s t : ℕ} {P : Prop} [Decidable P]
+    {ca cb : Option (List (Clause α))} (hs : a.strength = s) (ht : b.strength = t)
+    (hca : clausesOf a.held = ca) (hcb : clausesOf b.held = cb)
+    (h : ∃ (index : α → ℕ), Function.Injective index ∧
+      ∃ hints : List Hint, defeatsWith? index hints ca cb b s t = some (decide P)) :
+    Defeats a b ↔ P := by
+  subst hca hcb
+  exact defeats_iff_of_certified hs ht h
+
 end Attacks
 
 end Testimony.Logic.Horn

Testimony/Tools/Pages.lean

@@ -253,7 +253,11 @@ def deriveArgumentBodies (tableName : Ident) (root : Name) : CommandElabM Unit :
       | _ =>
         let some modIdx := env.getModuleIdxFor? n | continue
         let some k := modOrder[env.header.moduleNames[modIdx.toNat]!]? | continue
-        let line := (← findDeclarationRanges? n).map (·.range.pos.line) |>.getD 0
+        -- A declaration with no place in the source was generated by a command
+        -- (`prepare_clauses`'s clauses), machinery for the kernel, not
+        -- something written for a reader.
+        let some ranges ← findDeclarationRanges? n | continue
+        let line := ranges.range.pos.line
         let dname := n.getString!
         let headOf (e : Expr) : Option Name :=
           match e.getAppFn with

arguments/TestimonyArguments/BornOfAVirgin/Dispute.lean

@@ -513,6 +513,8 @@ theorem partyNode_strength : ∀ i, (partyNode i).strength = partyStrength i
   | .motyer => motyerReply_strength
   | .micah => micahParity_strength
 
+prepare_clauses isaiahDisputeClauses for isaiahDispute
+
 /-- **Who defeats whom**, all thirty-six pairs: the critic and the scriptural
 reading defeat each other; each reply defeats the critic; the critic defeats
 Berry and Motyer back, but neither of Postell's counterexamples; nothing
@@ -523,7 +525,8 @@ checked by the kernel; the table is what the computation is checked
 against. -/
 theorem isaiahDispute_defeats : ∀ i j, isaiahDispute.defeats i j ↔ partyDefeats i j := by
   intro i j
-  refine Horn.defeats_iff_of_certified (partyNode_strength i) (partyNode_strength j) ?_
+  refine Horn.defeats_iff_of_prepared (partyNode_strength i) (partyNode_strength j)
+    (isaiahDisputeClauses.spec i) (isaiahDisputeClauses.spec j) ?_
   cases i <;> cases j <;> horn_certify
 
 /-- The dispute in the form the verdict solver computes with. -/