在Coq中对我自己的==运算符使用重写策略 [英] Use rewrite tactic with my own == operator in Coq

问题描述

我正试图直接从领域公理证明简单的领域属性。在对Coq的本机字段进行了一些实验之后（像这样），我认为最好简单地编写降低10个公理并使其独立。当我需要将 rewrite 与我自己的 == 运算符一起使用时，遇到了困难，该运算符自然不起作用。我意识到我必须添加一些公理，我的 == 是自反的，对称的和可传递的，但是我想知道这是否是全部？还是有更简单的方法可以对用户定义的 == 使用 rewrite ？这是我的Coq代码：

I'm trying to prove simple field properties directly from the field's axioms. After some experiments with Coq's native field support (like this one) I decided it's better to simply write down the 10 axioms and make it self contained. I encountered a difficulty when I needed to use rewrite with my own == operator which naturally did not work. I realize I have to add some axioms that my == is reflexive, symmetrical and transitive, but I wondered if that is all it takes? or maybe there is an even easier way to use rewrite with a user defined ==? Here is my Coq code:

Variable (F:Type).
Variable (zero:F).
Variable (one :F).
Variable (add: F -> F -> F).
Variable (mul: F -> F -> F).
Variable (opposite: F -> F).
Variable (inverse : F -> F).
Variable (eq: F -> F -> Prop).

Axiom add_assoc: forall (a b c : F), (eq (add (add a b) c) (add a (add b c))).
Axiom mul_assoc: forall (a b c : F), (eq (mul (mul a b) c) (mul a (mul b c))).

Axiom add_comm : forall (a b : F), (eq (add a b) (add b a)).
Axiom mul_comm : forall (a b : F), (eq (mul a b) (mul b a)).

Axiom distr1 : forall (a b c : F), (eq (mul a (add b c)) (add (mul a b) (mul a c))).
Axiom distr2 : forall (a b c : F), (eq (mul (add a b) c) (add (mul a c) (mul b c))).

Axiom add_id1 : forall (a : F), (eq (add a zero) a).
Axiom mul_id1 : forall (a : F), (eq (mul a  one) a).
Axiom add_id2 : forall (a : F), (eq (add zero a) a).
Axiom mul_id2 : forall (a : F), (eq (mul one  a) a).

Axiom add_inv1 : forall (a : F), exists b, (eq (add a b) zero).
Axiom add_inv2 : forall (a : F), exists b, (eq (add b a) zero).

Axiom mul_inv1 : forall (a : F), exists b, (eq (mul a b) one).
Axiom mul_inv2 : forall (a : F), exists b, (eq (mul b a) one).

(*******************)
(* Field notations *)
(*******************)
Notation "0" := zero.
Notation "1" :=  one.
Infix    "+" :=  add.
Infix    "*" :=  mul.
(*******************)
(* Field notations *)
(*******************)
Infix "==" := eq (at level 70, no associativity).

Lemma mul_0_l: forall v, (0 * v == 0).
Proof.
  intros v.
  specialize add_id1 with (0 * v).
  intros H.

在这一点上，我假设 H ：0 * v + 0 == 0 * v 和目标
0 * v == 0 。当我尝试重写H 时，它自然会失败。

At this point I have the assumption H : 0 * v + 0 == 0 * v and goal 0 * v == 0. When I tried to rewrite H, it naturally fails.

推荐答案

广义重写（具有任意关系的重写）：

For generalized rewriting (rewriting with arbitrary relations):

1. Import Setoid （会加载一个重写 rewrite 策略的插件。）

1. Import Setoid (which loads a plugin which overrides the rewrite tactic).

将您的关系声明为等价关系（从技术上讲，重写也适用于较弱的假设，例如仅适用于传递性假设，但在步骤3）中，您还需要处理更精细的关系层次结构。

Declare your relation as an equivalence relation (technically rewrite also works with weaker assumptions, say with only transitive ones, but you would also need to work with a much more fine grained hierarchy of relations in step 3).

声明您的操作（添加， mul ，等）表示对该操作的尊重（例如，添加等效值必须得到等效值）。这也需要 Morphism 模块。

Declare your operations (add, mul, etc.) as being respectful of that operation (e.g., adding equivalent values must result in equivalent values). This also requires the Morphism module.

您需要执行以下步骤3重写子表达式。

You need step 3 to rewrite subexpressions.

Require Import Setoid Morphisms.

(* eq, add, etc. *)

Declare Instance Equivalence_eq : Equivalence eq.
Declare Instance Proper_add : Proper (eq ==> eq ==> eq) add.
Declare Instance Proper_mul : Proper (eq ==> eq ==> eq) mul.
(* etc. *)

Lemma mul_0_l: forall v, (0 * v == 0).
Proof.
  intros v.
  specialize add_id1 with (0 * v).
  intros H.
  rewrite <- H. (* Rewrite toplevel expression (allowed by Equivalence_eq) *)
  rewrite <- H. (* Rewrite subexpression (allowed by Proper_add and Equivalence_eq) *)

这篇关于在Coq中对我自己的==运算符使用重写策略的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！