coq Basics: bin_to_nat function

Question

I am passing Logical Foundations course and became stuck upon the last excersize of Basics:

Having binary number write a converter to it's unary representation:

Inductive bin : Type :=
  | Z
  | A (n : bin)
  | B (n : bin).

Fixpoint bin_to_nat (m:bin) : nat :=
  (* What to do here? *)

I solved the problem with a recursive function in C. The only thing, I used "0" istead of "A" and "1" instead of "B".

#include <stdio.h>

unsigned int pow2(unsigned int power)
{
    if(power != 0)
        return 2 << (power - 1);
    else
        return 1;
}

void rec_converter(char str[], size_t i)
{
    if(str[i] == 'Z')
        printf("%c", 'Z');
    else if(str[i] == '0')
        rec_converter(str, ++i);
    else if(str[i] == '1')
    {
        unsigned int n = pow2(i);

        for (size_t j = 0; j < n; j++)
        {
            printf("%c", 'S');
        }
        rec_converter(str, ++i);
    }
}

int main(void)
{
    char str[] = "11Z";

    rec_converter(str, 0);
    printf("\n");

    return 0;
}

My problem now is how to write this code in coq:

unsigned int n = pow2(i);

for (size_t j = 0; j < n; j++)
{
    printf("%c", 'S');
}
rec_converter(str, ++i);

SCappella · Accepted Answer · 2019-01-24T02:56:23.380

The main difference between your code and the Coq code is that the Coq code ought to return the natural number, rather than printing it. That means we'll need to keep track of everything that your solution printed and return the result all at once.

Since printing an S means that the answer is the successor of whatever else is printed, we'll need a function that can take the 2^(n)th successor of a natural number. There are various ways to do this, but I'd suggest recursion on n and noting that the 2^(n + 1)th successor of x is the 2^(n)th successor of the 2^(n)th successor of x.

That should be enough to get what you want.

unsigned int n = pow2(i);

for (size_t j = 0; j < n; j++)
{
    printf("%c", 'S');
}
rec_converter(str, ++i);

can be written (in pseudo-Coq) as

pow2_succ i (rec_converter str (S i)).

However, one other thing to note: you may not be able to directly access the ith "character" of the input, but this shouldn't be a problem. When you write your function as a Fixpoint

Fixpoint rec_converter (n: bin) (i: nat): nat :=
match n with
| Z => 0
| A m => ...
| B m => ...
end.

the first "character" of m will be the second "character" of the original input. So you'll just need to access the first "character", which is exactly what a Fixpoint does.

It is too bad that this answer basically gives the answer to an S.F. exercise. — Yves, Jan 22 '19 at 08:03
Yes, Software Foundations explicitly request _[Please do not post solutions to the exercises in a public place.](https://softwarefoundations.cis.upenn.edu/lf-current/Preface.html#lab10)_ — larsr, Jan 23 '19 at 12:10
@Yves (and larsr) I've edited that part out. Though I'll note that that link is directed at "readers" and I've never read any of Software Foundation's material. I based my approach on the Coq standard library. — SCappella, Jan 24 '19 at 03:01
@user. Great, your answer now incorporates the explanation I was trying to add. I will delete my answer. Thanks! — Yves, Jan 24 '19 at 07:15

score 2 · Answer 2 · answered Jan 24 '19 at 09:11

For the question on computing powers of 2, you should look at the following file, provided in the Coq libraries (at least up to version 8.9):

https://coq.inria.fr/distrib/current/stdlib/Coq.Init.Nat.html

This file contains a host of functions around the natural numbers, they could all be used as illustrations about how to program with Coq and this datatype.

score 0 · Answer 3 · answered Mar 26 '20 at 16:27

0

Fixpoint bin_to_nat (m:bin) : nat :=
  match m with
  | Z => O
  | A n =>2 * (bin_to_nat n)
  | B n =>2 * (bin_to_nat n) + 1
  end.

see: coq art's 2004. P167-P168. ( How to understand 'positive' type in Coq)

answered Mar 26 '20 at 16:27

user13130175

1

coq Basics: bin_to_nat function

3 Answers3