POPL Tutorial/Basics Starter

From The Twelf Project
Jump to: navigation, search
This is Literate Twelf
Code: here
Status: %% OK %%
Output: here.

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

}%