Missing hypothesis when splitting a formula with if-then-else and by
Consider the following code :
use int.Int
use seq.Seq
let function dirac (a b : int) =
if b = a then 1 else 0
let rec function count (x : int) (seq : seq int)
variant { Seq.length seq }
=
if Seq.length seq = 0
then 0
else dirac x seq[0] + count x seq[1..]
lemma count_case :
forall x h, t : seq int.
(if x = h
then (count x (cons h t) = count x t + 1
by dirac x h = 1)
else (count x (cons h t) = count x t
by dirac x h = 0))
by (cons h t)[1..] == t
When trying to prove the generated VCs (after split_vc) corresponding to the if-branches in the lemma,
the hypothesis (cons h t)[1..] == t
is missing from the context. This makes the solvers fail to prove
the VCs directly (at least on my machine, giving them a reasonable delay).