Dedekind cuts and Well Founded Recursion

Stream: maths

[RustyYato]

I'm trying to define Dedekind cuts as a way of formalizing the Reals, and it would be helpful for my proofs of addition if I could prove that starting from a value above the cut and going down towards the cut in equal-sized increments was well-founded. However, I'm not sure where to even start with this.

-- I've defined Dedekind Cuts like so...
structure DedekindCut (α: Type _) [LT α] where
  --- is a given rational below the cut
  cut: α -> Prop
  -- every Dedekind Cut partitions the rationals, so the proposition must be decidable, otherwise we may find
  -- rationals which aren't cut q or ¬cut q
  decide: ∀q, Decidable (cut q)
  -- each partition must be inhabited
  has_lt_partition: ∃q, cut q
  has_ge_partition: ∃q, ¬cut q
  -- cut must respect the < operator on rationals
  lower_cover: ∀{q r: α}, r < q -> cut q -> cut r
  -- cut must not have a maximum element (though it will have an upper bound)
  no_max: ∀q, cut q -> ∃r, q < r ∧ cut r

Now I want to prove something like

structure CutInd (α: Type _) [LT α] [Sub α] (dedekind: DedekindCut α) where
  value: α
  value_not_cut: ¬dedekind.cut value

instance CutInd.instLt [LT α] [Sub α] (dedekind: DedekindCut α) : LT (CutInd α dedekind) where
  lt a b := a.value < b.value

def DedekindCut.step_down_with_accessible
  [Sub α] [LinearOrder α] [cut_wf: DedekindCutWf α]
  (dedekind: DedekindCut α)
  (step_size: α) (step_size_positive: cut_wf.is_positive step_size):
  ∀(x: CutInd α dedekind), Acc LT.lt x := by -- not sure how to start filling this in somehow

where DedekindCutWf is any lemmas I need to make this work. I think I only need

class DedekindCutWf (α: Type _) [LT α] [Sub α] where
  is_positive: α -> Prop -- there might be something in mathlib for this, but not a big deal for now
  sub_decreasing: ∀(a b: α), is_positive b -> a - b < a

Intuitively this should work, since if you step down n times (for some n), you will end up below the cut.
And all values below the cut are < all values above the cut. Since the region below the cut is non-empty (by has_lt_partition), it shouldn't be possible to recurse infintely.
And it's not possible to construct CutInd for values below the cut.

This is all I've got so far, but not sure where to go forward from here or if this is even the right approach. Do you guys have some hints on how to go about this or if my approach isn't workable in some way?

def DedekindCut.step_down_with_accessible
  [Sub α] [LinearOrder α] [cut_wf: DedekindCutWf α]
  (dedekind: DedekindCut α)
  (step_size: α) (step_size_positive: cut_wf.is_positive step_size):
  ∀(x: CutInd α dedekind), Acc LT.lt x := by
  intro x
  have ⟨ q, q_is_below_cut ⟩  := dedekind.has_lt_partition
  cases @lt_or_ge α _ x.value q with
  | inl h =>
    have := x.value_not_cut <| dedekind.lower_cover h q_is_below_cut
    contradiction
  | inr h =>
      apply Acc.intro
      intro y y_lt_x
      sorry

[RustyYato]

I'm aware that mathlib4 uses Cauchy sequences to define the reals, but I'm doing this as a way to learn lean4 and how to write proofs. :smile:, and I don't think I found anything on Dedekind cuts, so I thought I would try my hand at it.

[Edward van de Meent]

i think first off you will want to be able to talk about the natural notion of integer multiplication given by repeated addition... secondly, you will want something saying that ∀ x y, ∃ z : y - z < y or in words "any distance can be bridged by some number". thirdly, the archimedian property will help. i think these three assumptions should be sufficient to prove this?

[Edward van de Meent]

for a bit more guidance on how to get the first, you may want to look into making your arbitrary α a(n additive) Group, to give it an appropriate instance of Module ℕ α

[RustyYato]

I see, that makes sense, I'll try that out. Thanks!

For ∀ x y, ∃ z : y - z < y did you mean to use x in there somewhere?

[Edward van de Meent]

ah yes. i meant ∀ x y, ∃ z : y - z < x (or ∀ x y, ∃ z : x - z < y, dealers choice)

[RustyYato]

hmm, so I tried this out and wasn't able to make it work. But I also found out that it likely wouldn't have helped anyways :(

The XY problem here is that I'm trying to define addition in terms on the cuts, but I am unable to prove the decidability of addition with the given proposition add.cut := ∃q_a q_b, q_a + q_b = q ∧ a.cut q_a ∧ b.cut q_b. NOTE: for this part I'm just working with the Rationals, not some generalized field.

Of course I could use Classical.decideProp, but then the addition is non-computable. Which is super unfortunate.
I think there should be a constructive proof of this, but it eludes me.

Maybe I can define a non-standard order for the rationals and just use induction to get a super slow implementation? (like inducting over the numerator and denominator, and checking all of them).

Does it being non-computable matter if I only intend to use this type for proofs?

[Alex J. Best]

While its true that we don't have a lot of material on dedekind cuts, a lot of the things in this file in mathlib https://github.com/leanprover-community/mathlib4/blob/18a35ebb796ef104676edcf9d6f02880f4e6af6a/Mathlib/Algebra/Order/CompleteField.lean make use of dedekind cuts implicitly to define maps between conditionally complete ordered fields (like the reals). Maybe you'll find some useful material there