Friday 27 March 2009

Type Checker

prototype


import Control.Monad
import Control.Monad.Error
import Control.Monad.Identity
import Data.Maybe
import Data.Char
import Text.ParserCombinators.ReadP

-- Proof irrelevance is implemented by:
--
-- erase(Gamma) |- phi : P
-- ----------------------- Prf
-- Gamma |- []phi : Prf(P)
--
-- []phi =def []psi : Prf(_)
--
-- Allow eliminations like P(x) -> Prf(x = y) -> P(y)
-- along the same schema as Coqs Prop sort, this gives us Axiom K.

-- * I am not a number: I am a free variable
-- * Verifying a Semantic beta-eta-Conversion Test for Martin-Löf Type Theory
-- * Intensionality, extensionality, and proof irrelevance in modal type theory

-- Syntax

type Ref = Int
newtype Scope a = Scope a
deriving Show

data Name
= Local Ref
| Global String
deriving (Eq, Show)

data T
= Type
| Pi T (Scope T)
| Prf T
| Lam T (Scope T)
| Square T
| App T T
| Def String
| Bound Ref
| Free Name
deriving Show

abstract x expr = Scope (rip 0 expr) where
rip i Type = Type
rip i (Pi tau (Scope sigma)) = Pi (rip i tau) (Scope (rip (i+1) sigma))
rip i (Prf p) = Prf (rip i p)
rip i (Lam tau (Scope sigma)) = Lam (rip i tau) (Scope (rip (i+1) sigma))
rip i (Square s) = Square (rip i s)
rip i (App m n) = App (rip i m) (rip i n)
rip i (Def d) = Def d
rip i (Bound j) = Bound j
rip i (Free j)
| x == j = Bound i
| otherwise = Free j

instantiate y (Scope expr) = shove 0 expr where
shove i Type = Type
shove i (Pi tau (Scope sigma)) = Pi (shove i tau) (Scope (shove (i+1) sigma))
shove i (Prf p) = Prf (shove i p)
shove i (Lam tau (Scope sigma)) = Lam (shove i tau) (Scope (shove (i+1) sigma))
shove i (Square s) = Square (shove i s)
shove i (App m n) = App (shove i m) (shove i n)
shove i (Def d) = Def d
shove i (Bound j)
| i == j = y
| otherwise = Bound j
shove i (Free j) = Free j

-- Parsing

-- *
-- /\(x:T),x
-- Prf(P)
-- \(x:T),x
-- []P
-- T T
-- x

parseTerm = readP_to_S pTerm

pTerm = pPi +++ pLam +++
do a <- skipSpaces >> pSimpleUnit ; as <- many (skipSpaces >> pUnit) ; skipSpaces ; return (foldl1 App (a:as))
pUnit = pType +++ pPi +++ pPrf +++ pLam +++ pSquare +++ pFree +++ parens pTerm
pSimpleUnit = pType +++ pPrf +++ pSquare +++ pFree +++ parens pTerm

pType = do string "*" ; return Type
pPi = do string "/\\" ; (x, t) <- binder ; string "," ; b <- pTerm ; return (Pi t (abstract x b))
pPrf = do string "Prf" ; m <- parens pTerm ; return (Prf m)
pLam = do string "\\" ; (x, t) <- binder ; string "," ; b <- pTerm ; return (Lam t (abstract x b))
pSquare = do string "[]" ; m <- pTerm ; return (Square m)
pFree = do a <- name ; guard (a /= "Prf") ; return (Free (Global a))

name = munch1 isAlpha
binder = b +++ parens b where
b = do a <- name ; string ":" ; x <- pTerm ; return (Global a,x)
parens p = do string "(" ; r <- p ; string ")" ; return r

-- bug 1: (\x:*,\y:*,x y)
-- parses as: (\x:*,(\y:*,(x y)))
-- or: (\x:*,(\y:*,x) y)
-- or: ((\x:*,\y:*,x) y)
-- fix: introduced 'simple' units and changed pTerm
-- from being applications of [unit unit ...] to [simpleUnit unit ...]

-- Typing

data V
= VType
| VPi V (V -> V)
| VPrf V
| VLam (V -> V)
| VSquare V
| VNeutral N
data N
= NApp N V
| NFree Name

VLam f % x = f x
VNeutral n % x = VNeutral (NApp n x)
_ % _ = error "Malformed application"

eval delta xi Type = VType
eval delta xi (Pi tau (Scope sigma)) = VPi (eval delta xi tau) (\x -> eval (x:delta) xi sigma)
eval delta xi (Prf p) = VPrf (eval delta xi p)
eval delta xi (Lam _ (Scope f)) = VLam (\x -> eval (x:delta) xi f)
eval delta xi (Square s) = VSquare (eval delta xi s)
eval delta xi (App m n) = eval delta xi m % eval delta xi n
eval delta xi (Def d) = fromJust (lookup d xi)
eval delta xi (Bound i) = delta !! i
eval delta xi (Free j) = VNeutral (NFree j)

quote q VType = Type
quote q (VPi tau sigmaF) = Pi (quote q tau) (abstract (Local q) (quote (q+1) (sigmaF (VNeutral (NFree (Local q))))))
quote q (VPrf p) = Prf (quote q p)
quote q (VLam f) = Lam Type (abstract (Local q) (quote (q+1) (f (VNeutral (NFree (Local q))))))
quote q (VSquare s) = Square (quote q s)
quote q (VNeutral n) = nquote q n
nquote q (NApp n v) = App (nquote q n) (quote q v)
nquote q (NFree j) = Free j

abstractV i VType _ = VType
abstractV i (VPi tau sigmaF) o = VPi (abstractV i tau o) (\e -> abstractV i (sigmaF e) o)
abstractV i (VPrf p) x = VPrf (abstractV i p x)
abstractV i (VLam sigmaF) o = VLam (\e -> abstractV i (sigmaF e) o)
abstractV i (VSquare s) x = VSquare (abstractV i s x)
abstractV i (VNeutral n) x = abstractN i n x
abstractN i (NApp n m) x = abstractN i n x % abstractV i m x
abstractN i (NFree j) x
| i == j = x
| otherwise = VNeutral (NFree j)

type Infer = ErrorT String Identity
runInfer :: Infer o -> Either String o
runInfer m = runIdentity (runErrorT m)

conv q gamma VType VType = True
conv q gamma (VPi tau sigmaF) (VPi tau' sigmaF') =
conv q gamma tau tau' && conv (q+1) ((Local q, tau):gamma) (sigmaF x) (sigmaF' x) where
x = VNeutral (NFree (Local q))
conv q gamma (VPrf p) (VPrf p') = conv q gamma p p'
conv q gamma (VNeutral n) (VNeutral m) = maybe False (const True) (convN q gamma n m)
conv q gamma _ _ = False
convV q gamma f g (VPi tau sigmaF) = convV (q+1) ((Local q, tau):gamma) (f % x) (g % x) (sigmaF x)
where x = VNeutral (NFree (Local q))
convV q gamma _ _ (VPrf _) = True
convV q gamma (VNeutral n) (VNeutral m) _ = maybe False (const True) (convN q gamma n m)
convV q gamma t s VType = conv q gamma t s
convN q gamma (NFree i) (NFree j)
| i == j = lookup i gamma
convN q gamma (NApp f x) (NApp g y) = do
VPi tau sigmaF <- convN q gamma f g
case convV q gamma x y tau of
True -> Just (sigmaF x)
False -> Nothing
convN q gamma n m = do
case (convN q gamma n n, convN q gamma m m) of
(Just (VPrf p), Just (VPrf p')) | conv q gamma (VPrf p) (VPrf p') -> Just (VPrf p)
_ -> Nothing

erase = map (\(q,tau) -> (q,eraseV tau))
eraseV (VPrf p) = eraseV p
eraseV sigma = sigma

infer :: Ref -> [(Name, V)] -> [(String, V)] -> T -> Infer V
infer q gamma xi Type = return VType
infer q gamma xi (Pi tau scopeSigma) = do
VType <- infer q gamma xi tau
VType <- infer (q+1) ((Local q, VType):gamma) xi (instantiate (Free (Local q)) scopeSigma)
return VType
infer q gamma xi (Prf p) = do
VType <- infer q gamma xi p
return VType
infer q gamma xi (Lam tau scopeM) = do
VType <- infer q gamma xi tau
tau' <- return $ eval [] xi tau
sigmaF <- infer (q+1) ((Local q, tau'):gamma) xi (instantiate (Free (Local q)) scopeM)
pi <- return $ VPi tau' (abstractV (Local q) sigmaF)
return pi
infer q gamma xi (Square s) = do
p <- infer q (erase gamma) xi s -- How do local definitions relate to erasure?
return (VPrf p)
infer q gamma xi (App m n) = do
pi <- infer q gamma xi m
case pi of
VPi sigma tauF -> do
sigma' <- infer q gamma xi n
case conv q gamma sigma sigma' of
True -> return (tauF (eval [] xi n))
False -> throwError (unlines [ "Type error in application: "
, " expected: " ++ show (quote q sigma)
, " received: " ++ show (quote q sigma')
])
_ -> throwError "Nonfunctional application"
infer q gamma xi (Def d) = do
infer q gamma xi (Free (Global d))
infer q gamma xi (Bound _) = do
throwError "Encountered a bound variable"
infer q gamma xi (Free j) = do
case lookup j gamma of
Just tau -> return tau
Nothing -> case j of
Local _ -> throwError "Free local variable"
Global j -> throwError ("Free global variable: " ++ j)

inferType gamma xi t = case runInfer (infer q gamma xi t) of
Left err -> Left err
Right tau -> Right (quote q tau)
where q = length gamma + 1

checkType gamma xi t tau = case runInfer (infer q gamma xi t) of
Left err -> Left err
Right tau' -> Right (conv q gamma tau tau')
where q = length gamma + 1

unstickDefinitions xi Type = Type
unstickDefinitions xi (Pi t (Scope b)) = Pi (unstickDefinitions xi t) (Scope (unstickDefinitions xi b))
unstickDefinitions xi (Prf p) = Prf (unstickDefinitions xi p)
unstickDefinitions xi (Lam t (Scope b)) = Lam (unstickDefinitions xi t) (Scope (unstickDefinitions xi b))
unstickDefinitions xi (Square p) = Square (unstickDefinitions xi p)
unstickDefinitions xi (App m n) = App (unstickDefinitions xi m) (unstickDefinitions xi n)
unstickDefinitions xi (Def d) = Def d
unstickDefinitions xi (Bound j) = Bound j
unstickDefinitions xi (Free (Local j)) = Free (Local j)
unstickDefinitions xi (Free (Global g)) =
case lookup g xi of
Nothing -> Free (Global g)
Just _ -> Def g
-- TODO: that was silly, find a sensible fold for T

-- User interfacing

repl gamma xi = do
putStr "> "
line <- getLine
case parseTerm line of
[] -> putStrLn "No parse"
[(t,"")] -> case inferType gamma xi (unstickDefinitions xi t) of
Left err -> putStrLn err
Right ty -> print ty
[(_,stuff)] -> putStrLn ("extra stuff at end of line: " ++ stuff)
ambiguous -> putStrLn ("ambiguous parse: " ++ show (length ambiguous) ++ " alternatives")
repl gamma xi

-- Examples/Toys

-- nat : *; Z : nat; S : nat -> nat
nat =
[ (Global "nat", VType)
, (Global "Z", zType)
, (Global "S", sType)
, (Global "natElim", natElimType)
]
natDefs =
[ ("natElim", natElimV)
]
zType = VNeutral (NFree (Global "nat"))
sType = VPi (VNeutral (NFree (Global "nat"))) (\_ -> VNeutral (NFree (Global "nat")))
natElimType = VPi (VPi (VNeutral (nfree "nat")) (\_ -> VType)) (\p -> -- forall P : nat -> Type,
VPi (p % (VNeutral (nfree "Z"))) (\_ -> -- P 0 ->
VPi (VPi (VNeutral (nfree "nat")) (\n -> -- (forall n : nat,
VPi (p % n) (\_ -> (p % (VNeutral (nfree "S") % n))))) (\_ -> -- P n -> P (S n)) ->
VPi (VNeutral (nfree "nat")) (\n -> p % n)))) -- forall n : nat, P n
where nfree = NFree . Global
natElimV = VLam (\motive -> VLam (\zero -> VLam (\succ -> VLam (\n -> natElim motive zero succ n))))
natElim motive zero succ (VNeutral (NFree (Global "Z"))) = zero
natElim motive zero succ (VNeutral (NApp (NFree (Global "S")) m)) = succ % m % natElim motive zero succ m
natElim motive zero succ stuck = VNeutral (NFree (Global "natElim")) % motive % zero % succ % stuck

-- add : Pi (Free (Global "nat")) (Scope (Pi (Free (Global "nat")) (Scope (Free (Global "nat")))))
-- := (\(x:nat),\(y:nat),natElim (\(n:nat),nat) x (\(T:nat),S) y)
add =
[ (Global "add", addType)
]
addDefs =
[ ("add", addValue)
]
addType = VPi (VNeutral (NFree (Global "nat"))) (\_ ->
VPi (VNeutral (NFree (Global "nat"))) (\_ ->
VNeutral (NFree (Global "nat"))))
addValue = VLam (\x -> VLam (\y ->
natElimV % (VLam (\_ -> VNeutral (NFree (Global "nat")))) % y % (VLam (\_ -> VNeutral (NFree (Global "S")))) % x))

-- eq : /\T:*, T -> T -> *; refl : /\T:*,/\t:T, eq T t t
eq =
[ (Global "eq", VPi VType (\t -> VPi t (\_ -> VPi t (\_ -> VType))))
, (Global "refl", reflType)
, (Global "eqElim", eqElimType)
, (Global "eqPrfElim", eqPrfElimType) -- eq has only one constructor so allow Proof eliminations
]
eqDefs =
[ ("eqElim", eqElimV)
, ("eqPrfElim", eqElimV)
]
reflType = VPi VType (\t -> VPi t (\t' -> VNeutral (NFree (Global "eq")) % t % t' % t'))
eqElimType = VPi VType (\a -> VPi a (\x -> VPi (VPi a (\_ -> VType)) (\p -> -- forall (A : Type) (x : A) (P : A -> Type),
VPi (p % x) (\_ -> VPi a (\y -> -- P x -> forall y : A,
VPi (VNeutral (NFree (Global "eq")) % a % x % y) (\_ -> p % y)))))) -- x = y -> P y
eqPrfElimType = VPi VType (\a -> VPi a (\x -> VPi (VPi a (\_ -> VType)) (\p -> -- forall (A : Type) (x : A) (P : A -> Type),
VPi (p % x) (\_ -> VPi a (\y -> -- P x -> forall y : A,
VPi (VPrf (VNeutral (NFree (Global "eq")) % a % x % y)) (\_ -> p % y)))))) -- Prf(x = y) -> P y
eqElimV = VLam (\a -> VLam (\x -> VLam (\motive -> VLam (\pX -> VLam (\y -> VLam (\eqPrf -> eqElim pX eqPrf))))))
eqElim pX (VNeutral (NApp (NFree (Global "refl")) _)) = pX
eqElim _ _ = error "not implemented"

-- Example session:
--
-- Main> repl (nat ++ add ++ eq) (natDefs ++ addDefs ++ eqDefs)
--
-- -- join for the Prf monad:
--
-- > \P:*,\phi:Prf(Prf(P)),[]phi
-- Pi Type (Scope (Pi (Prf (Prf (Bound 0))) (Scope (Prf (Bound 1)))))
--
-- -- proof of eq symmetry:
--
-- > (\T:*,\a:T,\b:T,\e:eq T a b,eqElim T a (\x:T,eq T x a) (refl T a) b e)
-- Pi Type (Scope (Pi (Bound 0) (Scope (Pi (Bound 1) (Scope (Pi (App (App (App (Free (Global "eq")) (Bound 2)) (Bound 1)) (Bound 0)) (Scope (App (App (App (Free (Global "eq")) (Bound 3)) (Bound 1)) (Bound 2)))))))))
--
-- -- that is: /\T:*,/\a:T,/\b:T,/\(a = b),b = a
--
-- proof of f_equal, x = y -> f x = f y
--
-- > (\x:nat,\y:nat,\f:(/\n:nat,nat),\e:eq nat x y,eqElim nat x (\y:nat,eq nat (f x) (f y)) (refl nat (f x)) y e)
-- Pi (Free (Global "nat")) (Scope (
-- Pi (Free (Global "nat")) (Scope (
-- Pi (Pi (Free (Global "nat")) (Scope (Free (Global "nat")))) (Scope (
-- Pi (App (App (App (Free (Global "eq")) (Free (Global "nat"))) (Bound 2)) (Bound 1)) (Scope (
-- App (App (App (Free (Global "eq")) (Free (Global "nat"))) (App (Bound 1) (Bound 3))) (App (Bound 1) (Bound 2))))))))))
--
-- Induction proof that: n + 0 = n
--
-- > (natElim (\n:nat,eq nat (add n Z) n) (refl nat Z) (\n:nat,\e:eq nat (add n Z) n,(\x:nat,\y:nat,\f:(/\n:nat,nat),\e:eq nat x y,eqElim nat x (\y:nat,eq nat (f x) (f y)) (refl nat (f x)) y e) (add n Z) n S e))
-- Pi (Free (Global "nat")) (Scope (
-- App (App (App (Free (Global "eq")) (Free (Global "nat")))
-- (App (App (App (App (Free (Global "natElim"))
-- (Lam Type (Scope (Free (Global "nat")))))
-- (Free (Global "Z")))
-- (Lam Type (Scope (Free (Global "S")))))
-- (Bound 0)))
-- (Bound 0)))

Sunday 1 March 2009

How to halve a number


(*
* How to halve a number
* ---------------------
*)

(* (* just so we start on the same page, what is a number? *)
*
* Inductive nat : Set :=
* | O : nat
* | S : nat -> nat.
*)

Module Type Halver.

Parameter half : nat -> nat.

Axiom e1 : half 0 = 0.
Axiom e2 : half 1 = 0.
Axiom e3 : forall n, half (S (S n)) = S (half n).

(* An equational specification is given as a module
* so now it is possible it give various implementations
*)

End Halver.

Module By_Default : Halver.

Fixpoint half (n : nat) : nat :=
match n with
| O => O
| S O => O
| S (S n) => S (half n)
end.

Definition e1 : half 0 = 0 := refl_equal _.
Definition e2 : half 1 = 0 := refl_equal _.
Definition e3 n : half (S (S n)) = S (half n) := refl_equal _.

(* This is the sort of thing one would normally start with,
* pattern match on a term and use recursive calls on a
* structurally smaller term, the idea of 'structurally smaller'
* is part of the type rules actually and it is the transitive
* closure of (1) p_i < C p_1 p_2 ... p_n
* and (2) f x < f
* rule (1) and (2) say that a term in smaller than any
* construction built from it, a construction being something
* literally built from constructor or a function
*)

End By_Default.

Module By_Divine_Inspiration : Halver.

(* Definition half n :=
* fst (nat_rect (fun _ => (nat * nat)%type)
* (O, O)
* (fun n Pn => let (p,q) := Pn in (q, S p))
* n).
* (* it seems impossible to prove this one correct *)
*)

Definition half n :=
fst (nat_rect (fun _ => (nat * nat)%type)
(O, O)
(fun n Pn => (snd Pn, S (fst Pn)))
n).

Definition e1 : half 0 = 0 := refl_equal _.
Definition e2 : half 1 = 0 := refl_equal _.
Definition e3 n : half (S (S n)) = S (half n) := refl_equal _.

End By_Divine_Inspiration.

Module By_Devising_Data : Halver.

(* This way seems like a 'view' in the sense of Wadler,
* The structure of the data make the program definition
* straight-forward.
*)

Inductive nat' : Set :=
| Zero : nat'
| One : nat'
| SuccSucc : nat' -> nat'.

Definition zero := Zero.
Fixpoint succ (n : nat') :=
match n with
| Zero => One
| One => SuccSucc Zero
| SuccSucc n => SuccSucc (succ n)
end.

Fixpoint nat_to_nat' (n : nat) : nat' :=
match n with
| O => zero
| S n => succ (nat_to_nat' n)
end.

Fixpoint half' (n : nat') : nat :=
match n with
| Zero => O
| One => O
| SuccSucc n => S (half' n)
end.

Definition half n := half' (nat_to_nat' n).

Definition e1 : half 0 = 0 := refl_equal _.
Definition e2 : half 1 = 0 := refl_equal _.

Lemma succ_succs n : succ (succ n) = SuccSucc n.
induction n; simpl; try reflexivity.
rewrite IHn; reflexivity.
Qed.

Theorem e3 n : half (S (S n)) = S (half n).
intro n.
unfold half.
simpl.
rewrite succ_succs.
reflexivity.
Qed.

End By_Devising_Data.

Module By_Mutual_Induction : Halver.

Inductive Even : nat -> Set :=
| EvenO : Even O
| EvenS n : Odd n -> Even (S n)
with Odd : nat -> Set :=
| OddS n : Even n -> Odd (S n).

Fixpoint even_or_odd n : Even n + Odd n :=
match n as n return Even n + Odd n with
| O => inl _ EvenO
| S n =>
match even_or_odd n with
| inl even => inr _ (OddS _ even)
| inr odd => inl _ (EvenS _ odd)
end
end.

Fixpoint halfE n (e : Even n) : nat :=
match e with
| EvenO => O
| EvenS n odd => S (halfO n odd)
end
with halfO n (o : Odd n) : nat :=
match o with
| OddS n even => halfE n even
end.

Definition half (n : nat) : nat :=
match even_or_odd n with
| inl even => halfE n even
| inr odd => halfO n odd
end.

(* Proving this program correct is quite a lot
* of work compared to the previous implementations,
* these tricky inversion lemmas which would be trivial
* to prove using pattern matching at least show some
* techniques.
*)

Lemma unique_lemma_1 (e : Even 0) : e = EvenO.
intro e.
refine (
match e as e' in Even Zero return
match Zero return Even Zero -> Prop with
| O => fun e'' : Even 0 => e'' = EvenO
| S _ => fun _ => True
end e'
with
| EvenO => refl_equal _
| EvenS _ _ => I
end
).
Qed.

Lemma unique_lemma_2 n (e : Even (S n)) : { o' : _ | e = EvenS n o' }.
intros n e.
refine (
match e as e' in Even SuccN return
match SuccN return Even SuccN -> Set with
| O => fun _ => True
| S n => fun e' : Even (S n) =>
{ o' : _ | e' = EvenS n o' }
end e'
with
| EvenO => I
| EvenS n' o' => exist _ o' (refl_equal _)
end
).
Qed.

Lemma unique_lemma_3 n (o : Odd (S n)) : { e' : _ | o = OddS n e' }.
intros n o.
refine (
match o as o' in Odd SuccN return
match SuccN return Odd SuccN -> Set with
| O => fun _ => True
| S n => fun o' : Odd (S n) =>
{ e' : _ | o' = OddS n e' }
end o'
with
| OddS n' e' => exist _ e' (refl_equal _)
end
).
Qed.

(* There is only one way to prove a number is Even
* and similarly to prove it's Odd
*)

Theorem unique_classificationE n (e e' : Even n) : e = e'
with unique_classificationO n (o o' : Odd n) : o = o'.
induction n; intros.

rewrite unique_lemma_1 with e.
rewrite unique_lemma_1 with e'.
reflexivity.

destruct (unique_lemma_2 _ e) as [o eq].
destruct (unique_lemma_2 _ e') as [o' eq'].
rewrite eq; rewrite eq'.
rewrite (unique_classificationO n o o').
reflexivity.

destruct n.
intro H; inversion H.
intros.
destruct (unique_lemma_3 _ o) as [e eq].
destruct (unique_lemma_3 _ o') as [e' eq'].
rewrite eq; rewrite eq'.
rewrite (unique_classificationE n e e').
reflexivity.
Qed.

Lemma halfE_SS n e e' : halfE (S (S n)) e' = S (halfE n e)
with halfO_SS n o o' : halfO (S (S n)) o' = S (halfO n o).
intros.
destruct (unique_lemma_2 _ e') as [o eq].
destruct (unique_lemma_3 _ o) as [e'' eq'].
subst.
simpl.
assert (e = e'') as E by apply unique_classificationE.
rewrite E; reflexivity.

intros.
destruct (unique_lemma_3 _ o') as [e eq].
destruct (unique_lemma_2 _ e) as [o'' eq'].
subst.
simpl.
assert (o = o'') as O by apply unique_classificationO.
rewrite O; reflexivity.
Qed.

Definition which P Q : P + Q -> bool :=
fun choice =>
match choice with
| inl _ => true
| inr _ => false
end.
Lemma even_or_odd_SS n : which _ _ (even_or_odd (S (S n))) = which _ _ (even_or_odd n).
induction n.
reflexivity.
simpl in *.
destruct (even_or_odd n).
reflexivity.
reflexivity.
Qed.

Definition e1 : half 0 = 0 := refl_equal _.
Definition e2 : half 1 = 0 := refl_equal _.
Theorem e3 n : half (S (S n)) = S (half n).
intro n.
unfold half.
generalize (even_or_odd_SS n).
destruct (even_or_odd n); destruct (even_or_odd (S (S n)));
simpl; intro hyp; try discriminate hyp.
apply halfE_SS.
apply halfO_SS.
Qed.

End By_Mutual_Induction.

Module By_Well_Founded_Induction : Halver.

Section Well_Founded_Relations.

Variable A : Type.
Variable R : A -> A -> Prop.

Inductive Acc (x : A) : Prop :=
| below : (forall y : A, R y x -> Acc y) -> Acc x.

(* x must be a parameter (instead of Acc : A -> Prop) for
* Set/Type elimination, but why?
*)

Definition Well_Founded := forall x : A, Acc x.

Inductive Transitive_Closure : A -> A -> Prop :=
| step x y : R x y -> Transitive_Closure x y
| transitivity x y z : R x y -> Transitive_Closure y z -> Transitive_Closure x z.

Definition Well_Founded_Induction
(W : Well_Founded)
(P : A -> Type)
(rec : forall x, (forall y, R y x -> P y) -> P x)
: forall a, P a :=
fun a => Acc_rect P (fun x _ hyp => rec x hyp) a (W a).

End Well_Founded_Relations.

Section Transitive_Relation.

Variable A : Type.
Variable R : A -> A -> Prop.

Theorem Transitive_Closure_Well_Founded :
Well_Founded A R -> Well_Founded A (Transitive_Closure A R).
Proof.
unfold Well_Founded; intros R_Acc x.

induction (R_Acc x) as [x R_ind T_ind].

apply below; intros y Trans.

induction Trans.

apply T_ind; assumption.

pose (IHTrans R_ind T_ind) as IH; inversion IH as [H']; subst.
apply H'.
apply step.
assumption.
Defined.

End Transitive_Relation.

Section Nat_Structural_Measure.

(* Looking at the definition of nat: *)

(*
* Inductive nat : Set :=
* | O : nat
* | S : nat -> nat.
*)

(* shows there is one (simple) recursive field *)

Inductive nat_step : nat -> nat -> Prop :=
| nat_step_a : forall x, nat_step x (S x).

(* the nat_step relation expresses this recursion
* every inductive type admits a step relation
* (indexed inductives define indexed relations,
* but maybe wrappig them in sigT would be better?)
*)

Theorem nat_step_Well_Founded : Well_Founded nat nat_step.

unfold Well_Founded.

induction x;
apply below; intros y Ry.

inversion Ry.

inversion Ry.
subst.
assumption.

Defined.

(* Could one generically define all Φ_step relations,
* and give a generic proof that they are all Well_Founded?
*)

(* The transitive closure of the step relation corresponds to
* the usual idea of lt/(<) on nat:
*)

Definition nat_struct := Transitive_Closure nat nat_step.
Definition nat_struct_Well_Founded :=
Transitive_Closure_Well_Founded nat nat_step nat_step_Well_Founded.

(* In general terms it is a typed version of the 'structurally smaller'
* relation in the metatheory which lets definitions like the one in
* By_Default be accepted
*)

End Nat_Structural_Measure.

(* Now the equations we want to satisy are: *)

(*
* half O := O
* half (S O) := O
* half (S (S n)) := S (half n)
*)

(* so in terms of (toned down) eliminators that is:
*
* half n := nat_case n
* O
* (fun n' Pn' =>
* nat_case n'
* O
* (fun n'' Pn'' =>
* S (half n''))).
*
* clearly that definition is not acceptable with
* no termination argument what-so-ever! so to
* rectify that, we can let P express that this
* number is smaller than n, and use well founded
* induction on the size measure.
*)

Lemma SSsmaller m : nat_struct m (S (S m)).
intro m.
apply transitivity with (S m).
constructor.
apply step.
constructor.
Defined.

Definition half := Well_Founded_Induction nat nat_struct nat_struct_Well_Founded
(fun _ => nat)
(nat_rec (fun x => (forall y : nat, nat_struct y x -> nat) -> nat)
(fun rec => O)
(fun n Pn rec =>
nat_rec (fun x => (forall y : nat, nat_struct y (S x) -> nat) -> nat)
(fun rec => O)
(fun m Pm rec => S (rec m (SSsmaller m)))
n
rec)).

(*
* The definition may look a bit complicated but I think this could
* be computed automatically from the equational specification,
* the method seems like a good way to compile dependent pattern matching
* into a basic type theory though, so that we don't have to use something
* like a 'match' construct.
*)

Definition e1 : half 0 = 0 := refl_equal _.
Definition e2 : half 1 = 0 := refl_equal _.
Definition e3 n : half (S (S n)) = S (half n) := refl_equal _.

(*
* It's not luck (at least I think it's not, and I really hope so)
* that the recursive equality is provable by reflexivity, but it
* does require the SSsmaller proof term to be canonical (made up
* of constructors), since every proof that a term is structurally
* smaller than another can be a canonical proof that poses no
* problem. I don't yet know how it will interact with dependent
* pattern match specialization though. (I can't think of any
* functions over inductive families that aren't 'step' recursive
* though, does anyone know of some examples?)
*)

End By_Well_Founded_Induction.