Skip to content

use Qp inequality instead of frac validity for lemma statements

Ralf Jung requested to merge ralf/frac-valid into master

Many lemma statements use ✓ q instead of (q ≤ 1)%Qp to express validity of a fraction. There was no on Qp before Robbert's recent changes, so this makes sense historically. It is also true that ✓ q is shorter, but it is rather cryptic, and usually the user will think in terms of inequalities and not validity of fractions.

So with this MR I propose we change all these lemma statements to use inequality instead. I used rg '✓[^↔→⊢]*%Qp|✓[ {}n]*[qp]' to find the lemmas that would need changing from this; I hope I did not miss any. The one thing I did not change is the definition of validity of view, but I am happy to also change that if people prefer.

We should also avoid using for Qp addition and for , but I could not find any instances of that.

Edited by Ralf Jung

Merge request reports