extension to `lift` tactic

Stream: general

[Scott Morrison]

I'd love to see extensions to the lift tactic (possibly under a separate name) that allow me to write:

lemma foo (a b : ℕ) (h : a < b) : (a : ℤ) < (b : ℤ) :=
begin
  lift h to ℤ,
  exact h,
end

instead of having to know the name of the lemma:

lemma foo' (a b : ℕ) (h : a < b) : (a : ℤ) < (b : ℤ) :=
begin
  exact int.lt_to_nat.mp h,
end

[Scott Morrison]

I'm guessing we don't have any automation that does this at the moment.

[Scott Morrison]

I'm not really certain of the scope of this, but even something that moves inequalities from nat to int would be very useful.

[Johan Commelin]

In this specific case the norm_cast tactics do it right?

[Scott Morrison]

How do I do it with norm_cast?

[Scott Morrison]

oh...

[Scott Morrison]

you mean jsut write norm_cast?

[Kenny Lau]

does exact_mod_cast h work?

[Scott Morrison]

Awesome, I didn't realise how much work *_cast tactics could already do!

[Johan Commelin]

assumption_mod_cast

[Johan Commelin]

You don't even need to know the names of your hypotheses (-;

[Kenny Lau]

but norm_cast changes the goal

[Kenny Lau]

I suppose Scott wants a tactic that changes h

[Scott Morrison]

In my actual use case exact_mod_cast is perfect.

[Kenny Lau]

oh great

[Kenny Lau]

but nevertheless it would be beneficial to have a tactic that changes h

[Patrick Massot]

Can't you do norm_cast at h?

[Scott Morrison]

That goes the wrong way. h : a < b, doesn't have any coercions in it. The idea is to add the coercions to the hypothesis. (And of course everyone pointed out it was easier in this minimal example to remove the coercions from the goal.)

[Johan Commelin]

How about this example:

example (m n k : ℤ) (hn : n ≠ 0) (hk : ↑k = ↑m / ↑n) : m = n * k :=
begin
  admit
end

[Johan Commelin]

This came up in practice.

[Johan Commelin]

I don't want to remember how the fact "coercion from int to rat is injective" is called.

[Johan Commelin]

So I want to hit this with move_goal_to rat, which figures out what to do.

[Rob Lewis]

Johan Commelin said:

I don't want to remember how the fact "coercion from int to rat is injective" is called.

norm_cast knows about this so you shouldn't have to mention it. Do you have data.rat.cast imported?

[Johan Commelin]

@Rob Lewis norm_cast goes the wrong way, right?

[Johan Commelin]

I can't rw_mod_cast hk and end up with a goal in the rationals.

[Rob Lewis]

I mean, I think you can rephrase the proof to use norm_cast without making it longer.

[Johan Commelin]

How?

[Rob Lewis]

You can rewrite hk to make it multiplicative and norm_cast it, right?

[Johan Commelin]

    apply @int.cast_injective ℚ,
    have : (n : ℚ) ≠ 0, by exact_mod_cast hn,
    rw [int.cast_mul, hk, mul_div_assoc', mul_comm, mul_div_cancel _ this]

is what I have now

[Johan Commelin]

Rob Lewis said:

You can rewrite hk to make it multiplicative and norm_cast it, right?

Aha, but then I have to remember how to do that...

[Johan Commelin]

And those are still manipulations that don't come intuitively to me... they seem to work in the wrong direction, for me.

[Johan Commelin]

The proof I posted above seems to be the natural "flow" of the proof, for me.

[Johan Commelin]

    apply @int.cast_injective ℚ,
    have : (n : ℚ) ≠ 0, by exact_mod_cast hn,
    field_simp [hk, hn, mul_comm],

[Rob Lewis]

import data.rat.cast

example (m n k : ℤ) (hn : n ≠ 0) (hk : ( k : ℚ) = ↑m / ↑n) : m = n * k :=
begin
  rw eq_div_iff_mul_eq at hk, norm_cast at hk,
  cc, assumption_mod_cast
end

Not that I care how you do the arithmetic, but this seems the core of the proof. "change division to multiplication, do some cast and equality reasoning."

[Johan Commelin]

Thanks!

[Johan Commelin]

Total proof:

lemma rat.denom_div_cast_eq_one_iff (m n : ℤ) (hn : n ≠ 0) :
  ((m : ℚ) / n).denom = 1 ↔ n ∣ m :=
begin
  split,
  { intro h,
    lift ((m : ℚ) / n) to ℤ using h with k hk,
    use k,
    rw eq_div_iff_mul_eq _ _ (show (n:ℚ) ≠ 0, by exact_mod_cast hn) at hk,
    norm_cast at hk,
    rw [← hk, mul_comm], },
  { rintros ⟨d, rfl⟩,
    rw [int.cast_mul, mul_comm, mul_div_cancel, rat.coe_int_denom],
    exact_mod_cast hn }
end