Команды #define и #postulate

Команды #define и #postulate используются для введения определений и аксиом.

Синтаксис

#define <name> [uses (<vars>)] (<param>)* : <type> := <term>
#define <name> [uses (<vars>)] : <type> := <term>

#postulate <name> [uses (<vars>)] (<param>)* : <type>
#postulate <name> [uses (<vars>)] : <type>

Описание

#define

Команда #define вводит определение, связывая имя с термом заданного типа. Проверщик типов проверяет, что терм имеет указанный тип.

Аннотация uses (<vars>) явно указывает переменные, которые неявно используются в типе или определении (см. Секции и переменные для более подробной информации). Если таких переменных нет, аннотация опускается.

#postulate

Команда #postulate вводит аксиому (постулат) без предоставления определения. Это полезно, когда вы хотите предположить существование чего-то без доказательства.

Как и #define, аннотация uses (<vars>) указывает неявные переменные (используемые в типе постулированной аксиомы), если таковые имеются.

Пример

#lang rzk-1
-- Определить функцию
#define id (A : U)
  : A → A
  := \ x → x

-- Определить константу
#define unit-value
  : Unit
  := unit

-- Постулировать тип
#postulate Void
  : U

-- Постулировать аксиому (например, исключение двойного отрицания)
#postulate DNE (A : U)
  : ( ( ( A → Void) → Void) → A)

-- Постулировать с неявными предположениями
#variables A B : U
#variable f : B → A
#variable g : A → B

-- обратите внимание, что B используется неявно в этом постулате, поэтому uses (B)
#postulate f_f_is_id uses (B)
  ( x : A)
  : f (g x) = id A x

Примечания

• #def — это краткая версия команды #define
• Обе команды поддерживают параметры, которые можно использовать для создания функций
• rzk проверяет, что термы #define имеют правильные типы
• #postulate не требует терма, так как вводит предположение без доказательства