Stream: Coq users

Topic: ✔ Program Fixpoint measure - simple example


view this post on Zulip 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:

view this post on Zulip Paolo Giarrusso (Aug 12 2022 at 23:25):

That hypothesis is just the function itself, available for recursive calls on smaller inputs

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Aug 12 2022 at 23:33):

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
*)

view this post on Zulip Nikola Katić (Aug 13 2022 at 10:10):

@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.

view this post on Zulip Notification Bot (Aug 13 2022 at 10:14):

Nikola Katić has marked this topic as resolved.

view this post on Zulip Notification Bot (Aug 13 2022 at 21:20):

Nikola Katić has marked this topic as unresolved.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Nikola Katić (Aug 13 2022 at 21:50):

Thanks for your input :+1: I will definitely try Equations in future.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Aug 14 2022 at 09:16):

Can't tell from that line only: can you post a self-contained example?

view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip Nikola Katić (Aug 14 2022 at 10:40):

Hmm okay, so switching to Equations is my last hope then :smile:

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Aug 14 2022 at 10:42):

sorry: it might _not_ just be a matter of switching to Equations (i'll fix above)

view this post on Zulip Paolo Giarrusso (Aug 14 2022 at 10:43):

it seems back then I needed 2 things:

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Nikola Katić (Aug 14 2022 at 10:59):

Thanks a lot (again) :smile:

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Aug 14 2022 at 11:00):

apologies if the code is old and messy, I'm sure better examples exist

view this post on Zulip 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!

view this post on Zulip Nikola Katić (Aug 14 2022 at 11:09):

Thanks, going back to work it out. I'll probably have a question or two.

view this post on Zulip Nikola Katić (Aug 14 2022 at 14:31):

After adding decreasing fuel argument, everything was straightforward... Closing this topic :check:

view this post on Zulip Notification Bot (Aug 14 2022 at 14:31):

Nikola Katić has marked this topic as resolved.


Last updated: Jun 25 2024 at 15:02 UTC