The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 01/25/2015 11:03 AM, Saulo Araujo wrote:
> 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.

With richly typed functions like [string_dec], it often works to 
case-analyze everything and let basic automation pick up the pieces.

Proof.
  unfold strEq; intros; destruct (string_dec s s'), (string_dec s' s); 
congruence.
Qed.