The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

Can anyone help me figure out how to do setoid_rewrite under binders underneath fold_left?  I have the following code, which doesn't work:

Require Import Coq.Lists.List Coq.Classes.Morphisms.

Require Import Coq.Program.Basics.

Require Import Coq.Program.Tactics.

Require Import Coq.Relations.Relation_Definitions.

Require Import Coq.Classes.RelationClasses.

Require Import Coq.Setoids.Setoid.

(** Element-wise lifting *)

Fixpoint elementwise_relation {A} (R : relation A) (ls1 ls2 : list A) {struct ls1} : Prop

  := match ls1, ls2 with

       | nil, nil => True

       | _, nil => False

       | nil, _ => False

       | x::xs, y::ys => R x y /\ elementwise_relation R xs ys

     end.

Local Ltac list_rel_t' :=

  idtac;

  match goal with

    | _ => solve [ eauto ]

    | [ |- forall ls : list ?T, _ ] => let ls := fresh "ls" in intro ls; induction ls

    | [ H : _ /\ _ |- _ ] => destruct H

    | [ |- _ /\ _ ] => split

    | _ => progress hnf

    | _ => progress simpl in *

    | _ => progress unfold subrelation, impl, predicate_implication, respectful in *

    | _ => intro

    | [ H : False |- _ ] => solve [ destruct H ]

    | _ => solve [ etransitivity; eauto ]

  end.

Local Ltac list_rel_t := repeat list_rel_t'.

Local Obligation Tactic := list_rel_t.

Global Program Instance elementwise_subrelation {A} {R R'} `(sub : subrelation A R R')

: subrelation (elementwise_relation R) (elementwise_relation R') | 4.

Typeclasses Opaque elementwise_relation.

Arguments elementwise_relation A%type R%signature (_ _)%list : clear implicits.

Program Instance elementwise_reflexive {A R} `{@Reflexive A R} : Reflexive (elementwise_relation A R).

Program Instance elementwise_symmetric {A R} `{@Symmetric A R} : Symmetric (elementwise_relation A R).

Program Instance elementwise_transitive {A R} `{@Transitive A R} : Transitive (elementwise_relation A R).

Program Instance elementwise_equivalence {A R} `{@Equivalence A R} : Equivalence (elementwise_relation A R).

Add Parametric Morphism A B R R' : (@List.map A B)

with signature (R ==> R') ==> elementwise_relation _ R ==> elementwise_relation _ R'

  as map_elementwise_mor.

Proof. list_rel_t. Qed.

Add Parametric Morphism A B R : (@List.map A B)

with signature (pointwise_relation _ R) ==> @eq (list A) ==> elementwise_relation _ R

  as map_elementwise_pointwise_mor.

Proof. list_rel_t. Qed.

Add Parametric Morphism A B R R' : (@fold_left A B)

with signature (R ==> R' ==> R) ==> elementwise_relation B R' ==> R ==> R

  as fold_left_mor.

Proof. list_rel_t. Qed.

Add Parametric Morphism A B R R' : (@fold_right A B)

with signature (R' ==> R ==> R) ==> R ==> elementwise_relation B R' ==> R

  as fold_right_mor.

Proof. list_rel_t. Qed.

Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.RelationPairs Coq.Lists.List.

Instance foo: forall {A B} (RA : relation A) `{Reflexive A RA} (R R' : relation B) `(@subrelation B R R'), subrelation (RA ==> R) (pointwise_relation A R').

Proof.

  lazy.

  auto.

Qed.

Section bar.

  Context A B (f g : A -> B -> A) (R : relation B) (R' : relation A)

          (H : (R' ==> R ==> R')%signature f g)

          `{@Reflexive _ R}

          `{@Transitive _ R}

          `{@Reflexive _ R'}

          `{@Transitive _ R'}

          (ls  : list B) C (b : C * A).

  Axiom admit : forall {T}, T.

  Add Parametric Morphism R' : (@fold_left B A)

      with signature (R ==> R' ==> R) ==> elementwise_relation A R' ==> R ==> R

        as foldl_mor.

  Proof. admit. Qed.

  Add Parametric Morphism R' : (@fold_left B A)

      with signature (R ==> R' ==> R) ==> elementwise_relation A R' ==> R ==> R

        as foldl_mor'.

  Proof. admit. Qed.

  Add Parametric Morphism R' : (@fold_left B A)

      with signature (R ==> R' ==> R) ==> @eq (list A) ==> (@eq _) ==> R

        as foldl_mor''.

  Proof. admit. Qed.

  Instance: Proper ((R' ==> R ==> R')%signature) f := admit.

  Instance: Proper ((R' ==> R ==> R')%signature) g := admit.

  Goal (eq * R')%signature (fold_left (fun cb v => (fst cb, f (snd cb) v)) ls b) (fold_left (fun cb v => (fst cb, g (snd cb) v)) ls b).

  Proof.

    setoid_rewrite -> H.

Thanks,

KAson