Daniil Kolesnichenko
Daniil Kolesnichenko

Reputation: 63

Is there a way to call a function recursively from tactic mode or from match expressions in Lean?

Attempt #1:

def sget' {α : Type} {n : ℕ} (i : ℕ) {h1 : n > 0} {h2 : i < n} (s: sstack α n) : α :=
begin
  cases n with n0 nn,
  begin
    have f : false, from nat.lt_asymm h1 h1,
    tauto,
  end,
  induction s,
  cases s_val,
  begin
    have : stack.empty.size = 0, from @stack_size_0 α,
    tauto,
  end,
  cases i with i0 ri,
  exact s_val_x,
  exact sget' (pred i) s_val_s,
end

Attempt #2:

def sget' {α : Type} {n : ℕ} (i : ℕ) {h1 : n > 0} {h2 : i < n} (s: sstack α n) : α :=
match i, s with
  | 0, ⟨stack.push x s, _⟩ := x
  | i, ⟨stack.push _ s, _⟩ := sget' (pred i) ⟨s, _⟩
  | _, ⟨stack.empty, _⟩    := sorry  -- just ignore this

Lean in both cases throws unknown identifier sget' error. I know that I can call sget' recursively from ehh pattern guards (not sure how they are properly called), but is there any way to do something like that with tactics and/or match expressions?

Upvotes: 1

Views: 174

Answers (1)

Yury Kudryashov
Yury Kudryashov

Reputation: 146

You can do recursive calls if you use the equation compiler

def map (f : α → β) : list α → list β
| [] := []
| (a :: l) := f a :: map l

Otherwise you should use induction tactic or one of the explicit recursor functions (like nat.rec).

Upvotes: 1

Related Questions