Zulip Chat Archive

Stream: general

Topic: anonymous recursive functions


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

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

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

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

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

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

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

view this post on Zulip Simon Hudon (Jun 17 2018 at 17:53):

Cool hack :grin:


Last updated: May 08 2021 at 09:11 UTC