pyrites/twelf-experiments/peano/notes-on-proofs.md

Technical Notes on Distributivity Proof Attempts

Current Status (Session 6)

Latest Attempt: Using add-permute as Foundation

Key Insight: The existing add-permute lemma already captures exactly the pattern needed for the base case of distributivity:

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

This says: if M' + P = R1 and N + P = R, then N + R1 = R2 and M' + R = R2.

For distributivity base case (A=0):

• We have: add AB' AC' ABAC (i.e., AB' + AC' = ABAC)
• We have: add C AC' AC (i.e., C + AC' = AC)
• We need: add C ABAC R and add AB' AC R for the same R
• This is exactly what add-permute gives us!

The add-four-way Helper

Created a helper to generalize the pattern for the step case:

add-four-way : add B C BC -> add AB' AC' ABAC -> add B AB' AB -> add C AC' AC
                -> add BC ABAC R -> add AB AC R -> type.

Base case (B=0): Uses add-permute directly ✓

Step case (B = s B'): Structural recursion

• Given: add (s B') C (s BC') where add B' C BC'
• IH provides: add BC' ABAC R' and add AB'' AC R'
• Derive: add (s BC') ABAC (s R') and add (s AB'') AC (s R')

This helper loaded successfully with %% OK %% and passed totality checking!

mult-distrib-left Using add-four-way

mult-distrib-left : add B C BC -> mult A BC ABC -> mult A B AB -> mult A C AC
                     -> add AB AC ABC -> type.

Base case (A=0): Trivial - 0*(B+C) = 0 = 0 + 0 = 0*B + 0*C ✓

Step case (A = s A'):

• By definition: (s A') * (B+C) = (B+C) + A'*(B+C)
• By definition: (s A') * B = B + A'*B
• By definition: (s A') * C = C + A'*C
• By IH: A'*(B+C) = A'*B + A'*C, call this ABAC
• Need to show: (B+C) + ABAC = (B + A'*B) + (C + A'*C)
• This is exactly what add-four-way proves!

The Mode Error

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

Line 195 is the step case of mult-distrib-left.

Analysis: The variable X9 corresponds to AB (the result of B + A'*B). The issue is that in the mode declaration:

%mode mult-distrib-left +D1 +D2 -D3 -D4 -D5.

We have mult A B AB as an output (D3 is marked -), which means AB is an output. But in the step case, we're calling:

add-four-way Dadd_BC Dadd_AB'_AC' Dadd_B_AB' Dadd_C_AC' Dadd_BC_ABC Dadd_AB_AC

Where Dadd_B_AB' is add B AB' AB, and this is an input to add-four-way (marked + in its mode).

The fundamental problem:

• mult A B AB must be an OUTPUT of mult-distrib-left (we're constructing it)
• But add B AB' AB must be an INPUT to add-four-way (it needs it to compute)
• These are contradictory requirements!

Why This Happens

The step case structure is:

1. (s A') * B = B + A'*B - this gives us add B AB' AB where AB' is the result of A'*B
2. We need this derivation add B AB' AB to pass to add-four-way
3. But we're simultaneously trying to output the multiplication mult (s A') B AB

The issue is that we need to know AB before we can call add-four-way, but AB is determined by the multiplication definition itself.

The Root Cause: Output Factoring Mismatch

Looking at add-assoc as a model:

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.

This works because:

• Input: add A B AB (AB is known from this derivation)
• Input: add AB C ABC (ABC is known from this derivation)
• Output: add B C BC (BC is computed)
• Output: add A BC ABC (same ABC, verified to match)

For distributivity, we're trying:

• Input: add B C BC (BC is known)
• Input: mult A BC ABC (ABC is known)
• Output: mult A B AB (AB needs to be computed AND used as input to helper)
• Output: mult A C AC (AC needs to be computed AND used as input to helper)

The problem: We need AB and AC to call add-four-way, but they're outputs!

Possible Solutions

Solution 1: Change the Mode Declaration

What if we make AB and AC inputs instead of outputs?

%mode mult-distrib-left +D1 +D2 +D3 +D4 -D5.

Problem: Now the caller needs to provide the multiplications first. This defeats the purpose - we're trying to PROVE they exist and relate correctly.

Solution 2: Reorder the Helper Call

What if we compute the multiplications first, then verify with add-four-way?

Problem: We can't "compute" them without constructing the full derivations, which is what we're trying to do in the theorem itself. Circular dependency.

Solution 3: Use mult-total to Construct First

<- mult-total A B Dmult_AB'      %% Get A*B = AB
<- mult-total A C Dmult_AC'      %% Get A*C = AC
<- add-four-way ...              %% Then use in helper

Problem: mult-total gives us mult A B AB for some AB, but we need to extract the specific AB value to use in add-four-way. The derivation contains it, but Twelf's mode system doesn't let us "extract" it in the way we need.

Solution 4: Reformulate add-four-way with mult Terms

Instead of having add-four-way take addition derivations, what if it takes multiplication derivations?

Problem: This makes add-four-way dependent on mult, which is backwards - it's really a lemma about addition rearrangement.

Solution 5: Accept Incomplete and Document

The mathematical proof is sound. The issue is purely about Twelf's mode system and how it handles dependent outputs. This might be a fundamental limitation of the current formulation.

Comparison with Agda

In Agda (from PLFA):

*-distrib-+ : ∀ (m n p : ℕ) → (m + n) * p ≡ m * p + n * p
*-distrib-+ zero n p = refl
*-distrib-+ (suc m) n p rewrite *-distrib-+ m n p | +-assoc p (m * p) (n * p) = refl

The rewrite tactic:

1. Uses propositional equality ≡
2. Can substitute equals for equals anywhere
3. Doesn't require explicit derivation terms

In Twelf:

1. Relations, not functions
2. Explicit derivation terms required
3. Mode system requires strict input/output flow
4. Can't "rewrite" - must construct explicit derivation chains

What Worked: mult-comm-exists vs mult-comm

mult-comm (failed - 50+ attempts):

mult-comm : mult M N P -> mult N M P -> type.

Requires P to be both input (from type signature) and output (from construction).

mult-comm-exists (succeeded):

mult-comm-exists : mult M N P -> mult N M Q -> type.

P is input, Q is output. Proves existence without equality.

Lesson Learned

Twelf's mode system requires a strict DAG of information flow.

For a theorem with signature +inputs -> -outputs, every output must be:

1. Computable solely from the inputs
2. Not required as an input to intermediate lemmas
3. Not circularly dependent on other outputs

Distributivity violates rule 2: we need the output multiplications as inputs to the rearrangement helper.

Possible Path Forward

Idea: Two-phase proof

Phase 1: Existence

mult-distrib-left-exists : add B C BC -> mult A BC ABC ->
                           mult A B AB -> mult A C AC -> type.

Just proves the three multiplications can coexist (all as inputs).

Phase 2: Rearrangement

mult-distrib-rearrange : mult A BC ABC -> mult A B AB -> mult A C AC ->
                         add AB AC ABC -> type.

Given all three multiplications, prove they satisfy the distributive property.

But this still has the problem that phase 2 requires AB and AC as inputs to derive the addition...

Idea: Extract results using functionality

Since mult is functional, mult A B AB1 and mult A B AB2 implies AB1 = AB2. We could:

1. Use mult-total to get mult A B AB_exists
2. Use add-four-way with the RESULT of mult (extracted somehow)
3. Use mult-func to verify consistency

But Twelf doesn't have a clean way to "extract" the result from a derivation term.

Idea: Inline add-four-way into mult-distrib-left

Instead of calling add-four-way as a helper, inline its proof directly into the step case. This might give Twelf's mode checker more flexibility.

Problem: This creates a very complex proof with deeply nested recursion, and likely hits the same mode issues.

Conclusion

After 18+ systematic attempts across 6 sessions:

1. ✅ mult-comm-exists - Proved by reformulating to avoid circular dependency
2. ✅ add-permute - Key rearrangement lemma
3. ✅ mult-right-s - Key lemma for commutativity
4. ✅ add-four-way - The exact rearrangement needed for distributivity
5. ❌ mult-distrib-left - Blocked on mode system constraints

The mathematical content is complete. The blocker is encoding it in a way that satisfies Twelf's mode system.

Recommendation: Consult Twelf experts or search for published Twelf developments that prove distributivity for a relational multiplication encoding. The issue is not the mathematics but the encoding strategy.

Session 6 Specific Error Details

File: mult.elf, line 195 Error: "Occurrence of variable X9 in input (+) argument not necessarily ground"

X9 = AB (result of B + A'*B) Context: Calling add-four-way in the step case of mult-distrib-left Issue: AB is an output of mult-distrib-left but an input to add-four-way

The mode checker traces:

• mult-distrib-left has mode +D1 +D2 -D3 -D4 -D5
• D3 is mult A B AB (output)
• In step case, we construct mult (s A') B AB as mult/s Dadd_B_AB' Dmult_AB'
• Dadd_B_AB' is add B AB' AB
• This is passed as INPUT to add-four-way (position 3, marked +)
• But AB is only known AFTER we construct the output D3
• Circular dependency: need AB to call helper, but get AB from output

This is the precise technical reason the proof fails.