Axiom of dependent choice

Stream: Is there code for X?

[SnO2WMaN]

Is there already "Axiom of Dependent Choice"?
It would be good for me if there were proposition such as below code.

example
  (R : α → α → Prop)
  (h : ∃ s : Set α, s.Nonempty ∧ ∀ a ∈ s, ∃ b ∈ s, R a b)
  : ∃ f : ℕ → α, ∀ x, R (f x) (f (x + 1))
  := by sorry

This is pseudo example, h can be obtained from WellFounded. f might be more constraints.

[Yury G. Kudryashov]

Use tactic choose

[Yury G. Kudryashov]

Something like (not tested)

  obtain ⟨s, ⟨x, hx⟩, h'⟩ := h
  inhabit α
  choose! f hfs hR using h'
  use fun n ↦ f^[n] x
  intro n
  -- prove `R (f n) (f (n + 1))

[SnO2WMaN]

Oh Thanks. It might be good.

[SnO2WMaN]

FYI, simply this code passed.

example
  (R : α → α → Prop)
  (h : ∃ s : Set α, s.Nonempty ∧ ∀ a ∈ s, ∃ b ∈ s, R a b)
  : ∃ f : ℕ → α, ∀ x, R (f x) (f (x + 1))
  := by chooce

[Kevin Buzzard]

You're sure there are no errors in that file anywhere at all?

[SnO2WMaN]

Sorry above code is not worked. I missunderstood the error message was not appeared in this code but at the bottom.

[SnO2WMaN]

complete @Yury G. Kudryashov 's proof. (might be more simple)

example
  {R : α → α → Prop} (h : ∃ s : Set α, s.Nonempty ∧ ∀ a ∈ s, ∃ b ∈ s, R a b)
  : ∃ f : ℕ → α, ∀ x, R (f x) (f (x + 1))
  := by
  obtain ⟨s, ⟨x, hx⟩, h'⟩ := h;
  choose! f hfs hR using h';
  use fun n ↦ f^[n] x;
  intro n;
  simp only [Function.iterate_succ'];
  refine hR (f^[n] x) ?a;
  induction n with
  | zero => simpa;
  | succ n ih => simp only [Function.iterate_succ']; apply hfs _ ih;

[SnO2WMaN]

Because I think this lemma might be useful (since it is probably faithful representation of the dependent choice axiom), I would like to place this in Mathlib after some refactoring, how about?

[Kim Morrison]

I suspect this might be an answer in search of a question. What do you want to use it for?

I'm skeptical that this is a natural statement of the underlying fact: in particular, the Set plays no role here, and the statement would probably just as useful stated on the whole type (and allow the coerce from Set to Type to handle the special case of sets).

[SnO2WMaN]

I have used this lemma in several times in my formalizing modal logic (I cant give some example of other math propositions that using DC).
Your point about the absense of role for Set is right, because I simply show example code for questioning, and in using, the hypothesis h is actually obtained from negation of WellFounded.wellFounded_iff_has_min