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

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.

С приведенным выше представлением Iизбегайте вопросов о терминах, которые не имеют смысла, но теперь я должен иметь при себе доказательства всякий раз, когда умножаю на 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, в то время как другая позволяла ему оставаться неявным.Приведенный выше код должен работать в любом случае.