Arithmetic sequence

Stream: lean4

[Scott N. Walck]

Hi Folks,

I'm trying to write a function in Lean that produces an
arithmetic sequence, much like [a, a+dx .. b] in Haskell. Here a
is the initial element, dx is the step, and b is the maximum
element, or something close to it.

As the code below shows, I can do this with rational numbers and
with Floats. The code is essentially identical. I use a gas
tank to satisfy the termination checker. I believe I should be
able to do this with any number system that admits decidable
ordering.

But, as the final code segment shows, I do not know how to tell
Lean that "greater than" is decidable.

I'd appreciate any help.

Thanks,
Scott

import Lean.Data.Rat
open Lean

def arithSeqRatHelper (gastank : Nat) (dx : Rat) (b : Rat) (xs : List Rat) : List Rat :=
  match gastank with
  | 0          => xs
  | Nat.succ l => match xs with
                  | []        => arithSeqRatHelper l dx b [dx]
                  | (y :: ys) => if y + dx > b
                                 then xs
                                 else arithSeqRatHelper l dx b ((y+dx)::y::ys)

def arithSeqRat (gastank : Nat) (a : Rat) (dx : Rat) (b : Rat) : List Rat :=
  (arithSeqRatHelper gastank dx b [a]).reverse

def arithSeqFloatHelper (gastank : Nat) (dx : Float) (b : Float) (xs : List Float) : List Float :=
  match gastank with
  | 0          => xs
  | Nat.succ l => match xs with
                  | []        => arithSeqFloatHelper l dx b [dx]
                  | (y :: ys) => if y + dx > b
                                 then xs
                                 else arithSeqFloatHelper l dx b ((y+dx)::y::ys)

def arithSeqFloat (gastank : Nat) (a : Float) (dx : Float) (b : Float) : List Float :=
  (arithSeqFloatHelper gastank dx b [a]).reverse

#eval arithSeqRat 10 (mkRat 3 1) (mkRat 1 10) (mkRat 32 10)

#eval arithSeqFloat 10 3 0.1 3.2



def arithSeqHelper {w1 w2 : n} [Add n] [OfNat n 0] [LT n] [Decidable (w1 > w2)] (gastank : Nat) (dx : n) (b : n) (xs : List n) : List n :=
  match gastank with
  | 0          => xs
  | Nat.succ l => match xs with
                  | []        => arithSeqHelper l dx b [dx]
                  | (y :: ys) => if y + dx > b
                                 then xs
                                 else arithSeqHelper l dx b ((y+dx)::y::ys)

[Kim Morrison]

Hi @Scott N. Walck, please use #backticks when posting code examples; much easier to read!

[Alex J. Best]

Do you really want to use the Lean.Rat rationals? https://leanprover-community.github.io/mathlib4_docs/Lean/Data/Rat.html they don't have many instances on them.
[DecidableRel ((· > ·) : n → n → Prop)] is the standard way to assume > is decidable