The Coq mailing list

[Andrew Kennedy <akenn AT microsoft.com>]

Hi Matthieu

Thanks very much for the detailed response and suggested fix! Yes, I can see 
it's difficult to get the design right. In the full development from which I 
distilled this example, there were implicits everywhere so I couldn't even 
see the changes that "simpl" was making - and Set Printing All just (as 
usual) presented me with alphabet soup. 

Anyhow, I'd like to encourage you to develop the setoid rewriting feature 
further as it's very useful but somewhat undocumented and hard to debug. 
Backwards compatibility issues have never stopped Coq developments in the 
past, as many of us know to our cost :-)

Cheers
Andrew.

-----Original Message-----
From: Matthieu Sozeau 
[mailto:matthieu.sozeau AT gmail.com]
 
Sent: 26 November 2012 18:23
To: Andrew Kennedy
Cc: Thomas Braibant; coq-club
Subject: Re: [Coq-Club] Problem with setoid rewriting and reduction


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