## Stream: Coq users

### Topic: ✔ Program Fixpoint measure - simple example

#### 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. (* ...*)
``````

• 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.
``````

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

#### 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.
``````

#### Notification Bot (Aug 13 2022 at 10:14):

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:

#### 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:

• types of higher order functions needed to be explicitly carry around proofs that inputs were smaller than some bound.
• you might also need to replace `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

#### 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: Jun 25 2024 at 15:02 UTC