The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

On 26 nov. 2012, at 10:42, Andrew Kennedy 
<akenn AT microsoft.com>
 wrote:

> 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 behavior?

Sadly, it's the best I know how to do for now. Your rewrite fails because to 
apply D_morphism in your example 4 (after simpl)
we must unify:

  @Proper (Tm (plus ?440 globEnv) ?441 -> Tm (plus ?440 globEnv) ?441)
    (@respectful (Tm (plus ?440 globEnv) ?441) (Tm (plus ?440 globEnv) ?441)
       (tmEq ?440 ?441) (tmEq ?440 ?441)) (D (plus ?440 globEnv) ?441)

which comes from D_morphism and

  @Proper (Tm globEnv t -> Tm globEnv t)
    (@respectful (Tm globEnv t) (Tm globEnv t) (tmEq O t) ?98) 
    (D globEnv t)

which is the constraint that is inferred from the goal. Unification of 
applications
goes left to right and (plus ?440 globEnv) = globEnv cannot be resolved hence 
unification fails. It could work only with postponing of constraints, waiting 
for 
the unification of types (tmEq ?440 ?441) and (tmEq 0 t) to succeed.

The changes needed to use postponing are probably not that large but I've not 
done 
it because of backward compatibility issues…

In the meantime, you can have a special instance for D like the following, 
which 
uses refine and forces the information from env to instantiate the ?440 
metavariable
above.

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

Hint Extern 0 (@Proper _ (tmEq ?env _ ==> _) (D _ _)) =>
  refine (@D_morphism env _) : typeclass_instances.

Then [rewrite (BC 0)] will succeed.
-- Matthieu

> 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.
> 
>