Skip to content

Fix instance directions for fractional predicates

Isaac van Bakel requested to merge ivanbakel/iris:remove-fractional-coercion into ralf/as-fractional-bwd

Removing the as_fractional_fractional coercion and its hint mode broke instance progress for some proofs (including those weird mul instances which were Local to the fractional.v file.) I drilled down into why, and it turns out a lot of instances were trying to use AsFractional backwards by using it to bound output arguments on other class instances.

Following the example of !928 (merged) , this fixes those other instances to only use AsFractional forwards, with deterministic propositions in all output positions. I believe all of these instances are now correct.

It was helpful to define fractional_as_fractional for use in these new proofs, so I've added it locally. I'll still leave the discussion over whether or not to add it globally to !926 (closed) , and I've documented the reasons from that MR for not making it global.

Merge request reports