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.

2 comments:

Anonymous said...

holy jesus wtf

David Curran said...

You sir are a genius. I just would not ask you to help split a bill.