Dependently typed bounded range in Lean

Question

Suppose I would like to create a bounded integer Z with bounds a b.

def zbound (x₁ x₂ : ℤ) :=
  { n : ℤ // x₁ ≤ n ∧ n ≤ x₂ }

Is this a reasonable representation of a bounded integer?

Now I would like to create a range of numbers from a to b.

def range : ∀(a b : ℤ), list (zbound a b) 
  | fro to := if h : fro < to
              then ⟨fro, and.intro (le_refl _) (int.le_of_lt h)⟩
                   :: range (fro + 1) to
              else []

I can get this to work with range : ℤ → ℤ → list ℤ, including the proof of termination using using_well_founded. However, I find it impractical in this form, because it doesn't carry a proof that every number within the range is zbound a b.

As such, I would like to get my dependent version. However, I run into the isue that range (fro + 1) to is, naturally, of type list (zbound (fro + 1) to). What I need is list (zbound fro to). How does one get around this issue? I tried approaching the problem by showing that if x is lower bounded by a, then it is also bounded by every number less than a, therefore keeping the bound of form zbound fro to (os this obviously bounds zbound (fro + 1) to). I have however no idea how to use this idea, or even if it makes sense to use it.

Answer 1

I am not sure this is an ideal solution, but it does work for me. First we need a lemma to weaken the bounded range:

def range_weaken {a b : ℤ} : zbound (a + 1) b → zbound a b
  | ⟨i, ⟨lbound, rbound⟩⟩ :=
    ⟨i, and.intro
          (le_of_add_le_left _ 1 _ dec_trivial lbound)
          rbound⟩

Then we can redefine range in terms of weakened ranges:

def range : ∀(a b : ℤ), list (zbound a b) 
  | fro to := if h : fro < to
              then ⟨fro, and.intro (le_refl _) h⟩
                   :: list.map range_weaken (range (fro + 1) to)
              else []
  using_well_founded { ... }

Note: I couldn't find a lemma I was looking for, so I hand-proved the following:

def le_of_add_le_left (a b c : ℤ) : 0 ≤ b → a + b ≤ c → a ≤ c