The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Thu, 04 Oct 2012 00:16:37 +0200,
Jonas Oberhauser 
<s9joober AT gmail.com>
 a écrit :

> Hi all,
> 
> This example describes a "problem" I have encountered recently:
> 
> Goal True.
> pose (x := 3+2).
> assert (3+2 = 5) by auto.
> rewrite H in x.
> (* Error: Found no subterm matching "3 + 2" in x. *)
> 
> Is this a bug?
> 
> Kind regards, Jonas

I do not think so.

'rewrite' rewrites inside the type of a value, not the value itself.

You define 'x' as '3+2', you cannot change your mind and give it
another value.

Goal False.
  set (x := refl_equal (3+2)).
  assert (3+2 = 5) by auto.
  rewrite H in x.

Works since there is an occurence of "3 + 2" in the type of "x", but
then "x" is not defined by "refl_equal (3+2)" anymore.