CODEWITHSUNDEEP
coqcoq-tactic
thbl2012
thbl2012

Reputation: 37

Using "omega" for type "N"

For my research, I wrote a bunch of functions in Coq for the type nat and proved they are correct. Now I need to write the same functions for the type N but proving their correctness seems like a pain since the omega tactic does not work for this type. Is there an alternative for omega on N?

So far I have looked at the library Nnat and found several useful translation from N to nat and vice versa. If no omega alternative exists, is there a tactic to quickly transform a goal in N to nat and use omega on it?

Upvotes: 0

Views: 39

Answers (1)

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23592

The lia tactic, available in the Lia module, seems to work with N.

Upvotes: 1

Related Questions