-
Notifications
You must be signed in to change notification settings - Fork 298
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat(data/rat/floor): add norm_num support for int.{floor,ceil,fract}
#16502
Conversation
Does |
Edited :) |
🤣 I actually meant that the floor of |
I am not sure if this is better code, but it avoids some duplication: /-- A norm_num extension for `int.floor`, `int.ceil`, and `int.fract`. -/
@[norm_num] meta def eval_floor_ceil (e : expr) : tactic (expr × expr) := do
let (f, args) := e.get_app_fn_args,
let val := [`int.floor, `int.ceil, `int.fract].index_of f.const_name,
guard $ val ≠ 3,
some x ← pure args.last',
q ← x.to_rat,
let z := if val ≠ 1 then int.floor q else int.ceil q,
let ze := `(z),
if val ≠ 2 then do
t ← to_expr ``(%%e = %%ze),
((), p) ← solve_aux t (do
mk_mapp (ite (val = 0) `int.floor_eq_iff `int.ceil_eq_iff) ((args.take 3).map some) >>=
rewrite_target,
tactic.interactive.norm_num [] (interactive.loc.ns [none])),
p ← instantiate_mvars p,
pure (ze, p)
else do
let q' := int.fract q,
some R ← pure args.head',
ic ← mk_instance_cache R,
(ic, q'e) ← ic.of_rat q',
t ← to_expr ``(%%e = %%q'e),
((), p) ← tactic.solve_aux t (do
`[rw int.fract_eq_iff; norm_num],
refine ``(⟨%%ze, _⟩),
tactic.interactive.norm_num [] (interactive.loc.ns [none])),
p ← instantiate_mvars p,
pure (q'e, p) [I edited the code above]. |
open tactic | ||
|
||
/-- A norm_num extension for `int.floor`, `int.ceil`, and `int.fract`. -/ | ||
@[norm_num] meta def eval_floor_ceil : expr → tactic (expr × expr) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@[norm_num] meta def eval_floor_ceil : expr → tactic (expr × expr) | |
@[norm_num] meta def eval_floor_ceil_fract : expr → tactic (expr × expr) |
maybe, since it deals with int.fract
as well.
example : int.ceil (-15 / 16 : R) + 1 = 1 := by norm_num | ||
example : int.fract (-17 / 16 : R) - 1 = -1 / 16 := by norm_num | ||
|
||
end |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
end | |
end floor |
to please the linter
((), p) ← tactic.solve_aux t (do | ||
tactic.mk_mapp `int.ceil_eq_iff [some R, some inst_1, some inst_2] >>= tactic.rewrite_target, | ||
`[norm_num]), |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Should the tactic input to solve_aux
end with a done
, to make sure that it proves t
, or is it unnecessary in this case, since this is an extension anyway?
(Most of my comments are also for my own understanding!)
Ported to leanprover-community/mathlib4#13647 |
This is super sloppy code, but is a working version to improve upon.
It's unfortunate that where in a proof it's often sufficient to do:
the idiomatic norm_num handler is much more painful to write.
Closes #15992.