The Coq mailing list

[Andrew Kennedy <akenn AT microsoft.com>]

OK, the issue I presented below has been "fixed" in Coq 8.4. But setoid 
rewriting is still very sensitive to reduction. Here's an extended example 
with morphisms. As before, the use of "simplification" in type arguments in 
the goal severely affects whether setoid rewriting works or not. Is this 
intended behaviour?

Cheers
Andrew.



Require Import Setoid Morphisms.

Inductive Tm (env: nat) : nat -> Type :=
  B : forall t, Tm env t
| C : forall t, Tm env t
| D : forall t, Tm env t -> Tm env t.

Definition globEnv := 5.

Variable tmEq : forall (env t: nat), Tm (env + globEnv) t -> Tm (env + 
globEnv) t -> Prop.

Global Instance ctxtEq_Equivalence (env t: nat) : 
  @Equivalence (Tm _ _) (tmEq env t).
Proof. Admitted.

Axiom BC : forall env t, tmEq env t (B _ _) (C _ _).  

Global Instance D_morphism (env t: nat) : 
  Proper ((tmEq env t) ==> (tmEq env t)) (D _ t).
Proof. Admitted.

(* This works fine *)
Lemma REFLTEST (t: nat) (M: Tm (0+globEnv) t) : (tmEq 0 t M M). 
Proof. setoid_reflexivity. Qed. 

(* This fails in Coq 8.3 with
Error: Tactic failure: The relation tmEq is not a declared reflexive 
relation. 
Maybe you need to require the Setoid library.

It works in Coq 8.4.
*)
Lemma REFLTEST2 (t: nat) (M: Tm globEnv t) : (tmEq 0 t M M). 
Proof. setoid_reflexivity. Qed.

(* This works fine. *)
Lemma REFLTEST3 (t: nat) : tmEq 0 t (D _ _ (B _ _)) (D _ _ (C _ _)). 
Proof. 
setoid_rewrite BC. 
setoid_reflexivity. 
Qed. 


(* This one does not *)
Lemma REFLTEST4 (t: nat) : tmEq 0 t (D _ _ (B _ _)) (D _ _ (C _ _)). 
Proof. 
simpl. 
setoid_rewrite BC. 
setoid_reflexivity. 
Qed. 

(* This one does not work. *)
Lemma REFLTEST5 (t: nat) : tmEq 0 t (D _ _ (B _ _)) (D _ _ (C _ _)). 
Proof.
apply D_morphism. simpl. 
setoid_rewrite BC.
setoid_reflexivity. 
Qed. 

(* This one does work. *)
Lemma REFLTEST6 (t: nat) : tmEq 0 t (D _ _ (B _ _)) (D _ _ (C _ _)). 
Proof.
apply D_morphism. simpl. 
setoid_rewrite (BC 0).
setoid_reflexivity. 
Qed.

-----Original Message-----
From: 
coq-club-request AT inria.fr
 
[mailto:coq-club-request AT inria.fr]
 On Behalf Of Andrew Kennedy
Sent: 23 November 2012 10:25
To: Thomas Braibant
Cc: coq-club
Subject: RE: [Coq-Club] Problem with setoid rewriting and reduction

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.