induction missing constraint

Stream: new members

[Etienne Laurin]

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?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Etienne Laurin]

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

[Mario Carneiro]

use cases instead for that

[Mario Carneiro]

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

[Etienne Laurin]

Thanks, that seems to work

[Etienne Laurin]

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

[Mario Carneiro]

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

[Etienne Laurin]

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

[Mario Carneiro]

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

[Etienne Laurin]

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?

[Kevin Buzzard]

#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