Help with Lean

Stream: new members

[Ken Roe]

I just started using Lean. Can someone help me by telling me what I need to replace "sorry" with to prove this theorem:

def beq_nat : ℕ → ℕ → bool
| beq_nat 0 0 := tt
| beq_nat (x+1) (y+1) := (beq_nat x y)
| beq_nat a b := ff

example : beq_nat 3 3=tt := by sorry.

[Kenny Lau]

your definition does not compile

[Patrick Massot]

def beq_nat : ℕ → ℕ → bool
| 0 0 := tt
| (x+1) (y+1) := (beq_nat x y)
| a b := ff

example : beq_nat 3 3=tt := rfl

[Patrick Massot]

strange definition

[Kenny Lau]

I don't think it's strange

[Kenny Lau]

it's a viable way to prove that equality is decidable

[Patrick Massot]

it's less efficient than using the maths preamble

[Ken Roe]

I get the following using "rfl":

impHeap.lean:35:28: error
type mismatch, term
rfl
has type
?m_2 = ?m_2
but is expected to have type
beq_nat 3 3 = tt

[Kenny Lau]

we changed the definition

[Kenny Lau]

your original definition does not compile

[Ken Roe]

How do I fix the definition?

[Patrick Massot]

see my message

[Kenny Lau]

we already gave you the new definition

[Kenny Lau]

def beq_nat : ℕ → ℕ → bool
| 0 0 := tt
| (x+1) (y+1) := (beq_nat x y)
| a b := ff

example : beq_nat 3 3=tt := rfl

:point_up: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/subject/Help.20with.20Lean/near/129411605

[Ken Roe]

Thanks--didn't notice they were different. It appears the syntax for recursive definitions changed from Lean 2.0. This definition (copied from the Lean 2.0 tutorial) also fails:

definition fib : nat → nat
| fib 0 := 1
| fib 1 := 1
| fib (a+2) := fib (a+1) + fib a

[Kenny Lau]

how old is Lean 2.0 lol

[Kenny Lau]

I don't think I ever used Lean 2.0

[Kenny Lau]

definition fib : nat → nat
| 0 := 1
| 1 := 1
| (a+2) := fib (a+1) + fib a

[Patrick Massot]

You shouldn't be reading anything written for Lean 2. This is all difficult enough without adding this layer of confusion. Reading https://leanprover.github.io/theorem_proving_in_lean/ will already bring you a long way