The Coq mailing list

[Math Prover <mathprover AT gmail.com>]

Hi,

  Here's an SAT analogy question:

    "H: _ = _ " : "rewrite H"     ::     "a := _" : ????

  fail.v contains a minimal failure case.

### Working case

H: a = 3

=========

a + 2 = 5

In this case, I know how to do "rewrite a"

### Failure case

a := 3 : nat

============

a + 2 = 5

I'm not sure how to handle this case.

Now, "crush" solves it with eq_refl. However, this isn't quite sufficient for me. In the working case, I want to be able to do things like "rewrite H in ...", and it's not clear to me if such things are possible with eq_refl.

### Concrete Question

How do I do "rewriting" with terms of the form "a := ... " instead of "H: _ = _"

Thanks!

Attachment: fail.v
Description: Binary data