%% add.elf - Addition on Natural Numbers
%%
%% Addition is defined recursively:
%%   0 + N = N
%%   (S M) + N = S (M + N)

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

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

%% Addition is total (always produces a result)
add-total : {M:nat} {N:nat} add M N P -> type.
%mode add-total +M +N -D.
add-total/z : add-total z N add/z.
add-total/s : add-total (s M) N (add/s D)
               <- add-total M N D.
%worlds () (add-total _ _ _).
%total M (add-total M _ _).

%% ============================================================
%% LEMMAS FOR COMMUTATIVITY
%% ============================================================

%% Right identity: N + 0 = N
add-right-z : {N:nat} add N z N -> type.
%mode add-right-z +N -D.
add-right-z/z : add-right-z z add/z.
add-right-z/s : add-right-z (s N) (add/s D)
                 <- add-right-z N D.
%worlds () (add-right-z _ _).
%total N (add-right-z N _).

%% Right successor: M + (S N) = S (M + N)
%% If add M N P, then add M (s N) (s P)
add-right-s : add M N P -> add M (s N) (s P) -> type.
%mode add-right-s +D1 -D2.
add-right-s/z : add-right-s add/z add/z.
add-right-s/s : add-right-s (add/s D1) (add/s D2)
                 <- add-right-s D1 D2.
%worlds () (add-right-s _ _).
%total D (add-right-s D _).

%% ============================================================
%% COMMUTATIVITY OF ADDITION
%% ============================================================

%% Main theorem: M + N = N + M
%% If add M N P, then add N M P
add-comm : add M N P -> add N M P -> type.
%mode add-comm +D1 -D2.

add-comm/z : add-comm add/z D
              <- add-right-z _ D.

add-comm/s : add-comm (add/s D1) D3
              <- add-comm D1 D2
              <- add-right-s D2 D3.

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

%% ============================================================
%% ASSOCIATIVITY OF ADDITION
%% ============================================================

%% Associativity using output factoring
%% We prove: forall A B C AB ABC. add A B AB -> add AB C ABC ->
%%           exists BC. add B C BC /\ add A BC ABC
%%
%% This formulation allows Twelf to find BC as an output.

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.

add-assoc/z : add-assoc add/z D D add/z.

add-assoc/s : add-assoc (add/s D1) (add/s D2) D3 (add/s D4)
               <- add-assoc D1 D2 D3 D4.

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

%% ============================================================
%% CANCELLATION LAWS
%% ============================================================

%% Left cancellation: if A + B = A + C then B = C
add-cancel-left : add A B R -> add A C R -> nat-eq B C -> type.
%mode add-cancel-left +D1 +D2 -E.

add-cancel-left/z : add-cancel-left add/z add/z nat-eq/refl.
add-cancel-left/s : add-cancel-left (add/s D1) (add/s D2) E
                     <- add-cancel-left D1 D2 E.

%worlds () (add-cancel-left _ _ _).
%total D (add-cancel-left D _ _).

%% ============================================================
%% FUNCTIONALITY (Determinism)
%% ============================================================

%% Helper: equality lifts through successor
nat-eq-s : nat-eq M N -> nat-eq (s M) (s N) -> type.
%mode nat-eq-s +E1 -E2.
nat-eq-s/refl : nat-eq-s nat-eq/refl nat-eq/refl.
%worlds () (nat-eq-s _ _).
%total {} (nat-eq-s _ _).

%% Addition is functional: if add M N P and add M N Q then P = Q
add-func : add M N P -> add M N Q -> nat-eq P Q -> type.
%mode add-func +D1 +D2 -E.

add-func/z : add-func add/z add/z nat-eq/refl.
add-func/s : add-func (add/s D1) (add/s D2) E'
              <- add-func D1 D2 E
              <- nat-eq-s E E'.

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