Task 18 et al

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.
 
 ---