3

我在这里和 Coq 一起研究我定义的两种类型之间的关系。第一个类似于 的有限子集nat，只有三个元素：

Inductive N3 := zero | one | two.

第二种是 sigma 类型，其元素满足命题{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.
???

我完全不确定定义的其余部分。我也尝试在 onx和 on 上进行模式匹配(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.

谢谢您的帮助。

4

3 回答 3

3

如果您从 math-comp 中的 finType 机器中获利，您也可以获得一些乐趣。

例如，您可以使用序数的枚举 [与您的类型同构] 通过枚举所有值而不是做繁琐的情况来证明您的引理：

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为您的自定义数据类型定义实例，然后确定两个集合具有相同的基数！有很多引理组合可以在这里尝试，所以你会玩得开心！

于 2017-08-06T16:43:15.693 回答
2

由于您使用的是 ssreflect，因此最简单的方法是使用<(in 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有点复杂，但基本思想很简单：对于Ptype 上的任何布尔谓词T，规范投影{ x : T | P x = true } -> T都是单射的。正如 Vinz 所说，这依赖于证明不相关的布尔等式；也就是说，布尔值之间相等的任何两个证明本身都是相等的。因此，相等{x | P x = true}性完全由元素决定x；证明部分无关紧要。

于 2017-08-04T14:08:41.467 回答
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 的一些证明”，在右侧有“命名为 0 < 3 的确切证明l_0_3”。

因此，您必须研究身份证明的无关性/唯一性证明的方向（可通过 nat & lt 证明）。

于 2017-08-04T08:26:51.337 回答