(*

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

## Tuesday, 27 May 2008

### Easy Examples of Pattern Matching in Coq

Subscribe to:
Post Comments (Atom)

## 2 comments:

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?

No.

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

Post a Comment