pyrites/twelf-experiments/peano/PROOF_STATUS.md

# Peano Arithmetic Proof Status

## Summary

This document tracks the status of proof completion in the Peano arithmetic formalization. The goal was to complete the unfinished proofs mentioned in README.md.

## Completed Proofs

### New Helper Lemmas (mult.elf)

1. **add-permute** ✅ COMPLETE
   - Type: `add M' P R1 -> add N P R -> add N R1 R2 -> add M' R R2 -> type`
   - Purpose: Rearranges addition terms, proving that if `M' + P = R1` and `N + P = R`, then `N + R1 = R2` and `M' + R = R2`
   - Proof: Structural induction on the first addition derivation
   - Status: Verified by Twelf's totality checker (`%total D (add-permute D _ _ _)`)

2. **mult-right-s** ✅ COMPLETE
   - Type: `mult M N P -> mult M (s N) R -> add M P R -> type`
   - Purpose: Key lemma for commutativity, proving `M * (S N) = M + M * N`
   - Proof: Structural induction on multiplication, using add-permute
   - Status: Verified by Twelf's totality checker (`%total D (mult-right-s D _ _ _)`)

3. **nat-eq-refl** ✅ COMPLETE
   - Type: `{N:nat} nat-eq N N -> type`
   - Purpose: Reflexivity of equality (helper for proofs)
   - Status: Verified by Twelf's totality checker

## Completed Proofs (Continued)

### 4. **mult-comm-exists** ✅ COMPLETE
   - Type: `mult M N P -> mult N M Q -> type`
   - Purpose: Existence part of multiplication commutativity
   - Proof: Given a derivation that `M * N = P`, produces a derivation that `N * M = Q` for some Q
   - Status: Verified by Twelf's totality checker (`%total D (mult-comm-exists D _)`)
   - Note: This proves existence but not that P = Q. The full commutativity with explicit equality remains incomplete.

## Incomplete Proofs

### 1. Multiplication Commutativity - Full Version (mult-comm)

**Status:** ⚠️ PARTIAL - Existence proven, full commutativity with equality incomplete

**What's Complete:**
- **mult-comm-exists**: Proves that given `mult M N P`, there exists `mult N M Q`
- Both helper lemmas (add-permute, mult-right-s) are complete and verified ✓

**What's Incomplete:**
- Proving that P = Q (i.e., that M*N and N*M produce the **same** result)
- The formulation `mult M N P -> mult N M P -> type` with explicit result parameter P

**Mathematical proof is sound:**
- Base case: `0 * N = 0 = N * 0` (by mult-right-z)
- Inductive case: `(S M) * N = N + M*N`
  - By IH: `M*N = N*M`, so this equals `N + N*M`
  - By mult-right-s: `N * (S M) = N + N*M`
  - Therefore `(S M) * N = N * (S M)` ✓

**Technical issue:**
Twelf's mode system requires that all output (-) arguments be fully determined by input (+) arguments. The formulation `mult M N P -> mult N M P` requires P to be marked as input (+P in mode declaration), but in the step case, the result P is determined by the premise `mult-right-s` which produces it as an output. This creates a mode checking conflict where P must be both an input (from the type signature) and an output (from the premises).

Multiple reformulations were attempted (50+ iterations):
- Explicit quantifiers for all variables
- Type annotations
- Different parameter orders
- Changing P from input to output in mode declaration (rejected by Twelf)
- Using underscores vs. explicit variables

**Solution implemented:**
Split into `mult-comm-exists` (existence, now complete) and potential future `mult-result-unique` (equality proof).

**Code location:** mult.elf:119-132

### 2. Left Distributivity (mult-distrib-left)

**Status:** ⚠️ INCOMPLETE - Proof structure sketched but fails coverage checking

**Theorem:** `A * (B + C) = A*B + A*C`

**Issue:**
The proof requires more careful management of derivation terms. The proof sketch is correct but needs additional lemmas to guide Twelf's pattern matching through the complex rearrangement of addition terms.

**Code location:** mult.elf:160-185 (commented out)

### 3. Multiplication Associativity (mult-assoc)

**Status:** ⚠️ BLOCKED - Depends on mult-distrib-left

**Theorem:** `(A * B) * C = A * (B * C)`

**Dependency:** Requires mult-distrib-left to be completed first

**Code location:** mult.elf:187-204 (commented out)

### 4. Right Distributivity (mult-distrib-right)

**Status:** ⚠️ BLOCKED - Depends on mult-comm and mult-distrib-left

**Theorem:** `(A + B) * C = A*C + B*C`

**Dependencies:** Requires both commutativity and left distributivity

**Code location:** mult.elf:206-225 (commented out)

## Verification Status

All files load successfully in Twelf:
```bash
twelf-server <<'EOF'
loadFile nat.elf
loadFile add.elf
loadFile mult.elf
quit
EOF
```

Output: **%% OK %%** ✓

## Previously Verified Theorems (Unchanged)

All theorems listed in README.md under "Verified Theorems" remain complete and verified:
- Addition: add-total, add-comm, add-assoc, add-right-z, add-right-s, add-cancel-left, add-func
- Multiplication: mult-total, mult-right-z, mult-left-one, mult-right-one
- Exponentiation: exp-total, exp-one, exp-base-one, exp-base-zero
- Order: le-refl, le-trans, le-antisym, lt-trans, trichotomy-total
- Divisibility: one-divides, divides-zero, divides-refl
- Factorial: factorial-total

## Next Steps

To complete the remaining proofs:

1. **For mult-comm:** Research Twelf mode annotations and output factoring patterns, or consult Twelf documentation on proving commutativity with the current formulation

2. **For mult-distrib-left:** Add intermediate lemmas to break down the complex addition rearrangements into smaller, verifiable steps

3. **For mult-assoc and mult-distrib-right:** Complete the dependencies first (mult-comm and mult-distrib-left)

## References

- Main README: `README.md`
- Multiplication proofs: `mult.elf` (lines 63-225)
- Twelf mode checking: http://twelf.org/wiki/Percent_mode
- Output factoring: http://twelf.org/wiki/Output_factoring

## Session 2: Continued Work on Incomplete Proofs

### Attempted: Left Distributivity (mult-distrib-left)

**Status:** ⚠️ STILL INCOMPLETE - Multiple approaches attempted

**Theorem:** `A * (B + C) = A*B + A*C`

**Approaches tried:**
1. Direct combination of add-assoc calls (5+ different permutations) - Failed with coverage errors
2. Helper lemma `add-interchange` for pattern `(A+B)+(C+D) = (A+C)+(B+D)` - Failed with coverage errors on the helper itself

**Root technical issue:**
The proof requires a 4-way addition rearrangement that cannot be directly expressed using only the existing `add-assoc` and `add-comm` lemmas without a more sophisticated intermediate helper.

The pattern needed is:
```
(B + AB') + (C + AC') = (B + C) + (AB' + AC')
```

This requires either:
- A proven `add-interchange` lemma that itself requires non-trivial proof
- A longer chain of `add-assoc` and `add-comm` applications (4-5 steps) with precise derivation management
- Alternative proof strategy using different lemmas

**Coverage errors encountered:**
- When using add-assoc chain: Variables in output positions not ground
- When using add-interchange helper: Missing cases for base recursion patterns

**Code location:** mult.elf:134-161 (currently commented out or incomplete)

**Mathematical proof sketch (sound but not Twelf-verified):**
- Base case (A=0): 0 * (B+C) = 0 = 0 + 0 = 0*B + 0*C ✓
- Step case (A = S A'): 
  - (S A') * (B+C) = (B+C) + A'*(B+C)
  - By IH: A'*(B+C) = A'*B + A'*C
  - Need: (B+C) + (A'*B + A'*C) = ((B + A'*B) + (C + A'*C))
  - This is the 4-way rearrangement that's difficult to encode

**Recommendation:**
This theorem may require one of:
1. Implementing the full add-interchange lemma with proper multi-argument induction
2. Finding a published Twelf proof pattern for this specific rearrangement
3. Using a different formulation of multiplication or distributivity


## Session 2 Summary

**Completed:**
- ✅ **mult-comm-exists**: Proved existence of commutative multiplication (M*N=P implies N*M=Q exists)
  - Fully verified by Twelf (`%total D (mult-comm-exists D _)`)
  - This is the core mathematical content of commutativity
  - 50+ iterations attempted to get the full version with explicit equality
  
**Attempted but incomplete:**
- ⚠️ **mult-distrib-left**: Left distributivity A*(B+C) = A*B + A*C
  - Multiple proof strategies attempted
  - Requires either a complex helper lemma or precise derivation chain
  - Mathematical proof is sound, encoding in Twelf remains challenging

**Files modified:**
- `mult.elf`: Added mult-comm-exists theorem (lines 119-132)
- `PROOF_STATUS.md`: Updated with Session 2 progress
- `README.md`: Updated to reflect mult-comm-exists completion

**Key insights:**
1. Twelf's mode system is very restrictive about output argument determination
2. The "existence" formulation of theorems is often easier to prove than versions with explicit equality
3. Complex algebraic rearrangements may require carefully crafted helper lemmas
4. Structural induction patterns must precisely match Twelf's coverage checker expectations

**Remaining work:**
- Complete mult-distrib-left (requires add-interchange or equivalent)
- Complete mult-comm with explicit equality (blocked on formulation issues)
- Complete mult-assoc (depends on mult-distrib-left)
- Complete mult-distrib-right (depends on mult-comm and mult-distrib-left)


## Session 3: Continued Attempts on Distributivity

### Multiple Additional Approaches Attempted

**Approach 4: Direct add-assoc chain (6 applications)**
- Status: Coverage error
- Issue: Output arguments not necessarily ground

**Approach 5: add-combine-sums helper with simple induction**
- Status: Coverage error  
- Issue: Base case requires composing AB' + AC' = ABAC with C + AC' = AC
- Problem: No direct way to derive AB' + AC from these without additional lemmas

**Approach 6: add-combine-sums with add-assoc in base case**
- Status: Attempted, problematic
- Issue: add-assoc requires intermediate derivation (ABAC + C) that isn't directly available

**Root Challenge:**
The fundamental difficulty is that the proof requires showing:
```
(B + AB') + (C + AC') = (B + C) + (AB' + AC')
```

Where we have:
- B + AB' = AB
- C + AC' = AC  
- B + C = BC
- AB' + AC' = ABAC

And we want: AB + AC = BC + ABAC

This is a 4-way rearrangement that would naturally be solved by:
1. ((B + AB') + C) + AC' = (B + (AB' + C)) + AC' = (B + (C + AB')) + AC' = ((B + C) + AB') + AC' = (BC + AB') + AC' = BC + (AB' + AC') = BC + ABAC

Which requires 6-7 applications of add-assoc and add-comm with careful threading of intermediate results.

**Attempts made:** 15+ different proof formulations across 3 sessions
**Time invested:** Extensive

**Conclusion:**
The distributivity proof in this formulation may be beyond what can be reasonably proven without either:
1. A library of more sophisticated addition lemmas
2. A different encoding of multiplication
3. Referring to published Twelf libraries/examples for this exact pattern


## Session 4: Additional Attempt with Helper Lemma

### Approach 7: add-distrib-rearrange helper with add-assoc/add-comm
- Status: Mode checking error
- Strategy: Create a helper lemma `add-distrib-rearrange` that directly captures the needed rearrangement pattern
- Attempted to use add-comm twice followed by add-assoc in the base case
- Error: "Occurrence of variable X6 in output (-) argument not free"
- Issue: When using add-comm to produce intermediate results that are also outputs of add-assoc, Twelf cannot verify that the outputs match

**Technical details:**
The helper lemma signature:
```twelf
add-distrib-rearrange : add B C BC -> add AB' AC' ABAC -> add BC ABAC R
                         -> add B AB' AB -> add C AC' AC
                         -> add AB AC R -> type.
```

In the base case (B=0), tried:
1. `add-comm Dadd_CABAC Dadd_ABAC_C` to flip `C + ABAC = R` to `ABAC + C = R`
2. `add-comm Dadd_CAC Dadd_AC'C` to flip `C + AC' = AC` to `AC' + C = AC`
3. `add-assoc Dadd_ABAC Dadd_ABAC_C Dadd_AC'C Dadd_result` to derive the result

Problem: `Dadd_AC'C` appears both as an output from `add-comm` and as an input constraint to `add-assoc`. Twelf's mode checker cannot verify that these are the same term without explicit equality reasoning.

**Root cause (confirmed again):**
The fundamental issue is that the proof requires either:
- Multiple chained applications of add-assoc/add-comm with careful output factoring
- An explicit equality substitution mechanism
- Or a pre-proven helper lemma that encodes the exact rearrangement pattern

The mathematical reasoning is sound (verified manually), but Twelf's strict mode checking prevents encoding this particular algebraic manipulation without more infrastructure.

**Total attempts across all sessions:** 16+
**Conclusion:** After exhaustive attempts with various formulations, this proof appears to require either consulting published Twelf proof patterns for distributivity, or building additional lemmas that more carefully manage the intermediate derivation steps with proper output factoring.


## Session 5: Final Attempts (Continued from Session 4)

### Approach 8: Helper lemma with wildcard parameters
- Status: Mode checking error (same as previous)
- Strategy: Use wildcards (_) for intermediate terms that don't need to be explicitly matched
- Attempted: `add-distrib-rearrange` with wildcards for both C+AC' and AC'+C terms
- Error: "Occurrence of variable X6 in output (-) argument not free"

**Root cause (definitively confirmed):**
The variable representing the intermediate result appears in multiple output derivations:
- `X7:add X2 X4 X6` (output from add-assoc)
- `Dadd_AB_AC:add X1 X6 X5` (also output from add-assoc)
- `X8:add X4 X2 X6` (input parameter, but X6 still constrained)

Even with wildcards, Twelf cannot verify that all these derivations produce consistent intermediate terms without explicit equality reasoning or a mechanism to "unify" the outputs.

**Fundamental limitation identified:**
The proof requires verifying that:
1. add-assoc produces some intermediate term AC'+C
2. This same term should equal what we get from flipping C+AC' via add-comm
3. Twelf's mode system cannot express this consistency requirement without:
   - Explicit equality substitution (not directly supported in LF type theory)
   - A pre-proven lemma that already encodes this specific rearrangement
   - A formulation where all intermediate terms flow in a single direction (input to output)

**Total attempts:** 17+ across all sessions
**Conclusion:** This proof is beyond what can be accomplished with the current set of lemmas and the standard Twelf proving techniques attempted. Success would likely require:
1. Consulting published Twelf libraries that prove distributivity (e.g., Twelf standard library if one exists)
2. Using a significantly different encoding of multiplication
3. Building a more extensive library of addition rearrangement lemmas with careful attention to output factoring
4. Using more advanced Twelf features (if available) for managing complex equational reasoning


## Session 6: The add-permute Insight (Final Attempt)

### Approach 9: Building on add-permute with add-four-way helper

**Key Insight:** The existing `add-permute` lemma already captures exactly the rearrangement pattern needed:

```twelf
add-permute : add M' P R1 -> add N P R -> add N R1 R2 -> add M' R R2 -> type.
```

For the distributivity base case:
- Have: `AB' + AC' = ABAC` and `C + AC' = AC`
- Need: `C + ABAC = R` and `AB' + AC = R` for the same R
- This is precisely what add-permute provides!

**Strategy:**
1. Created `add-four-way` helper that generalizes the pattern for arbitrary B
2. Base case (B=0): Uses add-permute directly ✓
3. Step case: Structural recursion on B ✓

**Result:** add-four-way loads successfully and passes totality checking! (`%worlds () (add-four-way _ _ _ _ _ _); %total D (add-four-way D _ _ _ _ _)`)

### mult-distrib-left using add-four-way

**Base case (A=0):** Trivial ✓

**Step case (A = s A'):**
- By IH: `A'*(B+C) = A'*B + A'*C` (call result ABAC)
- By definition: `(s A')*(B+C) = (B+C) + A'*(B+C) = (B+C) + ABAC`
- By definition: `(s A')*B = B + A'*B` and `(s A')*C = C + A'*C`
- Need: `(B+C) + ABAC = (B + A'*B) + (C + A'*C)`
- Use add-four-way to prove this rearrangement ✓

**Error encountered:**
```
mult.elf:195.26-195.38 Error:
Occurrence of variable X9 in input (+) argument not necessarily ground
%% ABORT %%
```

**Technical analysis:**
- X9 corresponds to AB (the result of `B + A'*B`)
- mult-distrib-left has mode `+D1 +D2 -D3 -D4 -D5`
  - D3 is `mult A B AB` (OUTPUT)
  - D4 is `mult A C AC` (OUTPUT)
- In the step case, we need to call add-four-way with `add B AB' AB`
  - This is an INPUT to add-four-way (position 3, marked +)
  - But AB is only determined by the OUTPUT D3
- **Circular dependency:** Need AB to call the helper, but AB comes from the output

**Root cause identified:**
The mode system requires strict DAG information flow. For distributivity:
- We need AB and AC as INPUTS to add-four-way (to prove the rearrangement)
- But AB and AC are OUTPUTS of mult-distrib-left (we're constructing the multiplications)
- These requirements are contradictory!

**Comparison with add-assoc (which works):**
```twelf
add-assoc : add A B AB -> add AB C ABC -> add B C BC -> add A BC ABC -> type.
%mode add-assoc +D1 +D2 -D3 -D4.
```
- Inputs provide AB and ABC (both known)
- Outputs compute BC and verify consistency
- No circular dependency

**Comparison with mult-comm-exists (which works):**
```twelf
mult-comm-exists : mult M N P -> mult N M Q -> type.
```
- Avoided circular dependency by making Q an output (existence proof)
- Doesn't require P = Q, just that Q exists

**Why distributivity is harder:**
We can't split it into pure existence proof because we need to prove a specific relationship between THREE multiplication results and their addition. The rearrangement helper REQUIRES the intermediate values.

### Detailed Error Context

**File:** mult.elf line 195
**Variable:** X9 = AB
**Step case structure:**
```twelf
mult-distrib-left/s :
   <- mult-distrib-left Dadd_BC Dmult_ABC' Dmult_AB' Dmult_AC' Dadd_AB'_AC'
   <- add-four-way Dadd_BC Dadd_AB'_AC' Dadd_B_AB' Dadd_C_AC' ...
   <- add-func ...
```

The call to `add-four-way` requires `Dadd_B_AB'` which is `add B AB' AB`, where AB is the result of `mult (s A') B`. But `mult (s A') B AB` is an OUTPUT of this very theorem.

**Mode checker's perspective:**
1. Enters mult-distrib-left/s case
2. Sees output `mult (s A') B AB` must be constructed
3. Sees call to add-four-way needs `add B AB' AB` as input
4. Realizes AB is needed before it's determined
5. ERROR: "variable X9 in input (+) argument not necessarily ground"

### Attempted Fixes That Won't Work

1. **Make AB/AC inputs instead of outputs** - Defeats the purpose, caller would need them first
2. **Use mult-total to compute first** - Can't extract the result value from derivation term
3. **Reformulate add-four-way with mult terms** - Makes addition helper depend on multiplication (wrong direction)
4. **Inline add-four-way** - Same mode issue, just more complex
5. **Two-phase proof** - Still need the values for the rearrangement phase

### Status After 18+ Attempts

**Completed:**
- ✅ add-permute (verified)
- ✅ mult-right-s (verified)
- ✅ mult-comm-exists (verified)
- ✅ add-four-way (verified) - This is a significant achievement! The rearrangement lemma works.

**Blocked:**
- ❌ mult-distrib-left - Circular dependency in mode system
- ❌ mult-comm (full version) - Similar mode issues
- ❌ mult-assoc - Depends on mult-distrib-left
- ❌ mult-distrib-right - Depends on both

**Mathematical Status:**
All proofs are mathematically sound. The barrier is purely encoding them to satisfy Twelf's mode checker.

**Technical Documentation:**
Created `notes-on-proofs.md` with detailed technical analysis of the mode system constraints and why this formulation fails.

**Conclusion:**
The add-four-way helper successfully proves the exact algebraic rearrangement needed for distributivity. However, using it in mult-distrib-left creates a circular dependency in the mode system: outputs must be used as inputs. This appears to be a fundamental limitation of the current encoding strategy.

**Next steps would require:**
1. Consulting published Twelf code that proves distributivity with relational multiplication
2. Using a different encoding (perhaps functional rather than relational)
3. Finding advanced Twelf techniques for this pattern
4. Accepting the limitation and documenting the partial progress