recursive let in

Stream: new members

[Anatole Dedecker]

Programming question here. Is there some way to define a recursive function using a let ... in expression ? Here's an example in Haskell, which I don't manage to translate to Lean :

fac n =
  let
    aux 0 acc = acc
    aux n acc = aux (n-1) (n*acc)
  in
  aux n 1

[Reid Barton]

No, I think you have to float aux out to a top-level function if you want to use the equation compiler. Alternatively you could use the recursor directly (either in term mode or in tactic mode).

[Anatole Dedecker]

Ok, thanks !

[Anatole Dedecker]

Actually, we can even use tactic mode :sweat_smile:

def fac (n : ℕ) :=
  let aux : ℕ → ℕ → ℕ :=
    begin
      intros k,
      induction k with k hk,
      { exact id },
      { intros acc,
        exact hk ((k+1) * acc) }
    end
  in aux n 1

[Kevin Buzzard]

can you prove anything about it though?

[Kevin Buzzard]

I am a bit scared about the proof term which induction gives you...

[Anatole Dedecker]

It looks okay actually. And at least it evaluates correctly

[Reid Barton]

If you want to prove things about it then it's probably better to float it to top-level

[Anatole Dedecker]

Indeed !

[Kevin Buzzard]

can you prove (n+1)!=(n+1)*n! using your definition?

[Anatole Dedecker]

Oh that's quite annoying indeed...

[Chris Wong]

Is hk just the identity function here? Trying to wrap my head around what that induction is doing...

[Eric Wieser]

@Kevin Buzzard, I was able to prove it with

lemma rec_succ {C: ℕ → Type} {zero_f : C 0} {succ_f : Π n, C n → C n.succ} (n : ℕ) :
  @nat.rec C zero_f succ_f (n + 1) = succ_f n (@nat.rec C zero_f succ_f n) := rfl

example (n : ℕ) : fac (n + 1) = (n+1)*(fac n) := begin
  dsimp only [fac],
  conv_lhs {
    rw (rec_succ n),
    rw mul_one,
  },
  generalize : n + 1 = m,
  induction n with n' generalizing m,
  { simp, },
  {
    conv_lhs { rw n_ih},
    conv_rhs { rw n_ih},
    ring,
  }
end

Although I feel like rec_succ should be builtin somewhere

[Eric Wieser]

Ah, dsimp can handle it after a nat.add_one:

example (n : ℕ) : fac (n + 1) = (n+1)*(fac n) := begin
  rw nat.add_one n,
  dsimp only [fac],
  rw [mul_one, nat.add_one n],
  generalize : n.succ = m,
  induction n with n' generalizing m,
  { simp, },
  { conv_lhs { rw n_ih }, conv_rhs { rw n_ih }, ring, }
end