ListOfPredecessors
Often one wants to do Peano-style recursion over the binary number such as positive or N. The standard library Coq.ZArith.Wf_Z includes functions natlike_rec, natlike_rec2, and natlike_rec3 for this; however these functions cannot be used to compute within Coq because they depend on opaque lemmas. Even if the lemmas were not opaque, the computation is quite slow.
Sometimes one does no care about the order one processes the numbers, such as when computing the partial sum of a sequence. With the binary numbers it seems easier to sum the points out of order. To illustrate how to do this, here are two implementations that produce a list of the first n numbers (No proof of correctness is currently provided). These examples can be easily modified to be useful in more general situations.
Fixpoint predecessorsInNHelp (cont:N -> N) (x:positive) {struct x} : list N -> list N :=
match x with
|xI x'=> (fun l => (cont (Npos (xO x')))::
((predecessorsInNHelp (fun n => cont (Ndouble n)) x')
((predecessorsInNHelp (fun n => cont (Ndouble_plus_one n)) x') l)))
|xO x'=> (fun l =>
((predecessorsInNHelp (fun n => cont (Ndouble n)) x')
((predecessorsInNHelp (fun n => cont (Ndouble_plus_one n)) x') l)))
|xH => (cons (cont N0))
end.
Definition predecessorsInN (n:positive) := predecessorsInNHelp (fun x => x) n nil.
Eval compute in predecessorsInN 10.predecessorsInN takes a positive number n and returns a list N of numbers {0, ..., n - 1}
This solution was developed by BasSpitters and RussellOconnor
Fixpoint positiveFold (A:Type) (comb:positive -> A -> A) (limit:positive)
(above:bool)
(init:A) {struct limit} : A :=
match limit with
|xI x'=>
comb xH
(positiveFold A (fun n => comb (xI n)) x' above
(positiveFold A (fun n => comb (xO n)) x' false init
))
|xO x'=>
comb xH
(positiveFold A (fun n => comb (xI n)) x' true
(positiveFold A (fun n => comb (xO n)) x' above init
))
|xH => if above then init else comb xH init
end.
Definition predecessorsInPositive (n:positive) :=
positiveFold (list positive) (@cons positive) n false nil.
Definition predecessorsInPositiveStrict (n:positive) :=
positiveFold (list positive) (@cons positive) n true nil.
Eval compute in predecessorsInPositive 10.
Eval compute in predecessorsInPositiveStrict 10.predecessorsInPositive takes a positive number n and returns a list positive of numbers {1, ..., n} predecessorsInPositiveStrict takes a positive number n and returns a list positive of numbers {1, ..., n - 1}
This solution was developed by PierreCorbineau.
Feel free to edit these routines to generalize them and make improvements and/or documentation.
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.