finding an x s.t. trans_gen R x x

Stream: new members

[Andrew Souther]

Here is a puzzle I'm working on, and I feel stumped.

import logic.relation
import data.finset.basic
open relation
variables {σ : Type}

example (R : σ → σ → Prop) (S : finset σ) (hS: S.nonempty) (hR : ∀a ∈ S, ∃b ∈ S, R b a) :
    ∃ c ∈ S, trans_gen R c c := sorry

I'm pretty sure this is true, but I am not 100% sure. Here's a very rough way I think about the problem:

Let's say there are n elements in S. Since S is nonempty, let's find an element called x₁.
Either R x₁ x₁ (and the proof is pretty much done), or there exists another x₂ s.t. R x₂ x₁.
Now, either there exists k ≤ 2, s.t. R xₖ x₂ (and trans_gen R x₂ x₂), or there exists another x₃ s.t. Rx₃ x₂.
Repeat this process until we've found an element that "loops in on itself" or until we reach xₙ.
If we reach xₙ, there is no other element left in the set, so there must be k ≤ n, s.t. R xₖ xₙ. Then, trans_gen R xₖ xₙ.

However, I have no clue how to express this intuition in Lean! And maybe this idea is too imprecise to be formalized at all. Any quick suggestions appreciated.

[Kevin Buzzard]

I would be tempted to define a map F from the naturals into S by recursion. I'd use hS to define F 0 and I'd use hR to define F (n+1) given F n. I'd use hR and an induction argument on m>0 to prove trans_gen R (F (i+m)) (F i). Finally I'd use a result in the library saying that this map F can't be injective, to isolate i<j with F i = F j, and then set m=j-i. I'm the sort of person who sometimes stops what they're doing and just knocks this sort of puzzle off, but unfortunately I'm giving a talk tomorrow which I need to focus on writing!

[Andrew Souther]

That makes sense to me, thanks. I think I'd prefer to hear a quick roadmap and not a full proof :) Good luck with the talk!

[Kevin Buzzard]

The hardest part from a technical Lean perspective will be defining F, which you can either do outside the proof using classical.some and classical.some_spec, or inside the proof, in which case you might want to it like this:

import logic.relation
import data.finset.basic
open relation
variables {σ : Type}

example (R : σ → σ → Prop) (S : finset σ) (hS: S.nonempty) (hR : ∀a ∈ S, ∃b ∈ S, R b a) :
    ∃ c ∈ S, trans_gen R c c :=
begin
  cases hS with s0 hs0,
  choose next hnext1 hnext2 using hR,
  let F : ℕ → {s : σ | s ∈ S} := λ n, nat.rec_on n ⟨s0, hs0⟩
    (λ d a, ⟨next a.1 a.2, hnext1 a.1 a.2⟩),
  sorry
end

[Kevin Buzzard]

It's slightly more of a kerfuffle than it could be because sigma is really in some sense irrelevant; one could imagine instead proving the result for a fintype S with no sigma at all. The key thing which enables you to avoid classical.some is the choose tactic. I find it a lot cleaner to use choose.

[Mario Carneiro]

I think you can most easily prove this by finset induction

[Kevin Buzzard]

I thought about that, but the sequence F(0), F(1), F(2), ... is just some random ultimately periodic thing. I can believe that you can see a trick for doing it but I couldn't.

[Mario Carneiro]

example (R : σ → σ → Prop) (S : finset σ) (hS : S.nonempty) (hR : ∀a ∈ S, ∃b ∈ S, R b a) :
  ∃ c ∈ S, trans_gen R c c :=
begin
  replace hR : ∀a ∈ S, ∃b ∈ S, trans_gen R b a :=
    λ a ha, let ⟨b, hb, h⟩ := hR a ha in ⟨b, hb, trans_gen.single h⟩,
  classical, refine finset.induction_on S (by rintro ⟨_, ⟨⟩⟩) _ hS hR,
  rintro a s hs IH - hR,
  obtain ⟨b, hb', ba⟩ := hR a (by simp),
  obtain rfl | hb := finset.mem_insert.1 hb', {exact ⟨_, by simp, ba⟩},
  obtain ⟨c, hc, h⟩ := IH ⟨_, hb⟩ (λ d hd, _), {exact ⟨c, by simp [hc], h⟩},
  obtain ⟨e, he, ed⟩ := hR d (by simp [hd]),
  obtain rfl | he := finset.mem_insert.1 he,
  {exact ⟨_, hb, ba.trans ed⟩}, {exact ⟨_, he, ed⟩}
end

[Kevin Buzzard]

replace hR : ∀a ∈ S, ∃b ∈ S, trans_gen R b a -- very nice!

[Andrew Souther]

Thank you for this! I'll be honest, this proof just feels above my pay-grade, especially the induction.
But I'm positive I'll run into more puzzles like this. If I've finished the tutorial project and I've just started Mathematics in Lean, any suggestions for what I should start reading to get a better grasp on induction...? Should I try jumping to the chapters on Induction in TPIL? Do I just need to open p. 1 of TPIL and start making my way through?

[Kevin Buzzard]

I learnt a lot about induction by trying to prove basic facts about lists, for example that the reverae of the reverse of a list is itself. I spent some time translating parts of Coq's "software foundations" book into Lean.

[Kevin Buzzard]

However, are you sure that this proof is above your pay grade? It is a relatively straightforward translation of a slightly sneaky maths proof into lean. It's been well-compactified but that's just Mario's style. Can you prove it by indication on the size of S on paper? If you can't then the problem is not the Lean. The proof is quite different from the one I was suggesting.

[Andrew Souther]

The replace line and all the concise obtain statements scared me at first, but I've played around trying to copy that style in other proofs, and you're right that it's not so bad. I see it's really just a proof by cases, and I think I do understand the pen-and-paper version of what Mario has done here.

I have a few more concrete questions about the proof though, if anyone has the chance:
--What exactly is the classical line doing here?
--Can someone help unpack what's going on here in the induction line: (by rintro ⟨_, ⟨⟩⟩)

I understand that you need to feed finset.induction_on three things: a finset, a proof that a proposition is true for the empty finset, and a proof that if it's true for some given finset, it's also true for the union of that finset and one more element. Mario has supplied S for the first term and left the third term blank to prove it later. But how does that second proof work?

[Kevin Buzzard]

classical -- remove it and see what happens! finset is quite constructive, the induction function needs an algorithm to figure out whether two terms of type sigma are equal. classical says "sure there exists an algorithm, I'm not going to tell it you, but you're not going to actually ask what it is".

[Kevin Buzzard]

The rintro line -- here it is, expanded out.

  refine finset.induction_on S _ _ hS hR,
  -- { rintro ⟨_, ⟨⟩⟩ },
  { intro h,
    cases h with s h2,
    -- h2: s ∈ ∅
    cases h2, -- no cases!
  },

[Andrew Souther]

About the rintro line -- I guess it's just false that s ∈ ∅, so it's sort of an ex falso quodlibet situation?
About classical-- If I remove it, I see Lean isn't convinced that this is true: [decidable_eq σ]. I also see on mathlib that finset.induction_on implicitly needs a term like this. I guess this term tells us "there exists an algorithm to determine whether two terms of type σ are equal."

I still don't really understand the mechanics of why finset.induction_on needs this though, but again maybe I would benefit from a bit more reading on induction.

[Mario Carneiro]

finset.induction_on needs decidable_eq because insert appears in the theorem statement

[Mario Carneiro]

and insert uses the decidable_eq proof in its definition

[Mario Carneiro]

It might be nice to make a variation on finset.induction_on using finset.cons instead to avoid the assumption

[Kevin Buzzard]

finsets are implemented constructively in Lean, meaning that lean carries around a list which contains every element of the finset exactly once. So you can't really do anything useful with a finset like adding an element to it without an algorithm for knowing whether the element is in the set already. Because I'm only interested in proving theorems about finsets rather than actually using them to compute stuff, I just switch on classical and this makes the problem go away. Then finsets become nonconstructive in the sense that if I'm trying to compute an explicit finset I might be in trouble, but if I just want to prove theorems about them I'm still fine. To give an example of what the problem is, lean has a computable function finset.card which is supposed to return the size of a finset, but if you ran it on the finset $\{\sum_{n\geq1}n^{-2},\pi^2/6\}$ you'd be asking lean to figure out whether the sum is $\pi^2/6$ or not, and this is a tricky little theorem rather than something a computer can do automatically.

[Andrew Souther]

It's subtle, but it makes sense -- thank you both. Interesting that insert is the culprit.