Zulip Chat Archive

Stream: new members

Topic: Induction on well founded relation


view this post on Zulip Pedro Minicz (Sep 25 2020 at 18:25):

I am suck in this seemingly innocuous proof:

lemma nat.div_two_mul_two (n : ) : (n / 2) * 2  n :=
begin
  induction n with n ih,
  { refl },
  { sorry }
end

My problem is: I don't know how to proceed. If nat.div was defined using "normal" induction," I am pretty sure I would be able to unfold n.succ / 2 into something (hopefully) more useful. How to generally work with definitions that use well_founded?

view this post on Zulip Pedro Minicz (Sep 25 2020 at 18:27):

I am not sure I understand even half of the definition of nat.div. I'd love to know where I can read more about well founded relations. I know there is something in Theorem Proving in Lean, but not much.

view this post on Zulip Yakov Pechersky (Sep 25 2020 at 19:10):

You might like to look at nat.le_div_iff_mul_le

view this post on Zulip Yakov Pechersky (Sep 25 2020 at 19:10):

Which I found via just guessing the name nat.div_mul_le_self

view this post on Zulip Pedro Minicz (Sep 26 2020 at 00:51):

I managed to do what I wanted. It was basically a less general version of nat.le_div_iff_mul_le. For future reference: nat.strong_induction_on is pretty cool. :sunglasses:


Last updated: May 12 2021 at 22:15 UTC