The Coq mailing list

[Math Prover <mathprover AT yahoo.com>]

Auger: Good call. Added topic. Sorry about that.

Fero: Thanks! This worked flawlessly for me (in actual codebase.


----- Original Message -----
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 4:43 AM
Subject: Re: [Coq-Club] 

Another round of guesswork :), an explanation of what happens behind
the scene would be very much appreciated!

Following the source for nat, I found a way to register the decision proc:

Inductive aa := asdf : aa.
Theorem eq_aa_dec : forall n m : aa, {n = m} + {n <> m}. decide equality. Qed.

(*this registers the decision proc*)
Instance aa_eq_eqdec : EqDec aa eq := eq_aa_dec.

Definition fun3 (lst: list (aa * aa)) (k: aa) := assocList2_r lst k.


On Sat, May 18, 2013 at 12:52 PM, Math Prover 
<mathprover AT yahoo.com>
 wrote:
> [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!



-- 
Give me liberty or give me cash!