The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

I want to define the following 2 ways of constructing new rings from existing ones.

1) given a setoid A and a ring B, I want to define a ring over the setoid representing A -> B where the operations (e.g. +, *) are just the corresponding operations on B (pointwise)

2) Given a ring B and a property (B -> Type) that respects the equality on the underlying setoid of B, and proofs that the ring operations on B are closed under the property, I want to construct the "usual" sub-ring.

If anyone knows about existing Coq definition/proofs of the above structures, I'd be grateful to know about them.

If these definitions are based on the algebraic hierarchy defined in CoRN or MathClasses, I might be able to used them directly.

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/