使用Coq字段公理 [英] Using Coq Field axioms

问题描述

我正在尝试Coq字段模块，试图直接从字段公理证明以下简单身份： forall v，0v == v 。我看到 0 和 == 都具有现有的符号，所以我尝试了此操作（但失败了）：

I'm experimenting with the Coq field module trying to prove the following simple identity directly from field axioms: forall v, 0v == v. I saw that both 0 and == have existing notations, so I tried this (but failed):

(***********)
(* IMPORTS *)
(***********)
Require Import Coq.setoid_ring.Field_theory.

(*********************)
(* forall v, 0v == v *)
(*********************)
Lemma mul_0_l: forall v,
  ("0" * v "==" "0")%R_scope.
Proof.

我收到此错误消息：

Unknown scope delimiting key R_scope.

当我看着字段库， R_scope 肯定存在，
，所以我一定很想念

When I looked at the field library, R_scope is definitely there, so I must be missing something.

推荐答案

实际上，这些符号位于一节中，这意味着它们不能从外部获得。

Actually, those notations are in a section, which means that they are not available from the outside.

此外，所有这些定义都由字段结构参数化，因此，如果要证明有关字段的一般结果，则需要在本地声明（或实例化）这些参数。

Furthermore, all these definitions are parameterized by the field structure, so if you want to prove general results about fields you will need to declare (or instantiate) those parameters locally.

我不确定它是否真的打算以这种方式使用。我的建议是在Github上打开一个问题，询问setoid_ring插件的用途。

I'm not sure it is actually meant to be used that way. My advice is to open an issue on Github to ask the purpose of the setoid_ring plugin.

Require Import Coq.setoid_ring.Field_theory.
Require Import Coq.setoid_ring.Ring_theory.
Require Import Setoid.

Section MyFieldTheory.

(* Theory parameterized by a field R *)
Variable (R:Type)
         (rO:R) (rI:R)
         (radd rmul rsub : R -> R -> R)
         (ropp : R -> R)
         (rdiv : R -> R -> R)
         (rinv : R -> R)
         (req : R -> R -> Prop)
.
Variable Rfield : field_theory rO rI radd rmul rsub ropp rdiv rinv req.
Variable Reqeq : Equivalence req.
Variable Reqext : ring_eq_ext radd rmul ropp req.

(* Field notations *)
Notation "0" := rO : R_scope.
Notation "1" := rI : R_scope.
Infix "+" := radd : R_scope.
Infix "*" := rmul : R_scope.
Infix "==" := req : R_scope.

(* Use these notations by default *)
Local Open Scope R_scope.


(* Example lemma *)

Lemma mul_0_l: forall v, (0 * v == 0).
Proof.
  intros v.
  apply ARmul_0_l with rI radd rsub ropp.
  apply F2AF, AF_AR in Rfield; auto.
Qed.

---

关于符号

请注意，引号是注释 / 中缀命令的语法的一部分

---

About notation

Note that the quotes are part of the syntax for the Notation/Infix command

Infix "+" := radd : R_scope.

您现在可以只写 x + y ，没有引号。

You can now just write x + y, no quotes.

将范围分配给符号是一种很好的做法（通过上面的：R_scope 批注例如），这样就可以为同一符号启用消除歧义的机制。特别是使符号可用的主要两种方法是：

It is good practice to assign scopes to your notations (via the : R_scope annotation above for example) as that enables mechanisms for disambiguation of different meanings for the same notation. In particular the main two ways to make notations available are:

• 本地开放范围R_scope。使所有 R_scope 符号可用于当前文件。

• Local Open Scope R_scope. make all R_scope notations available for the current file.

使用任何绑定范围R_scope。将定界键 任何内容关联到范围 R_scope 。分隔键是％符号后面用来在给定表达式中打开范围的内容，因此您可以编写（0 == 0 * v）不管什么，无论以前是否使用本地打开范围打开 R_scope 。

Bind Scope R_scope with whatever. associates a delimiting key whatever to the scope R_scope. The delimiting key is what goes after the % symbol to open a scope in a given expression, so you could write (0 == 0 * v)%whatever, whether or not R_scope was previously opened using Local Open Scope.

这篇关于使用Coq字段公理的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！