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? *)