Zulip Chat Archive

Stream: new members

Topic: induction missing constraint


view this post on Zulip Etienne Laurin (Sep 01 2018 at 15:05):

Given (a b : ℕ) (h : a ≤ b), after doing induction h, the case less_than_or_equal.refl doesn't have any hypothesis allowing to conclude a = b. Why not? Is there another way to perform induction that does introduce a = b in that case?

view this post on Zulip Mario Carneiro (Sep 01 2018 at 15:07):

in the refl case, you should already have b replaced by a in the goal

view this post on Zulip Mario Carneiro (Sep 01 2018 at 15:09):

By the way, I don't recommend doing induction on an le hypothesis. Instead, do induction on a and/or b and use lemmas on le to satisfy the induction hypothesis

view this post on Zulip Etienne Laurin (Sep 01 2018 at 15:14):

What if a and b are expressions? In this example, the goal is still a ≤ b

example (a b : ℕ) (h : nat.succ a ≤ nat.succ b) : a ≤ b := begin
  induction h,
  case nat.less_than_or_equal.refl { sorry }
end

view this post on Zulip Mario Carneiro (Sep 01 2018 at 15:15):

use cases instead for that

view this post on Zulip Mario Carneiro (Sep 01 2018 at 15:16):

If you need to combine induction with the parameter equalities, you should first use generalize h : nat.succ a with all the variables you are holding fixed in the induction, then use induction

view this post on Zulip Etienne Laurin (Sep 01 2018 at 15:24):

Thanks, that seems to work

view this post on Zulip Etienne Laurin (Sep 01 2018 at 15:24):

I haven't used a lot of explicit lemmas so far, I often have trouble finding the right one. I usually get by with a lot of unfold/delta/induction/cases followed by simp

view this post on Zulip Mario Carneiro (Sep 01 2018 at 15:25):

That's not very sustainable. I suggest learning to browse the source files of core lib and/or mathlib

view this post on Zulip Etienne Laurin (Sep 01 2018 at 15:27):

I recently discovered M-. will jump to lean and mathlib sources, I'll start using it more

view this post on Zulip Mario Carneiro (Sep 01 2018 at 15:27):

autocompletion also helps for discoverability, once you learn the naming convention

view this post on Zulip Etienne Laurin (Sep 01 2018 at 15:32):

Oh nice. But I notice that doesn't work too well if I haven't imported the right theory. Is there a better way to find lemmas than grep?

view this post on Zulip Kevin Buzzard (Sep 01 2018 at 15:34):

#find might be helpful for you. But I would definitely recommend (a) learning the rules of thumb for lemma names and (b) the ctrl-space dance for auto-completion. If you're trying to prove something about int then just import data.int.basic


Last updated: May 12 2021 at 23:13 UTC