The Coq mailing list

[Saulo Araujo <saulo2 AT gmail.com>]

Hi,

I am trying to prove the following theorem:

Definition strEq x y := if string_dec x y then true else false.

Theorem strEq_t1 :

  forall s s',

    strEq s s' = true -> strEq s' s = true.

My best attempt at prooving it is below:

Proof.

  unfold strEq.

  intros.

  destruct (string_dec s s').

  assert (s' = s).

  symmetry.

  trivial.

  rewrite H0.

But now I need to prove that string_dec is reflexive.

Could someone help me proving it?

Thanks in advance,

Saulo