The Coq mailing list

[Chantal Keller <chantal.keller AT wanadoo.fr>]

Hi,

geng chen a écrit :
> Hi, everyone.
>   I've met a problem about pattern matching. for example there is a 
> function:
>
> Definition check_a (a : nat) : bool :=
> match  a  with
>   1 => true
>   | _ => false
> end.
>
> and result of check_a is "true". So how can I prove that a = 1 ?
> It is important for me. Could any one help me?

You should have a look at the case tactic [1]. Using it twice solves the 
problem here.


Chantal.


[1] 
http://coq.inria.fr/refman/Reference-Manual011.html#@tactic84