The Coq mailing list

[Math Prover <mathprover AT yahoo.com>]

[Changed to a human sounding name.]

I have another stupid question. Please see attached fail (pasted below).

This is what baffles me:

Why does this work with EquivDec, but not { x = y } + { x <> y} ?

What makes absolutely no sense to me is:

* There is only one way to define structural equality.

* There are many possible equivalence definitions
  * Example 1: structural equality
  * Example 2: return true on everything


Now, in the following code, I have two pieces of code that are syntactically 
almost the same -- yet, in the "structural equality" case, Coq can't infer 
Keq, yet ... in the "more general" Equivalence case, Coq can infer Keq.


What incorrect assumption am I making? :-)


=====

~/z/cur$ cat fail.v 
Require Import Bool Arith ZArith Arith.Peano_dec List Coq.Classes.EquivDec.
Local Open Scope Z_scope.

Section assocList1.

  Variable K: Type.
  Variable V: Type.
  Variable Keq: forall k1 k2: K, {k1 = k2} + {k1 <> k2}.
  Variable Veq: forall v1 v2: V, {v1 = v2} + {v1 <> v2}.

  Function assocList1_r (lst: list (K * V)) (k: K) : option V :=
    match lst with
    | nil => None
    | (k',v') :: xs => if Keq k k' then Some v' else assocList1_r xs k
    end.

End assocList1.

Section assocList2.

  Variable K: Type.
  Variable V: Type.
  Variable Keq: EqDec K eq.

  Function assocList2_r (lst: list (K * V)) (k: K) : option V :=
    match lst with
    | nil => None
    | (k',v') :: xs => if Keq k k' then Some v' else assocList2_r xs k
    end.

End assocList2.

Implicit Arguments assocList1_r [K V Keq].
Implicit Arguments assocList2_r [K V Keq].

(* up to this line all works *)

(* the next line also works *)
Definition fun2 (lst: list (nat * nat)) (k: nat) := assocList2_r lst k.

(* why did the previous line work ??? *)  


(* the next line fails with error:
  Error: Cannot infer the implicit parameter Keq of assocList1_r.  *)
Definition fun1 (lst: list (nat * nat)) (k: nat) := assocList1_r lst k.






________________________________
From: Feró 
<ferenc.tamasi AT gmail.com>
To: Math Prover 
<mathprover AT yahoo.com>
 
Cc: 
"coq-club AT inria.fr"
 
<coq-club AT inria.fr>
 
Sent: Saturday, May 18, 2013 2:45 AM
Subject: Re: [Coq-Club] 


Speculations follow, I hope someone will correct me:

I guess, Check does not do "instantiation" only type checking, and for
that there's enough information.

If you do `Definition x := (assocList_r lst1 1).' instead of Check, it
will also fail. That is, Coq will not try to guess which decision
procedure you want to use as Keq.

On Sat, May 18, 2013 at 3:36 AM, Math Prover 
<mathprover AT yahoo.com>
 wrote:
> I'm using Coq 8.4 (downloaded from the main Coq website).
>
> In the following block of code (also attached), I get an "Error: Cannot
> infer the implicit parameter Keq of assocList_r." error.
>
> I believe what I have is a minimal example.
>
> What confuses me is that:
>
>   * when I use "Check" on the same types, it works
>
>   * when I define it as part of a Function, I get an "Cannot infer the
> implicit parameter" error
>
>
> Can someone please help me with:
>
>   1) Letting me know if there's anyway I can reformat my question to make it
> easier to answer. (Or any additional information I should provide.)
>
>   2) Tell me what I'm doing wrong / misunderstanding?
>
>
> ===== Code ======
>
>
> Require Import List Coq.Classes.EquivDec.
>
>
> Section assocList.
>
>   Variable K: Type.
>   Variable V: Type.
>
>   Variable Keq: forall k1 k2: K, {k1 = k2} + {k1 <> k2}.
>
>   Function assocList_r (lst: list (K * V)) (k: K) : option V :=
>     match lst with
>     | nil => None
>     | (k',v') :: xs =>
>       if Keq k k' then Some v' else assocList_r xs k
>     end.
>
> End assocList.
>
> Implicit Arguments assocList_r [K V Keq].
>
> Definition lst1 := (1,2)::nil.
>
> Check (assocList_r lst1 1).
>
> (* Up until this line, all works *)
>
>
> (* The following line gives me the error:
>   Error: Cannot infer the implicit parameter Keq of assocList_r.    *)
>
> Function f (lst: list (nat * nat)) (k: nat) :=
>   assocList_r lst k.



-- 
Give me liberty or give me cash!

Attachment: fail.v
Description: Binary data