%% mult.elf - Multiplication on Natural Numbers
%%
%% Multiplication is defined recursively:
%%   0 * N = 0
%%   (S M) * N = N + (M * N)

mult : nat -> nat -> nat -> type.
%mode mult +M +N -R.

mult/z : mult z N z.
mult/s : mult (s M) N R
          <- mult M N P
          <- add N P R.

%% Multiplication is total
mult-total : {M:nat} {N:nat} mult M N P -> type.
%mode mult-total +M +N -D.

mult-total/z : mult-total z N mult/z.
mult-total/s : mult-total (s M) N (mult/s Dadd Dmult)
                <- mult-total M N Dmult
                <- add-total N _ Dadd.

%worlds () (mult-total _ _ _).
%total M (mult-total M _ _).

%% ============================================================
%% BASIC MULTIPLICATION LEMMAS
%% ============================================================

%% Right zero: N * 0 = 0
mult-right-z : {N:nat} mult N z z -> type.
%mode mult-right-z +N -D.

mult-right-z/z : mult-right-z z mult/z.
mult-right-z/s : mult-right-z (s N) (mult/s add/z D)
                  <- mult-right-z N D.

%worlds () (mult-right-z _ _).
%total N (mult-right-z N _).

%% Left identity: 1 * N = N
mult-left-one : {N:nat} mult (s z) N N -> type.
%mode mult-left-one +N -D.

mult-left-one/base : mult-left-one N (mult/s Dadd mult/z)
                      <- add-right-z N Dadd.

%worlds () (mult-left-one _ _).
%total {} (mult-left-one _ _).

%% Right identity: N * 1 = N
mult-right-one : {N:nat} mult N (s z) N -> type.
%mode mult-right-one +N -D.

mult-right-one/z : mult-right-one z mult/z.
mult-right-one/s : mult-right-one (s N) (mult/s (add/s add/z) D)
                    <- mult-right-one N D.

%worlds () (mult-right-one _ _).
%total N (mult-right-one N _).

%% ============================================================
%% HELPER LEMMAS FOR MULTIPLICATION
%% ============================================================

%% Helper: If M' + P = R1 and N + P = R, then N + R1 = M' + R
%% This is needed for mult-right-s step case
%% Proof: N + R1 = N + (M' + P) = (N + M') + P = (M' + N) + P = M' + (N + P) = M' + R
add-permute : add M' P R1 -> add N P R -> add N R1 R2 -> add M' R R2 -> type.
%mode add-permute +D1 +D2 -D3 -D4.

add-permute/z : add-permute add/z D D add/z.

add-permute/s : add-permute (add/s D1) D2 D3' (add/s D4)
                 <- add-permute D1 D2 D3 D4
                 <- add-right-s D3 D3'.

%worlds () (add-permute _ _ _ _).
%total D (add-permute D _ _ _).

%% ============================================================
%% MULTIPLICATION BY SUCCESSOR
%% ============================================================

%% Key lemma: M * (S N) = M + M * N
%% Given mult M N P, construct mult M (s N) R and add M P R
mult-right-s : mult M N P -> mult M (s N) R -> add M P R -> type.
%mode mult-right-s +D1 -D2 -D3.

mult-right-s/z : mult-right-s mult/z mult/z add/z.

mult-right-s/s : mult-right-s (mult/s Dadd Dmult) (mult/s (add/s Dadd_NR1) Dmult') (add/s Dadd_MR)
                  <- mult-right-s Dmult Dmult' Dadd1
                  <- add-permute Dadd1 Dadd Dadd_NR1 Dadd_MR.

%worlds () (mult-right-s _ _ _).
%total D (mult-right-s D _ _).

%% ============================================================
%% COMMUTATIVITY OF MULTIPLICATION
%% ============================================================

%% Helper for mult-comm: equational reasoning
%% Since we know add is functional, if add N P' P1 and add N P' P2, then P1 = P2
%% This allows us to connect derivations that should be equal
nat-eq-refl : {N:nat} nat-eq N N -> type.
%mode nat-eq-refl +N -E.

nat-eq-refl/base : nat-eq-refl _ nat-eq/refl.

%worlds () (nat-eq-refl _ _).
%total {} (nat-eq-refl _ _).

%% ============================================================
%% MULTIPLICATION COMMUTATIVITY
%% ============================================================

%% Existence: M * N produces some result, and so does N * M
mult-comm-exists : mult M N P -> mult N M Q -> type.
%mode mult-comm-exists +D1 -D2.

mult-comm-exists/z : mult-comm-exists mult/z D
                      <- mult-right-z _ D.

mult-comm-exists/s : mult-comm-exists (mult/s Dadd Dmult) Dmult''
                      <- mult-comm-exists Dmult Dmult'
                      <- mult-right-s Dmult' Dmult'' _.

%worlds () (mult-comm-exists _ _).
%total D (mult-comm-exists D _).

%% ============================================================
%% LEFT DISTRIBUTIVITY - Attempt Using add-permute
%% ============================================================

%% Helper: The key 4-way rearrangement for distributivity
%% Pattern: (B+C) + (AB'+AC') = (B+AB') + (C+AC')
%% Given: add B C BC, add AB' AC' ABAC, add B AB' AB, add C AC' AC
%% Prove: exists R such that add BC ABAC R and add AB AC R
%%
%% Key insight: add-permute does: if M'+P=R1 and N+P=R, then N+R1=R2 and M'+R=R2
%% We can use: add-permute AB' AC' ABAC (add C AC' AC) gives us:
%%   add C ABAC R and add AB' AC R for the same R

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.
%mode add-four-way +D1 +D2 +D3 +D4 -D5 -D6.

%% Base case: B = 0
%% Have: add z C C, add AB' AC' ABAC, add z AB' AB', add C AC' AC
%% Use add-permute: AB' + AC' = ABAC and C + AC' = AC
%% Gives: C + ABAC = R and AB' + AC = R
add-four-way/z : add-four-way add/z Dadd_ABAC add/z Dadd_CAC Dadd_C_ABAC Dadd_AB_AC
                  <- add-permute Dadd_ABAC Dadd_CAC Dadd_C_ABAC Dadd_AB_AC.

%% Step case: B = s B'
%% Have: add (s B') C (s BC') where add B' C BC'
%%       add AB' AC' ABAC (unchanged)
%%       add (s B') AB' (s AB'') where add B' AB' AB''
%%       add C AC' AC (unchanged)
%% IH gives: add BC' ABAC R' and add AB'' AC R'
%% We derive: add (s BC') ABAC (s R') and add (s AB'') AC (s R')
add-four-way/s : add-four-way (add/s Dadd_BC') Dadd_ABAC (add/s Dadd_BAB') Dadd_CAC
                               (add/s Dadd_BC'_ABAC) (add/s Dadd_AB''_AC)
                  <- add-four-way Dadd_BC' Dadd_ABAC Dadd_BAB' Dadd_CAC
                                  Dadd_BC'_ABAC Dadd_AB''_AC.

%worlds () (add-four-way _ _ _ _ _ _).
%total D (add-four-way D _ _ _ _ _).

%% ============================================================
%% LEFT DISTRIBUTIVITY (INCOMPLETE - Mode System Limitation)
%% ============================================================

%% A * (B + C) = A*B + A*C
%%
%% STATUS: The add-four-way helper (above) successfully proves the required
%% algebraic rearrangement and passes Twelf's totality checker. However,
%% using it in mult-distrib-left creates a circular mode dependency.
%%
%% TECHNICAL ISSUE:
%% The theorem signature requires:
%%   mult-distrib-left : add B C BC -> mult A BC ABC
%%                       -> mult A B AB -> mult A C AC -> add AB AC ABC -> type.
%%   %mode mult-distrib-left +D1 +D2 -D3 -D4 -D5.
%%
%% In the step case, we need to call:
%%   add-four-way Dadd_BC Dadd_AB'_AC' Dadd_B_AB' Dadd_C_AC' ...
%%
%% Where Dadd_B_AB' is `add B AB' AB`. This requires AB as an input.
%% But AB comes from the OUTPUT `mult A B AB` (D3).
%%
%% Circular dependency: need AB to call helper, but AB is the output.
%%
%% ERROR: "Occurrence of variable X9 in input (+) argument not necessarily ground"
%%
%% COMPARISON WITH add-assoc (which works):
%% - Inputs provide all needed values (AB, ABC)
%% - Outputs just compute new values (BC) and verify consistency
%% - No circular dependencies
%%
%% MATHEMATICAL STATUS: The proof is mathematically sound.
%% TECHNICAL STATUS: Blocked on Twelf's mode system constraints.
%%
%% See notes-on-proofs.md for detailed analysis.
%%
%% The proof sketch is:
%%
%% mult-distrib-left/z : mult-distrib-left _ mult/z mult/z mult/z add/z.
%%
%% mult-distrib-left/s : mult-distrib-left Dadd_BC (mult/s Dadd_BC_ABC' Dmult_ABC')
%%                                         (mult/s Dadd_B_AB' Dmult_AB')
%%                                         (mult/s Dadd_C_AC' Dmult_AC')
%%                                         Dadd_AB_AC
%%                       <- 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'
%%                                       Dadd_BC_ABC Dadd_AB_AC.

%% ============================================================
%% ASSOCIATIVITY OF MULTIPLICATION (INCOMPLETE)
%% ============================================================

%% (A * B) * C = A * (B * C)
%%
%% STATUS: Depends on mult-distrib-left which is incomplete
%%
%% Would require mult-distrib-left to be completed first.

%% mult-assoc : mult A B AB -> mult AB C R1 -> mult B C BC -> mult A BC R1 -> type.
%% %mode mult-assoc +D1 +D2 +D3 -D4.
%%
%% mult-assoc/z : mult-assoc mult/z mult/z _ mult/z.
%%
%% mult-assoc/s : mult-assoc (mult/s Dadd1 Dmult1) (mult/s Dadd2 Dmult2) DmultBC (mult/s Dadd4 Dmult4)
%%                 <- mult-assoc Dmult1 Dmult2 DmultBC Dmult3
%%                 <- mult-total B C DmultBC
%%                 <- mult-distrib-left Dmult4 Dadd1 Dmult3 DmultBC Dadd3
%%                 <- add-func Dadd2 Dadd3 nat-eq/refl.
%%
%% %worlds () (mult-assoc _ _ _ _).
%% %total D (mult-assoc D _ _ _).

%% ============================================================
%% RIGHT DISTRIBUTIVITY (INCOMPLETE)
%% ============================================================

%% (A + B) * C = A*C + B*C
%%
%% STATUS: Depends on mult-comm and mult-distrib-left which are incomplete
%%
%% Would require both commutativity and left distributivity.

%% mult-distrib-right : mult AB C R -> add A B AB -> mult A C AC -> mult B C BC -> add AC BC R -> type.
%% %mode mult-distrib-right +D1 +D2 +D3 +D4 -D5.
%%
%% mult-distrib-right/case : mult-distrib-right Dmult1 DaddAB DmultAC DmultBC DaddResult
%%                            <- mult-comm Dmult1 Dmult1'
%%                            <- mult-comm DmultAC DmultAC'
%%                            <- mult-comm DmultBC DmultBC'
%%                            <- mult-distrib-left Dmult1' DaddAB DmultAC' DmultBC' DaddResult.
%%
%% %worlds () (mult-distrib-right _ _ _ _ _).
%% %total {} (mult-distrib-right _ _ _ _ _).