(*

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

## Sunday, 1 March 2009

### How to halve a number

Subscribe to:
Post Comments (Atom)

## 2 comments:

holy jesus wtf

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

Post a comment