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.

Easy Examples of Pattern Matching in Coq

(*
 * A couple of difficulties in Coq or dependently typed programming
 * are having to write impossible cases in pattern matches and
 * getting at the new information provided by a pattern match.
 *)

(* I'll use vectors (lists which have their length as part of the
 * type) to explain this since they are very simple objects
 *)

Inductive Vec (A : Set) : nat -> Set :=
| VNil : Vec A 0
| VCons : forall n, A -> Vec A n -> Vec A (S n).

(* It's pretty easy to define a total function taking the head
 * of any vector using tactics:
 *
Definition head (A : Set)(n : nat) :
  Vec A (S n) -> A.
intros.
inversion H.
exact H1.
Defined.
 * but actually this results in something terrifying:
Print head.

head = 
fun (A : Set) (n : nat) (H : Vec A (S n)) =>
let H0 :=
  match H in (Vec _ n0) return (n0 = S n -> A) with
  | VNil =>
      fun H0 : 0 = S n =>
      let H1 :=
        eq_ind 0 (fun e : nat => match e with
                                 | 0 => True
                                 | S _ => False
                                 end) I (S n) H0 in
      False_rec A H1
  | VCons n0 H0 H1 =>
      fun H2 : S n0 = S n =>
      let H3 :=
        let H3 :=
          f_equal (fun e : nat => match e with
                                  | 0 => n0
                                  | S n1 => n1
                                  end) H2 in
        eq_rect n (fun n1 : nat => A -> Vec A n1 -> A)
          (fun (H4 : A) (_ : Vec A n) => H4) n0 (sym_eq H3) in
      H3 H0 H1
  end in
H0 (refl_equal (S n))
     : forall (A : Set) (n : nat), Vec A (S n) -> A
 *
 * It would be much shorter to simple define it by pattern matching
 * but there is a problem,
 *)

(*
Definition head (A : Set)(n : nat) :
  Vec A (S n) -> A :=
  fun v =>
    match v with
      | VCons n a _ => a
    end.
 *
 * it seems ok but what we know (that a vector of length one or more
 * cannot ever be VNil) hasn't been made clear to Coq:
 *
   Error: Non exhaustive pattern-matching:
          no clause found for pattern VNil
 *)

(* To define head by pattern matching we must cover all cases
 * but there is certainly not object of type A to return given
 * a VNil object of type Vec A (S _), of course this is absurd.
 * So I'll use the solution given here:
 * http://pauillac.inria.fr/pipermail/coq-club/2008/003508.html
 *)

Definition head (A : Set)(n : nat) :
  Vec A (S n) -> A :=
  fun v =>
    match v in Vec _ m return
      match m with
        | 0 => True
        | _ => A
      end
      with
      | VNil => I
      | VCons n a _ => a
    end.

(* This is perfect, the trick is very clever!
 * the key is that [match m with | 0 => True | _ => A end] is
 * convertable to A since m = (S n).
 * then VNil is given a trivial case which must be of type True
 * (chosen arbitrarily) and VCons gives the actual definition
 * we wished for.
 *)

(* this is a big hassle, let's avoid going through it again .. *)
Definition tail (A : Set)(n : nat) :
  Vec A (S n) -> Vec A n.
intros; inversion H; trivial.
Defined.

(*
Theorem worm (A : Set)(n : nat) :
  forall (v : Vec A (S n)),
    v = VCons _ _ (head _ _ v) (tail _ _ v).
Proof.
  intros.
  inversion v.
*)
(*
  A : Set
  n : nat
  v : Vec A (S n)
  n0 : nat
  H0 : A
  H1 : Vec A n
  H : n0 = n
  ============================
   v = VCons A n (head A n v) (tail A n v)
*)

(* so now I tried to prove a theorem relating these functions,
 * but of course hit a brick wall, there's just not enough information
 * relating the terms to prove it
 *)

(* before (when defining head), we met trouble due to not giving a
 * total coverage of the type, (that is we ignored Vec A 0) so a
 * possible lemma to consider would be an identity on all Vectors
 * which takes VNil to VNil and VCons _ _ to VCons (head v) (tail v)
 * Actually I had some trouble even writing this, so I let Coq do it
 * for me
 *)

(*
Definition Vid (A : Set)(n : nat) :
  Vec A n -> Vec A n.
destruct n.
tauto.
intro v.
exact (VCons _ _ (head _ _ v) (tail _ _ v)).
Qed.
Print Vid.
 *
 Vid = 
 fun (A : Set) (n : nat) =>
 match n as n0 return (Vec A n0 -> Vec A n0) with
 | 0 => fun H : Vec A 0 => H
 | S n0 => fun v : Vec A (S n0) => VCons A n0 (head A n0 v) (tail A n0 v)
 end
      : forall (A : Set) (n : nat), Vec A n -> Vec A n
 * but actually I'd like to have the proof term here in a simpler
 * form if possible, so I rewrote it in the way it way synthesized:
 *)

Definition Vid (A : Set)(n : nat) :
  Vec A n -> Vec A n :=
  match n return Vec A n -> Vec A n with
    | 0 => fun v => v
    | S m => fun v => VCons _ _ (head _ _ v) (tail _ _ v)
  end.

Lemma Vid_is_id (A : Set)(n : nat) :
  forall v : Vec A n,
    v = Vid _ _ v.
Proof.
  destruct v; reflexivity.
Qed.

Theorem worm (A : Set)(n : nat) :
  forall (v : Vec A (S n)),
    v = VCons _ _ (head _ _ v) (tail _ _ v).
Proof.
  intros; apply Vid_is_id with (v := v).
Qed.

(* What next? *)

Scheme Pattern Matching with syntax-rules

(define-syntax ?member?
  (syntax-rules ()
    ((_ e () sk fk) fk)
    ((_ e (x . xs) sk fk)
     (let-syntax ((test (syntax-rules (x)
                          ((test x) sk)
                          ((test ?) (?member? e xs sk fk)))))
       (test e)))))

(define-syntax match
  (syntax-rules (quasiquote unquote make-k)
    ((match `() <exp> <env> <sk> <fk>) (if (null? <exp>) <sk> <fk>))
    ((match `,<place> <exp> <env> <sk> <fk>)
     (let-syntax ((extend-environment
                   (syntax-rules (match)
                     ((_ <ext> (match <pattern> <exp2> <env2> <sk2> <fk2>))
                      (match <pattern> <exp2> (<ext> . <env2>) <sk2> <fk2>))
                     ((_ <ext> <else>) <else>))))
       (?member? <place> <env>
                 (if (equal? <exp> <place>) <sk> <fk>)
                 (let ((<place> <exp>))
                   (extend-environment <place> <sk>)))))
    ((match `(<car> . <cdr>) <exp> <env> <sk> <fk>)
     (if (pair? <exp>)
         (let ((exp-car (car <exp>)) (exp-cdr (cdr <exp>)))
           (match `<car> exp-car <env>
                  (match `<cdr> exp-cdr <env> <sk> <fk>) <fk>))
         <fk>))
    ((match `<symbol> <exp> <env> <sk> <fk>)
     (if (equal? '<symbol> <exp>) <sk> <fk>))))

(define-syntax pattern-case*
  (syntax-rules (else)
    ((pattern-case* <exp>)
     (void))
    ((pattern-case* <exp> (else <body> ...))
     (begin <body> ...))
    ((pattern-case* <exp> (<pattern> <body> ...) <clauses> ...)
     (let ((failure (lambda ()
                      (pattern-case* <exp> <clauses> ...))))
       (match <pattern> <exp> () (begin <body> ...) (failure))))))

(define-syntax pattern-case
  (syntax-rules ()
    ((pattern-case <exp> <clauses> ...)
     (let ((exp <exp>))
       (pattern-case* exp <clauses> ...)))))

(define-syntax pattern-lambda
  (syntax-rules ()
    ((pattern-lambda (<pattern> <body> ...) ...)
     (lambda args
       (pattern-case args (<pattern> <body> ...) ...)))))


(define append
  (pattern-lambda
   (`(() ,ys) ys)
   (`((,x . ,xs) ,ys) (cons x (append xs ys)))))

(define simpl
  (pattern-lambda
   (`((+ 0 ,x)) (simpl x))
   (`((+ ,x 0)) (simpl x))
   (`((* 1 ,x)) (simpl x))
   (`((* ,x 1)) (simpl x))
   (`((- ,x 0)) (simpl x))
   (`((- ,x ,x)) 0)
   (`((/ ,x 1)) (simpl x))
   (`((/ ,x ,x)) 1)
   (`((,op ,x ,y)) `(,op ,(simpl x) ,(simpl y)))
   (`(,x) x)))

(define d
  (pattern-lambda
   (`(,x ,x)        1)
   (`(,x (+ ,u ,v)) `(+ ,(d x u) ,(d x v)))
   (`(,x (- ,u ,v)) `(- ,(d x u) ,(d x v)))
   (`(,x (* ,u ,v)) `(+ (* ,u ,(d x v)) (* ,v ,(d x u))))
   (`(,x (/ ,u ,v)) `(/ (- (* ,(d x u) ,v) (* ,(d x v) ,u)) (* ,v ,v)))))