Coq: доказать, что индуктивный тип без рекурсивного конструктора необитаем - PullRequest
Новая
       56

Coq: доказать, что индуктивный тип без рекурсивного конструктора необитаем

2 голосов
/ 11 мая 2019

Я новичок в Coq и его основной теории. Предположим, что есть индуктивный тип, у которого нет нерекурсивных конструкторов. Невозможно представить экземпляр этого. Но можно ли это доказать? 

Inductive impossible : Type :=
  | mk (x : impossible).

Theorem indeed_impossible : forall (x : impossible), False.

Если нет - это недостаток Coq или особенность CoC?

1 Ответ

3 голосов
/ 12 мая 2019

Это легко доказать по индукции на x. Вы получаете только индуктивный шаг с гипотезой абсурдной индукции, и нет базового случая, который потребовал бы от вас на самом деле произвести абсурд. 

Theorem indeed_impossible : forall (x : impossible), False.
Proof.
  induction 1.
  (* just need to show [False |- False] *)
  trivial.
Qed.

Редактировать: @simpadjo: Альтернативное доказательство, которое лично мне более понятно: 

Theorem indeed_impossible : forall (x : impossible), False.
Proof.
 intros. induction x. assumption. Qed.
...