Confused with a failure of a generalized rewrite

Dear Coq hacker,

I thought I had a decent grip on generalized rewriting, but found myself lost on a very simple case once again Today. Consider the following minimal example inlining the problem:

From Coq Require Import
     Morphisms
     Setoid.

(* We are currently working with heterogeneous relations *)
Definition relation (A B : Type) := A -> B -> Prop.

(* We work with our relations up-to extensional equality *)
Definition subrel {A B} (R S : relation A B) : Prop :=
  forall (x : A) (y : B), R x y -> S x y.
Definition eq_rel {A B} (R : A -> B -> Prop) (S : A -> B -> Prop) :=
  subrel R S /\ subrel S R.
Infix "≡" := eq_rel (at level 89, no associativity).

(* My problem is quite trivial: since this notion of equivalence of relations is basically double pointwise [iff],
   I want to be able to rewrite it as such.
   So for instance consider the following idiotic goal:
 *)
Goal forall {A B: Type} (R S: relation A B) x y,
    R ≡ S -> S x y -> R x y.
Proof.
  intros A B R S x y EQ H.
  (* We want to rewrite EQ, which of course fails without help *)
  Fail rewrite EQ.
Abort.

(* It's a bit of a different case from my usual [Proper] instances, but the error message nicely tells me what's needed:
   [eq_rel] is indeed a subrelation of pointwise iff.
 *)
Instance eq_rel_rewrite {A B}: subrelation eq_rel (pointwise_relation A (pointwise_relation B iff)).
Proof.
  repeat intro; destruct H; split; intro; [apply H | apply H0]; auto.
Qed.

Goal forall {A B: Type} (R S: relation A B) x y,
    R ≡ S -> S x y -> R x y.
Proof.
  intros A B R S x y EQ H.
  (* And indeed things works nicely *)
  rewrite EQ.
  exact H.
Qed.

(* Now here is where I get confused. Consider the transpose operation that flips a relation *)
Definition transpose {A B: Type} (R: A -> B -> Prop): B -> A -> Prop :=
  fun b a => R a b.
Notation "† R" := (transpose R) (at level 5).

(* I have a morphism on relations that commutes with [transpose], and want to rewrite this equation *)
Goal
  forall (A B : Type) (R : relation A B) (F: forall {A B}, (A -> B -> Prop) -> (A -> B -> Prop)) x y,
    F († R) ≡ † (F R) ->
    † (F R) x y ->
    F († R) x y.
Proof.
  intros.
  rename H into EQ.
  (* It is as far as I can tell, the exact same situation as previously, but with
     [R] = [F †R] and [S] = [† (F R)]
     Yet, it now fails:
   *)
  Fail rewrite EQ. (* Tactic failure: Nothing to rewrite. *)
  Fail setoid_rewrite EQ. (* Tactic failure: setoid rewrite failed: Nothing to rewrite. *)
  (* I fail to see what is the issue. Can anyone help me out? *)
Abort.

Thanks a bunch in advance!
Best,
Yannick

P.S. : This is on 8.10.2

f ≡ g doesn’t imply f x ≡ g x for an arbitrary , even tho it does for yours. My usual fix for such issues would give rewrite (EQ _ _) here, but that assumes the following definition for eq_rel.

Definition eq_rel {A B} (R : A -> B -> Prop) (S : A -> B -> Prop) :=
  forall (x : A) (y : B), R x y <-> S x y.

I’ve run into similar issues before and discussed them in: Extensional setoids on functions, and rewriting.

Hi @Blaisorblade ,

Thanks a lot for your answer!
However, as much as this connex question is also very much of interest to me as well, I do not believe it to be directly related to this issue at hand.

The instance eq_rel_rewrite does allow extensional rewriting in this context, which actually is what happens in the first Goal (I rewrite R ≡ S in the goal R x y by virtue of the pointwise_relation part of the instance).

The failure is the exact same case, but instantiated with slightly more complex “R” and “S”. The equation F († R) ≡ † (F R) is already in my context, I do not need to derive it.

Best,
Yannick

Hi, an intermediate solution is by abstraction (and thus reduction to the first case):

Proof.
  intros * EQ H.
  change ((fun x y => F B A † R x y) ≡ † (F A B R)) in EQ.
  change ((fun x y => F B A † R x y) x y).
  rewrite EQ. exact H.
Qed.

Oh I see, thanks! This solution is certainly impractical as is, but it helped me understand much better the issue, and how indeed it is related to the other thread.

To be certain though, the problem has to do with the difficulty for the rewrite tactic to parse the goal as the appropriate function application for it to trigger the search for the appropriate pointwise_relation ... instance in the first place. But the rewrite would be valid for any relation, assuming only the existence of one such instance. The smaller, more abstract, example below show cases this I believe.

Section Abstract.

  Definition D (A: Type) := A -> Prop.
  Variable eqD: forall {A: Type}, (A -> Prop) -> (A -> Prop) -> Prop.

  Context {proper: forall {A}, subrelation eqD (pointwise_relation A iff)}.

  Infix "≡" := eqD (at level 89, no associativity).

  Goal forall {A: Type} (P Q: D A) x,
      Q ≡ P -> P x -> Q x.
  Proof.
    intros * EQ H.
    rewrite EQ.
    exact H.
  Qed.

  Variable F G: forall {A} (P: D A), D A.

  Goal
    forall (A : Type) (P : D A) x,
      F (G P) ≡ G (F P) ->
      G (F P) x ->
      F (G P) x.
  Proof.
    intros * EQ H.
    Fail rewrite EQ.
    change ((fun x => F (G P) x) ≡ G (F P)) in EQ.
    change ((fun x => F (G P) x) x).
    rewrite EQ.
    exact H.
  Qed.

End Abstract.

It intuitively (naively maybe?) feels like the type of EQ should contain enough information to automate this process. I’ll get back to reading the other thread now that the situation is clearer in my mind.

Best,
Yannick

EDIT: What I meant by having intuitively enough information is this dirty piece of Ltac I guess:

  Ltac super_rewrite EQ :=
    match type of EQ with
    | ?T ≡ ?T' =>
      match type of T with
      | Prop => rewrite EQ
      | Type => rewrite EQ
      | _ -> Prop =>
        change ((fun x => T x) ≡ T') in EQ;
        match goal with
          |- _ ?x => change ((fun x => T x) x)
        end
      end
    end;
    rewrite EQ.

@Yannick Found a solution for your reduced example. You’re right, my link is likely not relevant, and your subrelation instance might be a solution to the problem there.

Instead, your problem seems to be with unification — I’m guessing that somewhere, rewrite checks your goal contains an application by unifying ?f ?x against F (G P) x; while solving ?f = F (G P) might seem easy, in general this is an instance of higher-order unification, which is famously undecidable and which Coq approximates.

I’m surprised that your case is a problem, but ssreflect’s rewrite fixes it by using Coq’s new unification algorithm. The fix for the first example takes two lines:

From Coq.ssr Require Import ssreflect.
Context `{rew: forall {A: Type}, RewriteRelation (@eqD A)}. (* Because ssreflect's rewrite requires such an instance to recognize rewritable relations, unless it's implied by other instances. *)

EDIT: This also works for the second example (with one more instance for RewriteRelation); complete code appended below.

FWIW, you can select the base Coq’s rewrite tactic with rewrite -> H instead of rewrite H, but usually ssreflect’s one is better.

Complete code:

From Coq Require Import Morphisms Setoid.
From Coq.ssr Require Import ssreflect.
Section Abstract.

  Definition D (A: Type) := A -> Prop.
  Variable eqD: forall {A: Type}, (A -> Prop) -> (A -> Prop) -> Prop.

  Context {proper: forall {A}, subrelation eqD (pointwise_relation A iff)}.
  Context `{rew: forall {A: Type}, RewriteRelation (@eqD A)}.

  Infix "≡" := eqD (at level 89, no associativity).

  Goal forall {A: Type} (P Q: D A) x,
      Q ≡ P -> P x -> Q x.
  Proof.
    intros * EQ H.
    rewrite EQ.
    exact H.
  Qed.

  Variable F G: forall {A} (P: D A), D A.

  Goal
    forall (A : Type) (P : D A) x,
      F (G P) ≡ G (F P) ->
      G (F P) x ->
      F (G P) x.
  Proof.
    intros * EQ H.
    rewrite EQ.
    exact H.
  Qed.

End Abstract.

(* We are currently working with heterogeneous relations *)
Definition relation (A B : Type) := A -> B -> Prop.

(* We work with our relations up-to extensional equality *)
Definition subrel {A B} (R S : relation A B) : Prop :=
  forall (x : A) (y : B), R x y -> S x y.
Definition eq_rel {A B} (R : A -> B -> Prop) (S : A -> B -> Prop) :=
  subrel R S /\ subrel S R.
Infix "≡" := eq_rel (at level 89, no associativity).

(* My problem is quite trivial: since this notion of equivalence of relations is basically double pointwise [iff],
   I want to be able to rewrite it as such.
   So for instance consider the following idiotic goal:
 *)
Goal forall {A B: Type} (R S: relation A B) x y,
    R ≡ S -> S x y -> R x y.
Proof.
  intros A B R S x y EQ H.
  (* We want to rewrite EQ, which of course fails without help *)
  Fail rewrite EQ.
Abort.

(* It's a bit of a different case from my usual [Proper] instances, but the error message nicely tells me what's needed:
   [eq_rel] is indeed a subrelation of pointwise iff.
 *)
Instance eq_rel_rewrite {A B}: subrelation eq_rel (pointwise_relation A (pointwise_relation B iff)).
Proof.
  repeat intro; destruct H; split; intro; [apply H | apply H0]; auto.
Qed.
Instance rewrite_eq_rel {A B}: RewriteRelation (@eq_rel A B) := {}.

Goal forall {A B: Type} (R S: relation A B) x y,
    R ≡ S -> S x y -> R x y.
Proof.
  intros A B R S x y EQ H.
  (* And indeed things works nicely *)
  rewrite EQ.
  exact H.
Qed.

(* Now here is where I get confused. Consider the transpose operation that flips a relation *)
Definition transpose {A B: Type} (R: A -> B -> Prop): B -> A -> Prop :=
  fun b a => R a b.
Notation "† R" := (transpose R) (at level 5).

(* I have a morphism on relations that commutes with [transpose], and want to rewrite this equation *)
Goal
  forall (A B : Type) (R : relation A B) (F: forall {A B}, (A -> B -> Prop) -> (A -> B -> Prop)) x y,
    F († R) ≡ † (F R) ->
    † (F R) x y ->
    F († R) x y.
Proof.
  intros * EQ H.
  (* It is as far as I can tell, the exact same situation as previously, but with
     [R] = [F †R] and [S] = [† (F R)]
     Yet, it now fails:
   *)
  Fail setoid_rewrite EQ. (* Tactic failure: setoid rewrite failed: Nothing to rewrite. *)

  rewrite EQ.
  exact H.
Qed.

PS: Thanks @Yannick for finding out this trick — it seems to fix my original issue (pending more extensive testing, also for performance) so I plan to contribute this to the library where I run into this. I credited you in the relevant issue:

Hey @Blaisorblade,

Thanks a lot for this ssreflect-based solution! It is a bit frustrating to have these three incomparable rewrite tactics at the moment, but I’ll give a shot at systematizing the use of ssreflect’s implementation in our code base and see what happens.

Glad the discussion has also benefited you by side-effect :slight_smile:

1 Like