# Predecessors of Binary Numbers

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.

## Solution for N

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

## Solution for positive

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

## Future Work

Feel free to edit these routines to generalize them and make improvements and/or documentation.

##### Clone this wiki locally
You can’t perform that action at this time.
Press h to open a hovercard with more details.