Установить изоморфизм между конечными натуральными числами и сигмой

Я бы начал с чего-то вроде

Definition eq_lt3_lt3 (x: lt3) : eq x (N3_to_lt3 (lt3_to_N3 x)).
Proof.
destruct x as [ n h ].
destruct n as [ | [ | [ | p ]]]; simpl in *.

На этом этапе у вас будут такие цели, как:

exist (fun x : nat => x < 3) 0 h = exist (fun x : nat => x < 3) 0 l_0_3

По сути, единственная разница теперь состоит в том, что у вас есть «некоторое доказательство того, что 0‹ 3 с именем h »слева и« Ваше точное доказательство того, что 0 ‹3 с именем l_0_3» с правой стороны.

Таким образом, вам придется искать в направлении доказательства несоответствия / уникальности удостоверений личности (что можно доказать с помощью nat & lt).

Вы также можете повеселиться, если воспользуетесь механизмом finType в math-comp.

Например, вы можете использовать перечисление ординалов [изоморфных вашему типу], чтобы доказать свою лемму, перечислив все значения вместо громоздких случаев:

From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Lemma falseP T : false -> T.
Proof. by []. Qed.

Inductive N3 := zero | one | two.

Definition lt3_to_N3 (n: 'I_3) : N3 :=
  match n with
  | Ordinal 0 _ => zero
  | Ordinal 1 _ => one
  | Ordinal 2 _ => two
  | Ordinal _ f => falseP _ f
  end.

Definition N3_to_lt3 (n: N3) : 'I_3 :=
  match n with
  | zero => @Ordinal 3 0 erefl
  | one  => @Ordinal 3 1 erefl
  | two  => @Ordinal 3 2 erefl
  end.

Lemma eq_lt3_lt3 : cancel lt3_to_N3 N3_to_lt3.
Proof.
apply/eqfunP; rewrite /FiniteQuant.quant0b /= /pred0b cardE /enum_mem.
by rewrite unlock /= /ord_enum /= !insubT.
Qed.

(* We can define an auxiliary lemma to make our proofs cleaner *)
Lemma all_by_enum (T : finType) (P : pred T) :
  [forall x, P x] = all P (enum T).
Proof.
apply/pred0P/allP => /= H x; first by have/negbFE := H x.
suff Hx : x \in enum T by exact/negbF/H.
by rewrite mem_enum.
Qed.

Lemma eq_lt3_lt3' : cancel lt3_to_N3 N3_to_lt3.
Proof.
by apply/eqfunP; rewrite all_by_enum enumT unlock /= /ord_enum /= !insubT.
Qed.

Как видите, текущий дизайн math-comp не очень хорошо подходит для этой работы, но, тем не менее, интересно познакомиться с библиотекой побольше.

Еще одно интересное упражнение - определить экземпляр finType для вашего пользовательского типа данных, а затем установить, что оба набора имеют одинаковую мощность! Есть много комбинаций лемм, которые можно попробовать здесь, так что вам будет весело!

Поскольку вы используете ssreflect, самый простой способ - использовать вычислительное определение < (в ssrnat), а затем применить лемму val_inj:

From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.

Inductive N3 := zero | one | two.

Definition less_than_3 := {x| x < 3}.

Definition lt3_to_N3 (n: less_than_3) : N3 :=
match n with
  | exist 0 _ => zero
  | exist 1 _ => one
  | exist 2 _ => two
  | exist _ _ => two
end.

Definition N3_to_lt3 (n: N3) : less_than_3 :=
match n with
  | zero => exist _ 0 erefl
  | one => exist _ 1 erefl
  | two => exist _ 2 erefl
end.

Lemma eq_lt3_lt3 (x: less_than_3) : eq x (N3_to_lt3 (lt3_to_N3 x)).
Proof.
by apply: val_inj; case: x => [[| [|[|x]]] Px].
Qed.

Оператор val_inj немного сложен, но основная идея проста: для любого логического предиката P типа T каноническая проекция { x : T | P x = true } -> T инъективна. Как выразился Винц, это полагается на то, что логические равенства не имеют отношения к доказательству; то есть любые два доказательства равенства между логическими значениями сами равны. По этой причине равенство на {x | P x = true} полностью определяется элементом x; компонент доказательства не имеет значения.