Основы coq: функция bin_to_nat

Основное различие между вашим кодом и кодом Coq состоит в том, что код Coq должен возвращать натуральное число, а не печатать его. Это означает, что нам нужно отслеживать все, что печатало ваше решение, и возвращать результат сразу.

Поскольку печать S означает, что ответ является преемником того, что еще печатается, нам понадобится функция, которая может взять 2 ^ (n) -й преемник натурального числа. Есть разные способы сделать это, но я бы предложил рекурсию по n и отметить, что 2 ^ (n + 1) -й преемник x является 2 ^ (n) -ым преемником 2 ^ (n) -го преемника х.

Этого должно быть достаточно, чтобы получить то, что вы хотите.

unsigned int n = pow2(i);

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

можно записать (в псевдококке) как

pow2_succ i (rec_converter str (S i)).

Однако следует отметить еще одну вещь: вы не сможете получить прямой доступ к i-му «символу» ввода, но это не должно быть проблемой. Когда вы пишете свою функцию как Fixpoint

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

, первый «символ» из m будет вторым «символом» исходного ввода. Так что вам просто нужно получить доступ к первому «персонажу», что и делает Fixpoint.

Что касается вопроса о вычислительных мощностях 2, вам следует обратиться к следующему файлу, предоставленному в библиотеках Coq (по крайней мере, до версии 8.9):

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

Этот файл содержит множество функций вокруг натуральных чисел, все они могут использоваться в качестве иллюстраций о том, как программировать с помощью Coq. и этот тип данных.