Zulip Chat Archive

Stream: general

Topic: tactics for numbers

Johan Commelin (Aug 09 2019 at 14:21):

I'm about to leave on vacation (-; If anyone happens to get bored during the holidays, here is a little silly idea for a tactic. We discussed these kind of issues before, but maybe not exactly this.
(Ooh, and the norm_cast bundle is really fantastic, it makes life a lot easier!)
Suppose that n : int and h : n ≥ 0.
Then every mathematician (and especially if they are new to Lean) wants to say n : nat. But that is not possible.
So I wish for a tactic

lift_int_to_nat h (with name)?`

that will create a new N : nat and a proof hN : n = (N : int).

Johan Commelin (Aug 09 2019 at 14:22):

Extra goodies: figure out if n is an atom, and if so call subst n afterwards.

Johan Commelin (Aug 09 2019 at 14:22):

Also, that goodie should automatically re-use the name of the atom for the new nat (so n in this example).

Johan Commelin (Aug 09 2019 at 14:23):

The N : nat could be defined as n.nat_abs.

Johan Commelin (Aug 09 2019 at 14:23):

We could have similar tactics lift_rat_to_int and maybe lift_rat_to_nat.

Johan Commelin (Aug 09 2019 at 14:24):

Maybe they all be bundled into one super-tactic.

Johan Commelin (Aug 09 2019 at 14:24):

Also: suggestions for better names are very welcome!

Mario Carneiro (Aug 09 2019 at 18:21):

isn't this just cases on an appropriate theorem?

Mario Carneiro (Aug 09 2019 at 18:22):

and you can do the other stuff with rcases or obtain

Floris van Doorn (Aug 09 2019 at 21:35):

You mean something like this?

example (n m k : ) (h : n  0) (hk : k + n  0) : n = m :=
  lift n to  using h, -- new goal: ↑n = m
  lift m to , -- new goals: ↑n = ↑m and m ≥ 0
  lift (k + n) to  using hk with l hl, -- new assumptions: l : ℕ and hl : ↑l = k + ↑n

I'm currently cleaning up my tactic.
Mario is right that it's basically just cases on an appropriate theorem, but it's useful to have syntax that is a shortcut for that.

Floris van Doorn (Aug 09 2019 at 21:37):

In the back-end there is the following class you have to provide an instance for:

class can_lift (α : Type u) (β : Type v) : Type (max u v) :=
(coe : α → β)
(cond : β → Prop)
(prf : ∀(y : β), cond y → ∃(x : α), coe x = y)

The instance I needed to provide for my previous tactic script (to lift from to ) is:

@[can_lift_simp] instance : can_lift ℕ ℤ :=
⟨coe, λ n, n ≥ 0, λ n hn, ⟨n.nat_abs, int.nat_abs_of_nonneg hn⟩⟩

Floris van Doorn (Aug 09 2019 at 22:41):

What is the canonical way to make an expression application in tactic mode?

  • If I do
my_expr ← mk_app `can_lift.prf [new_tp, old_tp, inst, e, prf]

then I get an error, saying it cannot unify the type of prf with the expected type. It seems that mk_app is doing this unification in the "wrong order", because it doesn't seem to know the other arguments to can_lift.prf yet (which it needs to do the unification).

  • If I do
let my_expr := `(@can_lift.prf.{0 0} %%new_tp %%old_tp %%inst %%e %%prf),

I have to manually check that this type-checks (which is fine, I guess). I also need to figure out the universe levels myself (is there an easier way than doing infer_type on my types, and then match the result with expr.sort u?)

Floris van Doorn (Aug 09 2019 at 22:43):

My mostly complete tactic is here: https://github.com/leanprover-community/mathlib/blob/lift_to/src/tactic/lift.lean

Kevin Buzzard (Aug 09 2019 at 22:54):

I don't think Johan will be looking at the chat for about two weeks :-) But I'm sure he'll be very grateful! I love the way that people just do stuff for other people here.

Kevin Buzzard (Aug 09 2019 at 22:55):

I guess it's because lean is fun. The Imperial guy seemed very impressed with the community's efforts on the 1988 IMO problem, although I don't know how much he understood...

Scott Morrison (Aug 09 2019 at 23:57):

This looks really cool, and I love the user experience!

Floris van Doorn (Aug 10 2019 at 19:41):

PR'd the tactic: #1315

Floris van Doorn (Aug 11 2019 at 02:09):

@Kevin Buzzard: Yeah, I also like that about this community.

I also think that it is really valuable to have these kinds of tactics that make common patterns more convenient to do (other examples include rcases, rintro, simpa, norm_cast, norm_num, and many more).

Lastly, it is good for me to regularly work on short projects. When I only work on long-term projects, I sometimes lose track of the reasons that they are important.

Johan Commelin (Aug 24 2019 at 14:52):

@Floris van Doorn Thanks a lot for writing this!

Johan Commelin (Aug 24 2019 at 14:56):

I see that the tactic is even merged into mathlib already!!

Johan Commelin (Aug 24 2019 at 14:56):

I should probably go on holiday more often (-;

Last updated: Aug 03 2023 at 10:10 UTC