Proving binary_search meets a very general proposition

[briangmilnes]

I have had no success attempting to take a well proven binary_search against boolean functions, and attempting to prove it
against a very general membership predicate.

let memberp (s: seq int) (key: int) : prop = (exists i. ((0 <= i) /\ (i < length s)) ==> (index s i) = key)

[@@ expect_failure]
let rec lemma_memberp_binary_search_some (s: seq int{sorted s}) (key: int):
Lemma (requires memberp s key)
(ensures (Some? (binary_search s key)))
= ()

[@@ expect_failure]
let rec lemma_binary_search_some_memberp (s: seq int{sorted s}) (key: int):
Lemma (requires (Some? (binary_search s key)))
(ensures memberp s key)
= ()

Anyone have an examples they can recommend of proving against a membership proposition or a general proposition?

[klinvill]

There's several files in ulib that have properties that use mem, a membership function. In particular you can look at union_lemma in https://github.com/FStarLang/FStar/blob/master/ulib/FStar.OrdSetProps.fst. There's also a more comprehensive example in the tutorial that implements quicksort and proves it correct: https://www.fstar-lang.org/tutorial/book/part1/part1_quicksort.html. Both these examples use recursive lemmas which correspond to inductive proofs. I suspect you'll need to do something similar here as well. You can read a little more about proofs by induction here: https://www.fstar-lang.org/tutorial/book/part1/part1_lemmas.html.

Alternatively, could you provide a self-contained code snippet of what you're trying to prove? I (or someone else) may be able to help you identify where the proof is falling short.