Индуктивные типы, несущие доказательства

Question

В "Основах программного обеспечения" есть одно упражнение, которое я уже некоторое время пытаюсь решить правильно, но на самом деле я попал в тупик, пытаясь записать требуемую функцию. Вот соответствующая часть упражнения

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

• нуль,
• дважды двоичное число, или
• один более чем в два раза двоичное число.

(a) Сначала напишите индуктивное определение типа bin, соответствующего этому описанию двоичных чисел.

Наивное определение не совсем работает, потому что вы в конечном итоге можете составить термины, которые добавляют 1 к числу, к которому уже добавлен 1, или умножаете ноль на 2 без веской причины. Чтобы избежать тех, что я решил, я бы закодировал какой-то переход состояния в конструкторы, чтобы избежать их, но это немного сложно, так что это было лучшее, что я мог придумать

Inductive tag : Type := z | nz | m. (* zero | nonzero | multiply by 2 *)

Inductive bin_nat : tag -> Type :=
  (* zero *)
  | Zero : bin_nat z
  (* nonzero *)
  | One : bin_nat nz
  (* multiply by 2 -> nonzero *)
  | PlusOne : bin_nat m -> bin_nat nz
  (* nonzero | multiply by 2 -> multiply by 2 *)
  | Multiply : forall {t : tag}, (t = m \/ t = nz) -> bin_nat t -> bin_nat m.

С помощью приведенного выше представления я избегаю вопросов о терминах, которые не имеют смысла, но теперь мне приходится носить с собой доказательства всякий раз, когда я умножаю на 2. Я на самом деле понятия не имею, как использовать эти вещи в рекурсивных функциях.

Я знаю, как построить доказательства и термины, и они выглядят так

(* nonzero *)
Definition binr (t : tag) := or_intror (t = m) (eq_refl nz).
(* multiply by 2 *)
Definition binl (t : tag) := or_introl (t = nz) (eq_refl tag m).
(* some terms *)
Check Zero.
Check One.
Check (Multiply (binr _) One).
Check (Multiply (binl _) (Multiply (binr _) One)).
Check PlusOne (Multiply (binl _) (Multiply (binr _) One)).

Я также могу записать "доказательство" теоремы, что я хочу соответствовать функции, но я не знаю, как на самом деле преобразовать ее в функцию. Вот доказательство для функции преобразования

Definition binary_to_nat : forall t : tag, bin_nat t -> nat.
Proof.
intros.
einduction H as [ | | b | t proof b ].
  { exact 0. } (* Zero *)
  { exact 1. } (* One *)
  { exact (S (IHb b)). } (* PlusOne *)
  { (* Multiply *)
    edestruct t.
    cut False.
    intros F.
    case F.
    case proof.
    intros F.
    inversion F.
    intros F.
    inversion F.
    exact (2 * (IHb b)).
    exact (2 * (IHb b)).
  }
Defined.

Я знаю, что этот термин - функция, которую я хочу, потому что я могу убедиться, что получаю правильные ответы, когда вычисляю его

Section Examples.

Example a : binary_to_nat z Zero = 0.
Proof.
lazy.
trivial.
Qed.

Example b : binary_to_nat nz One = 1.
Proof.
lazy.
trivial.
Qed.

Example c : binary_to_nat m ((Multiply (binl _) (Multiply (binr _) One))) = 4.
Proof.
lazy.
trivial.
Qed.

End Examples.

Итак, наконец, вопрос: есть ли простой способ преобразовать вышеприведенный термин доказательства в реальную функцию простым способом или я должен попытаться перепроектировать термин доказательства?

Answer 1

Мне нравится ваша идея представления действительного двоичного числа с использованием состояний и индексированного индуктивного типа. Тем не менее, как показывает вопрос, с индуктивным типом можно обойтись всего тремя конструкторами: ноль, умножение на 2, умножение на 2 и добавление одного. Это означает, что единственный переход, который мы должны избежать, это умножение нуля на 2.

Inductive tag : Type := z | nz. (* zero | nonzero *)

Inductive bin_nat : tag -> Type :=
  (* zero *)
  | Zero : bin_nat z
  (* multiply by 2 *)
  | TimesTwo : bin_nat nz -> bin_nat nz
  (* multiply by 2 and add one *)
  | TimesTwoPlusOne : forall {t : tag}, bin_nat t -> bin_nat nz.

Тогда, например,

Let One := TimesTwoPlusOne Zero. (* 1 *)
Let Two := TimesTwo One. (* 10 *)
Let Three := TimesTwoPlusOne One. (* 11 *)
Let Four := TimesTwo Two. (* 100 *)

Так TimesTwo добавляет ноль в конец двоичного представления и TimesTwoPlusOne добавляет один.

Если вы хотите попробовать это сами, не смотрите дальше.

(Я бы поместил это в теги спойлера, но, очевидно, блоки кода в тегах спойлера не работают)

Увеличение двоичного числа.

Fixpoint bin_incr {t: tag} (n: bin_nat t): bin_nat nz :=
match n with
| Zero => One
| TimesTwo n' => TimesTwoPlusOne n'
| @TimesTwoPlusOne _ n' => TimesTwo (bin_incr n')
end.

Определение помощника для конвертации nat в двоичный файл

Definition nat_tag (n: nat): tag :=
match n with
| 0 => z
| S _ => nz
end.

преобразование nat в двоичный файл

Fixpoint nat_to_bin (n: nat): bin_nat (nat_tag n) :=
match n with
| 0 => Zero
| S n' => bin_incr (nat_to_bin n')
end.

Преобразование двоичного файла в nat, Обратите внимание, что здесь используются обозначения для умножения и сложения натуральных чисел. Если это не работает, возможно, у вас не открыты нужные области.

Fixpoint bin_to_nat {t: tag} (n: bin_nat t): nat :=
match n with
| Zero => 0
| TimesTwo n' => 2 * (bin_to_nat n')
| @TimesTwoPlusOne _ n' => 1 + 2 * (bin_to_nat n')
end.

Мы получаем фактические функции из этих определений (обратите внимание, что 20 - это 10100 в двоичном виде).

Compute nat_to_bin 20.
= TimesTwo
     (TimesTwo (TimesTwoPlusOne (TimesTwo (TimesTwoPlusOne Zero))))
 : bin_nat (nat_tag 20)

Compute bin_to_nat (nat_to_bin 20).
= 20
 : nat

Еще одно техническое замечание. Я использовал этот код в двух версиях Coq (8.6 и 8.9+alpha), и одна версия требовала, чтобы я вставил тег явно при сопоставлении с TimesTwoPlusOneв то время как другой позволил ему остаться неявным. Приведенный выше код должен работать в любом случае.