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] *)
Would a solution using the
refine tactic be better?
You need well-founded recursion, and I recommend using the support in the Equations plugin.
The reason is that
Nat.div n 2 isn't _structurally_ smaller than
n, according to the built-in order between terms and subterms.
But it is a smaller number (when n is nonzero), which is enough for well-founded recursion
Would it be too tedious to do using built-in constructs available in coq?
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.
there's also https://coq.github.io/doc/master/refman/language/coq-library.html#well-founded-recursion
@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.
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.
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
And isn't the term
n available during pattern matching inside
Equations? I had to use
S n' instead.
you need to specify the well-founded measure
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. ...
And isn't the term
navailable during pattern matching inside
Equations? I had to use
you can actually write
bin n := Nat.modulo n 2 :: bin (Nat.div n 2).
S n0 behind the scenes.
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
(I'm particularly unfamiliar with doing proofs with inequalities)
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
Yes, and then you need to prove that the recursive calls are indeed applied to arguments smaller than
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
change a tactic that is built-in coq? Or is it from the
Equations module? Couldn't find the docs for it.
How do we figure out that the goal that we needed was really
S n0 / 2 < S n0?
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.
To check whether change is built-in, you can find it here: https://coq.inria.fr/refman/coq-tacindex.html#cap-c
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.
Ju-sh has marked this topic as resolved.
Last updated: Sep 26 2023 at 11:01 UTC