Zulip Chat Archive

Stream: new members

Topic: IFF Question


view this post on Zulip Dev-Indra (Mar 19 2020 at 16:07):

Here is the iff lemma I am trying to prove:

lemma another_helper (u v : ) : v  u  v*v  v*u :=
begin
    split,

    induction v with d hd,
    rw mul_zero,
    rw zero_mul,
    simp,

    rw succ_eq_add_one,
    rw mul_add,
    rw mul_one,
    rw mul_comm,
    rw mul_add,
    rw mul_one,
    rw add_mul,
    rw one_mul,


end

I am trying to prove the first goal with induction, but I am stuck after the last line. Can anyone help, or suggest a better way to prove this?

view this post on Zulip Kevin Buzzard (Mar 19 2020 at 16:48):

You should use {} brackets to ensure that you only have one goal at all times. Your question is hard for me to understand because your code doesn't compile and I'm not entirely sure which rewrites are supposed to apply to which goals.

view this post on Zulip Shing Tak Lam (Mar 19 2020 at 16:48):

There is a lemma in mathlib called mul_le_mul_left, which you can use by importing data.nat.basic. To solve your inductive case here, you can just use

intro h,
apply nat.mul_le_mul_left (succ d) h,

instead of the bunch of rws. Which will close the goal.

Also you don't need induction here, since you don't need the induction hypotheses.

As mul_le_mul_left is already an iff statement, you can pretty much just use it to solve your goal without needing to split it.

A complete proof just using mul_le_mul_left as an iff statement is like this:

lemma another_helper (u v : ) : v  u  v*v  v*u :=
begin
  cases v,
  { split,
    { intro h,
      simp,
    },
    intro, exact zero_le u,
  },
  {
    symmetry,
    apply mul_le_mul_left,
    simp,
  }
end

view this post on Zulip Kevin Buzzard (Mar 19 2020 at 16:49):

@Dev-Indra: note the brackets @Shing Tak Lam used!

view this post on Zulip Shing Tak Lam (Mar 19 2020 at 16:56):

I've golfed it slightly :) Apparently norm_num is a lot more powerful than I thought.

lemma another_helper (u v : ) : v  u  v*v  v*u :=
begin
  cases v,
  { norm_num },
  norm_num
end

Curiously, just norm_num by itself doesn't work, but using casesthen norm_num does.

view this post on Zulip Dev-Indra (Mar 19 2020 at 16:58):

Thanks. @Kevin Buzzard I will take note of the use of {}


Last updated: May 14 2021 at 04:22 UTC