The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

Regarding the issue with bullets (- + *), I think it may be resolved
by installing the latest version of PG. I do not know about the
Program issues (most of the time using dependent types, I prefer to
make an interactive definition, and do some amount of refine "by
hand", in order to simplify what Program would have inferred).

But, ok, I reckon that it makes sense to stick with 8.3 in order to
avoid these pitfalls.

Is it possible to solve your real problem using simple hacks like the
following definition ?

Global Instance foo (n: nat) : Reflexive (@tmEq 0 n).  apply
ctxtEq_Reflexive.  Qed.

Here, [foo] is just a simpl handler to help the typeclass resolution
mechanism (indeed, this is just a problem with the way the resolution
is done, since you could always finish your proof of the REFLTEST2
using apply ctxtEq_Reflexive, and one can guess that somehow, this
improved between 8.3 and 8.4.)

Thomas


On Fri, Nov 23, 2012 at 11:25 AM, Andrew Kennedy 
<akenn AT microsoft.com>
 wrote:
> OK, thanks, I've just installed coq 8.4 side-by-side. I have other problems
> with it (Program Definition looping on some examples, I'm told that this
> is fixed in trunk, also proof general not working properly on the - + * 
> markers
> from ssreflect) so I had reverted to coq 8.3. Now I'm not sure which way to 
> turn...
>
> Cheers
> Andrew.
>
> -----Original Message-----
> From: Thomas Braibant 
> [mailto:thomas.braibant AT gmail.com]
> Sent: 23 November 2012 10:13
> To: Andrew Kennedy
> Cc: coq-club
> Subject: Re: [Coq-Club] Problem with setoid rewriting and reduction
>
> Your particular example works well using Coq 8.4. I do not know the deep 
> reason for that change, though.
>
> Thomas
>
>
> On Fri, Nov 23, 2012 at 10:54 AM, Andrew Kennedy 
> <akenn AT microsoft.com>
>  wrote:
>> Hello
>>
>>
>>
>> I've encountered a problem with setoid rewriting where the search for
>> the relation doesn't succeed "up to" some simple reductions. I'm not
>> sure if this is expected behaviour, but it's certainly a bit
>> frustrating. Here's my example, boiled down to something small.
>>
>>
>>
>> Inductive Tm (env: nat) : nat -> Type :=
>>
>>   C : forall t, Tm env t.
>>
>>
>>
>> Definition globEnv := 5.
>>
>>
>>
>> Definition tmEq (env: nat) (t: nat) (M1 M2: Tm (env + globEnv) t) :=
>>
>>   match M1, M2 with C _, C _ => True end.
>>
>>
>>
>> Global Instance ctxtEq_Reflexive (env t: nat) :
>>
>>   @Reflexive (@Tm _ _) (@tmEq env t).
>>
>> Proof. intros x. destruct x. simpl. auto. Qed.
>>
>>
>>
>> (* This works fine *)
>>
>> Lemma REFLTEST (t: nat) (M: Tm (0+globEnv) t) : (@tmEq 0 t M M).
>>
>> Proof. setoid_reflexivity. Qed.
>>
>>
>>
>> (* This fails with
>>
>> Error: Tactic failure: The relation tmEq is not a declared reflexive
>> relation.
>>
>> Maybe you need to require the Setoid library.
>>
>> *)
>>
>> Lemma REFLTEST2 (t: nat) (M: Tm globEnv t) : (@tmEq 0 t M M).
>>
>> Proof. setoid_reflexivity. Qed.
>>
>>
>>
>>
>>
>> In essence, I have a "strongly-typed syntax", with terms parameterized
>> on an environment and a type, here, for simplicity, just nats. Then I
>> define a relation "tmEq", add an instance of Reflexive, and attempt to
>> prove a trivial equivalence using setoid_reflexivity. But note the
>> nat-computation inside the definition of tmEq. I would expect both
>> REFLTEST and REFLTEST2 to succeed, as they differ only by a simple 
>> reduction, but REFLTEST2 fails.
>>
>>
>>
>> Any ideas or pointers for help would be much appreciated. Although I
>> have a workaround (the first lemma), I spent a long time tracking it
>> down and I suspect the same thing might happen again in another
>> context. I'm using Coq 8.3.
>>
>>
>>
>> Cheers
>>
>> Andrew.
>