coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Matthieu Sozeau <matthieu.sozeau AT gmail.com>
- To: Andrew Kennedy <akenn AT microsoft.com>
- Cc: Thomas Braibant <thomas.braibant AT gmail.com>, coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Problem with setoid rewriting and reduction
- Date: Mon, 26 Nov 2012 13:23:06 -0500
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.
>
>
- [Coq-Club] Problem with setoid rewriting and reduction, Andrew Kennedy, 11/23/2012
- Re: [Coq-Club] Problem with setoid rewriting and reduction, Thomas Braibant, 11/23/2012
- RE: [Coq-Club] Problem with setoid rewriting and reduction, Andrew Kennedy, 11/23/2012
- Re: [Coq-Club] Problem with setoid rewriting and reduction, Thomas Braibant, 11/23/2012
- RE: [Coq-Club] Problem with setoid rewriting and reduction, Andrew Kennedy, 11/26/2012
- Re: [Coq-Club] Problem with setoid rewriting and reduction, Matthieu Sozeau, 11/26/2012
- RE: [Coq-Club] Problem with setoid rewriting and reduction, Andrew Kennedy, 11/27/2012
- Re: [Coq-Club] Problem with setoid rewriting and reduction, Matthieu Sozeau, 11/26/2012
- RE: [Coq-Club] Problem with setoid rewriting and reduction, Andrew Kennedy, 11/23/2012
- Re: [Coq-Club] Problem with setoid rewriting and reduction, Thomas Braibant, 11/23/2012
Archive powered by MHonArc 2.6.18.