Simplest possible example?

Stream: Lean for teaching

[Alexander Kurz]

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]

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

[Alexander Kurz]

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]

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]

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]

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]

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

[Kevin Buzzard]

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]

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]

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

[Alexander Kurz]

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

[Kevin Buzzard]

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]

(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]

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]

Yes, that's it

[Kyle Miller]

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]

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

[Damiano Testa]

docs#False is pretty simple too.

[Alexander Kurz]

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