## Stream: general

### Topic: anonymous recursive functions

#### Andrew Ashworth (Jun 17 2018 at 04:31):

is it possible to define an anonymous recursive function? so for I've been making auxiliary defs as needed, but I'm copying a development from coq that uses them a lot

#### Andrew Ashworth (Jun 17 2018 at 04:32):

something like this from CPDT

Definition check_even : forall n : nat, [isEven n].
Hint Constructors isEven.

refine (fix F (n : nat) : [isEven n] :=
match n with
| 0 => Yes
| 1 => No
| S (S n') => Reduce (F n')
end); auto.
Defined.


#### Mario Carneiro (Jun 17 2018 at 05:46):

Unfortunately no, at least not in term mode. As a workaround you can use induction, but the only way to get the full power of the equation compiler is to have an auxiliary def, and this is what I usually do.

#### Simon Hudon (Jun 17 2018 at 13:12):

You could write

nat.rec Yes (λ f n, match n with
| 0 := No
| (succ n') := Reduce (f n')
end )


#### Mario Carneiro (Jun 17 2018 at 17:30):

There is also a somewhat hackish way. Did you ever wonder about those _match and _let_match variables in the context sometimes? Those are the same mechanism used to support recursive definitions using the equation compiler, and if you refer to them it will get compiled to a recursive function just like a recursive def. For example:

def fib (n : ℕ) : ℕ :=
match n with
| 0 := 0
| 1 := 1
| n+2 := by rename _match fib; exact fib n + fib (n+1)
end


This doesn't work in term mode though:

def fib (n : ℕ) : ℕ :=
match n with
| 0 := 0
| 1 := 1
| n+2 := _match n + _match (n+1)
end


fails unless you insert by exact on the last line.

#### Mario Carneiro (Jun 17 2018 at 17:42):

I guess the main reason this isn't already supported officially is because there is no obvious place in match notation to put the name of the defined function

#### Mario Carneiro (Jun 17 2018 at 17:51):

Examples of the other two match types:

inductive tree : Type
| mk : ∀ n, (fin n → tree) → tree

def path : tree → Type :=
λ ⟨n, t⟩, by exact Σ n, _fun_match (t n)

def path' (T : tree) : Type :=
let ⟨n, t⟩ := T in
by exact Σ n, _let_match (t n)


#### Simon Hudon (Jun 17 2018 at 17:53):

Cool hack :grin:

Last updated: May 08 2021 at 09:11 UTC