## 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.` 