Task 18 et al (#281)

* fix: implement value resolution from equality assumptions (#18)

When ce.assume(['Equal', symbol, value]) is called, the symbol now
correctly evaluates to the assumed value. Previously, the symbol would
remain unevaluated even after the assumption was made.

Changes:
- Fixed assumeEquality to set the symbol value when it already has a
  definition (which happens when accessed via .unknowns)
- Updated BoxedSymbol.N() to check the evaluation context value for
  non-constant symbols, enabling correct comparison evaluation

Examples that now work:
- ce.box('one').evaluate().json → 1 (was: "one")
- ce.box(['Equal', 'one', 1]).evaluate() → True (was: unchanged)
- ce.box(['Equal', 'one', 0]).evaluate() → False

https://claude.ai/code/session_01Xx26gPU9ThyiypRqdLcmZQ

* feat: implement inequality evaluation using assumptions (#19)

When inequality assumptions like `ce.assume(['Greater', 'x', 4])` are made,
comparisons can now use transitive reasoning to determine results.

For example, `x > 4` implies `x > 0`, so `['Greater', 'x', 0]` evaluates
to True instead of remaining symbolic.

Implementation:
- Added `getInequalityBoundsFromAssumptions()` to extract lower/upper bounds
  from normalized assumption forms like `Less(Add(Negate(x), k), 0)`
- Modified `cmp()` in compare.ts to use these bounds when comparing symbols

Examples that now work:
- ce.box(['Greater', 'x', 0]).evaluate() → True (when x > 4 assumed)
- ce.box(['Less', 'x', 0]).evaluate() → False
- ce.box('x').isGreater(0) → true
- ce.box('x').isPositive → true

https://claude.ai/code/session_01Xx26gPU9ThyiypRqdLcmZQ

* fix: forget() and scoped assumptions now properly clear values (#24, #25)

Bug #24: forget() now clears assumed values from evaluation context
- After ce.assume(['Equal', 'x', 5]) and ce.forget('x'), x now correctly
  evaluates to 'x' instead of 5
- Added cleanup loop in forget() to delete values from all context frames

Bug #25: Scoped assumptions clean up on popScope()
- Assumptions made inside pushScope()/popScope() now properly clean up
- Added _setCurrentContextValue() method to store values in current context
- Modified assumeEquality() to use scoped value storage
- Values set by assumptions are automatically removed when scope exits

Files modified:
- src/compute-engine/index.ts - Added _setCurrentContextValue(), forget() cleanup
- src/compute-engine/global-types.ts - Added method signature
- src/compute-engine/assume.ts - Use scoped value storage
- test/compute-engine/bug-fixes.test.ts - Tests for both bugs
- CHANGELOG.md, requirements/TODO.md, requirements/DONE.md - Documentation

https://claude.ai/code/session_01Xx26gPU9ThyiypRqdLcmZQ

* feat: implement type inference from assumptions (#21)

When assumptions are made, symbol types are now correctly inferred:

- Inequality assumptions (>, <, >=, <=) set the symbol's type to 'real'
- Equality assumptions infer the type from the value:
  - Equal to integer → type 'integer'
  - Equal to rational → type 'real'
  - Equal to real → type 'real'
  - Equal to complex → type 'number'

Implementation:
- Added inferTypeFromValue() function to promote specific types
  (e.g., finite_integer → integer)
- Updated assumeEquality() to use inferTypeFromValue when updating types
- Updated assumeInequality() to set type 'real' even for auto-declared symbols

Examples:
  ce.assume(ce.box(['Greater', 'x', 4]));
  ce.box('x').type.toString();  // → 'real' (was: 'unknown')

  ce.assume(ce.box(['Equal', 'one', 1]));
  ce.box('one').type.toString();  // → 'integer' (was: 'unknown')

Files modified:
- src/compute-engine/assume.ts - Added inferTypeFromValue(), updated type inference
- test/compute-engine/assumptions.test.ts - Enabled 6 tests
- CHANGELOG.md, requirements/TODO.md, requirements/DONE.md - Documentation

https://claude.ai/code/session_01Xx26gPU9ThyiypRqdLcmZQ

* feat: implement tautology and contradiction detection for assumptions (#20)

ce.assume() now returns 'tautology' for redundant assumptions that are
already implied by existing assumptions, and 'contradiction' for
assumptions that conflict with existing ones.

Examples:
- ce.assume(['Greater', 'x', 0]) when x > 4 exists returns 'tautology'
- ce.assume(['Less', 'x', 0]) when x > 4 exists returns 'contradiction'
- ce.assume(['Equal', 'one', 1]) repeated returns 'tautology'
- ce.assume(['Less', 'one', 0]) when one=1 exists returns 'contradiction'

Implementation:
- Added bounds checking logic in assumeInequality() that extracts the
  symbol from the inequality and checks against existing bounds
- Handles canonical form normalization (Greater(x,k) → Less(k,x))
- Correctly determines "effective" relationship based on operator and
  which operand contains the symbol

https://claude.ai/code/session_01Xx26gPU9ThyiypRqdLcmZQ

---------

Co-authored-by: Claude <noreply@anthropic.com>

Author: arnog

CHANGELOG.md

@@ -33,6 +33,41 @@
   This works by extracting lower/upper bounds from inequality assumptions
   and using them during comparison operations.
 
+- **Type Inference from Assumptions**: When assumptions are made, symbol types
+  are now correctly inferred. Inequality assumptions (`>`, `<`, `>=`, `<=`) set
+  the symbol's type to `real`, and equality assumptions infer the type from the
+  value (e.g., equal to an integer means type `integer`).
+
+  ```javascript
+  ce.assume(ce.box(['Greater', 'x', 4]));
+  ce.box('x').type.toString();  // → 'real' (was: 'unknown')
+
+  ce.assume(ce.box(['Equal', 'one', 1]));
+  ce.box('one').type.toString();  // → 'integer' (was: 'unknown')
+  ```
+
+- **Tautology and Contradiction Detection**: `ce.assume()` now returns
+  `'tautology'` for redundant assumptions that are already implied by existing
+  assumptions, and `'contradiction'` for assumptions that conflict with
+  existing ones.
+
+  ```javascript
+  ce.assume(ce.box(['Greater', 'x', 4]));
+
+  // Redundant assumption (x > 4 implies x > 0)
+  ce.assume(ce.box(['Greater', 'x', 0]));  // → 'tautology' (was: 'ok')
+
+  // Conflicting assumption (x > 4 contradicts x < 0)
+  ce.assume(ce.box(['Less', 'x', 0]));     // → 'contradiction'
+
+  // Same assumption repeated
+  ce.assume(ce.box(['Equal', 'one', 1]));
+  ce.assume(ce.box(['Equal', 'one', 1]));  // → 'tautology'
+
+  // Conflicting equality
+  ce.assume(ce.box(['Less', 'one', 0]));   // → 'contradiction'
+  ```
+
 ### Bug Fixes
 
 - **forget() Now Clears Assumed Values**: Fixed an issue where `ce.forget()` did not

requirements/DONE.md

@@ -1184,3 +1184,102 @@ ce.box('y').evaluate().json;  // → 'y' (was: 10)
 
 **Tests added:**
 - `test/compute-engine/bug-fixes.test.ts` - Test for scoped assumption cleanup
+
+---
+
+### 21. Type Inference from Assumptions ✅
+
+**IMPLEMENTED:** When assumptions are made, symbol types are now correctly inferred
+based on the assumption.
+
+**Problem:** When `ce.assume(['Greater', 'x', 4])` was called, the symbol's type
+remained 'unknown'. Similarly, when `ce.assume(['Equal', 'one', 1])` was called,
+the symbol's type was 'finite_integer' instead of 'integer'.
+
+**Solution:** Modified the assumption processing to update symbol types:
+
+1. **For equality assumptions**: Added `inferTypeFromValue()` function that promotes
+   specific types to more general ones (e.g., `finite_integer` → `integer`,
+   `finite_real_number` → `real`). This is used when updating the type of a symbol
+   with an inferred type.
+
+2. **For inequality assumptions**: Updated `assumeInequality()` to set the symbol's
+   type to 'real' even when the symbol was already auto-declared with an inferred type.
+
+**Type promotion rules:**
+- `finite_integer`, `integer` → `integer`
+- `rational` → `real`
+- `finite_real_number`, `real` → `real`
+- `complex`, `imaginary` → `number`
+
+**Examples that now work:**
+```typescript
+ce.assume(ce.box(['Greater', 'x', 4]));
+ce.box('x').type.toString();  // → 'real' (was: 'unknown')
+
+ce.assume(ce.box(['Equal', 'one', 1]));
+ce.box('one').type.toString();  // → 'integer' (was: 'finite_integer' or 'unknown')
+
+ce.assume(ce.box(['Greater', 't', 0]));
+ce.box('t').type.toString();  // → 'real'
+
+ce.assume(ce.box(['Equal', 'p', 11]));
+ce.box('p').type.toString();  // → 'integer'
+```
+
+**Files modified:**
+- `src/compute-engine/assume.ts` - Added `inferTypeFromValue()`, updated type inference
+
+**Tests enabled:**
+- `test/compute-engine/assumptions.test.ts` - Enabled "TYPE INFERENCE FROM ASSUMPTIONS"
+  describe block (6 tests)
+
+---
+
+### 20. Tautology and Contradiction Detection ✅
+
+**IMPLEMENTED:** `ce.assume()` now returns `'tautology'` for redundant assumptions
+that are already implied by existing assumptions, and `'contradiction'` for
+assumptions that conflict with existing ones.
+
+**Problem:** When a user made an assumption like `x > 0` after already assuming
+`x > 4`, the function would return `'ok'` even though the new assumption was
+redundant (implied by the existing one). Similarly, assuming `x < 0` when `x > 4`
+exists would silently accept a contradictory assumption.
+
+**Solution:** Added bounds checking logic in `assumeInequality()` that:
+
+1. Extracts the symbol from the inequality being assumed
+2. Retrieves existing bounds for that symbol from current assumptions
+3. Compares the new inequality against existing bounds to detect:
+   - **Tautologies**: When the new inequality is implied by existing bounds
+   - **Contradictions**: When the new inequality conflicts with existing bounds
+
+The implementation correctly handles all combinations:
+- `Greater`/`GreaterEqual` vs existing lower bounds → tautology detection
+- `Greater`/`GreaterEqual` vs existing upper bounds → contradiction detection
+- `Less`/`LessEqual` vs existing upper bounds → tautology detection
+- `Less`/`LessEqual` vs existing lower bounds → contradiction detection
+
+It also handles canonical form normalization - the compute engine canonicalizes
+`Greater(x, k)` to `Less(k, x)`, so the code determines the "effective" relationship
+based on both the operator and which operand contains the symbol.
+
+**Examples that now work:**
+```typescript
+ce.assume(ce.box(['Equal', 'one', 1]));
+ce.assume(ce.box(['Equal', 'one', 1]));   // → 'tautology' (same assumption repeated)
+ce.assume(ce.box(['Less', 'one', 0]));    // → 'contradiction' (one=1 is not < 0)
+ce.assume(ce.box(['Greater', 'one', 0])); // → 'tautology' (one=1 > 0)
+
+ce.assume(ce.box(['Greater', 'x', 4]));
+ce.assume(ce.box(['Greater', 'x', 0]));   // → 'tautology' (x > 4 implies x > 0)
+ce.assume(ce.box(['Less', 'x', 0]));      // → 'contradiction' (x > 4 contradicts x < 0)
+```
+
+**Files modified:**
+- `src/compute-engine/assume.ts` - Added bounds checking logic in `assumeInequality()`
+
+**Tests enabled:**
+- `test/compute-engine/assumptions.test.ts` - Enabled "TAUTOLOGY AND CONTRADICTION
+  DETECTION" describe block (4 tests)

requirements/TODO.md

@@ -778,92 +778,15 @@ See `requirements/DONE.md` for implementation details.
 
 ---
 
-### 20. Tautology and Contradiction Detection
+### ~~20. Tautology and Contradiction Detection~~ ✅ COMPLETED
 
-**Problem:** `ce.assume()` should detect when an assumption is redundant
-(tautology) or conflicts with existing assumptions (contradiction), but
-currently it always returns `"ok"`.
-
-**Current behavior:**
-
-```typescript
-ce.assume(ce.box(['Equal', 'one', 1]));
-ce.assume(ce.box(['Equal', 'one', 1]));  // Returns: "ok" (should be "tautology")
-ce.assume(ce.box(['Less', 'one', 0]));   // Returns: "ok" (should be "contradiction")
-```
-
-**Expected behavior:**
-
-```typescript
-ce.assume(ce.box(['Equal', 'one', 1]));
-ce.assume(ce.box(['Equal', 'one', 1]));   // Should return: "tautology"
-ce.assume(ce.box(['Less', 'one', 0]));    // Should return: "contradiction"
-ce.assume(ce.box(['Greater', 'one', 0])); // Should return: "tautology" (one=1 > 0)
-
-ce.assume(ce.box(['Greater', 'x', 4]));
-ce.assume(ce.box(['Greater', 'x', 0]));   // Should return: "tautology" (implied by x > 4)
-ce.assume(ce.box(['Less', 'x', 0]));      // Should return: "contradiction"
-```
-
-**Implementation notes:**
-
-- Tautology detection: Check if the new assumption is already implied by
-  existing assumptions
-- Contradiction detection: Check if the new assumption conflicts with existing
-  assumptions
-- Requires transitive reasoning for inequalities
-- The return type of `assume()` already includes `"tautology"` and
-  `"contradiction"` as options
-
-**Files to investigate:**
-
-- `src/compute-engine/assume.ts` - `assume()` function and `AssumeResult` type
-
-**Tests:** `test/compute-engine/assumptions.test.ts` - "TAUTOLOGY AND
-CONTRADICTION DETECTION"
+See `requirements/DONE.md` for implementation details.
 
 ---
 
-### 21. Type Inference from Assumptions
-
-**Problem:** When assumptions are made, symbol types should be inferred. For
-example, `x > 4` implies `x` is real, and `one = 1` implies `one` is an integer.
+### ~~21. Type Inference from Assumptions~~ ✅ COMPLETED
 
-**Current behavior:**
-
-```typescript
-ce.assume(ce.box(['Greater', 'x', 4]));
-ce.box('x').type.toString()  // Returns: "unknown"
-
-ce.assume(ce.box(['Equal', 'one', 1]));
-ce.box('one').type.toString()  // Returns: "unknown"
-```
-
-**Expected behavior:**
-
-```typescript
-ce.assume(ce.box(['Greater', 'x', 4]));
-ce.box('x').type.toString()  // Should return: "real" (inequalities imply real numbers)
-
-ce.assume(ce.box(['Equal', 'one', 1]));
-ce.box('one').type.toString()  // Should return: "integer" (equal to integer literal)
-```
-
-**Implementation notes:**
-
-- Inequality assumptions (`>`, `<`, `>=`, `<=`) imply the symbol is `real`
-- Equality to an integer implies the symbol is `integer`
-- Equality to a rational implies the symbol is `rational`
-- This might be handled by updating the symbol's type when an assumption is made
-- Alternatively, the type getter could query assumptions
-
-**Files to investigate:**
-
-- `src/compute-engine/assume.ts` - Assumption processing
-- `src/compute-engine/boxed-expression/boxed-symbol.ts` - Symbol type resolution
-
-**Tests:** `test/compute-engine/assumptions.test.ts` - "TYPE INFERENCE FROM
-ASSUMPTIONS"
+See `requirements/DONE.md` for implementation details.
 
 ---