Enforcing a binary search tree ordering in the data type

[Tornai]

Hello all,

First, a tl;dr: Is it possible to prove the ordering of the data inside a binary search tree inside the definition of the data structure, where the data is a generic Ord? If it is possible (and I assume it is since it's possible with refinement types, which are arguably weaker than dependent types), what would be the right way of doing it?

Now, for the whole story: I've been working on this project for some time now, it's supposed to be a part of my bachelor thesis where I'm comparing Liquid Haskell to Idris, but I'm struggling to understand how exactly am I supposed to enforce what seems to be a simple boolean test inside the data structure of a tree. Also,I'm not sure it'll make a difference but I'm using Idris 1.

For starters, I'm trying to do something like I was able to do following the Liquid Haskell tutorial, where with refinement types I can enforce the ordering of a binary search tree inside the data structure with simple boolean conditions. A working code can be found here: https://github.com/LucasTornai/pgc-ufabc/blob/main/haskell-structures/MyBST.hs

That being said, when trying to apply the same rules to Idris, I first seem to have fallen in a trap with "Data.So", where I couldn't manage to prove what I wanted with it. A non-working code sample can be found here, where I manage to compile it, but the ordering rule is able to be broken in the insert function, where I can add bigger numbers than the root in the left side and vice-versa (the wrongInsert function don't prevent the compilation and actually works): https://github.com/LucasTornai/pgc-ufabc/blob/main/idris-structures/MyBST.idr 

After looking in a lot of places, what I thought was the most helpful to get where I was wanting to get was this conversation in the mailing list https://groups.google.com/g/idris-lang/c/qujHxNuZjZg/m/ji5t_qufAwAJ, but it has a problem I find with most ways to prove thins I'm finding for Idris: it's always using "Nat". In my definition of a binary search tree, I wanted to prove the ordering of the data for any Ord, but I fail to understand what's the missing step from the Nat to a more generic Ord to write this kind of proof.

Also, I'm not sure the way I'm approaching it is right, because I want the proof to be contained inside the data structure, and if you checked the Idris code I wrote, I'm using a dependent tuple where I have a simple tree, and together with it the definition of a BST, which is basically the ordering. Checking this repo I found which seems to have good implementations (and also helped me to learn a lot about Idris): https://github.com/jfdm/idris-containers, I've seem the BST implementation is also not made the way I want it to be done (they enforce the ordering in the functions, not in the data structure itself), so it makes me doubt what I'm doing a bit.

Having the confirmation that it can be done would already be good, but if so, can someone help to show me how exactly can I enforce this kind of boolean proof inside a data structure? (Not necessarily a BST).

[James Cook]

Caveats: I'm not that familiar with Idris 1,  and I haven't read very much of your code.

Thoughts:

* Does your code still compile with %default total? Those case statements where you only have a "proofYes" case made me suspicious the compiler's letting you get away with missing cases in your proofs.

* I suspect you will need some properties of the Ord implementation. I wonder if you could do something like this:

interface Ord a => CorrectOrd a where

  transitive : (x : a) -> (y : a) -> (z : a) -> x <= y -> y <= z -> x <= z

  reflexive: (x : a) -> x <= x

  (and maybe others)

Otherwise you'd have to prove your code works even if the Ord implementation makes no sense.

* I suspect the proof can be made more integral to the data structure. For example (NB I haven't tried compiling this, and also am used to Idris 2):

data TreeBetween : (a : Type) -> Ord a => (min : a) -> (max : a) -> Type where

  -- A tree where all values are between min and max.

  Leaf : TreeBetween a min max

  Node : Ord a => (key : a) -> (less : a <= max = True) -> (more : a >= min = True) -> (left : TreeBetween min key) -> (right : TreeBetween key max) -> TreeBetween a min max

This appeals to me a bit more because the constraints live on the nodes of the tree.

[Denis Buzdalov]

`Ord` is particularly painful to work with in the proof-world setting. First, it has a lot of different functions that must be coherent with each other; then order-related properties must hold on comparison functions; and equivalence-related properties must hold on equality-part of ordering.

 

Now, for the whole story: I've been working on this project for some time now, it's supposed to be a part of my bachelor thesis where I'm comparing Liquid Haskell to Idris, but I'm struggling to understand how exactly am I supposed to enforce what seems to be a simple boolean test inside the data structure of a tree. Also,I'm not sure it'll make a difference but I'm using Idris 1.

You really should be using Idris 2, it's much more stable and reliable, Idris 1 is unsupported.

For starters, I'm trying to do something like I was able to do following the Liquid Haskell tutorial, where with refinement types I can enforce the ordering of a binary search tree inside the data structure with simple boolean conditions. A working code can be found here: https://github.com/LucasTornai/pgc-ufabc/blob/main/haskell-structures/MyBST.hs

That being said, when trying to apply the same rules to Idris, I first seem to have fallen in a trap with "Data.So", where I couldn't manage to prove what I wanted with it.

I can see that you are using `So` datatype in the wrong way. `So x` is actually the proof that `x` is `True`. You are trying to write a function

```

mkIsLft : Ord a => (x : a) -> (l : Tree a) -> IsLft x l

```

which actually is

```

mkIsLft : Ord a => (x : a) -> (l : Tree a) -> So (moreTree x l)

```

In other words you are trying to prove that for any given type `a`, for any given ordering of `a`, for any element `x` of type `a` and for any `Tree` of type `a` this `x` is more than any elements inside the tree `l`, which is obviously does not hold.

 

Also, I'm not sure the way I'm approaching it is right, because I want the proof to be contained inside the data structure, and if you checked the Idris code I wrote

If you want a proof-carrying data structure, there are a lot of ways for doing this. I wrote some code to give you some feeling of this: https://gist.github.com/buzden/f1e2e9b2d36b0a5dd550078331352b19

Please mind that this is not a comlete thing and I didn't bother to declare some lawful extension interface for odering, I just assumed some laws for the standard `Ord` -- just for simplicity. And, of course, sorry, but the example uses Idris 2 significantly.