tactics for numbers

Stream: general

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

We could have similar tactics lift_rat_to_int and maybe lift_rat_to_nat.

[Johan Commelin]

Maybe they all be bundled into one super-tactic.

[Johan Commelin]

Also: suggestions for better names are very welcome!

[Mario Carneiro]

isn't this just cases on an appropriate theorem?

[Mario Carneiro]

and you can do the other stuff with rcases or obtain

[Floris van Doorn]

You mean something like this?

example (n m k : ℤ) (h : n ≥ 0) (hk : k + n ≥ 0) : n = m :=
begin
  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
end

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]

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]

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]

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

[Kevin Buzzard]

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]

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]

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

[Floris van Doorn]

PR'd the tactic: #1315

[Floris van Doorn]

@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]

@Floris van Doorn Thanks a lot for writing this!

[Johan Commelin]

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

[Johan Commelin]

I should probably go on holiday more often (-;