Into: Jake

Stream: new members

[Jake S]

Hi all, my name is Jake. I'm a developer looking and venturing into dependently typed languages using lean 4! I will be using lean to do the advent of code this year: https://adventofcode.com

I've been reading through the functional programming in lean and trying to get through "the Bible" (theorem proving in lean 4) but I definitely have lots of questions that I'm hoping you all can help me with or at least give me some pointers on where to learn more!

One thing that I'm running in to: I want to define a new number type to represent a AOC problem number (day 1 through 25) and I'm wondering what the best way to do that is? So far I have this:

structure ProblemNumber : Type where
  of ::
  day: Nat
  dayMin: day > 0
  dayMax: day ≤ 25

But I don't know how to create an instance of this type (I don't know how to supply a proposition of type 1 > 0 : Prop.)

instance : OfNat ProblemNumber 1 where
  ofNat := ProblemNumber.of 1 ___ ___

Any pointers or thoughts on better ways of modeling this?

[Anne Baanen]

One proof would be Nat.lt_succ_self 0 (docs4#Nat.lt_succ_self). However, a much nicer way exists! Lean can just compute 1 > 0 as a boolean, so you can write (by decide) to solve goals that can be checked by direct computation (of course, Lean will check that the result of 1 > 0 is indeed true).

[Yakov Pechersky]

Why supply the proof when you can get the computer to do it for you?

structure ProblemNumber : Type where
  of ::
  day: Nat
  dayMin: day > 0 := by decide
  dayMax: day ≤ 25 := by decide

example : ProblemNumber := .of 1

[Yakov Pechersky]

Here, I am using "default fields" for a structure, where the default value (RHS of walrus) is a tactic, which describes _how_ to create a default value

[Anne Baanen]

(Is "walrus" an official name for :=?)

[Yakov Pechersky]

It is in python :snake:

[Yakov Pechersky]

https://docs.python.org/3/whatsnew/3.8.html#assignment-expressions

[Jake S]

This is amazing! Thank you both for the help here. Thank you @Anne Baanen - I would like to look into supplying this proof my self. I think I may need to spend more time reading up on theorem proving in lean :)

I found similar code from timelib here: https://github.com/ammkrn/timelib/blob/main/Timelib/Date/Ymd.lean#L19-L20
But I didn't realize that they must have been proving these explicitly

Follow up question: Is defining each instance of OfNat (1-25) the best way... or is it possible to model this in some more succinct way like for Positive numbers from the book:

instance : OfNat Pos (n + 1) where
  ofNat := ...

(edit: except with bounds in my case)

or is that what you're saying @Yakov Pechersky — will example : ProblemNumber := .of 1 also elaborate to 1-25?

[Yakov Pechersky]

OfNat ProblemNumber YOURNUMBERHERE will only work if you explicitly construct (either through copy-paste, or some Lean meta code) the 25 instances. Typeclass search does not execute tactics, so unfortunately you can't say something like:

structure ProblemNumber : Type where
  of ::
  day: Nat
  dayMin: day > 0 := by decide
  dayMax: day ≤ 25 := by decide

example : ProblemNumber := .of 1

instance {n : Nat} {h0 : n > 0} {h25 : n ≤ 25}: OfNat ProblemNumber n := ⟨.of n h0 h25⟩

#check (1 : ProblemNumber) -- doesn't work, TC search can't populate h0 and h25

[Yakov Pechersky]

So either I suggest you stay with .of 1, .of 2, or you just remove the dayMin and dayMax from your structure. In mathlib, we often make structures/definitions that have no proof obligations on their own. It is only in the _theorems_ about those structures/definitions that some assumption about the structure is necessary

[Jake S]

Awesome, thank yoU! something to think about. Appreciate the help from everyone!!

[Jake S]

Typeclass search does not execute tactics, so unfortunately you can't say something like:

This is a bummer though... maybe someday :)

[Alex J. Best]

You could also decide that (28 : ProblemNumber) should mean 25 (or 3), and either use min (or mod) to define the instance for any n.

[Jake S]

interesting thought! thanks. I was more looking for the compiler to error if I tried to write a problem number that doesn't exist (or is out of bounds)

[Yakov Pechersky]

structure ProblemNumber : Type where
  of ::
  day: Nat
deriving BEq, DecidableEq, Ord, Inhabited

example : ProblemNumber := .of 1

instance {n : Nat} : OfNat ProblemNumber n := ⟨.of n⟩

#check (1 : ProblemNumber)
#eval (1 : ProblemNumber) = .of 1
#eval (1 : ProblemNumber) == .of 1
#reduce (1 : ProblemNumber) = .of 1
#reduce (1 : ProblemNumber) == .of 1

instance : LE ProblemNumber := leOfOrd
instance : LT ProblemNumber := ltOfOrd

#eval (1 : ProblemNumber) < (.of 7)

[Yakov Pechersky]

If you want that "compile-time" check, then stick with your "proofs as part of the structure" and use .of 24

[Jake S]

Yeah I think for me for now the exercise I was trying to achieve was a bounded Nat type, to understand how to enforce bounds.

What @Yakov Pechersky described was something like what I was looking for

instance {n : Nat} {h0 : n > 0} {h25 : n ≤ 25}: OfNat ProblemNumber n := ⟨.of n h0 h25⟩

But I hear you all on alternative ways to model this, and I appreciate the discussion! Thanks for the help!