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