Use rewrite tactic with my own == operator in Coq

Question

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.

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.

Li-yao Xia Li-yao Xia · Accepted Answer · 2019-05-12T13:58:07

For generalized rewriting (rewriting with arbitrary relations):

Import Setoid (which loads a plugin which overrides the rewrite tactic).
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), using the Equivalence class.
Declare your operations (add, mul, etc.) as being respectful of that equivalence (e.g., adding equivalent values must result in equivalent values), using the Proper class. This also requires the Morphisms module.

You need step 3 to rewrite subexpressions.

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

Use rewrite tactic with my own == operator in Coq

2 Answers