Используйте coqtop, чтобы проверить тип выражения - PullRequest
Новая
       5

Используйте coqtop, чтобы проверить тип выражения

0 голосов
/ 08 января 2019

Мне любопытно, какой тип сущностей Coq эквивалентен связям в логике. Ради конкретики, скажем, -> и /\. Если -> - магическая не [первоклассная сущность], тогда давайте просто использовать /\ в качестве сущности. Мне любопытно, является ли его домен опорой или сетом.

Можно ли использовать coqtop для получения типа выражения?

Я хочу сделать что-то подобное с ghci. 

> ghci
:GHCi, version 8.6.3:  :? for help
Prelude> :t (**)
(**) :: Floating a => a -> a -> a

1 Ответ

0 голосов
/ 08 января 2019

/\ и -> являются обозначениями, а не фактическими константами в Coq. Чтобы найти их подписи, вы должны сначала определить, для чего они используются. Выполнение команды Locate "/\". должно вывести что-то вроде 

Notation
"A /\ B" := and A B : type_scope
(default interpretation)

То есть /\ это обозначение константы and. Затем вы можете использовать команду Check, чтобы найти ее тип. Check and. дает 

and
     : Prop -> Prop -> Prop

Итак, and берет два Prop с и дает Prop.

Аналогично, A -> B - это обозначение для forall _: A, B. В отличие от and, forall не является константой, а является ключевым словом на языке Coq, поэтому вы не можете использовать Check forall. для получения подписи. В этом случае вы можете обратиться к справочнику по продуктам и увидеть, что

Выражение forall ident : type, term обозначает произведение переменная ident типа type, в течение срока term. Что касается абстракций, forall сопровождается списком переплетов и продуктами более переменные эквивалентны итерации произведений с одной переменной. Обратите внимание, что term предназначен для типа.

То есть, A и B должны быть типами, что означает, что они могут быть элементами любой из вселенных Prop, Set или Type.

...