I was trying to make a function that finds the binary representation of a nat
. The binary represent being a list of nat
s 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.
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
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
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.
...
Ju-sh said:
And isn't the term
n
available during pattern matching insideEquations
? I had to useS 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.
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)
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 n
.
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
.
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
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.
Ju-sh has marked this topic as resolved.
Thanks.
Last updated: Oct 13 2024 at 01:02 UTC