Zulip Chat Archive

Stream: Lean for teaching

Topic: Simplest possible example?

Alexander Kurz (Sep 30 2023 at 17:07):

Hi, I am new to Lean and want to explore whether I can use Lean for teaching logic. I am trying to find the simplest possible example. So I started to define my own natural numbers.

inductive N : Type
  | o : N
  | s : N  N

def zero : N := N.o
def one : N := N.s N.o
def two : N := N.s one

def add (m : N) (n : N) : N :=
  match m with
  | N.o => n
  | N.s m' => N.s (add m' n)

#eval add one two

But now, when I hover over eval, I get an error message and not the expected result (N.s(N.s(N.s N.o))). I dont understand why that happens as add is just a functional program that should run.

Kevin Buzzard (Sep 30 2023 at 17:09):

Did you read the error message which carefully tells you the problem and exactly what you need to do to fix it?

Alexander Kurz (Sep 30 2023 at 17:11):

yes, but I dont understand why eval "failed to be synthesized" ... in fact, I dont understand why we need to synthesize eval in the first place ... if Lean is a functional programming language (as I read somewhere) it should already have an interpreter than can evaluate functional programs like 'add'

Kevin Buzzard (Sep 30 2023 at 17:12):

It is Repr, not #eval, which failed to be synthesized. #eval outputs a string. You have not told Lean how to turn the term of type N into a string.

Kevin Buzzard (Sep 30 2023 at 17:13):

def N.eval : N  String
| o => "o"
| s n => "s(" ++ N.eval n ++ ")"

instance : Repr N where
  reprPrec := fun n _ => N.eval n

#eval add one two -- s(s(s(o)))

Kyle Miller (Sep 30 2023 at 17:15):

You just need a Repr instance, and you just need to tell Lean to derive one:

inductive N : Type
  | o : N
  | s : N  N
  deriving Repr

Kyle Miller (Sep 30 2023 at 17:15):

Not every inductive type can have a faithful Repr instance, so it's up to you to tell it to generate one.

Kevin Buzzard (Sep 30 2023 at 17:18):

Off-topic (1): it might be best to do namespace N before defining things like zero, giving it the better name of N.zero. Off-topic (2) Addition on Lean's naturals is defined by induction on the 2nd variable not the first, so if at some point you want to compare your N with Lean's Nat then this might be something to bear in mind.

Alexander Kurz (Sep 30 2023 at 17:18):

I am not sure I understand correctly, but I take what you say to mean that Lean, as opposed to functional programming languages like Idris, does not have an interpreter. Rather, I need to implement my own interpreter ... Edit: I understand this now ... thanks for your help @Kevin Buzzard @Patrick Massot

Alexander Kurz (Sep 30 2023 at 17:24):

Thanks @Kyle Miller that works for me. Now I can continue :-)

Alexander Kurz (Sep 30 2023 at 17:34):

@Kevin Buzzard the namespace N trick is really useful ... thanks

Kevin Buzzard (Sep 30 2023 at 17:41):

Yeah, then you can just talk about s and o rather than N.s etc; it makes exposition in the classroom much less cluttered.

Kevin Buzzard (Sep 30 2023 at 17:42):

(I also teach natural numbers to undergraduates using Lean and indeed I even have a school talk where I do what you are doing above)

Alexander Kurz (Sep 30 2023 at 18:39):

It took me some time to find where the official Nat is defined ... it is here, right? https://github.com/leanprover/lean4/blob/master/src/Init/Prelude.lean#L1038

Kyle Miller (Sep 30 2023 at 18:49):

Yes, that's it

Kyle Miller (Sep 30 2023 at 18:50):

You can use the mathlib documentation to locate things. docs#Nat is a link to the documentation and click "source". You can also do things like type #check Nat in VS Code and then right click on Nat and click "Go to definition"

Martin Dvořák (Sep 30 2023 at 18:52):

The simplest possible example is probably the type Bool; prove basic stuff like DeMorgan.

Damiano Testa (Sep 30 2023 at 19:10):

docs#False is pretty simple too.

Alexander Kurz (Sep 30 2023 at 19:15):

Thanks to all of you ... I am blown away by how helpful this community is ... looking forward to spending more time on Lean.

Last updated: Dec 20 2023 at 11:08 UTC