Stream: Coq users

Topic: ✔ Making well-formed recursion for a function


view this post on Zulip Julin S (Nov 25 2021 at 09:02):

I was trying to make a function that finds the binary representation of a nat. The binary represent being a list of nats whose every element is either a 0 or a 1. The MSB of the binary representation is the last element of the list.

This is what I tried:

Fixpoint bin (n : nat) : list nat :=
  match n with
  | O => []%list
  | S n' => Nat.modulo n 2 :: bin (Nat.div n 2)
  end.

got error saying primitive recursion couldn't be figured out:

Recursive definition of bin is ill-formed.
In environment
bin : nat -> list nat
n : nat
n' : nat
Recursive call to bin has principal argument equal to
"Nat.div n 2" instead of "n'".
Recursive definition is:
"fun n : nat => if n is 0 then [] else Nat.modulo n 2 :: bin (Nat.div n 2)".

How can I make the recursion well formed?

Result that I was aiming at was like:

bin 4.  (* [0; 0; 1] *)
bin 10.  (* [0; 1; 0; 1] *)

view this post on Zulip Julin S (Nov 25 2021 at 09:03):

Would a solution using the refine tactic be better?

view this post on Zulip Paolo Giarrusso (Nov 25 2021 at 09:32):

You need well-founded recursion, and I recommend using the support in the Equations plugin.

view this post on Zulip Paolo Giarrusso (Nov 25 2021 at 09:33):

The reason is that Nat.div n 2 isn't _structurally_ smaller than n, according to the built-in order between terms and subterms.

view this post on Zulip Paolo Giarrusso (Nov 25 2021 at 09:34):

But it is a smaller number (when n is nonzero), which is enough for well-founded recursion

view this post on Zulip Julin S (Nov 25 2021 at 09:49):

Would it be too tedious to do using built-in constructs available in coq?

view this post on Zulip Karl Palmskog (Nov 25 2021 at 09:55):

the "built-in constructs" are generally more verbose than Equations, and they typically have the same status (implemented using the OCaml interface to Coq). And Equations may become "built-in" in the not-too-distant future. Since Equations is part of the Coq Platform, it will generally be available for Coq releases going forward.

view this post on Zulip Gaëtan Gilbert (Nov 25 2021 at 10:03):

there's also https://coq.github.io/doc/master/refman/language/coq-library.html#well-founded-recursion

view this post on Zulip Paolo Giarrusso (Nov 25 2021 at 12:27):

@Ju-sh it's tedious, error-prone, and you'd have to relearn various tricks used by the implementation. At the very least, you do _not_ want to allow simpl or even unfold to reduce a well-founded definition.

view this post on Zulip Paolo Giarrusso (Nov 25 2021 at 12:29):

what you want to get is a fully opaque function which satisfies your defining equations — bin 0 = [] and bin n@(S _) = Nat.modulo n 2 :: bin (Nat.div n 2); that's what Equations will produce.

view this post on Zulip Julin S (Nov 25 2021 at 15:33):

Thanks folks.

I tried

From Equations Require Import Equations.

Equations bin (n : nat) : list nat :=
bin O := List.nil;
bin (S n') := Nat.modulo (S n') 2 :: bin (Nat.div (S n') 2).

but again ran into the error:

Recursive definition of bin is ill-formed.
In environment
bin : nat -> list nat
n : nat
n0 : nat
Recursive call to bin has principal argument equal to
"Nat.div (S n0) 2" instead of "n0".
Recursive definition is:
"fun n : nat =>
 match n with
 | 0 => Datatypes.nil
 | S n0 => (Nat.modulo (S n0) 2 :: bin (Nat.div (S n0) 2))%list
 end".

How can I fix this?

This is my first foray into the equations module. :D

view this post on Zulip Julin S (Nov 25 2021 at 15:34):

And isn't the term n available during pattern matching inside Equations? I had to use S n' instead.

view this post on Zulip Alexander Gryzlov (Nov 25 2021 at 15:43):

you need to specify the well-founded measure

view this post on Zulip Alexander Gryzlov (Nov 25 2021 at 15:43):

e.g.

Equations bin (n : nat) : list nat by wf n lt :=
bin O := List.nil;
bin (S n') := Nat.modulo (S n') 2 :: bin (Nat.div (S n') 2).
Next Obligation.
...

view this post on Zulip Alexander Gryzlov (Nov 25 2021 at 15:44):

Ju-sh said:

And isn't the term n available during pattern matching inside Equations? I had to use S n' instead.

you can actually write
bin n := Nat.modulo n 2 :: bin (Nat.div n 2).
it'll expand n to S n0 behind the scenes.

view this post on Zulip Julin S (Nov 25 2021 at 16:16):

How can I solve off the obligation?

The goal becomes:

1 subgoal

n0 : nat
bin : forall x : nat, x < S n0 -> list nat

========================= (1 / 1)

fst (Nat.divmod n0 1 0 0) < S n0

But I couldn't figure how to dispose of it. Tried random tactics (like lia, simpl, etc).

(I'm particularly unfamiliar with doing proofs with inequalities)

view this post on Zulip Julin S (Nov 25 2021 at 16:18):

And what does the by wf n lt signify in Equations bin (n : nat) : list nat by wf n lt?

Is it a way of telling coq the recursion is well-founded on n by <?

view this post on Zulip Li-yao (Nov 25 2021 at 16:24):

Yes, and then you need to prove that the recursive calls are indeed applied to arguments smaller than n.

view this post on Zulip Li-yao (Nov 25 2021 at 16:30):

The goal is too simplified here, it's really S n0 / 2 < S n0 (which you can get back by change (S n0 / 2 < S n0)) and a good lemma to apply then is Nat.div_lt.

view this post on Zulip Julin S (Nov 26 2021 at 05:46):

Is change a tactic that is built-in coq? Or is it from the Equations module? Couldn't find the docs for it.

view this post on Zulip Julin S (Nov 26 2021 at 05:47):

How do we figure out that the goal that we needed was really S n0 / 2 < S n0?

view this post on Zulip Julin S (Nov 26 2021 at 05:48):

It worked perfect. But I was curious as to how the solution was figured out.

Equations bin (n : nat) : list nat by wf n lt :=
bin O := List.nil;
bin n := Nat.modulo n 2 :: bin (Nat.div n 2).
Next Obligation.
  change (S n0 / 2 < S n0).
  apply Nat.div_lt; lia.
Qed.

view this post on Zulip Paolo Giarrusso (Nov 26 2021 at 07:40):

To check whether change is built-in, you can find it here: https://coq.inria.fr/refman/coq-tacindex.html#cap-c

view this post on Zulip Paolo Giarrusso (Nov 26 2021 at 08:02):

Regarding S n0 / 2 < S n0, that asserts the input of bin (Nat.div n 2) is smaller (via <) than the input to bin n: the input of the recursive call is smaller than the input to the original call. I assume n0 comes up because n expands to S n0 as @Alexander Gryzlov mentioned.

view this post on Zulip Notification Bot (Nov 27 2021 at 06:04):

Ju-sh has marked this topic as resolved.

view this post on Zulip Julin S (Nov 27 2021 at 06:04):

Thanks.


Last updated: Feb 01 2023 at 11:04 UTC