Problems rewriting with type valued relations

Using Coq
1

Hello! I’m trying to define relations as "Type"s so that the values are not erased like values of "Prop"s are. I also want to use rewriting rules, eventually including rewriting under binders. I’ve successfully done this using Prop valued relations, but am having trouble with Type valued relations even without trying to rewrite under binders. I found a brief section on the website [1] describing rewriting with type valued relations but it doesn’t go into details.

[1] Generalized rewriting — Coq 8.16.1 documentation

My first attempt was to use “Add Parametric Morphism”, but this command fails with a universe inconsistency before entering proof mode. I guess that just means the command only works for prop valued relations.

I then tried creating instances of Proper directly. This works in some cases but not others and I don’t understand why. Maybe I’m supposed to be doing something else instead.

I pasted a cut-down example below and the commands marked with Fail do indeed fail for me with the messages I included. I’m trying to prove theorem attempt_1 using rewrite rules. It may seem pointless, but this is a cut-down example.

Any help would be appreciated.

Neil.

Require Setoid.
Require Import Coq.Classes.CMorphisms.
Require Import Coq.Classes.CRelationClasses.

(* These is my operator.  It's duplicated to make attempt_2 and
   attempt_3 independent. *)
Definition t_not (P:Type): Type := P -> False.
Definition t_not_2 := t_not.

(* This is my relation. *)
Definition c_impl (P Q:Type): Type := t_not (t_not (P -> Q)).

Instance c_impl_refl: Reflexive c_impl.
Proof.
  intros P [].
  intros H0; apply H0.
Qed.

Instance c_impl_trans: Transitive c_impl.
Proof.
  intros P Q R H0 H1 H2.
  destruct H0; intros H0.
  destruct H1; intros H1.
  destruct H2; intros H2.
  apply H1, H0, H2.
Qed.

(* It seems this command only works with Prop valued relations. *)
Fail Add Parametric Relation: Type c_impl
  reflexivity proved by c_impl_refl
  transitivity proved by c_impl_trans
  as c_impl_rel.
(*
The command has indeed failed with message:
The term "c_impl" has type "Type -> Type -> Type"
while it is expected to have type "Relation_Definitions.relation Type"
(universe inconsistency: Cannot enforce c_impl.u2 <= Prop).
*)

(* The arrow relation implies c_impl. *)
Instance arrow_c_impl_subrel: subrelation arrow c_impl.
Proof.
  intros P0 P1 HP [].
  intros H0.
  apply HP, H0.
Qed.

(* A first attempt. *)
Global Instance t_not_mor:
  Proper (c_impl --> arrow) t_not.
Proof.
  intros P Q H H0 H1.
  destruct H; intros H.
  apply H0, H, H1.
Qed.

Theorem attempt_1: forall P Q:Type,
  (arrow Q P) ->
  (arrow (t_not P) (t_not Q)).
Proof.
  intros P Q H.
  (* H : arrow Q P *)
  (* I would expect the following command to find the subrelation and
     morphism, but it doesn't. *)
  Fail rewrite -> H.
(*
The command has indeed failed with message:
Tactic failure: setoid rewrite failed: Unable to satisfy the following constraints:
UNDEFINED EVARS:
 ?X23==[P Q H |- crelation Type] (internal placeholder) {?c}
 ?X24==[P Q H (do_subrelation:=do_subrelation)
         |- Proper (arrow ==> ?c) t_not] (internal placeholder) {?p}
 ?X25==[P Q H (do_subrelation:=do_subrelation)
         |- Proper (?c ==> flip arrow) (arrow (t_not P))]
         (internal placeholder) {?p0}
TYPECLASSES:?X23 ?X24 ?X25
.
*)
  pose (H0 := arrow_c_impl_subrel _ _ H).
  (* H0 : c_impl Q P *)
  (* We can rewrite using c_impl Q P so the problem is something to
     do with the subrelation. *)
  rewrite -> H0.
  reflexivity.
Qed.

(* A second attempt using a different morphism. *)
Global Instance t_not_2_mor:
  Proper (flip c_impl --> flip arrow) t_not_2.
Proof.
  unfold t_not_2.
  intros P Q H.
  rewrite -> H.
  reflexivity.
Qed.

Theorem attempt_2: forall P Q:Type,
  (arrow Q P) ->
  (arrow (t_not_2 P) (t_not_2 Q)).
Proof.
  intros P Q H.
  (* The following command succeeds because the t_not_2 morphism includes
     flip. *)
  rewrite -> H.
  reflexivity.
Qed.

(* A third attempt using the original morphism but a different
   subrelation. *)
Instance flip_arrow_c_impl_subrel: subrelation (flip arrow) (flip c_impl).
Proof.
  intros P0 P1 HP.
  rewrite -> HP.
  reflexivity.
Qed.

Theorem attempt_3: forall P Q:Type,
  (arrow Q P) ->
  (arrow (t_not P) (t_not Q)).
Proof.
  intros P Q H.
  rewrite -> H.
  reflexivity.
Qed.

Edit: I also tried Add Parametric Morphism:

Fail Add Parametric Morphism: t_not with signature
  (c_impl --> arrow) as t_not_mor_1.
(*
The command has indeed failed with message:
The term "(c_impl --> arrow)%signature" has type "crelation (Type -> Type)"
while it is expected to have type
 "Relation_Definitions.relation (Type -> Type)"
(universe inconsistency: Cannot enforce Top.12407 = Prop because Prop < Set
< t_not.u1 <= c_impl.u2 <= Top.12411 <= Top.12403 <= Top.12407).
*)
2

After some more experiments, it looks like this problem is more to do with subrelations than with the relations being type valued. I changed the example to use Prop instead of Type and impl instead of arrow; It still failed. The rewrite succeeds when the theorem’s proposition is changed to use c_impl rather than arrow as below.

Theorem attempt_1: forall P Q:Type,
  (c_impl Q P) ->
  (c_impl (t_not P) (t_not Q)).

My current hypothesis is that where there is an instance of Proper with a signature like (rel_1 → rel_2), subrelations will only be used to change rel_2, not rel_1. Maybe it’s more subtle than that.

3

I have an example which works with relations but not with crelations. Is that a bug?

The rewrite command below does fail as written, but removing the Cs before Morphisms and RelationClasses results in it succeeding.

Require Import Basics.
Require Import Classes.CMorphisms.
Require Import Classes.CRelationClasses.
Require Setoid.

Definition prop := Prop.

Definition rel (P Q:prop): prop := P -> Q.

Definition op (P Q:prop): prop := and P Q.

Instance rel_refl: Reflexive rel.
Proof.
  intros P H; apply H.
Qed.

Instance rel_trans: Transitive rel.
Proof.
  intros P Q R H0 H1 H2.
  apply H1, H0, H2.
Qed.

Instance impl_rel_subrel: subrelation impl rel.
Proof.
  intros P Q H0.
  apply H0.
Qed.

Instance op_mor: Proper (rel ++> rel ++> impl) op.
Proof.
  intros P0 P1 HP Q0 Q1 HQ [H0 H1].
  split.
  + apply HP, H0.
  + apply HQ, H1.
Qed.

Theorem attempt_1: forall P Q R S:prop,
  (rel P Q) ->
  (op (op P R) S) ->
  (op (op Q R) S).
Proof.
  intros P Q R S H0 H1.
  Fail rewrite -> H0 in H1.
(*
The command has indeed failed with message:
Tactic failure: setoid rewrite failed: Unable to satisfy the following constraints:
UNDEFINED EVARS:
 ?X26==[P Q R S H0 H1 |- Relation_Definitions.relation prop]
         (internal placeholder) {?r}
 ?X27==[P Q R S H0 H1 |- Relation_Definitions.relation prop]
         (internal placeholder) {?r0}
 ?X28==[P Q R S H0 H1 (do_subrelation:=Morphisms.do_subrelation)
         |- Morphisms.Proper
              (Morphisms.respectful rel (Morphisms.respectful ?r0 ?r)) op]
         (internal placeholder) {?p}
 ?X29==[P Q R S H0 H1 |- Morphisms.ProperProxy ?r0 R] (internal placeholder) {?p0}
 ?X30==[P Q R S H0 H1 |- Relation_Definitions.relation prop]
         (internal placeholder) {?r1}
 ?X31==[P Q R S H0 H1 (do_subrelation:=Morphisms.do_subrelation)
         |- Morphisms.Proper
              (Morphisms.respectful ?r (Morphisms.respectful ?r1 impl)) op]
         (internal placeholder) {?p1}
 ?X32==[P Q R S H0 H1 |- Morphisms.ProperProxy ?r1 S] (internal placeholder) {?p2}
TYPECLASSES:?X26 ?X27 ?X28 ?X29 ?X30 ?X31 ?X32
.
*)
  trivial.
  eapply op_mor; [|apply rel_refl|apply H1].
  eapply op_mor; [|apply rel_refl].
  apply H0.
Qed.
4

First if you want to work with relations with output in Prop (relation) you should use Morphisms, RelationClasses, etc. If you want to work with relations with output in Type (crelation) you should use the C-versions: CMorphisms, CRelationClasses, etc.
With your last example it gives:

Require Import Classes.Morphisms.
Require Setoid.

Definition prop := Prop.

Definition rel (P Q:prop): prop := P -> Q.

Definition op (P Q:prop): prop := and P Q.

#[local]
Instance rel_refl: Reflexive rel.
Proof.
  intros P H; apply H.
Qed.

#[local]
Instance op_mor: Proper (rel ++> rel ++> Basics.impl) op.
Proof.
  intros P0 P1 HP Q0 Q1 HQ [H0 H1].
  split.
  + apply HP, H0.
  + apply HQ, H1.
Qed.

Theorem attempt: forall P Q R S:prop,
  (rel P Q) ->
  (op (op P R) S) ->
  (op (op Q R) S).
Proof.
  intros P Q R S H0 H1.
  rewrite -> H0 in H1.
  exact H1.
Qed.

and

Require Import Classes.CMorphisms.
Require Setoid.

Definition prop := Type.

Definition rel (P Q:prop): prop := P -> Q.

Definition op (P Q:prop): prop := prod P Q.

#[local] Instance op_mor: Proper (rel ++> rel ++> arrow) op.
Proof.
  intros P0 P1 HP Q0 Q1 HQ [H0 H1].
  split.
  + apply HP, H0.
  + apply HQ, H1.
Qed.

Theorem attempt: forall P Q R S:prop,
  (rel P Q) ->
  (op (op P R) S) ->
  (op (op Q R) S).
Proof.
  intros P Q R S H0 H1.
  rewrite -> H0 in H1.
  exact H1.
Qed.

However it is not clear to me why the Prop case requires the Reflexive rel instance but not the Type case.

Second there are situations where rewriting with Type does not work as well as rewriting in Prop.

5

Thanks for the response. It helps to know that there are open issues with rewriting in Type.