Тип неравенства без аргументов кардинальности - PullRequest
Новая
       11

Тип неравенства без аргументов кардинальности

3 голосов
/ 18 апреля 2020

Как я могу получить Coq, чтобы я смог доказать синтактическое c неравенство типов?

Отрицательная однолистность

Я прочитал ответ на этот вопрос , который предполагает, что если вы предполагаете однолистность, то единственный способ доказать неравенство типов - это аргументы кардинальности.

Насколько я понимаю, - если логика Кока c согласуется с однолистностью, она также должна согласовываться с отрицанием однозначности. Хотя я понимаю, что отрицание однолистности действительно означает, что некоторые изоморфные c типы не равны, я считаю, что express должно быть возможно, что no isomorphi c типы (которые не идентичны) равны.

Неравенство для конструкторов типов

Фактически, я бы хотел, чтобы Coq рассматривал типы и конструкторы типов как индуктивные определения и делал типичные inversion аргумент в стиле, чтобы сказать, что два моих совершенно разных типа не равны.

Можно ли это сделать? Это должно быть:

  1. Используется для конкретных типов, то есть без переменных типа, и поэтому
  2. Не обязательно решаемо

Это кажется мне слабым достаточно, чтобы быть последовательным.

Контекст

У меня есть полиморфное c суждение (фактически индуктивный тип с параметрами forall X : Type, x -> Prop), для которого конструкторы выбирают выбор X суждения.

Я хочу доказать, что для всех суждений для определенного выбора X (скажем, X = nat) какое-то свойство имеет место, но если я пытаюсь использовать inversion, некоторые конструкторы дают мне гипотезы типа nat = string (например). Эти гипотезы о равенстве типов появляются даже для типов с одинаковым количеством элементов, поэтому я не могу (и не хочу) приводить аргументы количества элементов для создания противоречия.

Невероятное ...

Должен ли я создать Inductive кодировку закрытого мира для типов, которые меня интересуют, и пусть это будет переменная polymorphi c приведенного выше суждения?

1 Ответ

2 голосов
/ 18 апреля 2020

Если вы хотите использовать неравенство типов, я думаю, что лучшее, что вы можете сделать, это принять аксиомы для каждой пары типов, которые вас интересуют: 

Axiom nat_not_string : nat <> string.
Axiom nat_not_pair : forall A B, nat <> A * B.
(* ... *)

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

Ваш "немыслимый" подход, пожалуй, самый удобный в этом случае, на самом деле.

(Nit: «если логика Coq c согласуется с однолистностью, она также должна согласовываться с отрицанием однолистности». Да, но только потому, что Coq не может доказать однолистность.)

...