coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Strange behavior of right-to-left setoid rewriting

From: Armaël Guéneau <armael.gueneau AT ens-lyon.fr>
To: coq-club AT inria.fr
Subject: [Coq-Club] Strange behavior of right-to-left setoid rewriting
Date: Thu, 26 Jan 2017 17:51:04 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=armael.gueneau AT ens-lyon.fr; spf=Pass smtp.mailfrom=armael.gueneau AT ens-lyon.fr; spf=None smtp.helo=postmaster AT labbe.ens-lyon.fr
Ironport-phdr: 9a23:R//aTBO579LRifkoXWsl6mtUPXoX/o7sNwtQ0KIMzox0Lfn5rarrMEGX3/hxlliBBdydsKMYzbeL+PG7EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQtFiT6ybL9oLBi7rQrdu80YjIB/Nqs/1xzFr2dSde9L321oP1WTnxj95se04pFu9jlbtuwi+cBdT6j0Zrw0QrNEAjsoNWA1/9DrugLYTQST/HscU34ZnQRODgPY8Rz1RJbxsi/9tupgxCmXOND9QL4oVTi+6apgVRnlgzoFOTEk6mHaktJ+gqJGrhyiqRJwzYHbb52OOfp7Yq/QZ8kXSXZPU8tTUSFKH4Oyb5EID+oEJetVs5P9p14UohyiAQmjHOLhyiJSgX/ww6I1yfkhGhzB0QM6BdIOtW7bo8vxNKsIXuC10bfHzTPdYPxMxDfw85bHchY6of2VWbJxcc3RyU81GwPLlFWdsIroNC6W2OQVq2WX8uVtWf61h2MlqQx9uCWjy8Yuh4XTmI4Z1E7I+T1kzIorJtC0Ukp2bNC+HJZRtiyWLYV7T8U/SG9yoik60KcJuZujcSgK1psnwxnfZuSDc4eS+R3sT/ieLS1mi3JjY7KznhKy8Einyu36TMW03kxKojJEktnKqH8NywTe5tWIR/dh5Eus2zSC2xrO5uxFI004j7TXJ4A/zrIok5ocq0XDHiv4mEXsi6+Wc10p9fKy6+TieLrpuJucO5V7igHjLKsunNKwDv4lMgUVQWeb//+82KTn/Uz5R7VKiOc6kqfDsJzCP8QUura5AxNJ0oYk8xuwEzCm0M0BkXYbKFJFZQmIgpPyO1DOJfD4Fe2wj06tkDdt3fDGP6fuDo/DLnjZw//deuN27FcZww4ux/he4YhVA/cPOqHdQEj04fXCCxa6Nzub3mfhBdxgntcXQ2eGD6vfP77ft1KB+8oiJfLJYJ4SvnDzMa52tLbVkXYllApFLuGS1pwNZSXgEw==

Hi all,

I'm observing a weird behavior of setoid rewrite, while trying to
rewrite using a custom reflexive, transative relation. The rewriting
doesn't involve any Proper instance, it AFAICT only boils down to
transitivity.

Basically, it works left-to-right, but not right-to-left. I think the
minimal example that follows (also attached) describes best the issue.

Is this a normal behavior? Is there a way to make it work?

Cheers,
Armaël

Require Import Coq.Setoids.Setoid.

Parameter myrel : nat -> nat -> Prop.
Parameter myrel_reflexive : forall a, myrel a a.
Parameter myrel_transitive : forall a b c, myrel a b -> myrel b c ->
myrel a c.

Add Relation nat myrel
reflexivity proved by myrel_reflexive
transitivity proved by myrel_transitive
as myrel_preorder.

Parameter lemma : forall a b, myrel a b.

Goal forall a c, myrel a c.
intros a c.
rewrite lemma. (* works, replaces [a] by an evar. *) Undo.
rewrite lemma. rewrite <-lemma. (* works (??!), replaces [a] then [c]
by evars. *) Undo. Undo.
rewrite <-lemma. (* doesn't work. *)

(* The following works, as a workaround, but is annoying to use, and
requires writing [c] (which may be big) in the proof script. *)
rewrite <-lemma with (b := c).

Abort.

Require Import Coq.Setoids.Setoid.

Parameter myrel : nat -> nat -> Prop.
Parameter myrel_reflexive : forall a, myrel a a.
Parameter myrel_transitive : forall a b c, myrel a b -> myrel b c -> myrel a c.

Add Relation nat myrel
  reflexivity proved by myrel_reflexive
  transitivity proved by myrel_transitive
  as myrel_preorder.

Parameter lemma : forall a b, myrel a b.

Goal forall a c, myrel a c.
intros a c.
rewrite lemma. (* works, replaces [a] by an evar. *) Undo.
rewrite lemma. rewrite <-lemma. (* works (??!), replaces [a] then [c] by evars. *) Undo. Undo.
rewrite <-lemma. (* doesn't work. *)


(* The following works, as a workaround, but is annoying to use, and requires
   writing [c] (which may be big) in the proof script. *)
rewrite <-lemma with (b := c).

Abort.

[Coq-Club] Strange behavior of right-to-left setoid rewriting, Armaël Guéneau, 01/26/2017