Gaëtan Gilbert (May 20 2022 at 20:35): 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.?
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.
Karl Palmskog (May 20 2022 at 20:43):hmm, that kind of preprocessing sounds like what Trakt is aiming for...
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: Oct 03 2023 at 02:34 UTC