我正在尝试直接从场的公理证明简单的场属性。在使用 Coq 的本地字段支持 (like this one) 进行一些实验后,我决定最好简单地写下 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
。当我尝试重写 H
时,它自然会失败。
最佳答案
对于广义重写(具有任意关系的重写):
导入
Setoid
(它加载一个插件来覆盖rewrite
策略)。将您的关系声明为等价关系(技术上
rewrite
也适用于较弱的假设,例如仅传递假设,但您还需要使用更细粒度的层次结构步骤 3 中的关系),使用Equivalence
类。声明您的操作(
add
、mul
等)尊重该等效项(例如,添加等效值必须产生等效值),使用Proper
类。这也需要Morphisms
模块。
您需要第 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) *)
关于coq - 在 Coq 中使用我自己的 == 运算符重写策略,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/56099646/