POPL Tutorial/Basics Starter

Natural numbers

%sort nat %.
%term zero nat %.
%term succ %pi nat %-> nat %.

Addition

%sort add {_ nat} {_ nat} {_ nat} %.
%term add/z add zero N N %.
%term add/s %pi (add (succ M) N (succ P)) %<- (add M N P) %.

Example derivations

%define 1 nat succ zero %.
%define 2 nat succ 1 %.
%define 1+1is2 (add 1 1 2) add/s add/z %.

Exercise: Multiplication

%sort mult {_ nat} {_ nat} {_ nat} %.
%% 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"

Mode, worlds total

Right-hand zero

Right-hand succ

Exercise: Prove that addition is commutative

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

%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 _ _).

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 _).

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 _).