私は Coq と一緒に、私が定義した 2 つの型の間の関係を調べています。1 つ目は の有限部分集合のようなものでnat、要素は 3 つだけです。
Inductive N3 := zero | one | two.
2 つ目は、要素が命題を満たすシグマ型{x: nat | x < 3}です。その定義は次のとおりです。
Definition less_than_3 := {x| x < 3}.
この 2 つの型が同型であることを証明したいと思います。関係する 2 つの関数を次のように定義しました。
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.
???
残りの定義についてはまったくわかりません。xonと 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.
助けてくれてありがとう。