## Stream: general

### Topic: extension to lift tactic

#### Scott Morrison (May 24 2020 at 09:40):

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 (May 24 2020 at 09:41):

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

#### Scott Morrison (May 24 2020 at 09:42):

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 (May 24 2020 at 09:42):

In this specific case the norm_cast tactics do it right?

#### Scott Morrison (May 24 2020 at 09:42):

How do I do it with norm_cast?

oh...

#### Scott Morrison (May 24 2020 at 09:42):

you mean jsut write norm_cast?

#### Kenny Lau (May 24 2020 at 09:42):

does exact_mod_cast h work?

#### Scott Morrison (May 24 2020 at 09:43):

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

#### Johan Commelin (May 24 2020 at 09:43):

assumption_mod_cast

#### Johan Commelin (May 24 2020 at 09:43):

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

#### Kenny Lau (May 24 2020 at 09:44):

but norm_cast changes the goal

#### Kenny Lau (May 24 2020 at 09:44):

I suppose Scott wants a tactic that changes h

#### Scott Morrison (May 24 2020 at 09:44):

In my actual use case exact_mod_cast is perfect.

oh great

#### Kenny Lau (May 24 2020 at 09:45):

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

#### Patrick Massot (May 24 2020 at 10:18):

Can't you do norm_cast at h?

#### Scott Morrison (May 24 2020 at 10:24):

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 (May 29 2020 at 08:08):

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


#### Johan Commelin (May 29 2020 at 08:08):

This came up in practice.

#### Johan Commelin (May 29 2020 at 08:08):

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

#### Johan Commelin (May 29 2020 at 08:09):

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

#### Rob Lewis (May 29 2020 at 08:31):

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 (May 29 2020 at 08:31):

@Rob Lewis norm_cast goes the wrong way, right?

#### Johan Commelin (May 29 2020 at 08:32):

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

#### Rob Lewis (May 29 2020 at 08:32):

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

How?

#### Rob Lewis (May 29 2020 at 08:33):

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

#### Johan Commelin (May 29 2020 at 08:33):

    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 (May 29 2020 at 08:33):

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 (May 29 2020 at 08:34):

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

#### Johan Commelin (May 29 2020 at 08:34):

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

#### Johan Commelin (May 29 2020 at 08:36):

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


#### Rob Lewis (May 29 2020 at 08:36):

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."

Thanks!

#### Johan Commelin (May 29 2020 at 08:40):

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


Last updated: May 14 2021 at 04:22 UTC