Joins: find exclusions through shared keys, not every pair

Testimony/Semantics/Meaning.lean

@@ -108,13 +108,203 @@ def pairsOf {β : Type} : List β → List (β × β)
   | x :: xs => xs.map (x, ·) ++ pairsOf xs
 
 /-- **Every pair of claims whose meanings exclude each other**, under a given
-ontology: `(a, b)`, with `a` listed before `b`, when the two meanings, read for
-what their words mean, cannot both be held. -/
-def exclusionsUnder [DecidableEq α] (O : Ontology) : List (α × α) :=
+ontology, by definition: `(a, b)`, with `a` listed before `b`, when the two
+meanings, read for what their words mean, cannot both be held. Every pair is
+checked; `exclusionsUnder` computes the same list through shared keys. -/
+def exclusionsByPairs [DecidableEq α] (O : Ontology) : List (α × α) :=
   let shaped := (all : List α).map fun a => (a, Ontology.closed O (means a))
   (pairsOf shaped).filterMap fun ((a, s), (b, t)) =>
     if a ≠ b && Ontology.excludes O s t then some (a, b) else none
 
+/-! #### Exclusions through shared keys
+
+Two coherent meanings clash only where they share a key
+(`Testimony.Semantics.Ontology.shares_of_clash`): a fact, or a thing a relation
+is about. So the claims are taken from the last to the first, each against an
+index from every key to the later claims that hold it, and each claim is
+checked only against the claims it shares a key with. A pair sharing nothing is
+never compared, which is almost every pair: checking all of them was what made
+an argument's joins dear, quadratic in its claims and each check a comparison
+of whole facts. The list found is the definition's, pair for pair and in the
+same order (`exclusionsUnder_eq`). -/
+
+/-- An index from keys to the claims holding them. -/
+abbrev KeyIndex (α : Type) := List (Ontology.Key × List α)
+
+/-- The claims the index holds under a key. -/
+def KeyIndex.find : KeyIndex α → Ontology.Key → List α
+  | [], _ => []
+  | (k', as) :: rest, k => if k' = k then as else KeyIndex.find rest k
+
+/-- The index with one more claim under a key. -/
+def KeyIndex.add : KeyIndex α → Ontology.Key → α → KeyIndex α
+  | [], k, a => [(k, [a])]
+  | (k', as) :: rest, k, a =>
+    if k' = k then (k', a :: as) :: rest else (k', as) :: KeyIndex.add rest k a
+
+omit [HasMeanings α] in
+theorem KeyIndex.find_add (ix : KeyIndex α) (k k' : Ontology.Key) (a : α) :
+    KeyIndex.find (KeyIndex.add ix k a) k' =
+      if k = k' then a :: KeyIndex.find ix k' else KeyIndex.find ix k' := by
+  induction ix with
+  | nil => by_cases h : k = k' <;> simp [KeyIndex.add, KeyIndex.find, h]
+  | cons e rest ih =>
+    obtain ⟨k'', as⟩ := e
+    by_cases h₁ : k'' = k
+    · subst h₁
+      by_cases h₂ : k'' = k' <;> simp [KeyIndex.add, KeyIndex.find, h₂]
+    · by_cases h₂ : k'' = k'
+      · subst h₂
+        simp [KeyIndex.add, KeyIndex.find, h₁, Ne.symm h₁]
+      · simp [KeyIndex.add, KeyIndex.find, h₁, h₂, ih]
+
+omit [HasMeanings α] in
+theorem KeyIndex.mem_find_foldl_add (ks : List Ontology.Key) (a b : α) (k : Ontology.Key) :
+    ∀ ix : KeyIndex α, b ∈ KeyIndex.find (ks.foldl (fun ix k => KeyIndex.add ix k a) ix) k ↔
+      b ∈ KeyIndex.find ix k ∨ (k ∈ ks ∧ b = a) := by
+  induction ks with
+  | nil => simp
+  | cons k₀ ks ih =>
+    intro ix
+    rw [List.foldl_cons, ih, KeyIndex.find_add]
+    by_cases h : k₀ = k
+    · subst h; simp only [if_true, List.mem_cons, true_or, true_and]; tauto
+    · simp only [h, if_false, List.mem_cons]
+      constructor
+      · rintro (h' | ⟨hk, rfl⟩)
+        · exact .inl h'
+        · exact .inr ⟨.inr hk, rfl⟩
+      · rintro (h' | ⟨hk | hk, rfl⟩)
+        · exact .inl h'
+        · exact absurd hk.symm h
+        · exact .inr ⟨hk, rfl⟩
+
+/-- The exclusions among a list of claims, each with its meaning read under the
+ontology, and the index of the coherent ones by key: the claims from the last
+to the first, each checked against the later claims it shares a key with. Each
+meaning is read once, before the walk, and not once for every pair. -/
+def exclusionsGo [DecidableEq α] (O : Ontology) :
+    List (α × Shape) → List (α × α) × KeyIndex α
+  | [] => ([], [])
+  | (a, s) :: ys =>
+    match exclusionsGo O ys with
+    | (acc, ix) =>
+      let c := Ontology.coherent O s
+      let ks := Ontology.keysOf s
+      let near := if c then ks.flatMap (KeyIndex.find ix) else []
+      let found := ys.filterMap fun (b, t) =>
+        if near.contains b && a ≠ b && Ontology.clash O (s.lits ++ t.lits) (s.nogoods ++ t.nogoods)
+        then some (a, b) else none
+      (found ++ acc, if c then ks.foldl (fun ix k => KeyIndex.add ix k a) ix else ix)
+
+/-- Each claim with its meaning read under the ontology. -/
+def shapedUnder (O : Ontology) (xs : List α) : List (α × Shape) :=
+  xs.map fun a => (a, Ontology.closed O (means a))
+
+theorem mem_find_exclusionsGo [DecidableEq α] (O : Ontology) (k : Ontology.Key) (b : α) :
+    ∀ xs : List α, b ∈ KeyIndex.find (exclusionsGo O (shapedUnder O xs)).2 k ↔
+      b ∈ xs ∧ Ontology.coherent O (Ontology.closed O (means b)) = true ∧
+        k ∈ Ontology.keysOf (Ontology.closed O (means b))
+  | [] => by simp [shapedUnder, exclusionsGo, KeyIndex.find]
+  | a :: xs => by
+    have ih := mem_find_exclusionsGo O k b xs
+    simp only [shapedUnder, List.map_cons, exclusionsGo] at ih ⊢
+    split
+    · rename_i hc
+      rw [KeyIndex.mem_find_foldl_add, ih]
+      constructor
+      · rintro (⟨hb, hcb, hkb⟩ | ⟨hk, rfl⟩)
+        · exact ⟨List.mem_cons_of_mem _ hb, hcb, hkb⟩
+        · exact ⟨List.mem_cons_self, hc, hk⟩
+      · rintro ⟨hb, hcb, hkb⟩
+        rcases List.mem_cons.mp hb with rfl | hb
+        · exact .inr ⟨hkb, rfl⟩
+        · exact .inl ⟨hb, hcb, hkb⟩
+    · rename_i hc
+      rw [ih]
+      constructor
+      · rintro ⟨hb, hcb, hkb⟩
+        exact ⟨List.mem_cons_of_mem _ hb, hcb, hkb⟩
+      · rintro ⟨hb, hcb, hkb⟩
+        rcases List.mem_cons.mp hb with rfl | hb
+        · exact absurd hcb (by simpa using hc)
+        · exact ⟨hb, hcb, hkb⟩
+
+theorem exclusionsGo_fst [DecidableEq α] (O : Ontology) : ∀ xs : List α,
+    (exclusionsGo O (shapedUnder O xs)).1 =
+      (pairsOf (shapedUnder O xs)).filterMap
+        fun ((a, s), (b, t)) => if a ≠ b && Ontology.excludes O s t then some (a, b) else none
+  | [] => rfl
+  | a :: xs => by
+    have ih := exclusionsGo_fst O xs
+    have hmem := fun k b => mem_find_exclusionsGo O k b xs
+    rcases h : exclusionsGo O (shapedUnder O xs) with ⟨acc, ix⟩
+    rw [h] at ih hmem
+    simp only at ih hmem
+    have hcons : shapedUnder O (a :: xs) = (a, Ontology.closed O (means a)) :: shapedUnder O xs :=
+      rfl
+    rw [hcons]
+    simp only [exclusionsGo, h, pairsOf, List.filterMap_append, List.filterMap_map, ← ih]
+    simp only [shapedUnder, List.filterMap_map]
+    congr 1
+    apply List.filterMap_congr
+    intro b hb
+    simp only [Function.comp_apply, Ontology.excludes]
+    by_cases hca : Ontology.coherent O (Ontology.closed O (means a)) = true
+    · by_cases hcb : Ontology.coherent O (Ontology.closed O (means b)) = true
+      · have hnear : ((Ontology.keysOf (Ontology.closed O (means a))).flatMap
+            (KeyIndex.find ix)).contains b =
+            (Ontology.keysOf (Ontology.closed O (means a))).any
+              (· ∈ Ontology.keysOf (Ontology.closed O (means b))) := by
+          apply Bool.eq_iff_iff.mpr
+          simp only [List.contains_iff_mem, List.mem_flatMap, List.any_eq_true, decide_eq_true_eq,
+            hmem]
+          constructor
+          · rintro ⟨k, hk, -, -, hkb⟩; exact ⟨k, hk, hkb⟩
+          · rintro ⟨k, hk, hkb⟩; exact ⟨k, hk, hb, hcb, hkb⟩
+        simp only [hca, hcb, if_true, hnear, Bool.true_and]
+        by_cases hcl : Ontology.clash O ((Ontology.closed O (means a)).lits ++
+            (Ontology.closed O (means b)).lits) ((Ontology.closed O (means a)).nogoods ++
+            (Ontology.closed O (means b)).nogoods) = true
+        · have hsa : Ontology.clash O (Ontology.closed O (means a)).lits
+              (Ontology.closed O (means a)).nogoods = false := by
+            simp only [Ontology.coherent, Bool.and_eq_true, Bool.not_eq_true'] at hca; exact hca.2
+          have hsb : Ontology.clash O (Ontology.closed O (means b)).lits
+              (Ontology.closed O (means b)).nogoods = false := by
+            simp only [Ontology.coherent, Bool.and_eq_true, Bool.not_eq_true'] at hcb; exact hcb.2
+          obtain ⟨k, hk, hkb⟩ := Ontology.shares_of_clash hsa hsb hcl
+          have : (Ontology.keysOf (Ontology.closed O (means a))).any
+              (· ∈ Ontology.keysOf (Ontology.closed O (means b))) = true :=
+            List.any_eq_true.mpr ⟨k, hk, by simpa using hkb⟩
+          simp only [this, hcl, Bool.true_and, Bool.and_true]
+        · simp only [Bool.not_eq_true] at hcl
+          simp [hcl]
+      · simp only [Bool.not_eq_true] at hcb
+        have hnear : ((Ontology.keysOf (Ontology.closed O (means a))).flatMap
+            (KeyIndex.find ix)).contains b = false := by
+          apply Bool.eq_false_iff.mpr
+          intro hc
+          obtain ⟨k, -, hk⟩ := List.mem_flatMap.mp (List.contains_iff_mem.mp hc)
+          obtain ⟨-, hcb', -⟩ := (hmem k b).mp hk
+          simp [hcb] at hcb'
+        simp only [hca, if_true, hnear, hcb, Bool.false_and, Bool.and_false, Bool.false_eq_true,
+          if_false]
+    · simp only [Bool.not_eq_true] at hca
+      simp [hca]
+
+/-- **Every pair of claims whose meanings exclude each other**, under a given
+ontology: `(a, b)`, with `a` listed before `b`, when the two meanings, read for
+what their words mean, cannot both be held. Computed through shared keys, and
+the same list as the definition, `exclusionsByPairs` (`exclusionsUnder_eq`). -/
+def exclusionsUnder [DecidableEq α] (O : Ontology) : List (α × α) :=
+  (exclusionsGo O (shapedUnder O (all : List α))).1
+
+/-- **The exclusions through shared keys are the exclusions**, pair for pair and
+in the same order. -/
+theorem exclusionsUnder_eq [DecidableEq α] (O : Ontology) :
+    exclusionsUnder (α := α) O = exclusionsByPairs O :=
+  exclusionsGo_fst O _
+
 /-- **Every pair of claims whose meanings entail one another**, under a given
 ontology: `(a, b)` when the meaning of `a`, read for what its words mean,
 asserts everything the meaning of `b` does. -/

Testimony/Semantics/Ontology.lean

@@ -297,6 +297,106 @@ for what its words mean, every literal of the other and every nogood. -/
 def entails (O : Ontology) (s t : Shape) : Bool :=
   coherent O s && t.read && t.lits.all s.lits.contains && t.nogoods.all s.nogoods.contains
 
+/-! ### Where two meanings can meet
+
+Two meanings can clash only where they touch. A literal meets its negation in
+the same fact; a definition's rule (**only**, **functional**) relates two facts
+about the same thing; a nogood is completed by the other meaning's literal.
+So a meaning's **keys** are the facts of its literals and nogoods, and the
+things its relations are about, and two coherent meanings that share no key
+cannot clash (`shares_of_clash`). A claim is then checked only against the
+claims it shares a key with, found through an index of keys, rather than
+against every claim (`Testimony.Semantics.HasMeanings.exclusionsUnder`). -/
+
+/-- Where a meaning can meet another: a fact, or a thing a relation is about. -/
+inductive Key
+  /-- A fact a literal affirms or denies. -/
+  | fact (f : Fact)
+  /-- A thing a relation is about. -/
+  | term (t : Term)
+deriving DecidableEq
+
+/-- The keys of one fact: itself, and the things it relates, if a relation. -/
+def factKeys : Fact → List Key
+  | f@(.rel _ a b) => [.fact f, .term a, .term b]
+  | f => [.fact f]
+
+/-- **The keys of a meaning**: those of every fact it affirms or denies, and of
+every fact in its nogoods. -/
+def keysOf (s : Shape) : List Key :=
+  s.lits.flatMap (fun l => factKeys l.fact) ++ s.nogoods.flatMap (·.map fun l => Key.fact l.fact)
+
+theorem fact_mem_factKeys (f : Fact) : Key.fact f ∈ factKeys f := by
+  cases f <;> simp [factKeys]
+
+theorem mem_keysOf_of_lit {s : Shape} {l : Lit} {k : Key} (hl : l ∈ s.lits)
+    (hk : k ∈ factKeys l.fact) : k ∈ keysOf s := by
+  simp only [keysOf, List.mem_append, List.mem_flatMap]
+  exact .inl ⟨l, hl, hk⟩
+
+theorem mem_keysOf_of_nogood {s : Shape} {n : List Lit} {x : Lit} (hn : n ∈ s.nogoods)
+    (hx : x ∈ n) : Key.fact x.fact ∈ keysOf s := by
+  simp only [keysOf, List.mem_append, List.mem_flatMap, List.mem_map]
+  exact .inr ⟨n, hn, x, hx, rfl⟩
+
+/-- A definition's rule makes two literals clash only when their relations are
+about one same thing. -/
+theorem shares_of_clashes {a : Axiom} {l m : Lit} (h : a.clashes l m = true) :
+    ∃ t, Key.term t ∈ factKeys l.fact ∧ Key.term t ∈ factKeys m.fact := by
+  unfold Axiom.clashes at h
+  split at h
+  · rename_i _ _ _ _ b _ _ d
+    simp only [Bool.and_eq_true, beq_iff_eq, bne_iff_ne, ne_eq] at h
+    obtain ⟨⟨⟨-, -⟩, hbd⟩, -⟩ := h
+    exact ⟨b, by simp [factKeys], by simp [factKeys, hbd]⟩
+  · rename_i _ _ a _ _ c _
+    simp only [Bool.and_eq_true, beq_iff_eq, bne_iff_ne, ne_eq] at h
+    obtain ⟨⟨⟨-, -⟩, hac⟩, -⟩ := h
+    exact ⟨a, by simp [factKeys], by simp [factKeys, hac]⟩
+  · simp at h
+
+/-- **Two coherent meanings that clash share a key.** A clash between them is
+a literal and its negation, two literals a rule sets against each other, or a
+nogood of one completed by the other; none of these is inside one meaning alone,
+since each is coherent, so each joins the two, at a fact or at a thing their
+relations are about. -/
+theorem shares_of_clash {O : Ontology} {s t : Shape} (hs : clash O s.lits s.nogoods = false)
+    (ht : clash O t.lits t.nogoods = false)
+    (h : clash O (s.lits ++ t.lits) (s.nogoods ++ t.nogoods) = true) :
+    ∃ k ∈ keysOf s, k ∈ keysOf t := by
+  simp only [clash, Bool.or_eq_false_iff, Bool.or_eq_true, List.any_eq_false, List.any_eq_true,
+    List.all_eq_true, List.contains_iff_mem, List.mem_append, Bool.not_eq_true] at hs ht h
+  obtain ⟨⟨hs₁, hs₂⟩, hs₃⟩ := hs
+  obtain ⟨⟨ht₁, ht₂⟩, ht₃⟩ := ht
+  rcases h with (⟨l, hl, hn⟩ | ⟨l, hl, m, hm, d, hd, hc⟩) | ⟨n, hn, hall⟩
+  · -- a literal and its negation
+    rcases hl with hl | hl <;> rcases hn with hn | hn
+    · exact absurd (by simpa using hn) (hs₁ l hl)
+    · exact ⟨_, mem_keysOf_of_lit hl (fact_mem_factKeys _),
+        mem_keysOf_of_lit hn (fact_mem_factKeys _)⟩
+    · exact ⟨_, mem_keysOf_of_lit hn (fact_mem_factKeys _),
+        mem_keysOf_of_lit hl (fact_mem_factKeys _)⟩
+    · exact absurd (by simpa using hn) (ht₁ l hl)
+  · -- a rule setting two literals against each other
+    obtain ⟨u, hu₁, hu₂⟩ := shares_of_clashes hc
+    rcases hl with hl | hl <;> rcases hm with hm | hm
+    · exact absurd ⟨m, hm, d, hd, hc⟩ (hs₂ l hl)
+    · exact ⟨_, mem_keysOf_of_lit hl hu₁, mem_keysOf_of_lit hm hu₂⟩
+    · exact ⟨_, mem_keysOf_of_lit hm hu₂, mem_keysOf_of_lit hl hu₁⟩
+    · exact absurd ⟨m, hm, d, hd, hc⟩ (ht₂ l hl)
+  · -- a nogood completed across the two
+    rcases hn with hn | hn
+    · obtain ⟨x, hx, hxs⟩ : ∃ x ∈ n, x ∉ s.lits :=
+        Classical.byContradiction fun hno =>
+          hs₃ n hn fun x hx => Classical.byContradiction fun hxs => hno ⟨x, hx, hxs⟩
+      have hxt : x ∈ t.lits := (hall x hx).resolve_left hxs
+      exact ⟨_, mem_keysOf_of_nogood hn hx, mem_keysOf_of_lit hxt (fact_mem_factKeys _)⟩
+    · obtain ⟨x, hx, hxt⟩ : ∃ x ∈ n, x ∉ t.lits :=
+        Classical.byContradiction fun hno =>
+          ht₃ n hn fun x hx => Classical.byContradiction fun hxt => hno ⟨x, hx, hxt⟩
+      have hxs : x ∈ s.lits := (hall x hx).resolve_right hxt
+      exact ⟨_, mem_keysOf_of_lit hxs (fact_mem_factKeys _), mem_keysOf_of_nogood hn hx⟩
+
 end Ontology
 
 end Testimony.Semantics

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: 2319 definitions, 176 entries
 -/
 #guard_msgs in
 #check_citations under Testimony

arguments/bench/Engine.lean

@@ -33,6 +33,8 @@ The benchmarks, from the smallest unit up:
   arguments' own tables are proved; and a row of a hearing, where every party's
   inferences are re-rated under a standard, with the parties' re-rated strengths;
 - **a verdict**: the solver's checked witness for each of the two disputes;
+- **the joins**: the exclusions among sola fide's 111 claims, read for what
+  their words mean;
 - **an assessment** and **a rating**: Miller's dissent, searched and
   certified, and the laws' step;
 - **`establish`** on a package, the tactic every package's soundness uses;
@@ -255,6 +257,10 @@ example (j : JamesParty) :
     (rerated_strength .evidence .trentOnTheWord) (rerated_strength .evidence j) ?_
   cases j <;> horn_certify
 
+#bench (runs := 1) "joins: sola fide exclusions, 111 claims" in
+example : (Testimony.Semantics.HasMeanings.exclusions (α := Claim)).length = 6 := by
+  decide +kernel
+
 #bench "verdict: sola fide, only Paul's word unanswered" in
 example : Verdict solaFideDispute where
   finite := solaFideFinite