The Coq mailing list

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

Maybe I've missed the point here, but [simpl; rewrite T] seems to have 
the same effect as [setoid_rewrite T].  Why is [setoid_rewrite] so much 
more "useful" here?

On 12/04/2013 10:30 AM, Ilmārs Cīrulis wrote:
> Yay!
> setoid_rewrite is incredibly useful! :)
>
> Theorem T n: match n with O => O | _ => O end = O.
>  destruct n; reflexivity.
> Qed.
>
> Require Import Setoid.
> Theorem T0 n: (fix f1 n m :=
>   match n with
>   | 0 => match m with
>          | 0 => 0
>          | S _ => 0
>          end
>   | S n' => n + f1 n' m
>   end) 0 n = 0.
> Proof.
>  setoid_rewrite T.
>  reflexivity.
> Qed.