Доказательство того, что два изоморфных типа различны

Question

Учитывая эти два типа,

Inductive unit : Set := tt.
Inductive otherUnit : Set := ttt.

Может ли Coq доказать, что они разные, то есть unit <> otherUnit?

Оба являются синглтонами типа Set, поэтому нелегко найти Set -> Prop, который их отличает. Например, это даже не проверка типа

Definition singletonTT (A : Set) : Prop := forall x : A, x = tt.

потому что tt имеет тип unit вместо A.

Answer 1

На самом деле допустимо в Coq, что эти два типа равны; то есть вы не можете ни доказать, что они равны, либо различны, и логично предположить, что либо.

Вы не можете выразить singletonTT в терминах tt, потому что, как вы указали, он проверяет только тип для unit. Вместо этого вам нужно обработать A непрозрачно; например, вы можете выразить свойство быть одиноким как A /\ forall (x y:A), x = y. Конечно, оба типа являются синглетонами, поэтому это не различает их.

Если вы предполагаете Axiom unit_otherUnit : unit = otherUnit, то вы можете выразить что-то вроде singletonTT, приведя tt к otherUnit: eq_rec _ (fun S => S) tt otherUnit ax = ttt.

Когда типы имеют различную мощность (что означает, что они не изоморфны), вы можете использовать их мощность, чтобы различать их и доказать, что типы различны. Простые примеры включают False <> True и unit <> bool, а более сложный пример - nat <> (nat -> nat).