AVL Tree Case Study

[Michael Misamore]

Hi all,

Running into some trouble following the AVL tree case study. The SMT solver doesn't want to accept this definition:

-- This definition from the tutorial doesn't pass the SMT solver:
{-@ balL0 :: x:a
          -> l:{AVLL a x | noHeavy l}
          -> r:{AVLR a x | leftBig l r}
          -> AVLN a {realHeight l + 1}
@-}
balL0 v (Node lv ll lr _) r = mkNode lv ll (mkNode v lr r)

where "mkNode" is my version of "node". I've iterated on Lemmas to try to make this pass for about 6 hrs now without success, so I need another set of eyes. It's possible I'm just missing a postcondition somewhere.

https://github.com/mmisamore/liquidhaskell-examples/blob/f5de0280cc47e853bfb82a65d4ec0cf986c3ce6c/src/12%20AVL%20Trees.hs#L124

Thanks in advance,
Mike

[Ranjit Jhala]

Hi Michael,

Sorry about that! In brief, the issue was that there

are MULTIPLE definitions of height -- `realHeight` and

`getHeight` you need to tell LH that they are "equivalent".

Now, in reality, you HAVE told LH they are equivalent, with

the spec:

  {-@ getHeight :: t:AVL a -> {v:Nat | v = realHeight t} @-}

 

which _should_ generate the internal "invariant"

  {-@ invariant {v: AVL a | getHeight v == realHeight v} @-}

but which, for some reason is _not_ doing so. (This is a bug in LH, that I will look into.)

For now, you can make progress by adding the above `invariant` line.

Sorry about this bug; will look into it ASAP!

- Ranjit.

--
You received this message because you are subscribed to the Google Groups "liquidhaskell" group.
To unsubscribe from this group and stop receiving emails from it, send an email to liquidhaskell+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Michael Misamore]

The workaround works with my code. Thanks very much for the prompt response! I thought I was going mad :-) On the bright side I got pretty good at writing Lemmas in the process.

Cheers,
Michael

To unsubscribe from this group and stop receiving emails from it, send an email to liquidhaskel...@googlegroups.com.