Как работает принцип индукции для устройства синглтонного типа в Coq? - PullRequest
Новая
       6

Как работает принцип индукции для устройства синглтонного типа в Coq?

0 голосов
/ 17 декабря 2018

Я просматривал книгу Адама Члипалы о Кок, и она определила индуктивный тип: 

Inductive unit : Set :=
  | tt.

Я пытался понять принцип его индукции: 

Check unit_ind.
(* unit_ind
     : forall P : unit -> Prop, P tt -> forall u : unit, P u *)

Я не уверенесли я понимаю, что означает вывод Coq.

1) Итак, проверка дает мне возможность взглянуть на тип «объектов», верно?Итак, unit_ind имеет тип: 

forall P : unit -> Prop, P tt -> forall u : unit, P u

Верно?

2) Как читать этот тип?У меня проблемы с пониманием, где поставить скобки или что-то ... Во-первых, перед запятой, мне не имеет смысла читать это как: 

IF "for all P of type unit" THEN " Prop "

, поскольку гипотеза не являетсядействительно что-то правда или ложь.Итак, я предполагаю, что реальный путь к реальности в первую очередь заключается в следующем: 

forall P : (unit -> Prop), ...

, так что P - это просто функция типа unit для поддержки.Это правильно?

Хотелось бы, чтобы это было правильно, но при такой интерпретации я не знаю, как прочитать часть после первой запятой: 

P tt -> forall u : unit, P u

Я бы ожидал всех количественных определенийсуществующих переменных, которые должны быть определены в начале предложения, но это не так, как это делается, поэтому я не уверен, что происходит ...

Может ли кто-нибудь помочь мне прочитать это предложение как формально, так и интуитивно?Я также хочу концептуально понять, что он пытается сказать, а не только из-за его деталей.

1 Ответ

0 голосов
/ 17 декабря 2018

Позвольте мне поставить несколько дополнительных (не очень необходимых) скобок: 

forall P : unit -> Prop, P tt -> (forall u : unit, P u)

Я бы перевел это как "Для любого предиката P над типом unit, если P содержит tt, то P содержит любой член типа unit ".

Интуитивно, поскольку tt является единственным значением типа unit, имеет смысл доказать P только дляэто уникальное значение.

Вы можете проверить, работает ли эта интуиция для вас, попытавшись интерпретировать принцип индукции для типа bool таким же образом. 

Check bool_ind.
bool_ind
     : forall P : bool -> Prop, P true -> P false -> (forall b : bool, P b)
...