What is that `.` in `rbmap`'s definition?

Stream: new members

[Marko Grdinić]

def rbmap (α : Type u) (β : Type v) (lt : α → α → Prop . rbtree.default_lt) : Type (max u v) :=
rbtree (α × β) (rbmap_lt lt)

I am wondering what Prop . rbtree.default_lt is supposed to be. The . operator here does not seem to be a function so it is probably some kind of built in, but I am not sure what it does.

It is too bad that β here is not dependent on α. I have a use case where that would be useful and am going to try to redesign the rbmap. It is good there is not much there.

[Kenny Lau]

it's \a \to \a \to Prop defaulting to rbtree.default_lt

[Marko Grdinić]

@Kenny Lau

I see. Does it get printed like lt : auto_param (α → α → Prop) (name.mk_string "default_lt" (name.mk_string "rbtree" name.anonymous)) for you?

Also...

def rbmap_lt {α : Type u} {β : Type u → Type v} (lt : α → α → Prop) (a b : Σ α, β α) : Prop :=
lt a.1 b.1

set_option auto_param.check_exists false

def rbmap (α : Type u) (β : Type u → Type v) (lt : α → α → Prop . rbtree.default_lt) : Type (max u v) :=
rbtree (Σ α, β α) (rbmap_lt lt)

type mismatch at application
  lt (a.fst)
term
  a.fst
has type
  Type u : Type (u+1)
but is expected to have type
  α : Type u

I am getting some type errors in both functions when trying to make a dependent map that I am not sure how to deal with. What is wrong here?

[Marko Grdinić]

def rbmap_lt {α : Type} {β : α → Type} (lt : α → α → Prop) (a b : Σ α, β α) : Prop :=
lt a.1 b.1

set_option auto_param.check_exists false

def rbmap (α : Type u) (β : α → Type v) (lt : α → α → Prop . rbtree.default_lt) : Type (max u v) :=
rbtree (Σ α, β α) (rbmap_lt lt)

type mismatch at application
  rbmap_lt lt
term
  lt
has type
  auto_param (α → α → Prop) (name.mk_string "default_lt" (name.mk_string "rbtree" name.anonymous)) : Type u
but is expected to have type
  ?m_1 → ?m_1 → Prop : Type

I've managed to figure out the first part. Now what is this?

[Mario Carneiro]

Notice that the type is Type instead of Type u

[Mario Carneiro]

the auto_param thing is not the problem

[Mario Carneiro]

When you defined rbmap_lt, you used Type for the type of alpha and beta (i.e. non universe polymorphic), but then you apply it in rbmap where alpha and beta now live in arbitrary universes

[Marko Grdinić]

def rbmap_lt {α : Type u} {β : α → Type v} (lt : α → α → Prop) (a b : Σ α, β α) : Prop :=
lt a.1 b.1

set_option auto_param.check_exists false

def rbmap (α : Type u) (β : α → Type v) (lt : α → α → Prop . rbtree.default_lt) : Type (max u v) :=
rbtree (Σ α, β α) (rbmap_lt lt)

So like this then. If I omit the universe levels in the type will it get inferred like so or will it be non-universe polymorphic? I can't check this easily because #check seems to fail with an error when I pass it this function.

[Marko Grdinić]

The error is invalid auto_param, unknown tactic 'rbtree.default_lt'.

[Scott Morrison]

Yeah, I was running into the same problem: rbtree.default_lt doesn't seem to actually exist...

[Mario Carneiro]

it's in init.data.rbtree.default

[Mario Carneiro]

this checks for me:

prelude
import init.data.rbtree.basic
universes u v

def rbmap_lt {α : Type u} {β : α → Type v} (lt : α → α → Prop) (a b : Σ α, β α) : Prop :=
lt a.1 b.1

set_option auto_param.check_exists false

def rbmap (α : Type u) (β : α → Type v) (lt : α → α → Prop . rbtree.default_lt) : Type (max u v) :=
rbtree (Σ α, β α) (rbmap_lt lt)

[Mario Carneiro]

If I don't use prelude then I get a duplicate definition error because this is all defined in init

[Mario Carneiro]

So like this then. If I omit the universe levels in the type will it get inferred like so or will it be non-universe polymorphic?

If you want to omit the universe level but keep it polymorphic, use Type* (or Type _ which is equivalent). The core library deliberately uses universe variables everywhere, but in mathlib the preference is for Type* unless universe inference fails

[Marko Grdinić]

If I don't use prelude then I get a duplicate definition error because this is all defined in init

Actually, I am using that as well as I just copy pasted the rbmap.basic into my own project. But even if I insert that #check rbmap in the original file, I get the same error.

[Mario Carneiro]

right, #check rbmap fails if you put it right after my code snippet

[Mario Carneiro]

If you import init.data.rbtree instead, then it calls the tactic (which fails)

[Mario Carneiro]

This is only a problem if you use the auto_param feature: that is, you leave implicit the lt argument

[Mario Carneiro]

#check @rbmap works fine

[Mario Carneiro]

obviously it can't call the tactic if it doesn't exist. Normally it errors when the auto_param is defined, but as you can see from the code snippet this check was explicitly disabled

[Mario Carneiro]

I'm not exactly sure why the definition was delayed, but I would guess it's because of bootstrapping the tactic framework

[Marko Grdinić]

Ok, I see. Just a bit more...

def drbmap_lt {α : Type u} {β : α → Type v} (lt : α → α → Prop) (a b : Σ α, β α) : Prop :=
lt a.1 b.1

I am a bit confused here. Why is this type definition right?

def drbmap_lt {α : Type u} {β : α → Type v} (lt : α → α → Prop) (a b : Σ (x : α), β x) : Prop :=
lt a.1 b.1

Shouldn't I have written it like this?

[Marko Grdinić]

drbmap :
  Π (α : Type u_1),
    (α → Type u_2) →
    auto_param (α → α → Prop) (name.mk_string "default_lt" (name.mk_string "rbtree" name.anonymous)) →
    Type (max u_1 u_2)

Also were you saying that the printing of the auto_param is not an error?

[Mario Carneiro]

The only difference between your two definitions is the name of the bound variable

[Mario Carneiro]

the first one is confusing because the bound variable α shadows the α earlier in the definition

[Mario Carneiro]

The auto_param thing is supposed to be there. A (x : foo . tac) binder is elaborated to (x : auto_param foo `tac). If you look at the definition, you will see that auto_param α tac := α, so this doesn't affect type correctness of anything. It just acts as a marker for the elaborator so it can remember what tactic you wanted to call in case the value is not provided

[Mario Carneiro]

A similar thing happens with opt_param, if you write (x : foo := val)

[Marko Grdinić]

def mem : α → rbnode α → Prop
| a leaf               := false
| a (red_node l v r)   := mem a l ∨ (¬ lt a v ∧ ¬ lt v a) ∨ mem a r
| a (black_node l v r) := mem a l ∨ (¬ lt a v ∧ ¬ lt v a) ∨ mem a r

Would it be worth it to change the above implementation of mem to the following one?

def mem : α → rbnode α → Prop
| a leaf               := false
| a (red_node l v r)   := (¬ lt a v ∧ ¬ lt v a) ∨ mem a l ∨ mem a r
| a (black_node l v r) := (¬ lt a v ∧ ¬ lt v a) ∨ mem a l ∨ mem a r

I am surprised it has not been done like this originally. Rather than traversing the left side of the tree first, it would be better to check immediately whether the element is a match and shortcut the search if it is.

[Kenny Lau]

or does not short circuit in Lean

[Mario Carneiro]

The implementation of rbmaps in core is... not good. You should probably not literally reuse it, but adapt it to your purposes if you like. There is an ordmap branch on mathlib with a faster implementation, but it's not completely proven correct yet

[Mario Carneiro]

@Kenny Lau , or does short circuit because of the decidable instance

[Floris van Doorn]

here is an example that shows or does short circuit:

#reduce if true ∨ (@to_bool false $ classical.prop_decidable _) then 1 else 0

[Marko Grdinić]

prelude
import init.data.rbtree
import init.data.rbtree.basic tactic.library_search

universes u v w

def drbmap_lt {α : Type u} {β : α → Type v} (lt : α → α → Prop) (a b : Σ α, β α) : Prop :=
lt a.1 b.1

set_option auto_param.check_exists false

def drbmap (α : Type u) (β : α → Type v) (lt : α → α → Prop . rbtree.default_lt) : Type (max u v) :=
rbtree (Σ α, β α) (drbmap_lt lt)

def mk_drbmap (α : Type u) (β : α → Type v) (lt : α → α → Prop . rbtree.default_lt) : Type (max u v) :=
rbtree (Σ α, β α) (drbmap_lt lt)

namespace drbmap
variables {α : Type u} {β : α → Type v} {δ : Type w} {lt : α → α → Prop}

def empty (m : drbmap α β lt) : bool :=
m.empty

def to_list (m : drbmap α β lt) : list (Σ α, β α) :=
m.to_list

def min (m : drbmap α β lt) : option (Σ α, β α) :=
m.min

def max (m : drbmap α β lt) : option (Σ α, β α) :=
m.max

def fold (f : ∀ (a : α), β a → δ → δ) (m : drbmap α β lt) (d : δ) : δ :=
m.fold (λ e, f e.1 e.2) d

def rev_fold (f : ∀ (a : α), β a → δ → δ) (m : drbmap α β lt) (d : δ) : δ :=
m.rev_fold (λ e, f e.1 e.2) d

private def mem' (a : α) : ∀ (m : rbnode (Σ α, β α)), Prop
| rbnode.leaf           := false
| (rbnode.red_node l ⟨ v, _ ⟩  r)  := (¬ lt a v ∧ ¬ lt v a) ∨ mem' l ∨ mem' r
| (rbnode.black_node l ⟨ v, _ ⟩  r)  := (¬ lt a v ∧ ¬ lt v a) ∨ mem' l ∨ mem' r

def mem (k : α) (m : drbmap α β lt) : Prop := @mem' α β lt k m.val

instance : has_mem α (drbmap α β lt) := ⟨mem⟩

instance [has_repr (Σ α, β α)] : has_repr (drbmap α β lt) :=
⟨λ t, "drbmap_of " ++ repr t.to_list⟩

def drbmap_lt_dec [h : decidable_rel lt] : decidable_rel (@drbmap_lt α β lt) :=
λ a b, h a.1 b.1

variable [decidable_rel lt]

def insert (m : drbmap α β lt) (k : α) (v : β k) : drbmap α β lt :=
@rbtree.insert _ _ drbmap_lt_dec m ⟨ k, v ⟩

Here is what I did so far. However the find function is giving me some trouble.

private def find (k : α) : rbnode (Σ α, β α) → option (β k)
| rbnode.leaf             := none
| (rbnode.red_node a k' b) :=
    if h_lt : lt k k'.1 then find a
    else if h_gt : lt k'.1 k then find b
    else
        let x := some k'.2 in
        have h_eq : k'.1 = k, by sorry,
        by { rw h_eq at x, from x }
| (rbnode.black_node a k' b) :=
    if h_lt : lt k k'.1 then find a
    else if h_gt : lt k'.1 k then find b
    else
        let x := some k'.2 in
        have h_eq : k'.1 = k, by sorry,
        by { rw h_eq at x, from x }

I have that ~ k < k'.1 /\ ~ k'.1 < k, so I should be able to prove that k = k'.1, but I am not sure how to do that. Any idea of how I should approach this?

[Marko Grdinić]

---

def to_value : option (α × β) → option β
| none     := none
| (some e) := some e.2

The last issue that I have before I am done with generalizing the rbmap is to figure out what to do with to_value. Here is how it was originally. If the tuple is replaced by a sigma type then the definition should be something like the following...

def to_value : option (Σ α, β α) → option _

What should that wildcard be here? Is it even possible to do anything here? I think there probably isn't as the type of the value depends on the key now, but I am not completely sure so I'll ask here.

[Marko Grdinić]

With regard to my find questions, after some thinking I've come to the conclusion that there is no way that both sides of lt being false would mean that propositional equality must be true. lt can be anything and can for example compare only part of a key. So with that in mind, the right implementation would be...

private def find (k : α) : rbnode (Σ α, β α) → option (Σ α, β α)
| rbnode.leaf             := none
| (rbnode.red_node a k' b) :=
    if lt k k'.1 then find a
    else if lt k'.1 k then find b
    else k'
| (rbnode.black_node a k' b) :=
    if lt k k'.1 then find a
    else if lt k'.1 k then find b
    else k'

def find_entry (m : drbmap α β lt) (k : α) : option (Σ α, β α) := @find _ _ lt _ k m.val

With this finishing the rest of the module is easy.

def contains (m : drbmap α β lt) (k : α) : bool :=
(find_entry m k).is_some

def from_list (l : list (Σ α, β α)) (lt : α → α → Prop . rbtree.default_lt) [decidable_rel lt] : drbmap α β lt :=
l.foldl (λ m p, insert m p.1 p.2)  (mk_drbmap α β lt)

end drbmap

def drbmap_of {α : Type u} {β : α → Type v} (l : list (Σ α, β α)) (lt : α → α → Prop . rbtree.default_lt) [decidable_rel lt] : drbmap α β lt :=
drbmap.from_list l lt

[Marko Grdinić]

As it turns out, these red black trees not being able to understand that the key being put in is the same as the one being taken out when doing indexing into them is a lot bigger problem than I thought at first. With dependent types, that means that it can no longer reduce based on the key and it is causing me all sorts of issues downstream.

These trees are useless as they are now. I'd recommend avoiding them in favor of something that uses direct equality.

[Marko Grdinić]

Alternatively, it might be worth rewriting the above to use some kind of decidable trichotomy.