Replies: 1 comment
-
The following seems to work but it feels a little different in spirit to the original lemma. lemma exercise3_1b(a_i: pos -> real, N: nat)
requires Limit(a_i, 0.001)
requires positiveNat(N) && forall n :: n > N ==> converges(a_i, n, 0.001, 0.001);
ensures forall n:: n > N ==> a_i(n) >= 0.0
{
forall n | n > N
ensures a_i(n) >= 0.0
{
assert converges(a_i, n, 0.001, 0.001);
}
}
method exercise3_1m(a_i: pos -> real) returns (ghost negatives: set<nat>)
requires Limit(a_i, 0.001)
ensures forall x :: x in negatives ==> a_i(x) < 0.0;
ensures exists N: nat :: positiveNat(N) && |negatives| <= N
{
var epsilon: real := 0.001;
assert positiveReal(epsilon);
ghost var N: nat :| positiveNat(N) && forall n :: n > N ==> converges(a_i, n, epsilon, 0.001);
ghost var i: nat := 1;
negatives := {};
while i < N
invariant 0 <= i <= N
invariant forall x :: x in negatives ==> a_i(x) < 0.0;
invariant |negatives| <= i
{
if a_i(i) < 0.0 {
negatives := {i} + negatives;
}
i := i + 1;
}
assert i <= N;
assert |negatives| <= N;
} |
Beta Was this translation helpful? Give feedback.
0 replies
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
-
I have run into the issue of Dafny not being able to ascertain that a set is of finite size a few times. I was wondering if there is some approach which the community has adopted to get around this issue or if some new feature in Dafny would be required?
Here is one example I ran into recently. I was playing around with verifying some real analysis proofs of sequences in Dafny.
Situation 1:
As far as I can tell, this statement just can't be proven inside of Dafny.
Situation 2:
Even though for a given Tree instance the setOfTreePaths() should be finite albeit very large. Dafny can't infer that and there doesn't seem to be anyway to convince Dafny that it should be the case. It seems odd to me that there isn't a flag or option that would allow us to say "yes this set is large but finite" or even the ability just to convince Dafny that it is indeed finite somehow.
I'm sure it is related to the z3 implementation underneath but is there hope for a solution to this?
Beta Was this translation helpful? Give feedback.
All reactions