Offloading decidable equality checks

Stream: general

[Sky Wilshaw]

Is there a way to offload decidable equality to the VM? If not, is ther a better way to write tests of my functions in this way?

import Lean.Data.Parsec

open Lean Parsec

def beginEnv (environment : String) : Parsec Unit := skipString s!"\\begin\{{environment}}"
def endEnv (environment : String) : Parsec Unit := skipString s!"\\end\{{environment}}"

def env (environment : String) (inner : Parsec α) : Parsec α :=
  beginEnv environment *> inner <* endEnv environment

deriving instance DecidableEq for Except

#eval (env "foo" (pstring "test")).run "\\begin{foo}test\\end{foo}" -- .ok "test"

theorem envTest :
    (env "foo" (pstring "test")).run "\\begin{foo}test\\end{foo}" = .ok "test" :=
  by decide -- timeout

[Sky Wilshaw]

Alternatively, are there simp lemmas for things in parsec?

[Alex J. Best]

You can use native_decide in place of decide I believe

[Shreyas Srinivas]

At the price of trusting the compiler

[Sky Wilshaw]

Ah great, that worked! I knew something like that had to exist.

[Eric Wieser]

rfl works there too

[Sky Wilshaw]

It takes too long to elaborate rfl unfortunately.

[Eric Wieser]

Weird, it works instantly for me

[Sky Wilshaw]

Interestingly enough by rfl is fast but rfl is slow. What's the difference?

[Eric Wieser]

Is this on the example above, or a much bigger example?

[Eric Wieser]

If the former, maybe you're on an older lean.

[Mauricio Collares]

There is a difference, but it was much more pronounced in earlier versions of Lean. Are you using an older Lean version?

[Sky Wilshaw]

It's just the example above. by rfl is instant, and rfl times out. I'm on leanprover/lean4:nightly-2023-05-09 .

[Eric Wieser]

That's 6 months old

[Eric Wieser]

I think it predates the first official release, and probably the FRO?

[Sky Wilshaw]

Ah, right. lake update wasn't doing anything so I just assumed I was already on a relatively recent one.

[Sky Wilshaw]

Does lake update even update the toolchain?

[Sky Wilshaw]

Just updated to 4.3.0-rc1 and now rfl is fast. Thanks for the help!

[Eric Wieser]

Sky Wilshaw said:

Does lake update even update the toolchain?

Only if you're using mathlib (!)

[Scott Morrison]

(Mathlib provides a post update hook that does this.)