I like the build up the basic types such as Integers and rationals to understand how the Coq system works, and I’m trying to establish Setoid equivalence of the rationals, but I’m not sure quite how to tell the system that I’m doing that.

In the standard library for the rationals, it starts doing Instance stuff, which is something I have not learned yet, so I was trying to go back to what is in Generalized Rewriting in the manual https://coq.inria.fr/refman/addendum/generalized-rewriting.html.

I’ve established my proofs on reflexivity, symmetry and transitivity (trans was a lot harder to prove than the others).

Definition Qeq (r1 : rat) (r2 : rat) :=

match r1, r2 with

| Qmake i p, Qmake j q => times_int_pos i q = times_int_pos j p

end.

Lemma Qeq_refl : forall (r : rat), Qeq r r.

destruct r. simpl. reflexivity.

Qed.

Lemma Qeq_sym : forall (r s : rat), Qeq r s → Qeq s r.

destruct r; destruct s; intros H.

unfold Qeq in H. unfold Qeq. rewrite H.

reflexivity.

Qed.

Lemma Qeq_trans : forall (r s t : rat), Qeq r s → Qeq s t → Qeq r t.

details omitted

Qed.

Add Relation Qeq

reflexivity proved by Qeq_refl

symmetry proved by Qed_sym

transitivity proved by Qeq_trans

as qeq_rel.

I assume I have some kind of syntax error in my Add Relation. The generalized rewriting guide only brushes over the non-parametric kind of relation, so I didn’t get an example of it’s syntax.

Any hints to lead me to the right path?