Zulip Chat Archive

Stream: new members

Topic: Transfinite Induction (But actually just code review)


Robert Maxton (Apr 01 2022 at 23:26):

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 (Apr 01 2022 at 23:27):

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 (Apr 01 2022 at 23:27):

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 (Apr 01 2022 at 23:28):

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

Arthur Paulino (Apr 01 2022 at 23:34):

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

Robert Maxton (Apr 01 2022 at 23:38):

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 (Apr 01 2022 at 23:42):

I see Mario in the comments section! :smiley:

Robert Maxton (Apr 01 2022 at 23:45):

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 (Apr 01 2022 at 23:46):

Arthur Paulino said:

I see Mario in the comments section! :smiley:

heh, small world :p

Robert Maxton (Apr 01 2022 at 23:55):

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

Arthur Paulino (Apr 02 2022 at 00:03):

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 (Apr 02 2022 at 00:06):

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 (Apr 02 2022 at 00:06):

it's possible I missed a trick, but

Arthur Paulino (Apr 02 2022 at 00:30):

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 (Apr 02 2022 at 00:31):

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 (Apr 02 2022 at 00:45):

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 (Apr 02 2022 at 00:49):

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 (Apr 02 2022 at 00:50):

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 (Apr 02 2022 at 00:51):

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

Arthur Paulino (Apr 02 2022 at 01:01):

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 (Apr 02 2022 at 01:06):

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

Robert Maxton (Apr 02 2022 at 01:06):

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 (Apr 02 2022 at 01:07):

for, uh, reasons lol

Robert Maxton (Apr 02 2022 at 01:08):

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 (Apr 02 2022 at 01:08):

I think is the logic?

Robert Maxton (Apr 02 2022 at 01:08):

but again, I'm not entirely clear

Robert Maxton (Apr 02 2022 at 01:10):

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

Robert Maxton (Apr 02 2022 at 01:10):

that does in fact confuse me lol

Arthur Paulino (Apr 02 2022 at 01:13):

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

Robert Maxton (Apr 02 2022 at 01:14):

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

Arthur Paulino (Apr 02 2022 at 01:14):

The definition of classical.arbitrary is indeed marked with noncomputable

Arthur Paulino (Apr 02 2022 at 01:16):

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 (Apr 02 2022 at 01:29):

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.


Last updated: Dec 20 2023 at 11:08 UTC