Setoids for beginners
Although the type Z of integers is already defined in Coq, it
is interesting to look at the usual mathematical building of the set of
integers as a quotient of the set of pairs of natural numbers by the
equivalence relation (a,b) R (c,d) if a+d = b+c.
In Coq, you will associate a setoid to this equivalence relation, and
register the usual operations : +, *, etc, as morphisms.
Prove also that you build a ring with unity and the property of integrity
(i.e. if xy = 0 then x = 0 or
y = 0 .)
In a second time, build the ring of integers modulo p (with p:nat).
Give some examples of setoid_replace and setoid_rewrite.
Solution