% 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+1)
	 <- succ> N <=-0 N<N+1.
build-1f: build  
	 (f91-1 (<=-1 N<N)) % that is, case N < N, which is impossible
	 _		    % Alas, Twelf can't see that. So, we prove
	 R                  % the impossibility explicitly
	 <- irrefl< N<N FALSUM
	 <- ex-falsum-f91 _ FALSUM R.
build-2: build
	 (f91-2 F-R1-K-K F-N1-K-R1 N<K)
	 F-N1-K1-K1
	 (f91-2 (f91-1 <=-0) F-N1-K1-K1 N<K+1)
	 <- succ> N (<=-1 N<K) N<K+1.
%worlds () (build _ _ _).
%total {P1} (build P1 _ _).

% Twelf isn't good at the pattern-matching of the output argument
% We have to convert outputs to inputs... sigh...
indN1: (1 K) ==nat K1 -> 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.