OptionM and DecEq

Stream: lean4

[Scott Viteri]

I have a datatype which contains an OptionM.
Though each individual part of my datatype derives DecidableEq, the proof that the whole datatype is DecidableEq does not go through.

inductive bleh : Type where
| dep : bleh
deriving DecidableEq

#eval decEq (Option.some bleh.dep : OptionM bleh)
            (Option.some bleh.dep : OptionM bleh)

structure bleh2 where val : OptionM bleh

theorem bleh2.eqOfVeq : ∀ {a b : bleh2}, Eq a.val b.val → Eq a b
| ⟨a⟩, ⟨b⟩, p => congrArg bleh2.mk p

instance : DecidableEq bleh2 :=
fun
 | ⟨a⟩, ⟨b⟩ => bleh2.eqOfVeq (decEq a b)

At (decEq a b) I get:

failed to synthesize instance
  DecidableEq (OptionM bleh)

[Mario Carneiro]

There appears to be a missing decidability instance for OptionM. If you add it things work as expected:

inductive bleh : Type
| dep : bleh
deriving DecidableEq

instance [DecidableEq α] : DecidableEq (OptionM α) := instDecidableEqOption

structure bleh2 where val : OptionM bleh
deriving DecidableEq

#synth DecidableEq bleh2

[Scott Viteri]

Hmm then why did the following run?

#eval decEq (Option.some bleh.dep : OptionM bleh)
            (Option.some bleh.dep : OptionM bleh)

[Mario Carneiro]

because type ascriptions don't actually change the type of anything, the decEq there is seeing two things of type Option bleh and calling the instance for Option

[Mario Carneiro]

if you use show OptionM bleh from Option.some bleh.dep instead it should call OptionM's instance

[Scott Viteri]

#check (1:Int) + 1
changes the type, so I am not sure what you mean

[Scott Viteri]

Also did you find instDecidableEqOption by looking through the c code?

[Mario Carneiro]

In that case (1:Int) was used to help infer what 1 means, resulting in something like @One.one Int which has type Int

[Mario Carneiro]

I used #synth

[Mario Carneiro]

I originally tried guessing the name but the naming scheme has changed from lean 3

[Scott Viteri]

ok

[Mario Carneiro]

here's an example of how type ascription doesn't actually change the type

def Foo := Nat
def foo : Nat := 1
#check (foo : Foo) -- foo : Nat
#check show Foo from foo -- (fun (this : Foo) => this) foo : Foo

[Mario Carneiro]

If Foo wasn't defeq to Nat then the first #check would have failed, but other than that and the side effects of unification it doesn't affect the term

[Mario Carneiro]

def Foo := Nat
def mysorry : ∀ α, α := sorry
#check mysorry _ -- mysorry ?m.17 : ?m.17
#check (mysorry _ : Foo) -- mysorry Foo : Foo
#check (mysorry Nat : Foo) -- mysorry Nat : Nat

this is the effect you are seeing with the 1:Nat example

[Scott Viteri]

I find it interesting that show Foo from foo creates a lambda and an application.
Do you have any idea how I would write the instDecidableEqOption proof by hand? Right now it is pushing a proof through the Id monad in a way that seems magical to me.

[Mario Carneiro]

instDecidableEqOption is just a proof that Option A has decidable equality by cases, the Id monad doesn't come up

[Mario Carneiro]

The observation here is that OptionM A is defeq to Option A, so the proof that Option A has decidable equality is also the proof that OptionM A has decidable equality

[Mario Carneiro]

That's because OptionM A is OptionT Id A which is Id (Option A) which is Option A

[Scott Viteri]

I don't see a proof that Option has decidable equality in the lean files?

[Mario Carneiro]

it links to

deriving instance DecidableEq for Option

in Init.Data.Option.Basic

[Mario Carneiro]

The #print proof looks a bit more mysterious:

def instDecidableEqOption.{u_1} : {α : Type u_1} → [inst : DecidableEq α] → DecidableEq (Option α) :=
[anonymous]

I guess it's been erased somehow? @Sebastian Ullrich do you know what's happening here?

[Scott Viteri]

also deriving for OptionM doesn't work

[Scott Viteri]

because "OptionM is not an inductive type"

[Mario Carneiro]

right, because it's not

[Scott Viteri]

which is why I thought I needed a separate proof in the first place

[Mario Carneiro]

well, mathlib has a derive handler for defs too, which maybe should be upstreamed to lean 4

[Scott Viteri]

with pp.all true

def instDecidableEqOption.{u_1} : {α : Type u_1} →
  [inst : DecidableEq.{u_1 + 1} α] → DecidableEq.{u_1 + 1} (Option.{u_1} α) :=
fun {α : Type u_1} [inst : DecidableEq.{u_1 + 1} α] =>
  @_private.Init.Data.Option.Basic.0.decEqOption.{u_1} α fun (a b : α) => inst a b

[Scott Viteri]

maybe it is anonymous because of this private bit

[Scott Viteri]

where I have no idea what inst is

[Mario Carneiro]

that's a variable

[Scott Viteri]

oh right

[Mario Carneiro]

oof I can't #print _private.Init.Data.Option.Basic.0.decEqOption, this is awkward

[Scott Viteri]

Cannot #check _private.Init.Data.Option.Basic.0.decEqOption

[Scott Viteri]

lean_object* l___private_Init_Data_Option_Basic_0__decEqOption____x40_Init_Data_Option_Basic___hyg_588____at_instDecidableEqOption___spec__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l___private_Init_Data_Option_Basic_0__decEqOption____x40_Init_Data_Option_Basic___hyg_588____at_instDecidableEqOption___spec__1___rarg), 3, 0);
return x_2;
}
}

[Mario Carneiro]

It's not even visible from inside Init.Data.Option.Basic, it looks like this

def instDecidableEqOption.{u_1} : {α : Type u_1} →
  [inst : DecidableEq.{u_1 + 1} α] → DecidableEq.{u_1 + 1} (Option.{u_1} α) :=
fun {α : Type u_1} [inst : DecidableEq.{u_1 + 1} α] => @_private.0.decEqOption✝.{u_1} α fun (a b : α) => inst a b

it's double protected, it's got the ✝ too

[Scott Viteri]

does cross mean irreducible?

[Mario Carneiro]

it means inaccessible

[Scott Viteri]

ok

[Mario Carneiro]

as in you can't type the name decEqOption and refer to it

[Mario Carneiro]

The definition exists, but you need tactic hacks to see it

[Scott Viteri]

I wonder why the proof of Option decEq is such a secret

[Scott Viteri]

maybe has to do with the staging?

[Mario Carneiro]

I'm guessing this is just done by default in the derive handler

[Scott Viteri]

but it is not like the c is generated from the derive handler

[Mario Carneiro]

The C has nothing to do with it

[Mario Carneiro]

The derive handler just made a private def

[Scott Viteri]

ok

[Mario Carneiro]

and private defs are a real pain to look at

[Mario Carneiro]

let alone prove properties about

[Scott Viteri]

ok, so mystery mostly solved

[Mario Carneiro]

ah, I got so close but printIdCore is private

[Scott Viteri]

how did you get closer

[Mario Carneiro]

eh, I'll just use homebrew #print

import Lean

open Lean Elab
#eval show TermElabM Unit from do
  let some d ← pure $ (← getEnv).find? `instDecidableEqOption | throwError ""
  let decEqOption := d.value!.bindingBody!.bindingBody!.getAppFn.constName!
  let some d ← pure $ (← getEnv).find? decEqOption | throwError ""
  logInfo d.value!

-- fun {α : Type u_1} (x x_1 : Option α) =>
--   match x, x_1 with
--   | none, none => isTrue proof_1
--   | none, some x => isFalse (proof_2 x)
--   | some x, none => isFalse (proof_3 x)
--   | some a, some b => if h : a = b then Eq.ndrec (isTrue (proof_4 a)) h else isFalse (proof_5 a b h)

[Mario Carneiro]

oh, and the excavation yielded an unexpected observation: that Eq.ndrec shouldn't be there, it should say isTrue (proof_4 a b h). Kernel computation can sometimes get stuck on that

[Scott Viteri]

what is this let decEqOption := d.value!.bindingBody!.bindingBody!.getAppFn.constName

[Scott Viteri]

you use that to get the name which you then search for?

[Mario Carneiro]

yeah, we know the name is being used in the definition of instDecidableEqOption so I pull it out of the expr

[Scott Viteri]

I see

[Mario Carneiro]

there is a fancy tactic for doing this in mathlib

[Scott Viteri]

how to search for proof_1

[Mario Carneiro]

more digging, of course that's private too

[Scott Viteri]

maybe the current name.proof_1

[Mario Carneiro]

none of these names can be typed explicitly

[Mario Carneiro]

they contain numeric components as well as hygiene suffixes

[Scott Viteri]

why shouldn't it be Eq.ndrec (isTrue ...) h

[Scott Viteri]

no I see, because the output is a decidability proof

[Scott Viteri]

must end in isTrue or isFalse

[Mario Carneiro]

because evaluating that expression to a constructor, i.e. isTrue ..., requires evaluating h, which might not work if h uses an axiom

[Scott Viteri]

but a = b is decidable itself?

[Scott Viteri]

and h : a = b

[Mario Carneiro]

right, which means h is coming from the decidability proof of DecidableEq A which could be anything

[Mario Carneiro]

it wouldn't be that unusual for an axiom to come up either, for example the proof of DecidableEq (Bool -> Nat) is surely going to use funext

[Scott Viteri]

so the issue is that if you prove a type has dec eq using some axioms, inference of Option dec eq might block?

[Mario Carneiro]

right

[Mario Carneiro]

well not inference but rather computation making use of the derived instance on Option

[Scott Viteri]

so Option (Bool -> Nat) cannot have dec eq?

[Mario Carneiro]

it has dec eq but if x = x then a else b = a won't be rfl when x has type Option (Bool -> Nat)

[Scott Viteri]

so if you eval to check if a= b where a b : Option (Bool -> Nat) it will block

[Mario Carneiro]

yes (in the kernel, not in C)

[Scott Viteri]

ok nice

[Mario Carneiro]

the compiler treats Eq.ndrec like an identity function so it doesn't block and it doesn't compute h either

[Scott Viteri]

I tried to instantiate the same solution for EvalMeta (Option a)

[Scott Viteri]

synth tells me to look for instMetaEval

[Scott Viteri]

but instMetaEval or Lean.instMetaEval does not seem to be in scope

[Scott Viteri]

grepping through lean src is similarly unsuccessful

[Scott Viteri]

trying

#eval show TermElabM Unit from do
  let some d ← pure $ (← getEnv).find? `instMetaEval | throwError ""
  logInfo d.value!

hangs

[Mario Carneiro]

make sure you have an up to date installation, the issue with empty messages hanging the server has been fixed recently

[Scott Viteri]

~/LocalSoftware/signatures/lean4 $ lean --version
Lean (version 4.0.0-nightly-2021-04-27, commit 1f05f5bf1193, Release)

[Sebastian Ullrich]

It was fixed in the extension, not Lean

[Scott Viteri]

then the question is which extension -- vscode or emacs (I'm using emacs)

[Mario Carneiro]

Scott Viteri said:

synth tells me to look for instMetaEval

how did you do this

[Mario Carneiro]

variable (a : Type) [MetaEval a]
#synth MetaEval (Option a)

doesn't seem to work for me

[Sebastian Ullrich]

Ah, it never was an issue in Emacs - it would simply show you the line and column and then an empty message afterwards

[Scott Viteri]

#synth Lean.MetaEval (Option Nat)

[Scott Viteri]

Ok, then not my issue

[Mario Carneiro]

#print instMetaEval reveals that it's actually Lean.instMetaEval

[Scott Viteri]

hmm tried it

[Mario Carneiro]

you can also use ``instMetaEval to make name resolution kick in

[Sebastian Ullrich]

Sebastian Ullrich said:

Ah, it never was an issue in Emacs - it would simply show you the line and column and then an empty message afterwards

Yep, that's exactly what it's doing for me:

Messages (2)
4:0:

4:0:

No hang

[Mario Carneiro]

#eval show TermElabM Unit from do
  let some d ← pure $ (← getEnv).find? ``instMetaEval | throwError "a"
  logInfo d.value!
-- fun {α : Type u} =>
--   { eval :=
--       fun (env : Lean.Environment) (opts : Lean.Options) (a : α) (hideUnit : Bool) =>
--         do
--           Lean.Eval.eval (fun (x : Unit) => a) hideUnit
--           pure env }

[Scott Viteri]

Oh, Lean.instMetaEval gives a different error message

[Scott Viteri]

I need to implement Eval as well

[Mario Carneiro]

although I'm getting Error: index out of bounds in the output window from something

[Scott Viteri]

oh, why does `` make it work in the metaprogram?

[Mario Carneiro]

That resolves names in the current namespace / open

[Mario Carneiro]

so since Lean is open it resolves to Lean.instMetaEval

[Mario Carneiro]

(I haven't been showing it but my file has

import Lean

open Lean Elab

at the top)

[Mario Carneiro]

btw

variable

is throwing a panic for me, is this already reported?

PANIC at Lean.Elab.Command.getBracketedBinderIds Lean.Elab.Command:292:56: unreachable code has been reached

[Scott Viteri]

Fixed my problems with

instance [DecidableEq α] : DecidableEq (OptionM α) :=
  instDecidableEqOption

instance [ToString α] : ToString (OptionM α) :=
  instToStringOption

instance [Lean.Eval α] [ToString α] : Lean.Eval (OptionM α) :=
  Lean.instEval

instance [Lean.MetaEval α] [ToString α] : Lean.MetaEval (OptionM α) :=
  Lean.instMetaEval

[Scott Viteri]

Mario Carneiro said:

That resolves names in the current namespace / open

Ok, and why does #print succeed when #check does not

[Mario Carneiro]

not sure what you mean?

[Mario Carneiro]

these both work for me

import Lean
open Lean Elab
#print instMetaEval
#check @instMetaEval

[Mario Carneiro]

you need the @ in check since otherwise it will try to solve a typeclass problem

[Scott Viteri]

ok that was my problem

[Scott Viteri]

didn't read the error

[Scott Viteri]

actually that is not true -- I just had it open somewhere that didn't have "open Lean Elab"

[Scott Viteri]

Sebastian Ullrich said:

Sebastian Ullrich said:

Ah, it never was an issue in Emacs - it would simply show you the line and column and then an empty message afterwards

Yep, that's exactly what it's doing for me:

Messages (2)
4:0:

4:0:

No hang

You are right -- I saw that #eval was not underlined, which made me think it was still computing