Tuesday 27 May 2008

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

2 comments:

Anonymous said...

Hi, this a rather neat but, does it work when the dependent types occur in the goal as well? For example, suppose I have the type

Inductive Ucf : nat -> Set :=
| mu : forall n, Ucf (S n) -> Ucf n
| vl : forall n, Ucf (S n)
| vs : forall n, Ucf n -> Ucf (S n).

an i wish to define the view on
Ucf (S n) as

Inductive UcfSnView (n : nat)
: Ucf (S n) -> Set :=
| is_vl : UcfSnView (vl n)
| is_wk : forall i : Ucf n, UcfSnView (vs i).

Definition ucfSnView (n : nat) : forall i : Ucf (S n), UcfSnView i :=
fun v => match v in (Ucf m) return
match m with
| 0 => True
| _ => Ucf m
end
with
| vl n' => is_vl n'
| vs _ i' => is_wk i'
| _ => I
end.

The latter function does not work : coq complains about I being of type True and not (match m with
| 0 => True
| _ => Ucf m
end ). Do you have any trick that can solve this?

Muad`Dib said...

No.

UcfSnView has no case for Ucf so I don't think it's possible.