make fractional_split truly forwards lemmas
As Upamanyu pointed out, these lemmas do seem to be using AsFractional backwards still.
But this opens some further questions:
- should we have a variant of fractional_merge that looks like
Φ (q1 + q2) -∗ P1 ∗ P2
? -
fractional_half
still looks suspicious
These lemmas are barely used in our CId projects: a grep for fractional_(merge|split|half)
has only 4 hits
coq-users/reloc/theories/logic/spec_ra.v
208: iApply (fractional_half_2 with "Hl1 Hl2").
coq-users/examples/theories/hocap/concurrent_runners.v
265: { iApply (fractional_split_2 with "Htoken Htoken2").
308: { iApply (fractional_split_2 with "HINIT HINIT'").
320: { iApply (fractional_split_2 with "HSETRES HSETRES'").
Edited by Ralf Jung