fix(tactic/ring): more precise pattern match for div #1557
Conversation
|
Could you please add a test showing the improvement? |
src/tactic/ring.lean
Outdated
| @@ -386,7 +386,7 @@ meta def eval : expr → ring_m (horner_expr × expr) | |||
| (e', p) ← lift $ norm_num.derive e, | |||
| lift $ e'.to_rat, | |||
| return (const e', p)) <|> eval_atom e | |||
| | `(%%e₁ / %%e₂) := do | |||
| | `(@has_div.div _ division_ring_has_div %%e₁ %%e₂) := do | |||
There was a problem hiding this comment.
Do you think the syntactic check here is too strong? What about matching the instance as %%inst and checking that it unifies with an application of division_ring_has_div?
There was a problem hiding this comment.
@robertylewis I suppose that's a possibility, but I don't actually think it comes up; there aren't any other competing instances for has_div that I'm aware of, everything filters through this instance. (There are many ways to prove the resulting division_ring goal, but AFAIK the only has_div instances are the ones for nat/int and the division ring div.)
There was a problem hiding this comment.
I dunno, that doesn't sound very robust. Is the current Travis failure related? (I'm not gonna compile it on my laptop right now.)
There was a problem hiding this comment.
There's another instance called division_ring_has_div'. This is causing the current travis failure.
robertylewis
added
the
awaiting-author
|
@digama0 Are you planning to come back to this? |
digama0
removed
the
awaiting-author
|
It looks like the breakage is |
|
@digama0 ping again? |
|
@digama0 ping again. |
|
@digama0 IIRC you were having trouble replicating this build failure locally. Is that still the case? I can locally reproduce the CI failure. |
robertylewis
added
ready-to-merge
…unity#1557) * fix(tactic/ring): more precise pattern match for div * add test * fix instance check for div * chore(algebra/quadratic_discriminant): add braces in have steps * use norm_num instead of ring to evaluate exponents * fix norm_num uses * fix norm_num pow bug * bugfix * fix proof Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
…unity#1557) * fix(tactic/ring): more precise pattern match for div * add test * fix instance check for div * chore(algebra/quadratic_discriminant): add braces in have steps * use norm_num instead of ring to evaluate exponents * fix norm_num uses * fix norm_num pow bug * bugfix * fix proof Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
No description provided.