This function is obviously terminating, i.e. has decreasing parameter n
:
Program Fixpoint is_upper (n : nat)
{measure (n)} : bool :=
if Init.Nat.ltb n 256
then if Init.Nat.ltb n 65
then false
else if Init.Nat.ltb n 91 then true
else false
else is_upper (n / 256).
Next Obligation. (* ...*)
I have two orthogonal questions about this example:
What should measure be in this case?
If n
is specified, then the following hypothesis appears:
is_upper : forall n0 : nat, n0 < n -> bool
.
How to interpret that kind of (function-like) hypothesis?
That hypothesis is just the function itself, available for recursive calls on smaller inputs
as written, you have to prove that n / 256 < n
, which isn't true:
Require Import Arith Lia.
Goal not (forall n, n / 256 < n).
intros H. specialize (H 0). lia.
but one can rephrase the code so that Program
remembers that Nat.ltb n 256
is false, aka n >= 256
:
Program Fixpoint is_upper (n : nat)
{measure (n)} : bool :=
match Init.Nat.ltb n 256 with
| true =>
if Init.Nat.ltb n 65
then false
else if Init.Nat.ltb n 91 then true
else false
| false => is_upper (n / 256)
end.
Goal state:
(*
n: nat
is_upper: forall n0 : nat, n0 < n -> bool
Heq_anonymous: false = (n <? 256)
1/1
fst (Nat.divmod n 255 0 255) < n
*)
@Paolo Giarrusso thanks for the feedback :smile:
In case someone else (new to this) comes accross a similar problem here is the rest:
Next Obligation.
destruct n as [|n'].
- discriminate.
- apply (Nat.div_lt _ 256) ; lia.
Qed.
Nikola Katić has marked this topic as resolved.
Nikola Katić has marked this topic as unresolved.
Somewhat less simple example, but still on the same topic...
This is the signature (although not quite a coq-lingo, I guess :smile:) of a function I implemented:
Fixpoint eval (e : env) (x : exp) (s : state) : (result * state) :=
To prove its termination, I changed it to Program Fixpoint
in the following way:
Program Fixpoint eval (e : env) (x : exp) (s : state) {measure (clock_ s)} : (result * state) :=
I'm getting this error message, I'm not sure I understand:
Error: The term "?T@{e0:=e; x0:=x; s0:=s; e:=e0; s:=s0}" has type "Type" which is not a (co-)inductive type.
I would really like to be able to prove it that way, but is this a hopeless try for any reason?
my standard advice when coming across some problem with Fixpoint
or Program Fixpoint
: switch to Equations and explicitly pass a relation that has been proved well-founded up front.
I'm sure plenty of people disagree, but I think Fixpoint
is more like proof assistant assembly at this point. Function definition packages have been used for decades in the HOL world, but we are underusing them in the Coq community.
Thanks for your input :+1: I will definitely try Equations in future.
I'm still interested in how this is any different from self contained is_upper
example from above which worked.
Can't tell from that line only: can you post a self-contained example?
This is the minimal example I extracted from the original code.
I am suspicious of fold_left
making a difference -- is that maybe the case?
IIRC that's a good guess: Program has to add extra arguments when translaying well-founded recursion, and there are complications with higher-order functions...
Hmm okay, so switching to Equations is my last hope then :smile:
it might not _just_ a matter of switching to equations: the type of evals
is not right...
I have dealt with this problem in the past:
https://github.com/Blaisorblade/minidot/blob/e74f443429b163d63f6d7d17fc9c9497eff86ff8/ecoop17/dsubsup_total_rec_monotone.v#L210
sorry: it might _not_ just be a matter of switching to Equations (i'll fix above)
it seems back then I needed 2 things:
ensure_t_reduction s' (eval e x s')
with ensure_t_reduction s' (eval e x s' _)
— where the _
will stand for the extra argument — but that is presumably just a workaround for some Program
bug.OTOH, if you're writing a fuel-based interpreter, you can probably avoid well-founded recursion and use structural recursion on fuel : nat
?
That is exactly what I wanted to achieve - fuel approach (didn't know it had its own name).
The initial idea behind the clock
field is a counter that will help me to prove termination of eval.
I think I'll try without it then and have an extra nat
argument, as you suggested.
Thanks a lot (again) :smile:
you probably want to decrease the fuel
instead of checking that it's smaller — if needed, here's an example for STLC
https://github.com/Blaisorblade/minidot/blob/e74f443429b163d63f6d7d17fc9c9497eff86ff8/ecoop17/stlc.v#L134-L177
apologies if the code is old and messy, I'm sure better examples exist
that doesn't solve the "mapping over lists", but it should be easier with an explicit translation: for instance, I think eval (S n)
can just map/fold eval n
over that list. Anyway, I'll stop for now, but feel free to ask follow-up Qs if you get stuck!
Thanks, going back to work it out. I'll probably have a question or two.
After adding decreasing fuel
argument, everything was straightforward... Closing this topic :check:
Nikola Katić has marked this topic as resolved.
Last updated: Oct 03 2023 at 04:02 UTC