115 lines
3.4 KiB
Plaintext
115 lines
3.4 KiB
Plaintext
|
%% 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
|