Nikola Katić (Aug 12 2022 at 22:51): Nikola Katić (Aug 12 2022 at 22:51):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?
Paolo Giarrusso (Aug 12 2022 at 23:25):That hypothesis is just the function itself, available for recursive calls on smaller inputs
Paolo Giarrusso (Aug 12 2022 at 23:32):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.
Notification Bot (Aug 13 2022 at 21:20):Nikola Katić has marked this topic as unresolved.
Nikola Katić (Aug 13 2022 at 21:20):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?
Karl Palmskog (Aug 13 2022 at 21:24):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.
Karl Palmskog (Aug 13 2022 at 21:29):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.
Nikola Katić (Aug 13 2022 at 21:50):Thanks for your input :+1: I will definitely try Equations in future.
Nikola Katić (Aug 13 2022 at 21:51):I'm still interested in how this is any different from self contained is_upper example from above which worked.
Paolo Giarrusso (Aug 14 2022 at 09:16):Can't tell from that line only: can you post a self-contained example?
Nikola Katić (Aug 14 2022 at 10:24):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?
Paolo Giarrusso (Aug 14 2022 at 10:33):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...
Nikola Katić (Aug 14 2022 at 10:40):Hmm okay, so switching to Equations is my last hope then :smile:
Paolo Giarrusso (Aug 14 2022 at 10:41):it might not _just_ a matter of switching to equations: the type of evals is not right...
Paolo Giarrusso (Aug 14 2022 at 10:41):I have dealt with this problem in the past:
https://github.com/Blaisorblade/minidot/blob/e74f443429b163d63f6d7d17fc9c9497eff86ff8/ecoop17/dsubsup_total_rec_monotone.v#L210
Paolo Giarrusso (Aug 14 2022 at 10:42):sorry: it might _not_ just be a matter of switching to Equations (i'll fix above)
Paolo Giarrusso (Aug 14 2022 at 10:43):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. Paolo Giarrusso (Aug 14 2022 at 10:48):OTOH, if you're writing a fuel-based interpreter, you can probably avoid well-founded recursion and use structural recursion on fuel : nat?
Nikola Katić (Aug 14 2022 at 10:58):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.
Nikola Katić (Aug 14 2022 at 10:59):Thanks a lot (again) :smile:
Paolo Giarrusso (Aug 14 2022 at 10:59):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
Paolo Giarrusso (Aug 14 2022 at 11:00):apologies if the code is old and messy, I'm sure better examples exist
Paolo Giarrusso (Aug 14 2022 at 11:02):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!
Nikola Katić (Aug 14 2022 at 11:09):Thanks, going back to work it out. I'll probably have a question or two.
Nikola Katić (Aug 14 2022 at 14:31):After adding decreasing fuel argument, everything was straightforward... Closing this topic :check:
Notification Bot (Aug 14 2022 at 14:31):Nikola Katić has marked this topic as resolved.
Last updated: Oct 03 2023 at 04:02 UTC