The Coq mailing list

[wataru yamazaki <wataru.yamazaki.nullptr AT gmail.com>]

The following code gets stuck in an infinite loop at last instance
decralation on coq-v8.3pl2.

(* code *)
Require Import Setoid.
Require Import SetoidClass.
Section Monoid.


Set Implicit Arguments.
Set Strict Implicit.
Unset Automatic Introduction.

Class Monoid_struct (S:Type) :=
{ dot : S -> S -> S
; mon_oid :> Setoid S
; dot_assoc : forall x y z, dot (dot x y) z ==dot x (dot y z)
; unit : S
; unit_id_l : forall y, dot unit y == y
; unit_id_r : forall x, dot x unit == x
}.

Record Monoid :=
{ Mset :> Type
; monoid_struct :> Monoid_struct Mset
}.

Instance Monoid_setoid : Setoid Monoid :=
{ equiv x y := Mset x = Mset y }.
split; unfold Reflexive, Symmetric, Transitive; auto.
intros x y z H H0.
transitivity y; auto.
Qed.

End Monoid.

Section MonoidHom.

Infix "*" := dot (at level 40).
Notation "'å'" := unit.

Class Monoid_mor_struct {A B:Type} (M:Monoid_struct A) (M':Monoid_struct B) :=
{ homM  : A -> B
; homM_morphism :> forall a,
          Proper (equiv)(homM a )
; hom_distr : forall x y:A, homM (x * y) == homM x * homM y
; hom_id : homM å == å
}.

End MonoidHom.

Section Monoid_cat.

Variable A B:Type.
Let Mmor (M M':Monoid) : Type.
intros.
eapply Monoid_mor_struct.
apply M.
apply M'.
Defined.

Instance Monoid_equiv : Setoid Monoid.

Notation "# f" := (homM (Monoid_mor_struct:=f)) (at level 0).

Definition Mmor_equiv (M M':Monoid) : relation (Mmor M M') :=
  fun (f g:Mmor M M') => (forall (x:M), #f x = #g x).

Program Instance Mmor_oid M M' : Setoid (Mmor M M') :=
{ equiv  :=  @Mmor_equiv M M' }.
Next Obligation.
unfold Mmor_equiv.
split.
intros f g.
reflexivity.
intros f g H x.
symmetry.
apply H.
intros f g h H0 H1 x.
transitivity (#g x).
apply H0.
apply H1.
Qed.

Class Cat_s (obj:Type)(mor: obj -> obj -> Type) := {
  mor_oid:> forall a b, Setoid (mor a b);
  comp: forall {a b c},
        mor a b -> mor b c -> mor a c;
  comp_oid:> forall a b c,
        Proper (equiv ==> equiv ==> equiv) (@comp a b c)
}.


Instance MON_struct : Cat_s (obj:=Monoid) (fun M M':Monoid =>
Monoid_mor_struct M M') :=
{ mor_oid := Mmor_oid }.
(* end code*)

If I use svn-head version of coqtop, this code dont't get infinite loop.
But head version has many other probles, so I want use stable version.

When I inturrupt this loop on coqtop, coqtop says,
'
In nested Ltac calls to "proper_reflexive", "class_apply" and
"autoapply c using typeclass_instances" (expanded to
"autoapply reflexive_proper using typeclass_instances"), last call failed.
'

How to declare Instance 'MON_struct' with avoiding infinite loop on coq 
8.3pl2 ?

Thank you.
---
wataru