coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
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:
IlmarsWhy ring_theory and field_theory can be build with req, which doesn't have any properties of equivalence?--
- [Coq-Club] Question about ring_theory and field_theory, Ilmārs Cīrulis, 05/27/2014
- Re: [Coq-Club] Question about ring_theory and field_theory, Ilmārs Cīrulis, 05/27/2014
- Re: [Coq-Club] Question about ring_theory and field_theory, Laurent Théry, 05/27/2014
- Re: [Coq-Club] Question about ring_theory and field_theory, Ilmārs Cīrulis, 05/28/2014
Archive powered by MHonArc 2.6.18.