Transfinite Induction (But actually just code review)

Stream: new members

[Robert Maxton]

So, having read a neat blog post on precisely when induction is valid, the proofs looked both simple enough and also interesting enough that I had the impulse to try translating it into Lean, just for fun

[Robert Maxton]

and, this time, that actually worked! lol. I'm a little proud of that since it's the first time I've managed to write up something nontrivial and not all that artificial (not a Lean specific homework problem) in Lean

[Robert Maxton]

That said, I rather feel my code, ah, could use a bit of work; I don't necessarily require them to be like mathlib's (in fact to some extent I'd rather them not, mathlib is almost unreadably dense to me), but they're still less than elegant

[Robert Maxton]

anyone willing to take a look at it, teach me good practice and help me clean it up?

[Arthur Paulino]

Show us :D
I'm not a mathematician but I'd like to see it regardless

[Robert Maxton]

the blog post in question is at https://math.blogoverflow.com/2015/03/10/when-can-we-do-induction/
and I've put my implementation at https://gist.github.com/robertmaxton42/e3afda89616126e13ae05326d4b85b75

[Arthur Paulino]

I see Mario in the comments section! :smiley:

[Robert Maxton]

I've only implemented the first two proofs from that blog so far
I'm going to go on to do partial orders in a bit

[Robert Maxton]

Arthur Paulino said:

I see Mario in the comments section! :smiley:

heh, small world :p

[Robert Maxton]

actually I may not bother, looks like the reasoning is all identical for posets

[Arthur Paulino]

Someone else might be able to help you better with this, but there aren't relevant occurrences of noncomputable theorem or noncomputable lemma in mathlib. I suspect you had to do this because you defined wellorder as a class

[Robert Maxton]

I mean, I know for a fact that well-ordering the reals requires the axiom of choice, so like, I wasn't exactly surprised when it showed up

[Robert Maxton]

it's possible I missed a trick, but

[Arthur Paulino]

Your class doesn't need noncomputable:

class wellorder (α: Type u) extends linear_order α :=
(well_all_sub_have_min: ∀ (β : set α), set.nonempty β → has_min β)

And stating ind_imp_well with def didn't require noncomputable either:

def ind_imp_well [linear_order α] --[nonempty α]
  (ind: ∀ A : set α, (∀ x, (∀ y, y < x → y ∈ A) → x ∈ A) → A = set.univ):
  (wellorder α)

[Arthur Paulino]

I'm not sure what's happening, but again, someone else might be able to help you better with this. My guess is that, by requiring a term of type wellorder α, you force yourself to compute data

[Jireh Loreaux]

See docs#well_founded.recursion and its sibling docs#well_founded.induction in case you weren't aware of them. They're related, albeit not exactly what you are doing.

[Robert Maxton]

well, the definition may or may not require noncomputable but any proof that would let me demonstrate the reals are well-ordered should require it
and I think this counts, since you can accept induction as an axiom without implying the axiom of choice right away?

[Robert Maxton]

The real reason I need noncomputable is that I need a way to get arbitrary values out of my nonempty sets, it gets introduced by set.nonempty.some

[Robert Maxton]

If it's possible to remove noncomputable it'll be by avoiding that constraint, but I'm not terrifically hopeful lol

[Arthur Paulino]

Do notice that I also removed [nonempty α]. This code typechecks:

def ind_imp_well [linear_order α] --[nonempty α]
  (ind: ∀ A : set α, (∀ x, (∀ y, y < x → y ∈ A) → x ∈ A) → A = set.univ):
  (wellorder α) :=
  begin
    fconstructor, intro B,
    contrapose, intro no_min,
    rw set.not_nonempty_iff_eq_empty,
    let A := Bᶜ, suffices : A = set.univ, by {simp at *, tauto},
    apply_assumption,
    have no_min2 : ¬ has_min B, by assumption,
    rw has_min at no_min, push_neg at no_min,
    intros x indh,
    by_contra,
    change A with Bᶜ at h, rw set.not_mem_compl_iff at h,
    have : has_min B,
    {
      use x, split, exact h,
      assume z, contrapose!,
        rw ← set.not_mem_compl_iff, change Bᶜ with A, rw set.not_not_mem,
      revert z, exact indh,
    }, contradiction
  end

[Robert Maxton]

I mean, I'm not entirely clear on the distinction/requirement myself

[Robert Maxton]

but I think it boils down to the use of \forall? The elimination rule for forall lets you introduce its arbitrary variable without invoking choice

[Robert Maxton]

for, uh, reasons lol

[Robert Maxton]

but well-ordered-ness says "forall subsets there exists a minimum element", and while you can use it to pull an arbitrary subset you can't use it to pull the arbitrary elements you need to finish the proof going the other way

[Robert Maxton]

I think is the logic?

[Robert Maxton]

but again, I'm not entirely clear

[Robert Maxton]

though that said, I am surprised that it seems to show up when using well-ordered-ness, but not when proving it

[Robert Maxton]

that does in fact confuse me lol

[Arthur Paulino]

There are several occurrences of docs#classical.arbitrary in proofs of theorems that don't require noncomputable. It does require nonempty ⋯ though

[Robert Maxton]

.... that's weird. I would've thought classical.arbitrary was like, the standard Thing That Is Noncomputable

[Arthur Paulino]

The definition of classical.arbitrary is indeed marked with noncomputable

[Arthur Paulino]

But if you're not asking me for an element of an empty set, but, instead, ask me to prove something about it, then I'm fine

[Kyle Miller]

A way to think about how the noncomputability checker works is that it recursively deletes everything that's a Prop or a Sort* then sees if there's anything still hanging around that's marked noncomputable. It's also able to delete certain arguments to certain functions/constructors that it knows aren't computationally relevant. (This isn't actually what it does, but I believe it's mostly equivalent.)

The well_all_sub_have_min axiom is a Prop, so it gets deleted.

By the way, I don't think noncomputable class does anything, only private and meta seem to be modifiers with any effect, and it's arguably a Lean bug that it doesn't throw an error if you try to do noncomputable class.