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.