如何解决Coq Z_3组定义左id定理
我试图证明Z3是一个小组。
Class Group G : Type :=
{
e : G;
mult : G -> G -> G;
inv : G -> G;
left_id : forall x:G,mult e x = x;
left_inv : forall x:G,mult (inv x) x = e;
assoc : forall x y z:G,mult x (mult y z) = mult (mult x y) z
}.
Record Z_3 : Type := Z3
{
n :> nat;
proof : n < 3
}.
(* Inhabitants of Z_3 type *)
Proposition lt_0_3 : 0 < 3.
Proof.
repeat constructor.
Qed.
Definition z3_0 : Z_3 := (Z3 0 lt_0_3).
Proposition lt_1_3 : 1 < 3.
Proof.
repeat constructor.
Qed.
Definition z3_1 : Z_3 := (Z3 1 lt_1_3).
Proposition lt_2_3 : 2 < 3.
Proof.
repeat constructor.
Qed.
Definition z3_2 : Z_3 := (Z3 2 lt_2_3).
(* End of inhabitants definition *)
Proposition three_ne_0 : 3 <> 0.
Proof.
intro. discriminate.
Qed.
Definition Z3_op (x y: Z_3) : Z_3 :=
let a := (x + y) mod 3 in
Z3 a (Nat.mod_upper_bound _ 3 three_ne_0).
Lemma Z_3_inv_lemma (k: nat) : (3 + k) < 3 -> False.
Proof.
intro. inversion_clear H. inversion_clear H0. inversion_clear H. inversion_clear H0.
Qed.
Lemma void {t : Set} : False -> t.
Proof.
intro. contradiction H.
Qed.
Definition Z_3_inv (x : Z_3) : Z_3 :=
match x with
| Z3 0 pf => Z3 0 pf
| Z3 1 pf => Z3 2 lt_2_3
| Z3 2 pf => Z3 1 lt_1_3
| Z3 (S (S (S k))) pf => void (Z_3_inv_lemma k pf)
end.
Proposition Z3_left_id : forall x: Z_3,(Z3_op z3_0 x) = x.
Proof.
intro. unfold Z3_op. destruct x. inversion proof0.
-
我在这里被困住了:
1 subgoal (ID 46)
n0 : nat
proof0 : n0 < 3
H0 : n0 = 2
============================
{|
n := (z3_0 + {| n := n0; proof := proof0 |}) mod 3;
proof := Nat.mod_upper_bound
(z3_0 + {| n := n0; proof := proof0 |}) 3
three_ne_0 |} = {| n := n0; proof := proof0 |}
rewrite H0.
不起作用。抱歉,当涉及到这些记录时,我很难进一步前进。
解决方法
首先应该创建并应用一个单独的引理,以证明Z3元素之间的相等性。然后您就可以简化为具有相等的sigma类型,例如跟随 https://stackoverflow.com/a/27080869/53974。
但是,在您的情况下,可以避免公理-您不需要功能扩展,并且可以通过存储证明可证明的不相关证明类型来避免不相关证明公理;可能z < 3
已经与证明无关,因为<
的编写是为了接纳唯一的居民。
但是,否则,您可以将z < 3
替换为z <? 3 = true
,这与赫德伯格定理无关( 证明)。