%% exp.elf - Exponentiation on Natural Numbers
%%
%% Exponentiation is defined recursively:
%%   N^0 = 1
%%   N^(S M) = N * N^M

exp : nat -> nat -> nat -> type.
%mode exp +Base +Exponent -Result.

exp/z : exp N z (s z).          %% N^0 = 1
exp/s : exp N (s M) R
         <- exp N M P           %% P = N^M
         <- mult N P R.         %% R = N * P = N * N^M = N^(M+1)

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

exp-total/z : exp-total N z exp/z.
exp-total/s : exp-total N (s M) (exp/s Dmult Dexp)
               <- exp-total N M Dexp
               <- mult-total N _ Dmult.

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

%% ============================================================
%% BASIC EXPONENTIATION PROPERTIES
%% ============================================================

%% N^1 = N
exp-one : {N:nat} exp N (s z) N -> type.
%mode exp-one +N -D.

exp-one/base : exp-one N (exp/s Dmult exp/z)
                <- mult-right-one N Dmult.

%worlds () (exp-one _ _).
%total {} (exp-one _ _).

%% 1^N = 1
exp-base-one : {N:nat} exp (s z) N (s z) -> type.
%mode exp-base-one +N -D.

exp-base-one/z : exp-base-one z exp/z.
exp-base-one/s : exp-base-one (s N) (exp/s Dmult Dexp)
                  <- exp-base-one N Dexp
                  <- mult-left-one (s z) Dmult.

%worlds () (exp-base-one _ _).
%total N (exp-base-one N _).

%% 0^(S N) = 0 (0 to any positive power is 0)
exp-base-zero : {N:nat} exp z (s N) z -> type.
%mode exp-base-zero +N -D.

exp-base-zero/z : exp-base-zero z (exp/s mult/z exp/z).
exp-base-zero/s : exp-base-zero (s N) (exp/s mult/z Dexp)
                   <- exp-base-zero N Dexp.

%worlds () (exp-base-zero _ _).
%total N (exp-base-zero N _).

%% ============================================================
%% EXPONENT LAWS
%% ============================================================

%% Law 1: N^(A+B) = N^A * N^B
%% exp-add : exp N A PA -> exp N B PB -> add A B AB ->
%%           mult PA PB PAB -> exp N AB PAB -> type.

%% We'll prove this by induction on B

exp-add : {N:nat} {A:nat} {B:nat} {PA:nat} {PB:nat} {AB:nat} {PAB:nat}
          exp N A PA -> exp N B PB -> add A B AB ->
          mult PA PB PAB -> exp N AB PAB -> type.
%mode exp-add +N +A +B +PA +PB +AB +PAB +Da +Db +Dadd +Dmult -Dab.

%% Base case: B = 0
%% N^(A+0) = N^A = N^A * 1 = N^A * N^0
exp-add/z : exp-add N A z PA (s z) A PA
             Da exp/z Dadd Dmult Da
             <- add-right-z A Dadd'
             %% Need: Dadd : add A z A
             %% Have: Dadd' : add A z A from add-right-z
             %% Need: Dmult : mult PA (s z) PA
             <- mult-right-one PA Dmult'.

%% The full proof requires showing the inductive step which involves
%% associativity of multiplication. We state it here for completeness.

%% Law 2: (N^A)^B = N^(A*B)
%% This is the power of a power rule

%% Law 3: (M*N)^A = M^A * N^A
%% This is the power of a product rule

%% These proofs follow similar patterns but require the multiplication
%% lemmas we've developed.

%% ============================================================
%% USEFUL COMPUTATIONS
%% ============================================================

%% Let's verify some concrete exponentiations
%% 2^2 = 4
%% 2^3 = 8

%% We can use Twelf's %solve to compute these:
%% %solve D22 : exp two two R.
%% Should give R = four

%% %solve D23 : exp two three R.
%% Should give R = s (s (s (s (s (s (s (s z)))))))  = 8