Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Question about ring_theory and field_theory

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Question about ring_theory and field_theory


Chronological Thread 
  • From: Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Question about ring_theory and field_theory
  • Date: Tue, 27 May 2014 17:38:26 +0300

Because of it best (at least now) what I could do, was like this.


Require Import Field Ring matrices.
Require Import Setoid.

Parameters (R: Type) (rO rI: R) (radd rmul rsub rdiv: R -> R -> R) (ropp rinv: R -> R) (req: R -> R -> Prop) .
Parameter (ring_instance: ring_theory rO rI radd rmul rsub ropp req).
Parameter (field_instance: field_theory rO rI radd rmul rsub ropp rdiv rinv req).

Parameters (req_refl: reflexive _ req) (req_sym: symmetric _ req) (req_trans: transitive _ req).
Add Parametric Relation: R @req
 reflexivity proved by req_refl
 symmetry proved by req_sym
 transitivity proved by req_trans
 as req_rel.



On Tue, May 27, 2014 at 12:42 PM, Ilmārs Cīrulis <ilmars.cirulis AT gmail.com> wrote:
Why ring_theory and field_theory can be build with req, which doesn't have any properties of equivalence?

--
Ilmars




Archive powered by MHonArc 2.6.18.

Top of Page