Stream: general

Topic: recursive def with match

Johan Commelin (Mar 09 2020 at 19:59):

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 (Mar 09 2020 at 19:59):

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

Johan Commelin (Mar 09 2020 at 20:00):

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 (Mar 09 2020 at 20:01):

For example

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


Reid Barton (Mar 09 2020 at 20:08):

I think it's not possible

Bryan Gin-ge Chen (Mar 09 2020 at 20:40):

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 (Mar 09 2020 at 20:41):

I wonder why the original doesn't work then!

Bryan Gin-ge Chen (Mar 09 2020 at 20:53):

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 (Mar 09 2020 at 21:08):

So much for term mode superiority

Johan Commelin (Mar 09 2020 at 21:09):

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 (Mar 09 2020 at 21:09):

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

Johan Commelin (Mar 09 2020 at 21:09):

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

Patrick Massot (Mar 09 2020 at 21:12):

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 (Mar 09 2020 at 21:17):

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 (Mar 09 2020 at 21:18):

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

Marc Huisinga (Mar 09 2020 at 21:47):

example {α} (p : α → Prop) (r : Prop) : (∀ x, p x ∨ r) → (∀ x, p x) ∨ r :=
(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 (Mar 09 2020 at 21:53):

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 (Mar 10 2020 at 01:25):

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 (Mar 10 2020 at 01:26):

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 (Mar 10 2020 at 01:28):

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

Mario Carneiro (Mar 10 2020 at 01:28):

as distinct from the top level command which is Fixpoint

Mario Carneiro (Mar 10 2020 at 01:29):

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 (Mar 10 2020 at 01:30):

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

Mario Carneiro (Mar 10 2020 at 01:44):

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 (Mar 10 2020 at 01:45):

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

Last updated: May 10 2021 at 19:16 UTC