Open mtzguido opened 1 month ago
We briefly talked about this last week. One possible solution could be to use total functions instead. That is:
let rec bigsum (m : nat) (n : nat) (f : nat -> r) : Tot r =
if m >= n then 0 else f (n-1) + bigsum m (n-1) f
This is also what the on_range
predicate does in pulse. In practice, this is not a big restriction as you can write bigsum m n (fun i -> if m <= i && i < n then f i else 0)
instead to make any range precondition in f
type check.
Not sure I can call this a bug, but:
You would expect this lemma to be easily provable like this
However this fails ("could not prove post-condition") regardless of how much one tries to spell out the proof. Even asserting the postcondition right after the recursive call fails:
The trick is that the implicit of
pointwise_add
is being instantiated differently. In the recursive call, the domain off
is refined to be betweenm
andn-1
instead ofm
andn
, so one would expect this to work:Alas, that also fails with the same error. The reason being that F* matched the refinements of both instances of
f
and computed their meet, which is their conjunction. So, finally, this works:The errors throughout this debugging are pretty bad. But, also, I think the last failed attempt should work as the refinements are logically equivalent (which F* can prove), so the refinement types should be considered equal.
(For proving the actual lemma, I think it has to be restated like this
)