Help with "(kernel) function expected"

Stream: new members

[Guilherme Drummond]

Hi there. This is my first time asking here, hope I'm not doing anthing wrong.

I'm trying to implement a record representation for a language in Lean. My advisor developed this code to help me get started: https://gist.github.com/guinasc2/403de98896b50b9ec0e8675d58aa9d5f

However, the evalExp function is giving this error:

(kernel) function expected
  @H1 H2

that is not very informative and left us stumped. From my limited understanding, the problem seems to be in the Exp.App case.

Does anyone know why and what exactly is happening? And how can I make Lean happy with this definition?

We are using Lean 4.7.0.

[Arthur Paulino]

Does that replicate in 4.104.11? If so, your post is likely to get much more traction. And if it doesn't, you might as well just move forward and adopt 4.104.11

[Kyle Miller]

There are no errors on 4.11.0-rc1, but I did need to modify evalExp very slightly:

  def evalExp {ctx t} : Exp ctx t → semCtx ctx → semTy t
  | Exp.Num _ n, _ => n
  | Exp.Var _ _ v, env => lookupVar v env
  | Exp.Abs _ _ _ e, env => by
    simp [semTy]
    intros v
    apply evalExp
    exact e
    simp [semCtx]
    constructor <;> assumption
  | Exp.App _ _ _ e1 e2, env => by
    have H1 := evalExp e1 env
    have H2 := evalExp e2 env
    simp [semTy] at H1
    simp [semTy] at H2
    exact (H1 H2)
  | Exp.MkRec _ _ fs, env => by
    simp [semTy]
    exact (evalFields fs env)
  | Exp.AccField _ _ _ e v, env => by
    have H1 := evalExp e env
    simp [semTy] at H1
    exact (lookupVar v H1)
  termination_by e env => sizeOf e
  decreasing_by
    all_goals simp_wf
    all_goals omega

[Kyle Miller]

I replaced each have h : _ := by exact v with have h := v

[Guilherme Drummond]

Sorry for the delay in responding.
Updating to 4.11.0-rc1 and making Kyle's modification resolved the issue.
Thank you for your help!

Do I need to mark the question as resolved or something else?

[Ruben Van de Velde]

No

[Guilherme Drummond]

Ok. Thank you again!

[Quang Dao]

I wanted to revive this thread since I'm encountering a similar error. Here is my MWE:

import Mathlib.Data.Fin.Basic

structure ProtocolSpec (n : Nat) where
  directions : Fin n → Fin 2
  types : Fin n → Type

abbrev Challenges {n : ℕ} (pSpec : ProtocolSpec n) :=
  (i : Fin n) → (h : pSpec.directions i = 0) → pSpec.types i

/-- Represents the interactive prover for a given protocol specification -/
structure Prover {n : Nat} (pSpec : ProtocolSpec n) (State : Type) where
  /-- Initial state of the prover -/
  init : State
  /-- Action for each step of the protocol -/
  step : (i : Fin n) → State → match pSpec.directions i with
    | 0 => pSpec.types i → State
    | 1 => pSpec.types i × State

variable {n : Nat} {pSpec : ProtocolSpec n} {State : Type}

def Prover.run (prover : Prover pSpec State) (chals : Challenges pSpec) (state : State) : State :=
  /-
  (kernel) function expected
    prover.step n pSpec State ⟨i, h⟩ state (chals ⟨i, h⟩ hDir)
  -/
  let rec loop (i : ℕ) (state : State) (chals : Challenges pSpec) : State :=
    if h : i < n then
      letI i' : Fin n := ⟨i, h⟩
      match hDir : pSpec.directions i' with
      | 0 => by
        letI f := prover.step i' state
        simp [hDir] at f
        haveI newState := loop (i + 1) (f (chals i' hDir)) chals
        exact newState
      | 1 => by
        letI f := prover.step i' state
        simp [hDir] at f
        haveI newState := loop (i + 1) (f.2) chals
        exact newState
    else
      state
  termination_by (n - i)
  loop 0 state chals

Some context: I'm trying to define an interactive proof system, where in each round the prover may either receive a challenge (direction 0) or send out a message (direction 1). The prover may also keep state, and the message & challenge type may vary between rounds.

The error happens when I try to define Prover.run, which given an initial state and a bunch of challenges, does the expected thing.

[Eric Wieser]

You can make that more minimal by replacing ℕ with Nat and changing the import to import Std

[Eric Wieser]

Then you should probably file a bug report on the lean4 repository

[Quang Dao]

I don't think my Std has the notation ℕ loaded yet. But it's surprising that this is a bug in lean4 (how can you be sure?); anyway I will file a bug report.

[Eric Wieser]

Quang Dao said:

I don't think my Std has the notation ℕ loaded yet.

Yes, that is why I told you to remove that notation

[Eric Wieser]

Quang Dao said:

how can you be sure?

An error in the kernel means that either you hit a resource limit (it would tell you), or that something between you and the kernel did the wrong thing and didn't detect it.

[Eric Wieser]

It wouldn't necessarily surprise me if the fix to lean didn't fix your code, but I would expect it to produce a non-kernel error message if it didn't

[Eric Wieser]

Here's a slightly simpler version of your function (which fails in the same way)

def Prover.run (prover : Prover pSpec State) (chals : Challenges pSpec) (state : State) : State :=
  /-
  (kernel) function expected
    prover.step n pSpec State ⟨i, h⟩ state (chals ⟨i, h⟩ hDir)
  -/
  let rec loop (i : Nat) (state : State) (chals : Challenges pSpec) : State :=
    if h : i < n then
      letI i' : Fin n := ⟨i, h⟩
      match hDir : pSpec.directions i' with
      | 0 =>
        letI f := prover.step i' state
        loop (i + 1) (by simp only [hDir] at f; exact f (chals i' hDir)) chals
      | 1 => state
    else
      state
  termination_by (n - i)
  loop 0 state chals

[Kyle Miller]

Here's some more minimization (haven't incorporated Eric's yet updated):

structure ProtocolSpec (n : Nat) where
  directions : Fin n → Bool
  types : Fin n → Type

abbrev Challenges {n : Nat} (pSpec : ProtocolSpec n) :=
  (i : Fin n) → (h : pSpec.directions i = false) → pSpec.types i

structure Prover {n : Nat} (pSpec : ProtocolSpec n) where
  step : (i : Fin n) → Bool → match pSpec.directions i with
    | false => pSpec.types i → Bool
    | true => pSpec.types i × Bool

--(kernel) function expected
--  @f (chals _x_2 hDir)
def loop {n : Nat} {pSpec : ProtocolSpec n} (prover : Prover pSpec) (i : Nat) (state : Bool) (chals : Challenges pSpec) : Bool :=
  if h : i < n then
    let i' : Fin n := ⟨i, h⟩
    match hDir : pSpec.directions i' with
    | false =>
      have f := prover.step i' state
      loop prover (i + 1) (by simp only [hDir] at f; exact f (chals i' hDir)) chals
    | true => state
  else
    state
termination_by (n - i)

[Eric Wieser]

Here's a working version:

def Prover.run (prover : Prover pSpec State) (chals : Challenges pSpec) (state : State) : State :=
  let rec loop (i : Nat) (state : State) (chals : Challenges pSpec) : State :=
    if h : i < n then
      letI i' : Fin n := ⟨i, h⟩
      match hDir : pSpec.directions i' with
      | 0 =>
        have f : pSpec.types i' → State := cast (by simp [hDir]) <| prover.step i' state
        loop (i + 1) (f (chals i' hDir)) chals
      | 1 =>
        have f : pSpec.types i' × State := cast (by simp [hDir]) <| prover.step i' state
        loop (i + 1) (f.2) chals
    else
      state
  termination_by (n - i)
  loop 0 state chals

[Eric Wieser]

If you replace the haves with lets then it fails

[Quang Dao]

Wow thanks. Should I still file a bug report then?

[Eric Wieser]

Adding id <| before the cast is also enough to fix it

[Eric Wieser]

I would say yes; the error is still indicative of a bug, even if it can be worked around

[Kyle Miller]

More minimized:

structure ProtocolSpec (n : Nat) where
  directions : Bool

abbrev Challenges {n : Nat} (pSpec : ProtocolSpec n) :=
  (h : pSpec.directions = false) → Bool

structure Prover {n : Nat} (pSpec : ProtocolSpec n) where
  step : Bool → match pSpec.directions with
    | false => Bool → Bool
    | true => Bool × Bool

--(kernel) function expected
--  @f (chals hDir)
def loop {n : Nat} {pSpec : ProtocolSpec n} (prover : Prover pSpec) (i : Nat) (state : Bool) (chals : Challenges pSpec) : Bool :=
  if h : i < n then
    match hDir : pSpec.directions with
    | false =>
      have f := prover.step state
      loop prover (i + 1) (by simp only [hDir] at f; exact f (chals hDir)) chals
    | true => state
  else
    state
termination_by (n - i)

[Eric Wieser]

Is cast somehow special-cased as something that is allowed to be unfolded?