%{ 

== Natural numbers ==

}%

nat : type.

zero : nat.
succ : nat -> nat.

%{

== Addition ==

}%

add : nat -> nat -> nat -> type.

add/z : add zero N N.

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

%{

=== Example derivations ===

}%

1 : nat = succ zero.
2 : nat = succ 1.
1+1is2 : add 1 1 2 = add/s (add/z).

%{

== Exercise: Multiplication ==

}%

mult : nat -> nat -> nat -> type.








%% The syntax '% .' (without the space)
%% causes Twelf to stop processing the file at this point
%% remove once you have completed the exercise
%.

%% note that the arguments are "backwards"
1*2is2 : mult 1 2 2 = mult/s (add/s (add/s add/z)) mult/z.

%{

== Mode, worlds total ==

}%

%mode add +M +N -P.
%worlds () (add _ _ _).
%total M (add M _ _).

%solve 1+1is2' : add 1 1 N.

%mode mult +M +N -P.
%worlds () (mult _ _ _).
%total M (mult M _ _).

%{

== Right-hand zero ==

}%

rhzero : {M : nat} add M zero M -> type.
%mode rhzero +M -D.

- : rhzero zero add/z.
- : rhzero (succ M) (add/s D)
     <- rhzero M (D : add M zero M).
     
%worlds () (rhzero _ _).
%total M (rhzero M _).

%{

== Right-hand succ ==

}%

rhsucc : add M N P -> add M (succ N) (succ P) -> type.
%mode rhsucc +D1 -D2.

- : rhsucc (add/z : add zero M M) (add/z : add zero (succ M) (succ M)).
- : rhsucc (add/s (D1 : add M N P)) (add/s D2)
     <- rhsucc D1 (D2 : add M (succ N) (succ P)).
     
%worlds () (rhsucc _ _).
%total M (rhsucc M _).

%{

== Exercise: Prove that addition is commutative ==

}%