The Coq mailing list

[Andrew Kennedy <akenn AT microsoft.com>]

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.