Hi all! I have a datatype similar to the following:

```
Definition T : Set := ...
Inductive EqT : nat -> T -> T -> Prop :=
| EqT_refl t : EqT 0 t t
| EqT_sym e t1 t2 : EqT e t1 t2 -> EqT e t2 t1
| EqT_trans e1 e2 t1 t2 t3 : EqT e1 t1 t2 -> EqT e2 t2 t3 -> EqT (e1 + e2) t1 t3
| ...
```

My question is: is there a way to use `rewrite`

(or `setoid_rewrite`

) to automatically apply `EqT_trans`

? I am interested in reusing the generalized rewriting stuff, because I have operations on `T`

that interact nontrivially with the `e`

index, and I would like to reuse the `Morphism`

machinery if possible. For example:

```
Definition op : T -> T -> T := ...
Check (EqT_op). (* forall t1 t2 t3 e, EqT (e_op e t3) t1 t2 -> EqT e (op t1 t3) (op t2 t3) *)
(* some instance of Proper for op *)
```

If I could do the following, this would be ideal:

```
(* Goal is EqT e (op t1 t3) t4 *)
(* Hypothesis H = EqT e' t1 t2 *)
rewrite H.
(* Goal is EqT e'' (op t2 t3) t4, with appropriate side conditions on e, e', and e'' derived from EqT_op and EqT_trans *)
```

Thanks!

It’s possible. To use EqT_trans etc, declare an instance proving that EqT n is an Equivalence. For other operations, declare the appropriate Proper instances. Are you asking how to use setoid rewriting at all, or are you wondering if the n index adds problems? I think it doesn’t; https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris/algebra/ofe.v#L15 is an indexed equivalence used extensively in a large ecosystem.

Thanks for the link! But `EqT n`

is not an equivalence, right? Since it is not the case that `EqT n`

is not transitive (the `n`

parameter adds up). But using type class resolution to perform the rewriting makes sense.

@Joshua Gancher ugh, apologies; seems I needed more coffee.

I _think_ you can still give instances for `Reflexive (EqT 0)`

and `Symmetric (EqT e)`

, right?

For `EqT_trans`

, I wonder if one could state that `EqT e`

is Proper over `EqT`

— but I wouldn't know how to write that statement because of the changing index...

Yes, the instances for reflexive and symmetric work well. I kind of think I need support for a dependent version of `==>`

, since `op`

changes the index, and does so depending on its operand..

I solved the problem by leveraging type class resolution. Feel free to message me if interested

Joshua Gancher has marked this topic as resolved.

I'm actually curious since I've wanted a dependent Proper at times, and never thought it was possible!

You can do dependent `Proper`

like this (though this particular instance isn't provable):

```
Axiom T : Set.
Inductive EqT : nat -> T -> T -> Prop :=
| EqT_refl t : EqT 0 t t
| EqT_sym e t1 t2 : EqT e t1 t2 -> EqT e t2 t1
| EqT_trans e1 e2 t1 t2 t3 : EqT e1 t1 t2 -> EqT e2 t2 t3 -> EqT (e1 + e2) t1 t3
.
Require Import Coq.Setoids.Setoid.
Require Import Coq.Classes.Morphisms.
Print "==>"%signature.
Definition ExistsR {A B} (R : A -> relation B) : relation B := fun f g => exists a : A, R a f g.
Definition ExistsRST {A B} (P : A -> Prop) (R : A -> relation B) : relation B := fun f g => exists a : A, P a /\ R a f g.
Definition ForallR {A B} (R : A -> relation B) : relation B := fun f g => forall a : A, R a f g.
Definition ForallRST {A B} (P : A -> Prop) (R : A -> relation B) : relation B := fun f g => forall a : A, P a -> R a f g.
Global Instance:
Proper
(forall_relation
(fun e1pe2
=> ForallR (fun e1 => ForallRST (fun e2 => e1pe2 = e1 + e2) (fun e2 => EqT e1 ==> EqT e2 ==> Basics.impl))))%signature
EqT.
```

Last updated: Jun 25 2024 at 15:02 UTC