The Coq mailing list

[Lionel Elie Mamane <lionel AT mamane.lu>]

On Tue, Feb 27, 2007 at 04:03:38PM +0000, Edsko de Vries wrote:

> This is sort of a follow-up from the previous thread on safe-head.
> Suppose I want to define a function

> Definition safe_head (A:Set) (l:list A) (pf: l <> nil) : A.

> I can start with

> intro A.
> refine(fun (l:list A) (pf: l <> nil)  => match l with
>   | nil => _
>   | cons x xs => _
>   end). 

> But I can no longer see that in the first goal l = nil, and in the
> second goal l = cons x xs. What am I doing wrong?

I think you need to do the match _before_ you consume the pf
argument. But this doesn't work either:

intro A.
refine (fun (l:list A) => match l  with
| nil => _
| cons x xs => _
end
).

So, I don't know, but here is how I would do this:

Definition safe_head (A:Set) (l:list A) (pf: l <> nil) : A.
intros A [ | a tl ] uneq.
 absurd (nil = nil); solve [ assumption | reflexivity ].
 exact a.
Defined.

Having done that, I can cheat and do "Print safe_head." which permits
me to tell you that you should have written:

refine (fun (l:list A) => match l as l0 return (l0 <> nil -> A) with
| nil => _
| cons x xs => _
end
).


Frankly, I find using the "case" tactic (or destructing patterns in my
intros) easier than thinking what the right "return" clause in my
match should be.

-- 
Lionel