The Coq mailing list

[Bill Wang <dramforever AT live.com>]

Hello coq-club,

I'm trying to add a ring of types up to isomorphism, but I cannot seem to get 
coq to understand that iso is indeed a setoid, despite having done "Add 
Parametric Relation". The error given is "cannot find setoid relation".

My code is pasted below. Can you help me fix it? Thanks.


(* I'm using coq 8.5 *)
Require Export Setoid Ring Ring_theory.

(* iso A B: Types A and B are isomorphic *)
Definition iso (A B : Type) : Prop :=
  exists (fw : A -> B) (bw : B -> A),
    (forall x, fw (bw x) = x) /\ (forall x, bw (fw x) = x).

(* Tactic iso for automagically solving (some) iso A B goals *)
Ltac de_iso := match goal with
                 | [ H : iso _ _ |- _ ] =>
                   let fw := fresh "fw" in
                   let bw := fresh "bw" in
                   let fw_bw := fresh "fw_bw" in
                   let bw_fw := fresh "bw_fw" in
                   destruct H as [fw [bw [fw_bw bw_fw]]]; de_iso
                 | _ => idtac
               end.

Ltac simpl_goal := match goal with
                     | [ H : unit |- _ ] => destruct H; simpl_goal
                     | _ => dintuition
                   end.

Ltac work_iso := dintuition; simpl; simpl_goal; congruence.

Ltac mk_iso :=
  match goal with
      |- iso ?A ?B =>
      refine (@ex_intro (A -> B) _ (ltac:(intuition))
                        (@ex_intro (B -> A) _ (ltac:(intuition))
                                   (conj _ _)))
  end.

Ltac iso := dintuition; de_iso; mk_iso; work_iso.

(* The actual relations *)
Add Parametric Relation : Type iso
    reflexivity proved by ltac:(unfold Reflexive; iso)
    symmetry proved by ltac:(unfold Symmetric; iso)
    transitivity proved by ltac:(unfold Transitive; iso)
      as iso_rel.

Add Parametric Morphism : sum
    with signature iso ==> iso ==> iso as sum_mor.
  iso. Defined.

Add Parametric Morphism : prod
    with signature iso ==> iso ==> iso as prod_mor.
  iso. Defined.

Definition iso_ring_theory : semi_ring_theory Empty_set unit sum prod iso.
  iso. Defined.

(* This one does not work, but I don't know why *)
Add Ring iso_ring : iso_ring_theory.
(* Error: cannot find setoid relation *)