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).
*)
```