Zulip Chat Archive

Stream: general

Topic: well_founded recursion

petercommand (Dec 16 2018 at 10:20):

Given that a relation R : a -> a -> Prop satisfies { f : stream a // forall n, R (f (n + 1)) (f n)} -> false, is it possible to get well_founded R?

petercommand (Dec 16 2018 at 10:21):

i.e. translate the traditional no infinite chain condition to well_founded in lean

Chris Hughes (Dec 16 2018 at 11:16):

example {α : Type*} (r : α  α  Prop)
  (h : Π f :   α,  n, ¬r (f (n + 1)) (f n)) :
  well_founded r :=
let f : Π a : α, ¬ acc r a  {b : α // ¬ acc r b  r b a} :=
  λ a ha, classical.indefinite_description _
      (λ hc, ha $ acc.intro _ (λ y hy,
        classical.by_contradiction (λ hy1, hc y, hy1, hy)))) in
  (λ a, classical.by_contradiction
    (λ ha, let g : Π n : , {b : α // ¬ acc r b} := λ n, nat.rec_on n a, ha
        (λ n b, f b.1 b.2, (f b.1 b.2).2.1 ) in
      have hg :  n, r (g (n + 1)) (g n),
        from λ n, nat.rec_on n (f _ _).2.2
          (λ n hn, (f _ _).2.2),
      exists.elim (h (subtype.val  g)) (λ n hn, hn (hg _))))

petercommand (Dec 16 2018 at 11:32):


Chris Hughes (Dec 16 2018 at 12:42):

PRed #519

Kenny Lau (Dec 16 2018 at 12:59):

maybe we should prove the axiom of dependent choice

Chris Hughes (Dec 16 2018 at 12:59):

What is that?

Reid Barton (Dec 16 2018 at 16:51):

There's also well_founded_iff_no_descending_seq already although the formulation is slightly different.

Kevin Buzzard (Dec 16 2018 at 16:57):

What is that?

In ZFC, countable dependent choice (DC) is the form of the axiom of choice which is used most often by mathematicians, usually without them even noticing. At the n'th step, n a natural, you have a non-empty set of things to choose from, and you choose one and call it xnx_n. Then the n+1n+1 st non-empty set appears (and this set could depend on the choice you made, hence "dependent", but it's certainly non-empty) and you can choose something from that, and so on. Mathematicians would use it to do the following sort of thing: if SS is a set of reals with the property that ϵ>0,sS\forall\epsilon>0, \exists s\in S with s<ϵ|s|<\epsilon, then to get a sequence s1,s2,s3,s_1,s_2,s_3,\ldots of elements of SS that tend to zero you apply countable choice to create a sequence with the property that sn<1/n|s_n|<1/n.

Kevin Buzzard (Dec 16 2018 at 16:59):

Aah. To get a non-increasing sequence you could use countable dependent choice.

Reid Barton (Dec 16 2018 at 17:11):

https://gist.github.com/rwbarton/7bd5b3b19d930f577355a596a5ed8b4d is basically dependent choice, without the choice part (but you could use choice in the inductive step)

Last updated: Aug 03 2023 at 10:10 UTC