New LT instance

Stream: lean4

[Gabriel Ebner]

Lean 4 just got a second instance for LT Nat that is not definitionally equal to the first one. I was just starting to jot down some notes for a pre-RFC, but I wasn't sure if there's a nice way to refactor this.

Clearly you want to avoid writing both Ord and LT instances. For programming, it's obviously a really bad idea to derive Ord from LT. And you can't define LT in terms of Ord either (it's not possible with partial orders in general; and using it as a default results in diamonds with e.g. pi instances).

The typical one-size-fits-all mathlib answer would be the following, right?

class Ord (α : Type u) [LT α] [BEq α] where
  compare : α → α → Ordering
  compare_correct : ∀ a b : α, -- not sure how helpful this is w/o laws on < and ==
    open Ordering in match compare a b with
      | lt => a < b
      | eq => a == b
      | gt => a > b

But that doesn't look helpful for Ord/LT. Is there a reasonable alternative to just removing the Ord α → LT α instance? Ideally one that addresses the motivation for this instance, i.e., not having to write a separate LT instance? Making it a def instead (but then you still need to write both instances)?

[Daniel Fabian]

I was thinking about the one you just described with BEq, when I was adding Ord, but I wasn't happy with it. I was also considering to do it using DecidableEq. But that wasn't truly satisfying either.

In the end, I just made explicit Ord instances and added the helper compareOfLessAndEq this latter one is definitely safe, since you control when it's applied. And for basic data types like number or chars, it certainly is reasonable to derive Ord from that. But for other more complex types, you'd want to derive it explicitly, avoiding to redo work.

Furthermore, Ord seems to imply a total order, but that's not quite right. In particular Eq a b doesn't imply a = b.

[Daniel Fabian]

on the other hand, if we had a total order, deriving an Ord instance for that seems perfectly reasonable, what do you think?

[Gabriel Ebner]

Daniel Fabian said:

on the other hand, if we had a total order, deriving an Ord instance for that seems perfectly reasonable, what do you think?

We want to avoid that for programming; an Ord instance defined in terms of < is never going to be fast (with the few exceptions that you've listed).

[Gabriel Ebner]

(The lexicographic order on strings is a decidable linear order. But you don't want to define an Ord instance from it.)

[Daniel Fabian]

Gabriel Ebner said:

Daniel Fabian said:

on the other hand, if we had a total order, deriving an Ord instance for that seems perfectly reasonable, what do you think?

We want to avoid that for programming; an Ord instance defined in terms of < is never going to be fast (with the few exceptions that you've listed).

which is precisely, why I added a helper function to construct it for the 20 or so cases, but haven't added a typeclass instance.

[Sebastian Ullrich]

How do the two instances for Nat compare? Does the old one have important defeqs the new one does not, e.g. n < m === n.succ <= m? (Is this one important?)

[Gabriel Ebner]

The problem is that there's two of them now, i.e. n < m =!= n < m

[Sebastian Ullrich]

Sure, but I'm asking whether we need the former one :big_smile:

[Gabriel Ebner]

IIRC @Floris van Doorn had some strong opinions on this. But I don't think there's any technical requirement for nice definitional reduction of <.

[Gabriel Ebner]

Removing the other LT Nat does not fix the issue though (I've just picked the most prominent instance for the thread title). The Ord α → LT α instance causes diamonds even if all the duplicate LT instances for types in the core library are fixed, and we adopt the policy that every concrete type only has Ord defined and not LT (where possible).

Blanket instances constructing data like Ord α → LT α always cause diamonds. Say you make a type LexPair α for lexicographically ordered pairs. You add an instance for Ord α → Ord (LexPair α) because you want your code to be fast. Then you add LT α → LT (LexPair α) because the lexicographic ordering also makes sense for types that do not have an Ord instance (e.g. if they're not totally ordered). And bam: you've got two instances LT (LexPair α) that are not definitionally equal.

[Daniel Fabian]

do you have a suggestion? That was something that was always annoying me about type classes. You don't even need a diamond, actually. Say, you have string comparison and case insensitive string comparison. Both are perfectly reasonable things to do. But the type class mechanism is based just on types, so there is really no sensible way to tell which instance you want applied, is there?

[Mario Carneiro]

Sebastian Ullrich said:

How do the two instances for Nat compare? Does the old one have important defeqs the new one does not, e.g. n < m === n.succ <= m? (Is this one important?)

Yes, this defeq is used a lot in mathlib.

[Mac]

Gabriel Ebner said:

Then you add LT α → LT (LexPair α) because the lexicographic ordering also makes sense for types that do not have an Ord instance (e.g. if they're not totally ordered).

Unless I'm mistaken though, Ord is not a total order. You can define and Ord instance for any type that has an decidable LT. For example,

def compareOfLess {α} [LT α] [DecidableRel (@LT.lt α _)] (x y : α) : Ordering :=
  if x < y then Ordering.lt
  else if x > y then Ordering.gt
  else Ordering.eq

instance [LT α] [DecidableRel (@LT.lt α _)] : Ord α :=
  ⟨ compareOfLess ⟩

In order to promote Ord to a true total order, a ((x <=> y) = Ordering.Eq) -> (x = y) law would need to be added.

[Gabriel Ebner]

Yes, these are all lawless. For illustrative purposes, I only picked examples where the instances are lawful though. Because the underlying point is the same no matter whether there are laws or not: blanket instances that construct data cause diamonds.

[Mario Carneiro]

My 2 cents: I think that the Ord -> LT instance should be a def, and instantiated explicitly for any types where the simplest way to prove LT is via Ord.

[Mac]

I think it might be worth it to demote the current Ord to POrd (i.e. a partial order) with Ordering := LT | GT | NA and then introduce a new Ord that has the ((x <=> y) = Ordering.NA) -> (x = y) law. That way any all LT/GT simply leverage POrd (if they have a decidable LT/GT ordering relation).

[Gabriel Ebner]

Daniel Fabian said:

string comparison and case insensitive string comparison [...] But the type class mechanism is based just on types, so there is really no sensible way to tell which instance you want applied, is there?

I think the cleanest way is to make type aliases, i.e., def LocaleSpecificSortingAccordingToUnicode (locale : String) : Type := String.

[Mario Carneiro]

Note that the idea of a function returning LT | GT | EQ already bakes in the concept of a "total preorder" for things like lt and cmp to cohere and be useful in data structures

[Mac]

hence why I suggested the rename to something more general

[Mario Carneiro]

It's not a partial order though

[Mario Carneiro]

Ord has signature A -> A -> Ordering where Ordering := LT | GT | EQ

[Mario Carneiro]

EQ doesn't necessarily mean equal, but it does mean comparable. A partial order would need a none option

[Mac]

Sorry for my imprecision. The point is pick a name that neither implies incomparability or comparability (i.e. Ordering := Less | Greater | Neutral and DecidableOrd for example) and use this more general Ord to always define decidable LT/GT.

[Mario Carneiro]

See Rust's PartialOrd: it needs to be a fourth option

[Gabriel Ebner]

I believe partial orders are a red herring when it comes to Ord instances. We only want Ord instances where the order needs to be total (sorting a list, keys in a tree map, etc.). What is a difficulty though is that Ordering.eq does not mean =, it rather means == (there's of course no law requiring it). For example Ord Expr would return eq for alpha-equivalent expresisons.

[Mario Carneiro]

I think it would be best to introduce a Cmp typeclass that just supplies the cmp : A -> A -> Ordering function, and then Ord can be reserved for the trifecta, possibly with laws relating them

[Mac]

Mario Carneiro said:

I think it would be best to introduce a Cmp typeclass that just supplies the cmp : A -> A -> Ordering function, and then Ord can be reserved for the trifecta, possibly with laws relating them

This is more-or-less what I was trying to suggest.

[Mario Carneiro]

in particular I'm not suggesting "and use this more general Ord to always define decidable LT/GT."

[Mario Carneiro]

There is no a priori relation between the basic typeclasses

[Mario Carneiro]

Ord would combine several ordering operators for convenience: BEq, LT, LE, Cmp, Decidable LE, Decidable LT

[Mario Carneiro]

POrd would have a partial_cmp : A -> A -> Option Ordering instead

[Mac]

Mario Carneiro said:

There is no a priori relation between the basic typeclasses

Why Not Though? From Cmp I can always get Lt/Le/Ge/Gt.

[Mario Carneiro]

Building data from data leads to the diamond problems that gabriel mentioned

[Mario Carneiro]

you don't want to use a generic construction to get Lt from Cmp when the base type is Nat, because nat already has a Lt

[Mac]

But why can't we remove those and just use Cmp for Cmp types?

[Mario Carneiro]

So the generic construction is just a def, available as the default field value in the Ord typeclass

[Mario Carneiro]

Mac said:

But why can't we remove those and just use Cmp for Cmp types?

because that's less efficient? Also it's less convenient when you don't want cmp to get involved in proofs

[Mario Carneiro]

Some types have lt as the basic notion and use it to define le and cmp; some have cmp as basic and define lt and le; others (like Nat!) have lt and le as basic and cmp is derived. When you have this kind of variety, you just need a class that supplies all of them as separate fields and you can pick which to define yourself and which to get automatically filled in

[Mario Carneiro]

Actually, it's even more complicated than that because there is both le and ble and they have separate definitions. (In mathlib le is an inductive predicate and ble is a recursive function.) Again, to please everyone you need them to be separate fields, with a coherence lemma

[Mac]

Mario Carneiro said:

When you have this kind of variety, you just need a class that supplies all of them as separate fields and you can pick which to define yourself and which to get automatically filled in

That is what I am going for. For example, something like this:

class BOrd.{u} (α : Type u) extends Cmp α, LT α, LE α, GT α, GE α where
  lt (a b : α) := cmp a b == Ordering.lt
  le (a b : α) := cmp a b != Ordering.gt
  gt (a b : α) := cmp a b == Ordering.gt
  ge (a b : α) := cmp a b != Ordering.lt
  eq (a b : α) := cmp a b == Ordering.eq

[Mario Carneiro]

oof, I really hope I don't have to worry about GT too

[Mac]

Mario Carneiro said:

oof, I really hope I don't have to worry about GT too

But the current definition of GT creates the same inefficiencies that are currently being railed against (flip is less efficient then a type that directly supports GT).

[Mario Carneiro]

GT doesn't create diamonds because we actually have a decent chance of actually ensuring that no alternate definitions are made

[Mario Carneiro]

also if you inline flip it shouldn't be any slower

[Mac]

It may not create diamonds but it does produce inefficient code (which is the reason why diamonds are bad).

[Mario Carneiro]

or better yet, just don't use GT

[Mac]

Mario Carneiro said:

also if you inline flip it shouldn't be any slower

Not if the source arguments are already in the opposite order.

[Mac]

If a I have foo a b := lt b a this will sometimes necessitate spending cycles to swap the argument order; foo := gt will never.

[Mario Carneiro]

Working with closures is a lot slower than either one

[Mario Carneiro]

always fully apply your functions if possible

[Mac]

I am pretty sure foo := gt is just as efficient as foo a b := gt a b (if not more so)

[Mario Carneiro]

they are compiled to the same thing, it looks like foo(a, b) { return gt(a, b) } when it gets translated to C

[Mario Carneiro]

and argument swapping is free at that point

[Mac]

Mario Carneiro said:

always fully apply your functions if possible

Are you sure about this? This is consider bad in most functional languages. I know this is definite no no in Haskell. I don't know enough about Lean's compiler to know if this is true in Lean though.

[Mario Carneiro]

Haskell has to do crazy things to put the variables back in. Pointfree style is just a design aesthetic

[Mac]

Mario Carneiro said:

and argument swapping is free at that point

no its not?

foo(a, b) { return gt(a, b) } is faster than foo(a, b) { return lt(b, a) } in C.

In fact, it is much faster in the standard C calling conventions as the latter requires swapping things on the stack.

[Mario Carneiro]

if haskell didn't inline so heavily it wouldn't be a reasonable option at all

[Mario Carneiro]

That function would not ever be called, it would be inlined

[Mario Carneiro]

swapping is free here because it's just changing the way the inlining goes

[Mac]

Mario Carneiro said:

Haskell has to do crazy things to put the variables back in. Pointfree style is just a design aesthetic

This is not true. I clearer remember a number of situations in a Haskell where pointfree explicitly provides performance benefits. Its been a while since I've used Haskell, so I don't remember the specifics. But, for thing, I think Haskell as to evaluate the function's thunk in to in order to apply it so I think applications hurt laziness.

[Mario Carneiro]

It's possible that haskell's evaluation semantics can cause a complication here, but you can still write in fully applied form if you evaluate the functions outside the lambda

[Mac]

Mario Carneiro said:

That function would not ever be called, it would be inlined

You are trusting inliners way to much. Second, it is completely possible that lt could be function pointer or a closure or something that is non-inlinable. foo could also be complex enough that it could not be inlined (or it could be being linked to in a manner that prevents inlining).

[Mac]

Mario Carneiro said:

It's possible that haskell's evaluation semantics can cause a complication here, but you can still write in fully applied form if you evaluate the functions outside the lambda

I am not arguing you can write in fully-applied form (and that there are probably cases where it is a good idea), but simply that (1) writing fully applied functions in Haskell is very bad style (in particular, linters will complain heavily about it) and (2) there are many cases where it is a performance problem and (3) it can also damage laziness

[Mario Carneiro]

You are trusting inliners way too much.

Functional programming languages depend on copious optimizations to work. The performance characteristics of a program change completely if you turn off the optimizer. Inlining in particular is really really important, and if it doesn't work then that's one of the first places to look for a performance issue.

Anyway, like I said the easiest solution is to just never use gt. It never comes up outside contrived situations like foo (which is literally just gt) which would be optimized.

[Mac]

Mario Carneiro said:

Anyway, like I said the easiest solution is to just never use gt. It never comes up outside contrived situations like foo (which is literally just gt) which would be optimized.

I disagree greatly with this. Having played around with compilers a lot, I can tell you there are many cases where argument reordering incurs performance penalties. Optimizers can only do so much.

[Mac]

Furthemore, at a notational level I may wish to define > for type without wanting to define <.

[Mario Carneiro]

It's very difficult to discuss this in the abstract, because there are so many confounding factors. It would need a full code example to say something more specific. Regarding notation, you can do that with macro magic, as ever.

[Mario Carneiro]

I fully intend to keep up the mathlib 3 ban on gt in mathlib 4

[Mac]

also I fail to see what the overhead in GT type class would be anyway

[Mario Carneiro]

the overhead of GT is the fact that the typeclass exists, and you have to relate the functions and duplicate all lemmas

[Mac]

Mario Carneiro said:

I fully intend to keep up the mathlib 3 ban on gt in mathlib 4

I think this is another good example of why alternative to mathlib will definitely pop up if/when Lean matures. It is far to opinionated to not acquire competition.

[Mario Carneiro]

perhaps. I have yet to see an actual reason to lift the ban though

[Mac]

Mario Carneiro said:

the overhead of GT is the fact that the typeclass exists, and you have to relate the functions and duplicate all lemmas

Can't you just elide the duplication with a a > b = b < a simp lemma?

[Mario Carneiro]

presumably some alternately-opinionated mathlib alternative would be able to supply such a reason

[Mario Carneiro]

Sure, but it still means the overhead of using simp more, supplying that lemma, larger proofs as a result, interaction between defeq and simp, etc etc

[Mario Carneiro]

The best code is the code you don't have to write

[Mac]

I just think you and I are just not going to agree on design standards anytime soon. :rolling_on_the_floor_laughing:

[Mac]

Except, oddly, I guess, for leanpkg.

[Mario Carneiro]

feel free to make a mathlib alternative and make it public

[Gabriel Ebner]

Mario Carneiro said:

the overhead of GT is the fact that the typeclass exists, and you have to relate the functions and duplicate all lemmas

Note that GT is not a typeclass, and wasn't in Lean 3 either. (Only God knows why it's nevertheless called GT.gt...) IIRC the only complications w.r.t. gt was that it broke simp and rw (due to head-symbol indexing), but could we write ε > 0 again if that's fixed?

[Sebastian Ullrich]

I wasn't quite sure myself, but it does currently work:

example (h : 0 < ε) : ε > 0 := by simp [h]
example (h : ε > 0) : 0 < ε := by simp [h]

This is because both patterns and queries are recursively brought into (reducible) whnf, before inserting/comparing them against each other in the discrimination tree (so you don't pay for all potential matches for each subexpression like in Lean 3)

[Daniel Fabian]

Gabriel Ebner said:

I believe partial orders are a red herring when it comes to Ord instances. We only want Ord instances where the order needs to be total (sorting a list, keys in a tree map, etc.). What is a difficulty though is that Ordering.eq does not mean =, it rather means == (there's of course no law requiring it). For example Ord Expr would return eq for alpha-equivalent expresisons.

It doesn't even mean ==, it just means not < and not >. I was struggling with this when I tried to relate Ord, LT and BEq or DecidableEq.

Or, more precisely, that's how it's used in the data structures.

[Gabriel Ebner]

Right it could be something different, so you shouldn't accidentally use == instead. What I wanted to say is that Ordering.eq is usually an equivalence relation and in general not the same as = (and in this way it is similar to ==).

[Mario Carneiro]

That comes back to the "total preorder" business mentioned earlier: you need x < y \/ x == y \/ x > y for the data structure to work

[Mario Carneiro]

that's what justifies using not < and not > as synonymous for ==

[Daniel Fabian]

and I was saying, that we don't rely x == y. It's a bit of an academic discussion, but it may be relevant in some of the more complicated types like Expr.

[Mario Carneiro]

You can use just < if you know that the ordering is induced by it, although using cmp is usually faster for the data structure

[Mario Carneiro]

it means you only need a [LT A] typeclass in the data structure instead of the whole zoo implied by Ord

[Daniel Fabian]

yeah, that's the refactoring we did.

[Daniel Fabian]

I took the LT implementation, and replaced it with Ord.

[Daniel Fabian]

But Eq is just the fallback case, essentially.

[Daniel Fabian]

Ord is a cheap way of getting < a and > a in one operation.

[Mario Carneiro]

I think the fact that these are lawless structures is confusing matters. The laws required for the data structure to work include transitivity, stuff like x < y -> !(x == y), and !(x < y) -> !(y < x) -> x == y

[Mario Carneiro]

just because they aren't literally used in the programming version doesn't mean they don't conceptually exist anyway

[Mario Carneiro]

it's mostly just simpler to leave the laws out since it means you don't have to prove anything while writing programs

[Daniel Fabian]

Yeah, I get it. And in principle it would be nice to have some kind of lemma carried around with Ord instances. But, alas, that's not the case currently.

[Mario Carneiro]

but the flip side of that is that it is safe to assume that when the laws don't hold, it is "undefined behavior", i.e. the data structure does something but we don't really care what

[Mario Carneiro]

(Personally, I would like to see more access to actual C undefined behavior, but that's a whole separate discussion.)

[Daniel Fabian]

It'd be nice to have a conditional proof, though. Something like "if the instance is lawful, then the RBSet behaves like a set" or something like that.

[Mario Carneiro]

Sure, that's something that mathlib could prove even if the lawless data structure itself is in lean core

[Daniel Fabian]

Nice

[Mario Carneiro]

Speaking of which, I've thought of a simple way to avoid the issue with having the wrong invariants in things like RBNode.WellFormed (they are too strict, they should talk about the black height): Add another constructor to WellFormed using the full red-black invariant. It doesn't ever have to be used in lean core, the only requirement is that the predicate itself is defined. Then mathlib et al can prove that the inductive type "generated by insert and erase and empty and the red-black invariant" is equivalent to "the red-black invariant" by proving that insert, erase, and empty preserve the red-black invariant. The upside is that it then becomes possible to define operations directly on red-black trees that don't go via insert/erase and satisfy the red-black invariant for a different reason

[Mario Carneiro]

Here's what the PR would look like:

+def blackHeight : RBNode α β → OptionM Nat
+  | leaf => pure 0
+  | node red l k v r => do
+    let n ← blackHeight l
+    guard (!isRed l && !isRed r && (← blackHeight r) == n)
+    pure n
+  | node black l k v r => do
+    let n ← blackHeight l
+    guard (!isRed l && (← blackHeight r) == n)
+    pure (n + 1)
+
+def ordered (cmp : α → α → Ordering) : RBNode α β → Bool
+  | leaf => true
+  | node _ l k _ r =>
+    all (fun x _ => cmp x k == Ordering.lt) l &&
+    all (fun y _ => cmp k y == Ordering.lt) r &&
+    ordered cmp l && ordered cmp r

 inductive WellFormed (cmp : α → α → Ordering) : RBNode α β → Prop where
   | leafWff : WellFormed cmp leaf
   | insertWff {n n' : RBNode α β} {k : α} {v : β k} : WellFormed cmp n → n' = insert cmp n k v → WellFormed cmp n'
   | eraseWff {n n' : RBNode α β} {k : α} : WellFormed cmp n → n' = erase cmp k n → WellFormed cmp n'
+  | balancedWff {n : RBNode α β} : (blackHeight n).isSome → ordered cmp n → WellFormed cmp n

[Daniel Fabian]

That doesn't feel like a good idea. The current predicate simply asserts that insertion is well-formed. Almost like an axiom. We should instead formulate the 5 invariants and show that the algorithm preserves them. Then the current predicate would simply assert that an rb tree was constructed by insertions. And your theorem would thus prove the invariants.

And you could define union or intersection etc.

[Mario Carneiro]

I would of course prefer to just prove the correctness of the operations. The advantage of this version is that the lean devs don't have to, it can be offloaded to a library like mathlib. As it currently is written it's not possible to prove this because the actual invariant as stated does not match the real red black invariant

[Daniel Fabian]

What if lean you take the predicate and show that it implies the invariants? As is, you know a tree came into existence as a sequence of applications of those 3 functions

[Mario Carneiro]

The "minimal" well formedness predicate is the inductive type generated by the operations you want to do on the data structure. The "maximal" well formedness predicate is the list of properties you expect (ordering, balance). The hard proof work that can be shifted around but not eliminated is showing that the minimum is less than the maximum. The predicate defined here is basically the larger of these two predicates, so it's obviously greater than the minimal one (so the operations are easy to define) and it's equivalent to the maximal predicate once you do the hard proof work

[Mario Carneiro]

As it is currently, it is possible to prove that WellFormed implies ordering and balance, but not vice versa (I'm not positive but I think the converse is false)

[Mario Carneiro]

Adding the balancedWff variant makes this true by fiat, and the hard proof work becomes showing that everything else in the WellFormed inductive type is superfluous

[Daniel Fabian]

There are 5 rb invariants. I'm pretty sure you need all of them in the induction. Also, it's an rb tree with all 5.

The predicate as is will create a provably well formed tree without proving it. If you formulate the 5 invariants, the current predicate should imply the 5 invariants.

The converse won't hold, because you clearly can create a tree however you like.

And only asserting a subset of the 5 invariants would be an rb tree anymore.

[Mario Carneiro]

what 5 invariants? I think ordering and balance, defined above, cover it

[Mario Carneiro]

If there are more invariants, yes they should show up (conjoined in that last balanceWff variant, not as separate constructors)

[Mario Carneiro]

The main point I'm making is that this can be done with little impact on the code besides the need to write down what the invariant is; no proofs are required in lean core

[Mario Carneiro]

The converse won't hold, because you clearly can create a tree however you like.

It's a nontrivial theorem to show that there are trees that satisfy the invariants without being created by some sequence of insertions and deletions (or that there aren't). It's certainly not obvious to me whether it holds or not - you can get quite a lot of trees by carefully ordering the insertions and maybe getting unusual color layouts by adding and removing other values.

[Mario Carneiro]

still, even if the given predicate is correct, because all well formed trees are accessible by some sequence of inserts and deletes, it seems like an unnecessarily hard theorem to deal with when simply stating the real predicate would solve the problem

[Mario Carneiro]

oh, I think the red black trees as implemented also have a black root node, so you need that too

| balancedWff {n : RBNode α β} : !isRed n → (blackHeight n).isSome → ordered cmp n → WellFormed cmp n

[Daniel Fabian]

Oh yes, I totally get where you're coming from. On the other hand, I don't see what's hard to prove? Just make a copy of insert call it insert' and you've just given a counterexample? I.e. a different way to build a valid tree.

Or did you mean to prove that any valid tree is somehow accessible as a construction of the aforementioned operations. Which I agree is non-obvious to say the least. Although, I don't see why you would care? Generally once a tree is valid, you get all the good properties like fast lookups, etc.

The are the coloring invariants, the root color invariant, the height invariant, sortedness invariant and the leaf color invariant. All 5 have to hold.

[Mario Carneiro]

Oh yes, I totally get where you're coming from. On the other hand, I don't see what's hard to prove? Just make a copy of insert call it insert' and you've just given a counterexample? I.e. a different way to build a valid tree.

No, because if insert' t x y = insert t x y then it still satisfies insertWff

[Mario Carneiro]

similarly, even if the function isn't defined using insert and erase, as long as it is provably equal to some sequence of insert and erase it is still well formed by the current predicate

[Mario Carneiro]

Although, I don't see why you would care? Generally once a tree is valid, you get all the good properties like fast lookups, etc.

The issue is that all operations on RBTree are gated behind this WellFormed predicate that is defined in terms of being accessible by insert and erase. If WellFormed contained the balancedWff variant then you could easily get around the need to prove some complicated accessibility thing by proving well formedness the normal way

[Daniel Fabian]

Ok, so consider an insertion algorithm that, say always replaces x with y and one that keeps it in the Ordering.Eq case. Now you have two different trees that are both valid, but distinct. And one is never constructable from one algorithm and the other is.

(We are talking about a case where x = y is not true, but Ordering.Eq x y is.

[Mario Carneiro]

(note that I'm talking about additions to the RBTree data structure outside the core, where changing the definition of WellFormed isn't an option)

[Daniel Fabian]

Mario Carneiro said:

Although, I don't see why you would care? Generally once a tree is valid, you get all the good properties like fast lookups, etc.

The issue is that all operations on RBTree are gated behind this WellFormed predicate that is defined in terms of being accessible by insert and erase. If WellFormed contained the balancedWff variant then you could easily get around the need to prove some complicated accessibility thing by proving well formedness the normal way

ok, that one, makes a lot of sense.

[Daniel Fabian]

but then you really want the full set of properties, imo

[Daniel Fabian]

and I'd drop the empty case, then.

[Daniel Fabian]

since that one trivially fulfills the complicated invariants.

[Mario Carneiro]

Yeah the empty case is easy to prove

[Mario Carneiro]

I checked wikipedia and it has a list of 5 properties but some are things like "every node is red or black" that don't need a mention

[Mario Carneiro]

I think this is the complete list of invariants

[Daniel Fabian]

that one not, but the color invariant definitely is needed

[Daniel Fabian]

i.e. red parents have black children.

[Mario Carneiro]

The blackHeight function bakes that in with internal !isRed checks

[Mario Carneiro]

It's also possible to write it as an inductive predicate, that might be a bit shorter/cleaner but this one is actually executable which might be useful

[Mario Carneiro]

like so

inductive Balanced : RBNode α β → Rbcolor → Nat → Prop
| leaf : Balanced leaf black 0
| red : Balanced l black n → Balanced r black n → Balanced (node red l k v r) red n
| black : Balanced l black n → Balanced r c n → Balanced (node black l k v r) black (n+1)

...
  | balancedWff {n : RBNode α β} {k} : Balanced n black k → ordered cmp n → WellFormed cmp n

[Daniel Fabian]

yeah, that's more or less the option I used when doing the RBTree with types. You can encode those type families too. Makes writing the algorithm a huge pain, though. Doing it as a predicate on the side might be fine option.

[Daniel Fabian]

And if we had a Decidable instance, we can make it executable that way, no?

[Mario Carneiro]

Yes, you can get the best of both worlds by adding decidability instances

[Mario Carneiro]

although blackHeight is able to decide \exists k c, Balanced t c k which is a bit less obvious with the inductive version

[Mario Carneiro]

For implementing the programming stuff, you wouldn't need to interact with these inductive types at all. It's only when you need to prove something is well formed that it comes up

[Mario Carneiro]

and for functions defined in core, they can cheat by using the other constructors and punt on the well formedness problem

[Daniel Fabian]

yes, if it's a predicate aside from the data structure. In my case, I had them weaved in. As in I had height index and a color index.

[Daniel Fabian]

now by construction you are balanced.

[Daniel Fabian]

but that means when you want to temporarily violate the invariants you need these intermediate types.

[Daniel Fabian]

it's not pretty.

[Mario Carneiro]

I've got an implementation of this stuff in a side project, complete with all the proofs

[Mario Carneiro]

you need some "broken invariant" invariants to deal with insert and erase

[Daniel Fabian]

yeah, pretty messy :-)

[Mario Carneiro]

but I like that the proposed approach means that core doesn't have to deal with any of that, it can be in mathlib where the supporting infrastructure for the proofs is more easily available

[Daniel Fabian]

sooo... how about we define the inductive pred, then and replace the empty ctor with one, where you give a proof of the predicate?

[Mario Carneiro]

Ditto for the WellFounded predicates in HashMap, HashSet, BinomialHeap, and PrefixTree, which use a similar technique. LMK if you want me to send the invariants for these structures

[Daniel Fabian]

please make a bug for now and I'll bring up the context next time I have chat with leo in the next few days. After that, I think you can just make the pr, if that works for you.

[Daniel Fabian]

Just to be clear, with these additional cases in the WellFounded predicates, we should be able to prove that lazy versions imply the invariant-based ones, correct?

[Mario Carneiro]

Yes, although those proofs will often require additional assumptions, for example that the cmp operation is "lawful" (reflexive, transitive, symmetric)

[Mario Carneiro]

that's another good reason to keep it out of core

[Daniel Fabian]

then, that's actually quite nice... Because we show that the internal operations build up something that may or may not be a valid tree using applications of those algorithms. And if for a particular\alpha and Ord \alpha you know lawfulness, you can lift the statement into a proper well-formedness proof.

[Daniel Fabian]

I like it.

[Mario Carneiro]

I'll write up the issue

[Daniel Fabian]

thx