POPL Tutorial/Basics Starter
From The Twelf Project
| This is Literate Twelf Code: here Status: %% OK %% Output: here. |
Contents |
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
}%
