Coq Z_3组定义左id定理

如何解决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,这与赫德伯格定理无关( 证明)。

版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。

相关推荐


Selenium Web驱动程序和Java。元素在(x,y)点处不可单击。其他元素将获得点击?
Python-如何使用点“。” 访问字典成员?
Java 字符串是不可变的。到底是什么意思?
Java中的“ final”关键字如何工作?(我仍然可以修改对象。)
“loop:”在Java代码中。这是什么,为什么要编译?
java.lang.ClassNotFoundException:sun.jdbc.odbc.JdbcOdbcDriver发生异常。为什么?
这是用Java进行XML解析的最佳库。
Java的PriorityQueue的内置迭代器不会以任何特定顺序遍历数据结构。为什么?
如何在Java中聆听按键时移动图像。
Java“Program to an interface”。这是什么意思?
Java在半透明框架/面板/组件上重新绘画。
Java“ Class.forName()”和“ Class.forName()。newInstance()”之间有什么区别?
在此环境中不提供编译器。也许是在JRE而不是JDK上运行?
Java用相同的方法在一个类中实现两个接口。哪种接口方法被覆盖?
Java 什么是Runtime.getRuntime()。totalMemory()和freeMemory()?
java.library.path中的java.lang.UnsatisfiedLinkError否*****。dll
JavaFX“位置是必需的。” 即使在同一包装中
Java 导入两个具有相同名称的类。怎么处理?
Java 是否应该在HttpServletResponse.getOutputStream()/。getWriter()上调用.close()?
Java RegEx元字符(。)和普通点?