Откуда мы знаем, что все конструкторы Coq инъективны и не пересекаются?

Согласно этому курсу все конструкторы (для индуктивных типов) являются инъективными и дизъюнктными:

... Подобные принципы применимы ко всем индуктивно определенным типам: все конструкторы являются инъективными, а значения, построенные из различных конструкторов, никогда не равны. Для списков конструктор cons является инъективным, и nil отличается от любого непустого списка. Для логических значений true и false не равны.

(И inversion тактика, основанная на этом предположении)

Мне просто интересно, откуда мы знаем, что это предположение верно?

Откуда мы знаем, что, например, мы не можем определить натуральные числа на основе

1) Преемник и, возможно, конструктор типа "Double", например:

Inductive num: Type :=
   | O : num
   | S : num -> num
   | D : num -> num.

а также

2) некоторые plus функционировать так, чтобы одно число 2 может быть достигнуто через две разные последовательности / маршруты конструкторов, S (S O) а также D (S O)?

Какой механизм в Coq гарантирует, что вышеописанное никогда не произойдет?

PS Я не предлагаю выше num пример возможен. Мне просто интересно, что делает это невозможным.

Спасибо

Источник

2 ответа

Решение

Когда вы определяете индуктивный тип данных в Coq, вы по существу определяете тип дерева. Каждый конструктор дает вид узла, который может встречаться в вашем дереве, а его аргументы определяют дочерние элементы и элементы, которые этот узел может иметь. Наконец, функции, определенные на индуктивных типах (с match пункт) может проверить конструкторы, которые были использованы для создания значения этого типапроизвольным образом. Это делает конструкторы Coq очень отличными от конструкторов, которые вы видите, например, в языке OO. Конструктор объекта реализован как обычная функция, которая инициализирует значение заданного типа; Конструкторы Coq, с другой стороны, перечисляют возможные значения, которые допускает представление нашего типа. Чтобы лучше понять эту разницу, мы можем сравнить различные функции, которые мы можем определить для объекта на традиционном ОО-языке и для элемента индуктивного типа в Coq. Давайте использовать ваш num введите в качестве примера. Вот объектно-ориентированное определение:

class Num {
    int val;

    private Num(int v) {
        this.val = v;
    }

    /* These are the three "constructors", even though they
       wouldn't correspond to what is called a "constructor" in
       Java, for instance */

    public static zero() {
        return new Num(0);
    }

    public static succ(Num n) {
        return new Num(n.val + 1);
    }

    public static doub(Num n) {
        return new Num(2 * n.val);
    }
}

И вот определение в Coq:

Inductive num : Type :=
| zero : num
| succ : num -> num
| doub : num -> num.

В примере ОО, когда мы пишем функцию, которая принимает Numаргумент, нет никакого способа узнать, какой "конструктор" был использован для создания этого значения, потому что эта информация не хранится вval поле. Особенно Num.doub(Num.succ(Num.zero())) а такжеNum.succ(Num.succ(Num.zero())) были бы равные значения.

В примере Coq, с другой стороны, все меняется, потому что мы можем определить, какой конструктор использовался для формирования num ценность, благодаря match заявление. Например, используя строки Coq, мы могли бы написать такую ​​функцию:

Require Import Coq.Strings.String.

Open Scope string_scope.

Definition cons_name (n : num) : string :=
  match n with
  | zero   => "zero"
  | succ _ => "succ"
  | doub _ => "doub"
  end.

В частности, даже если ваше предполагаемое значение для конструкторов подразумевает, что succ (succ zero) а также doub (succ zero) должны быть "морально" равны, мы можем различить их, применяя cons_nameФункция для них:

Compute cons_name (doub (succ zero)). (* ==> "doub" *)
Compute cons_name (succ (succ zero)). (* ==> "succ" *)

На самом деле, мы можем использовать match различать succа также doub произвольно:

match n with
| zero   => false
| succ _ => false
| doub _ => true
end

Сейчас, a = b в Coq означает, что нет никакого способа, которым мы можем различить a а также b, Приведенные выше примеры показывают, почему doub (succ zero) а также succ (succ zero) не может быть равным, потому что мы можем писать функции, которые не учитывают смысл, который мы имели в виду, когда писали этот тип.

Это объясняет, почему конструкторы не пересекаются. То, что они инъективны, на самом деле также является следствием сопоставления с образцом. Например, предположим, что мы хотели доказать следующее утверждение:

forall n m, succ n = succ m -> n = m

Мы можем начать доказательство с

intros n m H.

Ведет нас к

n, m : num
H : succ n = succ m
===============================
n = m

Обратите внимание, что эта цель по упрощению эквивалентна

n, m : num
H : succ n = succ m
===============================
match succ n with
| succ n' => n' = m
| _       => True
end

Если мы делаем rewrite H, мы получаем

n, m : num
H : succ n = succ m
===============================
match succ m with
| succ n' => n' = m
| _       => True
end

что упрощает до

n, m : num
H : succ n = succ m
===============================
m = m

На этом мы можем заключить с рефлексивностью. Этот метод является довольно общим, и на самом деле в основе того, что inversion делает.

Источник

Там нет ни одного: конструкторы O, S а также D действительно непересекающиеся и инъективные, но семантика для nums у вас в голове не является, как функция, инъекционным.

Поэтому num обычно считается плохим представлением натуральных чисел: работа до эквивалентности довольно раздражает.

Источник
Другие вопросы по тегам