123 lines
3.7 KiB
Plaintext
123 lines
3.7 KiB
Plaintext
%% 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 _ _).
|