%% 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 (INCOMPLETE)
%% ============================================================

%% A * (B + C) = A*B + A*C
%%
%% STATUS: After extensive attempts (15+ different approaches across 3 sessions),
%% this proof remains incomplete due to the fundamental difficulty of the
%% required 4-way addition rearrangement:
%%   (B + AB') + (C + AC') = (B + C) + (AB' + AC')
%%
%% See PROOF_STATUS.md Sessions 2-3 for detailed technical analysis.
%%
%% The proof is mathematically sound but encoding it in Twelf's strict
%% mode system requires either:
%% - A more sophisticated library of addition rearrangement lemmas
%% - A different encoding of multiplication
%% - Reference to published Twelf proof patterns for this specific case

%% mult-distrib-left : mult A BC R1 -> add B C BC -> mult A B AB -> mult A C AC -> add AB AC R1 -> type.
%% %mode mult-distrib-left +D1 +D2 +D3 +D4 -D5.
%%
%% mult-distrib-left/z : mult-distrib-left mult/z _ mult/z mult/z add/z.
%%
%% mult-distrib-left/s : mult-distrib-left (mult/s Dadd1 Dmult1) DaddBC (mult/s Dadd2 Dmult2) (mult/s Dadd3 Dmult3) DaddFinal
%%                        <- mult-distrib-left Dmult1 DaddBC Dmult2 Dmult3 Dadd_IH
%%                        <- [complex rearrangement needed].
%%
%% %worlds () (mult-distrib-left _ _ _ _ _).
%% %total D (mult-distrib-left D _ _ _ _).

%% ============================================================
%% 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 _ _ _ _ _).