Как решить задачи с неверными типами равенства в Coq?

Question

Мои сценарии проверки дают мне глупые равенства типа nat = bool или жеnat = list unit который мне нужно использовать для решения противоречивых целей.

В обычной математике это было бы тривиально. Данные наборы bool := { true, false } а такжеnat := { 0, 1, 2, ... } я знаю это true ∈ bool, но true ∉ natотсюда bool ≠ nat, В Coq я даже не знаю, как это утверждать true :̸ nat,

Вопрос

Есть ли способ показать, что эти равенства ложны? Или, может быть, это невозможно?

(Ред.: удален длинный список неудачных попыток, все еще просматриваемый в истории.)

Answer 1

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

Изоморфизм как равенство

Широко распространено мнение (и может быть даже где-то доказательство этого), что логика Кока согласуется с аксиомой о том, что изоморфные множества пропозиционально равны. Действительно, это является следствием аксиомы об однозначности от Владимира Воеводского, с которой людям сейчас так весело. Я должен сказать, что кажется очень правдоподобным, что он непротиворечив (в отсутствие типа), и что может быть построена вычислительная интерпретация, которая каким-то образом переносит значения между равными типами, вставляя любой компонент изоморфизма, необходимый в любой данный момент.

Если предположить, что такая аксиома непротиворечива, мы обнаружим, что неравенство типов в логике в том виде, в каком оно существует, может быть выполнено только путем опровержения существования изоморфизма типов. В результате ваше частичное решение, по крайней мере, в принципе, где оно находится. Перечислимость является ключом к показу неизоморфизма. Я не уверен, что статус nat = (nat -> nat) может быть, но из системы ясно, что каждый житель nat -> nat имеет нормальную форму и что существует счетное число нормальных форм: по крайней мере правдоподобно, что существуют согласованные аксиомы или принципы отражения, которые делают логику более интенсиональной и подтверждают эту гипотезу.

Автоматизация аргументов кардинальности

Я вижу два шага, которые вы могли бы предпринять, чтобы улучшить текущую ситуацию. Менее радикальный шаг заключается в улучшении вашей общей технологии для аргументации кардинальности за счет лучшего использования рефлексии. Вы идеально подходите для этого, потому что в целом вы хотите показать, что конечный набор отличается от некоторого большего набора. Предположим, у нас есть некоторое представление о DList A, список отдельных элементов A, Если вы можете построить исчерпывающий DList A и дольше DList B то можете опровергнуть A = B,

Есть прекрасное определение DList по индукции-рекурсии, но у Coq нет индукции-рекурсии. К счастью, это одно из тех определений, которое мы можем смоделировать, осторожно используя индексацию. Простите мой неформальный синтаксис, но давайте

Parameters
  A   : Set
  d   : A -> A -> bool
  dok : forall x y, d x y = true -> x = y -> False

Это d для "отличных". Если набор уже имеет разрешимое равенство, вы можете оборудовать его d очень легко. Большой набор может быть оснащен адекватным d для наших целей не так много работы. И на самом деле, это важный шаг: следуя мудрости команды SSReflect, мы пользуемся небольшим размером нашего домена, работая с bool скорее, чем Prop и заставить компьютер делать тяжелую работу.

Теперь давайте

DListBody : (A -> bool) -> Set

где индекс - тест свежести для списка

dnil  : DListBody (const true)       (* any element is fresh for the empty list *)
dsnoc : forall f, (xs : DListBody f) -> (x : A) -> is_true (f x) ->
          DListBody (fun y => f y /\ d x y)

И если вам нравится, вы можете определить DList упаковка DListBody экзистенциально. Возможно, это на самом деле скрывает информацию, которую мы хотим, потому что показывать такую ​​вещь исчерпывающе выглядит так:

Exhaustive (f : A -> bool)(mylist : DListBody f) = forall x : A, is_false (f x)

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

Тогда вам нужно только один раз привести аргумент в пользу голубя. Когда вы хотите опровергнуть равенство между типами (при условии, что у вас уже есть подходящие кандидаты для d), вы исчерпывающе перечисляете меньшее и выставляете более длинный список из большего, и все.

Работа во вселенной

Более радикальной альтернативой является вопрос, почему вы в первую очередь получаете эти цели и действительно ли они означают то, чего вы от них хотите. Какие типы должны быть на самом деле? Существует множество возможных ответов на этот вопрос, но, по крайней мере, открыто, что они в некотором смысле являются "кардиналами". Если вы хотите думать о типах как о более конкретных и синтаксических, отличных, если они построены с помощью различных конструкций, то вам может потребоваться снабдить типы более конкретным представлением, работая в юниверсе. Вы определяете индуктивный тип данных "имена" для типов вместе со средствами для декодирования имен как типов, а затем переоцениваете свою разработку в терминах имен. Вы должны обнаружить, что неравенство имен следует обычной дискриминации конструкторов.

Загвоздка в том, что вселенские конструкции могут быть немного хитрыми в Coq, опять же, потому что индукция-рекурсия не поддерживается. Это сильно зависит от того, какие типы вы должны рассмотреть. Может быть, вы можете определить индуктивно некоторые U : Set затем реализовать рекурсивный декодер T : U -> Set, Это, безусловно, правдоподобно для вселенных простых типов. Если вам нужна вселенная зависимых типов, все становится немного потеет. Вы можете по крайней мере сделать это много

U : Type   (* note that we've gone up a size *)
NAT : U
PI : forall (A : Set), (A -> U) -> U

T : U -> Set
T NAT = nat
T (PI A B) = forall (a : A), T (B a)

но обратите внимание, что домен PI не закодирован в Set, не в U, Индуктивно-рекурсивный Агданс может преодолеть это, определяя U а также T одновременно

U : Set   (* nice and small *)
NAT : U
PI : forall (A : U), (T A -> U) -> U   (* note the use of T *)

T : U -> Set
T NAT = nat
T (PI A B) = forall (a : T A), T (B a)

но у Coq этого не будет. Опять же, обходной путь заключается в использовании индексации. Здесь стоимость такова, что U неизбежно велик.

U : Set -> Type
NAT : U nat
PI : forall (A : Set)(B : A -> Set),
       U A -> (forall a, U (B a)) -> U (forall a, B a)

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

Answer 2

расширенное частичное решение

Для справки, вот мое доказательство nat = bool -> False, (Это довольно долго, но я надеюсь, что легко увидеть общую структуру этого доказательства.)

Goal nat = bool -> False.
  (* For any two types, if they are actually identical, the identity is an
     isomorphism. *)
  assert (forall (T U : Set), T = U ->
              exists (f : T -> U) (g : U -> T),
              (forall t, (g (f t)) = t) /\ (forall u, (f (g u)) = u))
          as Hiso
  by (intros T U H; rewrite H; exists (@id U); exists (@id U);
          split; intro; reflexivity).
  (* our nat = bool *)
  intro HC.
  (* combining the facts gives an iso between nat and bool *)
  pose proof (Hiso nat bool HC); clear HC Hiso.
  inversion H as [phi [phi_inv [Hl Hr]]]; clear H Hr.
  (* this breaks because ||bool|| = 2 while ||nat|| > 2 -- we get collisions *)
  assert (forall m n o,
              phi m = phi n \/ phi n = phi o \/ phi m = phi o)
   by (intros m n o;
        case (phi m); case (phi n); case (phi o); clear; tauto).
  (* building the collision for 0, 1 and 2 *)
  pose proof (H 0 1 2) as HC; clear H.
  (* (false) identity preservation for 0, 1, 2 *)
  pose proof (Hl 0) as H0; pose proof (Hl 1) as H1;
  pose proof (Hl 2) as H2; clear Hl.
  (* case analysis on phi calls yields equalities on non-equal numbers... *)
  destruct (phi 0); destruct (phi 1); destruct (phi 2);
  (* ...rewriting leads to an equality '0 = 2' or '0 = 1' or '1 = 2'... *)
  try (rewrite H2 in H0); try (rewrite H1 in H0); try (rewrite H2 in H1);
  (* ...which can be used to solve by constructor inequality *)
  try inversion H0; inversion H1.
Qed.

Как видите, это не очень удобно для больших конечных типов (даже если они автоматизированы) - термины слишком большие. Любое улучшение было бы здорово.