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,16 @@
+<script lang="ts">
+  import { checkNegation } from '@/stores/deduction'
+  import context from '@/context'
+  import type { Space, Property } from '@/types'
+  export let space: Space
+  export let property: Property
+  const { theorems, traits } = context()
+  $: redundant = checkNegation($theorems, space, $traits, property).kind === "contradiction"
+</script>
+
+{#if redundant}
+  <div class="alert alert-warning">
+    This asserted property can be deduced from the other asserted traits for
+    this space.
+  </div>
+{/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>
@@ -71,6 +72,7 @@
   <section class="description-markdown">
     <Source source={meta.description} internal external />
   </section>
+  <Redundancy {space} {property} />
   <h3>References</h3>
   <References references={meta.refs} />
 {:else}

packages/viewer/src/stores/deduction.ts

@@ -18,6 +18,7 @@ import type {
   Traits,
 } from '@/models'
 import { eachTick, read, subscribeUntil } from '@/util'
+import type { Result } from '@pi-base/core'
 
 export type State = {
   checked: Set<number>
@@ -188,3 +189,22 @@ function loadProof(
 
   return result
 }
+
+export function checkNegation(
+  theorems: Theorems,
+  space: Space,
+  traits: Traits,
+  property: Property,
+): Result<number, number> {
+  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]
+      }
+    }),
+  )
+  return deduceTraits(indexTheorems(theorems), map)
+}