在 Coq 中使用我自己的 == 运算符重写策略

我试图直接从字段的公理证明简单的字段属性。经过对 Coq 原生现场支持的一些实验（像这个）我决定最好简单地写下 10 条公理并使其自成一体。我在需要使用的时候遇到了困难rewrite与我自己的==运算符自然不起作用。我意识到我必须添加一些我的公理==自反、对称和传递，但我想知道这是否就是全部？或者也许有一种更简单的使用方法rewrite与用户定义的==？这是我的 Coq 代码：

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。当我尝试rewrite H，自然就失败了。

对于广义重写（任意关系重写）：

1. Import Setoid（它加载一个插件，该插件会覆盖rewrite战术）。

2. 将您的关系声明为等价关系（技术上rewrite也适用于较弱的假设，例如仅适用于传递性假设，但您还需要在步骤 3) 中使用更细粒度的关系层次结构，使用Equivalence class.

3. 声明您的操作（add, mul等）作为尊敬的的等价性（例如，添加等价的值必须产生等价的值），使用Proper班级。这也需要Morphisms module.

您需要第 3 步来重写子表达式。

Require Import Setoid Morphisms.

(* Define 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) *)