The Coq mailing list

[Laurent Thery <Laurent.Thery AT inria.fr>]

Hi,

a while ago, I have been interested in having Coq tactics to perform 
"human" simplifications (the idea was to follow closely paper proofs via 
tactics : pols would simplify polr would rewrite with = and <= and polf 
would factorize)

Incredibly enough the code is still compiling in 8.6 so I put it here

https://github.com/thery/PolTac

the idea behind the code is explained in this note

https://hal.inria.fr/inria-00070394

> 1) allow rewriting with equations/inequations where the term to be
> rewritten is not immediately found, but can be isolated:
>

you get rewrting modulo AC with polr so

polr H should work

> Example e2 (a b c : R) : exists (x : R), a * b * c = b * x * a.
> (* figure out that you should instantiate x with c *)

I would have thought that

eexists; pols; apply refl_equal

would do the job

Unfortunately, the code was written before evar came into fashion, so it 
does not support it but I'll look into it

--
Laurent