Zulip Chat Archive

Stream: general

Topic: extension to `lift` tactic


view this post on Zulip 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

view this post on Zulip Scott Morrison (May 24 2020 at 09:41):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 24 2020 at 09:42):

In this specific case the norm_cast tactics do it right?

view this post on Zulip Scott Morrison (May 24 2020 at 09:42):

How do I do it with norm_cast?

view this post on Zulip Scott Morrison (May 24 2020 at 09:42):

oh...

view this post on Zulip Scott Morrison (May 24 2020 at 09:42):

you mean jsut write norm_cast?

view this post on Zulip Kenny Lau (May 24 2020 at 09:42):

does exact_mod_cast h work?

view this post on Zulip Scott Morrison (May 24 2020 at 09:43):

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

view this post on Zulip Johan Commelin (May 24 2020 at 09:43):

assumption_mod_cast

view this post on Zulip Johan Commelin (May 24 2020 at 09:43):

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

view this post on Zulip Kenny Lau (May 24 2020 at 09:44):

but norm_cast changes the goal

view this post on Zulip Kenny Lau (May 24 2020 at 09:44):

I suppose Scott wants a tactic that changes h

view this post on Zulip Scott Morrison (May 24 2020 at 09:44):

In my actual use case exact_mod_cast is perfect.

view this post on Zulip Kenny Lau (May 24 2020 at 09:44):

oh great

view this post on Zulip Kenny Lau (May 24 2020 at 09:45):

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

view this post on Zulip Patrick Massot (May 24 2020 at 10:18):

Can't you do norm_cast at h?

view this post on Zulip 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.)

view this post on Zulip Johan Commelin (May 29 2020 at 08:08):

How about this example:

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

view this post on Zulip Johan Commelin (May 29 2020 at 08:08):

This came up in practice.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (May 29 2020 at 08:31):

@Rob Lewis norm_cast goes the wrong way, right?

view this post on Zulip Johan Commelin (May 29 2020 at 08:32):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 29 2020 at 08:33):

How?

view this post on Zulip Rob Lewis (May 29 2020 at 08:33):

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

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 29 2020 at 08:34):

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

view this post on Zulip 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],

view this post on Zulip 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."

view this post on Zulip Johan Commelin (May 29 2020 at 08:37):

Thanks!

view this post on Zulip 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