recursive def with match

Stream: general

[Johan Commelin]

Newbie question. How can I make a recursive call within a match expression?

def f : ℕ → ℕ :=
λ n, match n with
| 0 := 37
| (n+1) := _match n + 57 -- fails
end

[Johan Commelin]

Or is this not how it's supposed to be done?

[Johan Commelin]

I know I can just call f. But suppose that you're in a situation where the thing you are defining doesn't have a name...

[Johan Commelin]

For example

instance : has_neg ℕ :=
⟨λ n, match n with
| 0 := 37
| (n+1) := _match n + 57 -- fails
end⟩

[Reid Barton]

I think it's not possible

[Bryan Gin-ge Chen]

This works:

def f : ℕ → ℕ :=
λ n, match n with
| 0 := 37
| (n+1) := by exact _match n + 57 -- works
end

#eval f 3 -- 208

[Kevin Buzzard]

I wonder why the original doesn't work then!

[Bryan Gin-ge Chen]

Here's what Mario said in an older thread:

the "official" solution is to just have an auxiliary function, or use induction to construct the function. In lean 4, if my suggestion to sebastian worked, we will have an actual term mode notation for this using let

[Johan Commelin]

So much for term mode superiority

[Johan Commelin]

How about a syntax like this

def f : ℕ → ℕ :=
λ n, match n using g with
| 0 := 37
| (n+1) := g n + 57 -- works
end

#eval f 3 -- 208

[Reid Barton]

I mean, for structural recursion like this, you could just apply the recursor directly easily enough

[Johan Commelin]

Sure... but it seems less nice (from a syntactic point of view)

[Patrick Massot]

Johan, your punishment for bad mouthing term mode is to do the (∀ x, p x ∨ r) -> (∀ x, p x) ∨ r exercise in term mode without mathlib lemmas.

[Rob Lewis]

example {α} (p : α → Prop) (r : Prop) : (∀ x, p x ∨ r) -> (∀ x, p x) ∨ r :=
λ h, or.elim (classical.em r) or.inr (λ hr, or.inl $ λ x, or.resolve_right (h x) hr)

Doesn't seem :nauseated: to me?

[Patrick Massot]

Using or.resolve_right feels like cheating, but I've checked and it's in core.

[Marc Huisinga]

example {α} (p : α → Prop) (r : Prop) : (∀ x, p x ∨ r) → (∀ x, p x) ∨ r :=
λ h, by_contradiction (λ h',
  (h' ((em r).elim
    or.inr
    (λ hnr, or.inl (λ x, (h x).elim
      id
      (λ hr, absurd hr hnr))))).elim)

tactic mode could have prevented this

[Patrick Massot]

Of course tactic mode would be by finish probably. But I guess begin contrapose!, exact _ end should be a good compromise (where you still need to fill in the underscore).

[Mario Carneiro]

My proposed syntax for this using let, by the way, is

def f : ℕ → ℕ :=
λ n, let foo : ℕ → ℕ
| 0 := 37
| (n+1) := foo n + 5
in foo n

[Mario Carneiro]

In other words it's like normal let except you write | instead of := after the type, just like you would in a def, and usual equation compiler stuff comes after

[Mario Carneiro]

I think Coq uses a syntax like fix f (params) := body[f] for this kind of "let rec expression"

[Mario Carneiro]

as distinct from the top level command which is Fixpoint

[Mario Carneiro]

We could probably implement it in lean 3.x if we care to, it's mostly leveraging parsers and mechanisms that already exist in lean 3

[Reid Barton]

Johan, out of curiosity, do you want this for mathing, or programming?

[Mario Carneiro]

For mathing I recommend using an auxiliary function. Because this will get broken out as a separate definition by lean anyway, and if you don't give it a name it will get an ugly automatically generated one

[Mario Carneiro]

and that's what you will see when proving theorems about the definition