The Coq mailing list

[Amin Timany <amintimany AT gmail.com>]

Dear Micheal,

In coq, type class resolution is done in a way very similar to eauto, i.e., 
"typeclasses eauto”. In other words, coq tries to apply registered instances 
repeatedly to resolve an instance. Debug information here shows that in this 
case type class resolution gets stuck on the term:

 (EqDec
                     ((fix type (k : Kind) : Type :=
                         match k with
                         | Bool => bool
                         | Struct list =>
                             let fix typeaux (l : list (string * Kind)) :
                                   Type :=
                                   match l with
                                   | nil => unit
                                   | (_, elem) :: tail =>
                                       (type elem * typeaux tail)%type
                                   end in
                             typeaux list
                         end) ex1))

I don’t know if this is the intended behavior or a bug as "typeclasses eauto" 
seems to be able to simplify t2 and ext2 but not ext1 !?

To see details run the following code after the end of you original input.

Typeclasses eauto := debug 5. (* enabling debug mode for typeclasses eauto 
tactic and setting the search depth to 5 *)

Instance t2_dec : EqDec t2.
Fail typeclasses eauto. (* Check out debug message *)
cbv.
typeclasses eauto. (* this solves the goal *)
Abort.

Instance test_dec : EqDec ((((bool * (bool * unit) * (bool * (bool * unit) * 
unit)) * (bool * (bool * unit) * (bool * (bool * unit) * unit))) * ((bool * 
(bool * unit) * (bool * (bool * unit) * unit)) * (bool * (bool * unit) * 
(bool * (bool * unit) * unit)))))%type.
Fail typeclasses eauto. (* Fails as search does not go deep enough. 
increasing the depth "5" in command "Typeclasses eauto := debug 5." above 
will solve this problem *)
Typeclasses eauto := debug 7.
typeclasses eauto. (* this solves the goal *)
Abort.

This code also shows that even if typeclasses eauto would have been able to 
resolve such goals as EqDec t2, it would fail on big enough terms. The better 
way would be to define “Instance type_of_kind_eqb (k : Kind) : EqDec (type 
k).” explicitly. Here I have done this. To simplify proofs and definitions I 
have stopped coq from generating incorrect (inferred) induction/recursion 
schemes and have provided Kind_rect, Kind_rec and Kind_ind explicitly.

Require Import String.
Require Import List.
Open Scope string_scope.

Unset Elimination Schemes.

Inductive Kind: Set :=
| Bool: Kind
| Struct: list (string * Kind) -> Kind.

Theorem Kind_rect : forall P : Kind -> Type,
       P Bool ->
       P (Struct nil) ->
       (forall (a : string * Kind) (l : list (string * Kind)), P (snd a) -> P 
(Struct l) -> P (Struct (a :: l))) ->
       forall k : Kind, P k.
Proof.
  intros P PB PN PL k.
  refine (
      (fix rect m : P m :=
      match m with
        | Bool => PB
        | Struct list => let fix rectaux l : P (Struct l) :=
                             match l with
                               | nil => PN
                               | h::tail => PL _ _ (rect (snd h)) (rectaux 
tail)
                             end in rectaux list
      end
    ) k).
Defined.

Theorem Kind_rec : forall P : Kind -> Set,
       P Bool ->
       P (Struct nil) ->
       (forall (a : string * Kind) (l : list (string * Kind)), P (snd a) -> P 
(Struct l) -> P (Struct (a :: l))) ->
       forall k : Kind, P k.
Proof.
  intros; apply Kind_rect; trivial.
Defined.

Theorem Kind_ind : forall P : Kind -> Prop,
       P Bool ->
       P (Struct nil) ->
       (forall (a : string * Kind) (l : list (string * Kind)), P (snd a) -> P 
(Struct l) -> P (Struct (a :: l))) ->
       forall k : Kind, P k.
Proof.
  intros; apply Kind_rect; trivial.
Defined.

Set Elimination Schemes.

Fixpoint type (k : Kind) : Type :=
 match k with
 | Bool => bool
 | Struct list => let fix typeaux l : Type :=
   match l with
   | nil => unit
   | (name,elem)::tail => ((type elem)*(typeaux tail))%type
   end in typeaux list
 end.

Example ex1 := Struct (("a",Bool)::("b",Bool)::nil).
Example ex2 := Struct (("s",ex1)::("t",ex1)::nil).
Example t2 := type ex2.
Eval compute in t2.
(* = (bool * (bool * unit) * (bool * (bool * unit) * unit))%type : Type *)

Class EqDec (A : Type) := {
 eqb : A -> A -> bool ;
 eqb_leibniz : forall x y, eqb x y = true -> x = y
}.

Instance unit_EqDec : EqDec unit := {
 eqb x y := true;
 eqb_leibniz x y H := match x, y return x = y with tt, tt => eq_refl tt end
}.

Instance bool_EqDec : EqDec bool := {
 eqb x y := Bool.eqb x y
}.
Proof. intros; destruct x; destruct y; try reflexivity; try inversion H.
Defined.

Instance prod_eqb {A B : Type} (EA : EqDec A) (EB : EqDec B) : EqDec (A *
B) := {
 eqb x y := match x, y with
 | (la, ra), (lb, rb) => andb (eqb la lb) (eqb ra rb)
 end
}.
Proof.
 intros. destruct x. destruct y.
 assert(H0:=Bool.Is_true_eq_left _ H).
 assert(H1:=Bool.andb_prop_elim _ _ H0).
 inversion H1 as [H2 H3].
 assert(H4:=Bool.Is_true_eq_true _ H2).
 assert(H5:=Bool.Is_true_eq_true _ H3).
 assert(H6:=eqb_leibniz _ _ H4).
 assert(H7:=eqb_leibniz _ _ H5).
 subst. reflexivity.
Defined.

Example eqdec1 := (true,(false,tt)).
Example eqdec2 := (true,(true,tt)).
Eval compute in eqb eqdec1 eqdec1.
Eval compute in eqb eqdec1 eqdec2.

Example v1 := (true, (false, tt), (true, (false, tt), tt)).
Example v2 : t2 := (true, (false, tt), (true, (true, tt), tt)).
Eval compute in eqb v1 v2. (* => false *)
Eval compute in eqb v1 v1. (* => true *)
Example v3 : t2 := (true, (false, tt), (true, (false, tt), tt)).
Eval compute in eqb v3 v2. (* =>
    = (let (eqb, _) := ?257 in eqb)
        (true, (false, tt), (true, (false, tt), tt))
        (true, (false, tt), (true, (true, tt), tt))
    : bool
*)

Instance type_of_kind_eqb (k : Kind) : EqDec (type k).
Proof.
  induction k as [| |a k]; [| | destruct a as [str elm]]; typeclasses eauto.
Defined.

Eval compute in eqb v3 v2. (* =>
    = false
    : bool
*)

Regards,
Amin


> On 17 Dec 2014, at 09:58, Soegtrop, Michael 
> <michael.soegtrop AT intel.com>
>  wrote:
> 
> Dear Coq users,
> 
> one note on this: in case the type t2 is defined directly and not computed 
> by the fixpoint on the structure definition, the Type Class mechanism does 
> work. 
> Definition t2 := (bool * (bool * unit) * (bool * (bool * unit) * 
> unit))%type.
> 
> Example v1 := (true, (false, tt), (true, (false, tt), tt)).
> Example v2 : t2 := (true, (false, tt), (true, (true, tt), tt)).
> Eval compute in eqb v1 v2. (* => false *)
> Eval compute in eqb v1 v1. (* => true *)
> 
> Example v3 : t2 := (true, (false, tt), (true, (false, tt), tt)).
> Eval compute in eqb v3 v2. (* => false *)
> 
> Only if t2 is computed by the fixpoint given in my first post, it doesn't 
> work.
> 
> Example v3 : t2 := (true, (false, tt), (true, (false, tt), tt)).
> Eval compute in eqb v3 v2. (* =>
>     = (let (eqb, _) := ?257 in eqb)
>         (true, (false, tt), (true, (false, tt), tt))
>         (true, (false, tt), (true, (true, tt), tt))
>     : bool
> *)
> 
> Is this a bug in the Type Class mechanism?
> 
> Best regards,
> 
> Michael
>