Stream: Coq users

Topic: tactic for dealing with INR


view this post on Zulip Gaƫtan Gilbert (May 20 2022 at 20:35):

Is there a nice tactic for dealing with goals involving INR? for instance what the nicest way to solve forall a b, 0 <= INR a * INR b? Do I have to use the lemmase manually ie apply Rmult_le_pos;apply pos_INR.?

view this post on Zulip Guillaume Melquiond (May 20 2022 at 20:38):

Manual proof is what I would do. But theoretically, this falls in the fragment handled by psatz R. I have no idea, however, if the tactic already knows about INR or if you have to massage the goal beforehand using some other tactic.

view this post on Zulip Karl Palmskog (May 20 2022 at 20:43):

hmm, that kind of preprocessing sounds like what Trakt is aiming for...

view this post on Zulip Guillaume Melquiond (May 20 2022 at 20:52):

So, psatz R does not seem to know about INR. But doing generalize (pos_INR a) (pos_INR b) beforehand suffices.


Last updated: Jan 27 2023 at 00:03 UTC