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

Question

Я здесь с Coq изучаю отношения между двумя типами, которые я определил. Первый является чем-то вроде конечного подмножества natвсего тремя элементами:

Inductive N3 := zero | one | two.

Второй тип сигма с элементами, удовлетворяющими предложению {x: nat | x < 3}, Вот его определение:

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 l_0_3
  | one => exist _ 1 l_1_3
  | two => exist _ 2 l_2_3
end.

куда l_0_3, l_1_3, а также l_2_3 это просто аксиомы:

Axiom l_0_3 : 0 < 3.
Axiom l_1_3 : 1 < 3.
Axiom l_2_3 : 2 < 3.

Мне удалось определить первую часть изоморфизма

Definition eq_n3_n3 (n: N3) : lt3_to_N3 (N3_to_lt3 n) = n.
Proof.
by case n.
Defined.

Но я не могу определить другую сторону. Вот что я сделал до сих пор:

Definition eq_lt3_lt3 (x: less_than_3) : eq x (N3_to_lt3 (lt3_to_N3 x)).
Proof.
case: x.
move=> n p.
simpl.
???

Я совсем не уверен насчет остальной части определения. Я также пытался сопоставить с шаблоном x и на (N3_to_lt3 (lt3_to_N3 x)), но я не уверен, что вернуть.

Definition eq_lt3_lt3 (x: less_than_3) : eq x (N3_to_lt3 (lt3_to_N3 x)) :=
match N3_to_lt3 (lt3_to_N3 x) with
  | x => ???
end.

Спасибо за помощь.

Answer 1

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

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

По сути, теперь единственное отличие состоит в том, что у вас есть "некоторое доказательство того, что h"на левой стороне и" Ваше точное доказательство того, что 0 < 3 назван l_0_3"на правой стороне.

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

Answer 2

Вы также можете повеселиться, если воспользуетесь техникой 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 экземпляр для вашего пользовательского типа данных, а затем убедитесь, что оба набора имеют одинаковую мощность! Здесь есть много комбинаций лемм, чтобы вы могли повеселиться!

Answer 3

Поскольку вы используете 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; компонент доказательства не имеет значения.