The Coq mailing list

[Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>]

Thank you for the answer!

On Tue, May 27, 2014 at 7:42 PM, Laurent Théry <Laurent.Thery AT inria.fr> wrote:

On 05/27/2014 11:42 AM, Ilmārs Cīrulis wrote:

Why ring_theory and field_theory can be build with req, which doesn't have any properties of equivalence?

--
Ilmars

It has but it is handle by the setoid mechanism. Here is a way to get ring with your req


Require Import Relation_Definitions Ring.

Parameters (R: Type) (rO rI: R) (radd rmul rsub rdiv: R -> R -> R) (ropp rinv: R -> R) (req: R -> R -> Prop) .

Lemma Rref : reflexive _ req.
Proof. admit. Qed.

Lemma Rsym : symmetric _ req.
Proof. admit. Qed.

Lemma Rtrans : transitive _ req.
Proof. admit. Qed.

Add Relation R req
reflexivity proved by Rref
symmetry proved by Rsym
transitivity proved by Rtrans
as RSetoid.

Add Morphism radd : radd_morph .
admit.
Qed.

Add Morphism rmul : rmul_morph .
admit.
Qed.

Add Morphism ropp : ropp_morph .
admit.
Qed.

Parameter ring_instance: ring_theory rO rI radd rmul rsub ropp req.

Add Ring Rring : ring_instance.

Goal forall x y : R, req (radd x y) (radd y x).
intros.
ring.