The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi,

  this is indeed desirable and doable but cannot be performed with the current generalized rewriting

machinery. Technically, one needs to change the rule Lambda on p12 of http://jfr.unibo.it/article/view/1574/1077

to produce a ==> relation instead of a pointwise equivalence and do multiple rewrites 

at the same time recursively, i.e rewrite the body (f x /\ H) under the context (x x' : A) (Hx : ?R x x')

in general, logical-relation style. I'd be happy to guide anyone who wants to implement this :)

Best,

-- Matthieu

2015-04-08 20:32 GMT+02:00 Jason Gross <jasongross9 AT gmail.com>:

Hi,

What instances to I need to add to the environment to make this example work?

Require Import Coq.Setoids.Setoid Coq.Lists.List Coq.Program.Basics Coq.Classes.Morphisms.

Global Instance fold_right_flip_impl {A}

: Proper 

    (pointwise_relation A (flip impl ==> flip impl) ==> flip impl ==> eq ==> flip impl)

    (@fold_right _ A).

Proof.

  intros ??????? ls ?; subst.

  induction ls; simpl; trivial.

  unfold flip, impl, pointwise_relation, respectful in *.

  eauto.

Qed.

Goal forall A f g ls, (forall x : A, f x <-> g x) -> fold_right (fun x H => f x /\ H) True ls.

Proof.

  intros A f g ls H.

  Typeclasses eauto := debug.

  try timeout 2 setoid_rewrite H.

It seems that it gets stuck on trying to find an instance for

  (Proper

   (pointwise_relation A (pointwise_relation Prop iff) ==>

    ?92 ==> ?91 ==> flip impl) (fold_right (B:=A)))

and rightly fails.  But this transformation is possible, as the following tactic shows:

  cut (fold_right (fun x H => g x /\ H) True ls);

    [ induction ls; simpl in *; trivial; [];

      intros [H0' H1']; split; try apply H; eauto

    | ].

Show how to I get [setoid_rewrite] to consider [pointwise_relation A (R ==> iff)] for an arbitrary [Reflexive] [R], rather than just for [R] being [eq]?

Thanks,

Jason