CODEWITHSUNDEEP
coqisabelle
Ashley Yakeley
Ashley Yakeley

Reputation: 691

Coq auto-simplification similar to Isabelle?

In Isabelle, it's possible to mark facts (such as theorems) of the form P=Q with the "simp" attribute. Then when proving things, the "simp" and "auto" tactics will use such facts to convert occurrences of P to Q.

Does Coq have a similar mechanism?

Upvotes: 2

Views: 164

Answers (1)

Vinz
Vinz

Reputation: 6047

You should have a look at the documentation about auto and autorewrite, I think it is what you are looking for.

I know you can feed some hint database to auto (with Hint Resolve iirc) but I'm not sure you can do the same with autorewrite.

Upvotes: 2

Related Questions