The Coq mailing list

[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