RBMap not looking up value

Stream: new members

[Quinn]

import Lean.Data.RBMap
def Map := Lean.RBMap Nat Nat (fun _ _ => Ordering.lt)
def map: Map := Lean.RBMap.ofList [(1, 2)]
#eval map.find! 1

This is giving me 0, presumably the inhabited instance of nat. why isn't it giving me 2?

[Quinn]

oh, also: the lsp docs in my IDE for find! says it panics if there's no lookup, but it demands the target type is inhabited leading me to believe that it defaults if there's no lookup. am i confused or are the docs wrong? in my live.lean-lang.org link you can put a nonsense key in like 3 and it won't panic, it'll return zero

[Quinn]

update on panic: it panics when i do lean exe ... at terminal, but fills with inhabited instance (default) in the IDE session. is that how that works?

[Quinn]

AssocList is just as bad

import Lean.Data.AssocList

#check Lean.AssocList.empty.insert 1 2
def Map' : Type := Lean.AssocList Nat Nat
def map' : Map' := Lean.AssocList.empty.insert 1 2
#eval map.find? 1

returns none. should return some 2.

[Alex J. Best]

You are setting the ordering in a way that violates the assumptions. Use Lean.RBMap Nat Nat cmpLE instead and it works fine.

[Alex J. Best]

Your second example refers to map still and not map'

[Quinn]

Alex J. Best said:

Your second example refers to map still and not map'

oops! behavior is as expected when i fix that.

[Quinn]

so redblack trees are predicated on the ordering of keys being LE, not LT, I'm surmising. didn't know that!

[Quinn]

I think assoclist is more appropriate for my usecase, so i'm refactoring

[Alex J. Best]

Actually using cmp (the lt version) is probably better than cmpLE. The issue with your definition wasn't the difference between lt and le, rather that the definition you gave makes a < b true for any pair a,b so its not a well behaved relation at all

import Mathlib
def Map := Lean.RBMap Nat Nat cmp
def map: Map := Lean.RBMap.ofList [(1, 2)]
#eval map.find! 1

also workss

[Quinn]

oh. fun _ _ => Ordering.lt is just what got it to typecheck. I didn't know how to construct an Ordering type out of fun a b => a < b

[Quinn]

but this is in a mathlib-free project

[Quinn]

so cmp or cmpLE didn't work in live.lean-lang, since i wasn't importing anything mathlib

[Quinn]

what's going on with the part about how find! defaults to inhabited in lsp but panics at lake exe?