PR #443 replaces the frac hierarchy with a single type Qp. Since Qp is a subtype of Rat, its automation around the arithmetic tactics is worse. An alternative is to use the type Rat, and bake positivity into the validity predicate of Frac. Doing so has the potential to clean up some annoying coercion lemmas, at the cost of potentially needing to do Iris reasoning whenever the positivity of a fraction is required.
Once we have more in-depth usages of Frac we should re-evaluate to see if this is the better solution for Lean's automation suite.
PR #443 replaces the frac hierarchy with a single type
Qp. SinceQpis a subtype ofRat, its automation around the arithmetic tactics is worse. An alternative is to use the typeRat, and bake positivity into the validity predicate ofFrac. Doing so has the potential to clean up some annoying coercion lemmas, at the cost of potentially needing to do Iris reasoning whenever the positivity of a fraction is required.Once we have more in-depth usages of
Fracwe should re-evaluate to see if this is the better solution for Lean's automation suite.