Zulip Chat Archive

Stream: general

Topic: recursive def with match


view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 09 2020 at 19:59):

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

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Reid Barton (Mar 09 2020 at 20:08):

I think it's not possible

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 09 2020 at 20:41):

I wonder why the original doesn't work then!

view this post on Zulip Bryan Gin-ge Chen (Mar 09 2020 at 20:53):

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

view this post on Zulip Johan Commelin (Mar 09 2020 at 21:08):

So much for term mode superiority

view this post on Zulip 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

view this post on Zulip Reid Barton (Mar 09 2020 at 21:09):

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

view this post on Zulip Johan Commelin (Mar 09 2020 at 21:09):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Mar 09 2020 at 21:18):

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

view this post on Zulip Marc Huisinga (Mar 09 2020 at 21:47):

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

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip Mario Carneiro (Mar 10 2020 at 01:28):

as distinct from the top level command which is Fixpoint

view this post on Zulip 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

view this post on Zulip Reid Barton (Mar 10 2020 at 01:30):

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

view this post on Zulip 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

view this post on Zulip 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