% An advanced example of proving termination and other properties
% of functions. We use McCarthy's 91 function
% f(n,k) = if k <= n then n else f(f(n+1,k),k)
% as described in Shin-Cheng Mu's post
% http://www.iis.sinica.edu.tw/~scm/2008/well-founded-recursion-and-accessibility/
% The straightforward implementation of the function in Twelf
% cannot be proven terminating as this requires too advanced reasoning.
% This file shows how to do this advanced reasoning.
% We do not modify the code of the function: rather, we state
% the property of the function, f91-prop below, and constructively prove it.
% The proof relies on the lexicographic structural recursion (see f91-thm).
% The bulk of this file is stating and proving trivial properties of
% arithmetic. Twelf knows nothing about the arithmetic.
% A term N of type nat is a nonnegative integer.
% Constructors: 0, 1.
nat: type. %name nat N.
0: nat.
1: nat -> nat. %prefix 200 1.
% sample natural numbers:
n1 = 1 0.
n2 = 1 n1.
n3 = 1 n2.
n4 = 1 n3.
% addition
plus: nat -> nat -> nat -> type.
%mode plus +N1 +N2 -N3.
plus-0: plus 0 N N.
plus-1: plus (1 N1) N2 (1 R) <- plus N1 N2 R.
%worlds () (plus _ _ _).
%total {N} (plus N _ _).
% The judgment (N1 ==nat N2) means that N1 is equal to N2.
==nat: nat -> nat -> type. %name ==nat E. %infix none 100 ==nat.
==nat_refl: N ==nat N.
% n == n1 ==> n+1 == n1+1
succ==: N ==nat N1 -> 1 N ==nat 1 N1 -> type.
%mode succ== +E1 -E2.
-: succ== ==nat_refl ==nat_refl.
%worlds () (succ== _ _).
%total {} (succ== _ _).
% successor and addition `commute'
% i+1 + n == i + (n+1)
plus-ink: plus (1 I) N (1 K) -> plus I (1 N) K1 -> (1 K) ==nat K1 -> type.
%mode plus-ink +P1 +P2 -EQ.
-: plus-ink (plus-1 plus-0) plus-0 ==nat_refl.
-: plus-ink (plus-1 (plus-1 P)) (plus-1 P1) R1
<- plus-ink (plus-1 P) P1 R
<- succ== R R1.
%worlds () (plus-ink _ _ _).
%total {P1} (plus-ink P1 _ _).
% Establishing the order on natural numbers.
<: nat -> nat -> type. %infix none 200 <.
%mode < +N1 +N2.
<-0: 0 < (1 N).
<-1: (1 N1) < (1 N2) <- N1 < N2.
%worlds () (< N1 N2).
%terminates {N1} (< N1 _).
<=: nat -> nat -> type. %infix none 200 <=.
%mode <= +N1 +N2.
<=-0: N <= N.
<=-1: N1 <= N2 <- N1 < N2.
%worlds () (<= N1 N2).
%terminates {N1} (<= N1 _).
% Proving many properties of the order
% n <= k ==> n < k+1
succ>: {N} N <= K -> N < (1 K) -> type.
%mode succ> +N +P1 -P2.
-: succ> 0 <=-0 <-0.
-: succ> (1 N) <=-0 (<-1 R) <- succ> N <=-0 R.
-: succ> 0 (<=-1 <-0) <-0.
-: succ> (1 N) (<=-1 (<-1 P)) (<-1 R) <- succ> N (<=-1 P) R.
%worlds () (succ> _ _ _).
%total {N P} (succ> N P _).
% relation < is irreflexive
% Alas, Twelf can't see that. We have to prove it, by contradiction.
falsum: type.
% No constructors.
%worlds () (falsum).
irrefl<: N < N -> falsum -> type.
%mode irrefl< +P -F.
-: irrefl< (<-1 P) R <- irrefl< P R.
%worlds () (irrefl< _ _).
%total {P} (irrefl< P _).
% Finally we can write our function
% McCarthy's 91 function,
% f(n,k) = if k <= n then n else f(f(n+1,k),k)
f91: nat -> nat -> nat -> type.
%mode f91 +N1 +N2 -N3.
f91-1: f91 N K N <- K <= N.
f91-2: f91 N K R
<- N < K
<- f91 (1 N) K R1
<- f91 R1 K R.
% %terminates {N1 N2} (f91 N1 N2 _). Can't prove termination
% Proving the property of f91:
% We prove that f91 is terminating, and furthermore, it is the maximum
% function.
% We only prove the non-obvious case: f91 n k = k for n <= k.
% Actually, we prove the following: for all i n, f91 n (i+n) = i+n.
% First, we define the desired property: f91 n (i+n) = i+n.
f91-prop: nat -> nat -> type.
%mode f91-prop +N1 +N2.
f91p: f91-prop I N <- plus I N K <- f91 N K K.
% Now we prove that f91-prop holds for all natural I and N.
% That is, for any given I and N, we can construct the proof term
% of the type f91-prop I N. The construction process is terminating
% and has no pattern-match errors.
f91-thm: {I} {N} f91-prop I N -> type.
%mode f91-thm +N1 +N2 -P.
% Base case: I = 0
f91t-1: f91-thm 0 N (f91p (f91-1 <=-0) plus-0).
% Build the proof of f91 out of, well, nothing.
% Since we shall never obtain nothing, the build process is simple.
ex-falsum-f91: {N} falsum -> f91 N (1 N) (1 N) -> type.
%mode ex-falsum-f91 +N +F -P.
%worlds () (ex-falsum-f91 _ _ _).
%total {} (ex-falsum-f91 _ _ _).
% This is the induction step:
% given the proofs that f91 N K is K and f91 (1 N) (1 K) is (1 K),
% construct the proof that f91 N (1 K) is (1 K).
build: f91 N K K -> f91 (1 N) (1 K) (1 K) -> f91 N (1 K) (1 K) -> type.
%mode build +P1 +P2 -P3.
build-1: build
(f91-1 <=-0) % that is, case N = K
F-N1-K1-K1 % this is the proof f91 (1 N) (1 K) (1 K)
(f91-2 F-N1-K1-K1 F-N1-K1-K1 N N <=-0 N N (<=-1 N f91 (1 N) K1 K1 -> f91 (1 N) (1 K) (1 K) -> type.
%mode indN1 +EQ +PF1 -PF2.
-: indN1 ==nat_refl P P.
%worlds () (indN1 _ _ _).
%total {} (indN1 _ _ _).
f91t-2: f91-thm (1 I) N (f91p R (plus-1 Plus-NI))
<- f91-thm I N (f91p FIN (Plus-NI:plus I N K))
<- f91-thm I (1 N) (f91p FIN1 Plus-IN1)
<- plus-ink (plus-1 Plus-NI) Plus-IN1 EQ
<- indN1 EQ FIN1 FIN1'
<- build FIN FIN1' R.
%worlds () (f91-thm _ _ _).
%total {I N} (f91-thm I N _).
% And Twelf agrees f91-thm is total!
% It is a total program that produces the proof term f91-prop.
% We've got the proof.