Confused with a failure of a generalized rewrite

Yannick · April 15, 2020, 10:17pm

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

Blaisorblade · April 21, 2020, 5:23pm

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.

Yannick · April 21, 2020, 8:54pm

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

mwuttke97 · April 21, 2020, 10:50pm

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.

Yannick · April 22, 2020, 1:49am

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.

Blaisorblade · April 22, 2020, 8:53pm

@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.

Blaisorblade · April 22, 2020, 9:51pm

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:

Yannick · April 23, 2020, 10:37pm

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

mattam82 · July 1, 2020, 2:17pm

The problem you face is that setoid_rewrite does not deal with partial applications, i.e. when rewriting in f x y it will try to rewrite f and if that fails, the arguments x and y, but it will not try the application f x. That’s why it reports “nothing to rewrite”, it does not even launch the right unification problem. That certainly can be fixed though!

Topic		Replies	Views
Problems rewriting with type valued relations Using Coq	4	360	January 7, 2023
Setoid rewriting with implications Using Coq	1	695	July 1, 2020
Parametric rewriting under binders Using Coq	0	650	March 3, 2021
Using Add Relation for Setoid equivalence of rationals Using Coq	0	467	April 26, 2022
How to compose setoid_rewrite? Using Coq	2	479	May 17, 2019

Confused with a failure of a generalized rewrite

Related Topics