Induction on minimum "length"

Stream: new members

[Robert Spencer]

Suppose I have the setup below

variables {α β : Type}
def foo : α → set β := sorry
lemma foo_not_empty (a : α) : ∃ b : β, foo a b := sorry
def length : β → ℕ := sorry

and I wish to prove something about α, where I will induct on the minimum length of an element of foo a.

In maths parlance, I would say "Suppose b is an element of foo a of minimal length. We will induct on this minimal length..." and then I can induct. How do I set this up in lean. Are there any docs that I can read about this that aren't just uncommented code?

As an aside rant, am I doing something wrong in that I'm finding lean a really difficult language/framework to pick up? Simply finding the lemmas I need (or working out that they don't exist) is a huge pain, and #find in the mathlib doesn't seem to ever work for me. I feel as if I need to memorize what is where in the mathlib, and it is becoming quite a chore. I also find myself wishing for much more "the beginner's guide to proving stuff in mathlib about {lattices | rings | finite things | lists }"-like documentation. Ok. </rant> Any advice would be useful.

[Kevin Kappelmann]

I am pretty much a noob myself, but here is my almost surely way too complicated first attempt:

example {β : Type} : ∀ (a : α), P a :=
begin
  have s : α → set ℕ := λ a, { n | ∃ (b : β), foo a b ∧ length b = n },
  have is_min : α → ℕ → Prop := λ a m, ∀ (n ∈ s a), m ≤ n,
  have has_min : ∀ a, ∃ (m : ℕ), is_min a m, by sorry, -- show that there is a minimum
  -- you might use prop_deciable to remove the next sorry
  have min_of : α → ℕ := λ a, @nat.find (is_min a) sorry (has_min a),
  have r := λ a a', min_of a < min_of a',
  have : well_founded r, by sorry, -- show that r is well_founded
  assume a,
  exact well_founded.induction this a
  ( λ (x : α) (hyp : ∀ (y : α), r y x → P y),
    begin
      show P x, sorry
    end)
end

edit: fix le to lt

[Chris Hughes]

These docs might help with the induction. https://github.com/leanprover-community/mathlib/blob/master/docs/extras/well_founded_recursion.md

[Chris Hughes]

I think most people found Lean a very difficult language to pick up. Finding lemmas becomes easier once you learn the naming conventions, and eventually you end up just knowing the most used lemmas. Beginner's guides to proving stuff about rings etc is also definitely needed. I'm never quite sure what should go into these things, there is a file called theories in the docs folder right now, but I don't think it's that helpful at the moment.

[Chris Hughes]

Most people learn by asking questions here.

[Robert Spencer]

@Kevin Kappelmann: cheers for that. I'll take a look. I think well_founded.induction is what I was really looking for (which isn't mentioned in the mathlib docs as far as I can see?)

[Robert Spencer]

@Chris Hughes Yes, but I worry I am asking too many silly questions!

[Floris van Doorn]

You can use this lemma, which should be added to mathlib:

import data.set.basic tactic.localized

open set
open_locale classical
lemma find_min {α} (f : α → ℕ) (s : set α) (h : ∃ x, x ∈ s) :
  ∃(x ∈ s), ∀(y ∈ s), f x ≤ f y :=
begin
  cases h with x hx,
  have hn : ∃ n, n ∈ f '' s := ⟨f x, set.mem_image_of_mem f hx⟩,
  have := nat.find_spec hn, rw [mem_image] at this, rcases this with ⟨x', h1x', h2x'⟩,
  refine ⟨x', h1x', _⟩, intros y hy, rw [h2x'], exact nat.find_min' hn (mem_image_of_mem f hy)
end

[Kevin Buzzard]

@Robert Spencer it's not at all uncommon to find Lean hard to learn. We desperately need more docs, especially docs for mathematicians. I have repeatedly said I'll write some but there's always something more urgent to do. I have tried to teach many undergraduates Lean and it's very hard work

[Robert Spencer]

Yes, lean is currently almost hostile to mathematicians, I'm finding. I got into it "as a mathematician" after your talk about why mathematicians should care about these things at the CMS, but find myself doing far more "as a programmer": it just doesn't seem ready for mathematicians yet :oh_no:

[Robert Spencer]

Gah. Ok, for those who come after me and want to know what to do, here it is. The key is the function measure_wf which takes a measure and makes a well founded statement out of it.

A measure is the inverse image of < under some f : a -> nat. In my case, f is my "minimum length" function. Constructing that minimum length function used @Floris van Doorn's proof that minimum elements exist.

[Robert Spencer]

Don't let it be said I am a DenverCoder9
(https://xkcd.com/979/)

[Floris van Doorn]

Oh, after I started writing some Lean code, I forgot what you asked for, and solved a different problem. I'm glad that my lemma was still useful.

[Floris van Doorn]

Is this the induction principle you are looking for? I'm mostly posting this to show that you don't have to get into the gritty details with measure_wf or anything: (it uses the previous find_min lemma)

lemma length_strong_induction {α β} (P :α → Prop) (f : α → set β) (hf : ∀ x, ∃ y, y ∈ f x)
  (l : β → ℕ) : let Q := λ n, ∀ x, (∃ y ∈ f x, l y = n ∧ ∀ y' ∈ f x, l y ≤ l y') → P x in
    ∀(h_ind : ∀ n, (∀ m < n, Q m) → Q n) (x : α), P x :=
begin
  intros, have : ∀ n, Q n := λ n, nat.strong_induction_on n h_ind,
  rcases find_min l (f x) (hf x) with ⟨y, h1y, h2y⟩, exact this (l y) x ⟨y, h1y, rfl, h2y⟩
end

(edit: simplified code)

[Floris van Doorn]

This is the "strong induction" version, of course you can also prove a "simple induction" version.

[Kevin Buzzard]

Oh! You were at my CMS talk? That's great to hear! Do you know Ed Ayers?

[Kevin Buzzard]

I disagree that it's not ready for mathematians. I have supervised many Lean projects done by undergraduate mathematicians. You just have to teach them how to use Lean.

[Kevin Buzzard]

It's as simple as that

[Kevin Buzzard]

Once they can start formalising the problems they have, the computer scientists start fixing them

[Kevin Buzzard]

Just work on a project. Try to define a random hard thing and when you get stuck just ask loads of questions here

[Robert Spencer]

@Floris van Doorn Uhhh, possibly? That looks useful. Thanks. The gritty thing in my particular problem (which I watered down a bunch here) is that beta is actually dependent on alpha, so I can't copy paste your code, and don't feel like rewriting it to work in my case: sorry. Now I know though.

@Kevin Buzzard I don't think I know Ed Ayers... sorry. I understand your sentiment, and all opinions I make at the moment should be tempered by the understanding that I am currently quite frustrated, and so being a bit biased. I understand that it is a matter of learning the language, and perhaps my issue is with the amount of boilerplate I find myself writing. The disconnect is between me thinking "pick an X of minimum Y", which is "easy to conceptualize" and coding it. Granted, there is a lot in that statement (existence of an order on Y, realizable infema of sets of Y etc etc), but the lack of examples I can find (let alone commented code) means I can't even work out what I need to prove and what has been done for me in the allpowerful mathlib.

And as for your last advice, that is what I am doing (Jordan Holder for modules is my goal atm). Perhaps I should be more liberal in my admitting defeat and asking for help.

[Floris van Doorn]

Do you mean that β is defined in terms of α, or that you actually have β : α → Type? In the first case, you can still apply my induction principle (but if you have working code, I understand that you don't want to change it).

[Robert Spencer]

β : α → Type

Its still good to see this code. Thanks. May I ask where it comes from?

[Floris van Doorn]

I just wrote it ;)

[Kevin Buzzard]

Robert -- a major breakthrough I had with communicating with computer scientists is the importance of the MWE. Say you're stuck on a proof. Then sorry the bit you're stuck on, make the code compile modulo that one sorry and then just post the fully working Lean code into #new members and people will be more than ready to help. If you ask vague questions you can sometimes be met by incomprehensible answers because people just don't know your level. Posting working code is a much better way of communicating with them

[Kevin Buzzard]

Are you currently based in Cambridge @Robert Spencer ?

[Robert Spencer]

That's fair, and good coding practice in general. I've seen enough stackoverflow to appreciate a good MWE. My problem I suppose is I don't know how much I can strip out and still get enough info. I think I hit lucky in this thread, leaving out that beta was a dependent type of alpha and still getting enough to fudge myself a solution.

[Robert Spencer]

Yep, I'm doing a PhD at DPMMS