Когда конструкторы индуктивного типа являются исчерпывающими?

Question

Для простого индуктивного типа, такого как натуральные числа nat, легко доказать, что два конструктора (ноль и преемник) дают все возможные натуральные числа,

Lemma nat_destruct (n : nat) : n = O \/ exists m : nat, n = S m.
Proof.
  destruct n. left. reflexivity. right. exists n. reflexivity.
Qed.

Однако я слышал, что этоне все так просто для доказательства равенства.Существует только один конструктор равенства, eq_refl, но Coq не может доказать, что

eq_destruct : forall (A : Type) (x : A) (prEq : x = x), prEq = eq_refl

Что именно блокирует это доказательство?Вероятно, первая проблема заключается в том, что равенство - это не просто тип, а семейство типов eq : forall A : Type, A -> A -> Prop.Есть ли семейство более простых типов, где такое доказательство невозможно?С 1 или 2 аргументами вместо 3, может быть?

Answer 1

Я написал об этой проблеме в сообщении в блоге . В общем, это возникает, когда вы определяете семейство типов над типом, который не имеет разрешимого равенства. Например, рассмотрим следующий тип:

Inductive foo : Type -> Type :=
| Foo : foo unit.

Невозможно показать (я почти уверен), что каждый житель foo unit имеет форму Foo.

Это явление легче увидеть на уровне проверочных терминов. Когда вы уничтожаете член такой семьи, вы должны обобщить индекс семьи. Вы можете связать этот индекс только с известной формой, такой как unit, если тип имеет разрешимое равенство.