建立有限自然数与sigma同构
Establish isomorphism between finite natural numbers and sigma
我在这里和 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.
???
我完全不确定其余的定义。我还尝试在 x
和 (N3_to_lt3 (lt3_to_N3 x))
上进行模式匹配,但我不确定要 return.
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.
感谢您的帮助。
我会从类似
的内容开始
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
现在基本上唯一的区别是您在左侧有 "some proof that 0 < 3 named h
" 而在右侧有 "Your exact proof that 0 < 3 named l_0_3
"。
因此,您必须朝 证明身份证明的无关/唯一性方向(可通过 nat 和 lt 证明)。
由于您使用的是 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
的语句有点复杂,但基本思想很简单:对于类型T
上的任何布尔谓词P
,规范投影{ x : T | P x = true } -> T
是单射的。正如 Vinz 所说,这依赖于证明布尔等式无关紧要;也就是说,布尔值之间的任何两个相等证明本身都是相等的。因此,{x | P x = true}
上的相等性完全由元素 x
决定;证明部分无关紧要。
如果您从 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
实例,然后确定这两个集合具有相同的基数!这里有很多引理组合可以尝试,所以你会玩得开心!
我在这里和 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.
???
我完全不确定其余的定义。我还尝试在 x
和 (N3_to_lt3 (lt3_to_N3 x))
上进行模式匹配,但我不确定要 return.
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.
感谢您的帮助。
我会从类似
的内容开始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
现在基本上唯一的区别是您在左侧有 "some proof that 0 < 3 named h
" 而在右侧有 "Your exact proof that 0 < 3 named l_0_3
"。
因此,您必须朝 证明身份证明的无关/唯一性方向(可通过 nat 和 lt 证明)。
由于您使用的是 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
的语句有点复杂,但基本思想很简单:对于类型T
上的任何布尔谓词P
,规范投影{ x : T | P x = true } -> T
是单射的。正如 Vinz 所说,这依赖于证明布尔等式无关紧要;也就是说,布尔值之间的任何两个相等证明本身都是相等的。因此,{x | P x = true}
上的相等性完全由元素 x
决定;证明部分无关紧要。
如果您从 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
实例,然后确定这两个集合具有相同的基数!这里有很多引理组合可以尝试,所以你会玩得开心!