The Coq mailing list

[Guilhem Moulin <guilhem.moulin AT ens-lyon.org>]

Hello,

On Fri, 22 Jan 2010 at 22:41:13 +0800, geng chen wrote:
>  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?

I'd try to do some case analysis on `a' :

Lemma check_a_1: forall a, check_a a = true -> a=1.
Proof.
  intros a H.
  do 2 (destruct a; try discriminate).
  trivial.
Qed.

Hope this helps,
Guilhem.

Attachment: signature.asc
Description: Digital signature