flag redundant asserted traits

packages/core/src/index.ts

@@ -14,6 +14,7 @@ export {
   disproveFormula,
   proveTheorem,
 } from './Logic/index.js'
+export { type Result } from './Logic/Prover.js'
 export { type Space, SpacePage } from './Space.js'
 export { type Theorem, SerializedTheorem } from './Theorem.js'
 export { type Trait } from './Trait.js'

packages/viewer/src/components/Traits/Redundancy.svelte

@@ -0,0 +1,19 @@
+<script lang="ts">
+  import { checkIfRedundant } from '@/stores/deduction'
+  import context from '@/context'
+  import type { Space, Property } from '@/types'
+  import Table from '../Theorems/Table.svelte'
+  export let space: Space
+  export let property: Property
+  const { theorems, traits } = context()
+  $: result = checkIfRedundant(space, property, $theorems, $traits)
+</script>
+
+{#if result.redundant}
+  <div class="alert alert-warning">
+    <strong>Notice:</strong>
+    This asserted property can be deduced from the other asserted traits for this
+    space, due to the following theorems.
+  </div>
+  <Table theorems={result.theorems} />
+{/if}

packages/viewer/src/components/Traits/Show.svelte

@@ -2,6 +2,8 @@
   import type { Space, Property, Trait, Proof as ProofT } from '@/models'
   import { Icons, Link, References, Source, Typeset } from '@/components/Shared'
   import Proof from './Proof.svelte'
+  import Redundancy from './Redundancy.svelte'
+  import { contributingUrl } from '@/constants'
   export let space: Space
   export let property: Property
   export let trait: Trait | undefined
@@ -36,7 +38,6 @@
         ))[]
       }
     | undefined
-  import { contributingUrl } from '@/constants'
 </script>
 
 <h3>Space S{space.id} | Property P{property.id}</h3>
@@ -73,6 +74,7 @@
   </section>
   <h3>References</h3>
   <References references={meta.refs} />
+  <Redundancy {space} {property} />
 {:else}
   Please consider <a href={contributingUrl}>contributing</a> a proof or disproof
   of this property.

packages/viewer/src/stores/deduction.ts

@@ -188,3 +188,31 @@ function loadProof(
 
   return result
 }
+
+export function checkIfRedundant(
+  space: Space,
+  property: Property,
+  thms: Theorems,
+  traits: Traits,
+): { redundant: boolean; theorems: Theorem[] } {
+  const assertedTraits = traits.forSpace(space).filter(([_, t]) => t.asserted)
+  const map = new Map(
+    assertedTraits.map(([p, t]) => {
+      if (p === property) {
+        return [p.id, !t.value]
+      } else {
+        return [p.id, t.value]
+      }
+    }),
+  )
+  const result = deduceTraits(indexTheorems(thms), map)
+  const redundant = result.kind === 'contradiction'
+  if (!redundant) {
+    const theorems: Theorem[] = []
+    return { redundant, theorems }
+  }
+  const theorems = result.contradiction.theorems
+    .map(t => thms.find(t))
+    .filter(t => t !== null)
+  return { redundant, theorems }
+}