Stream: Coq users

Topic: ✔ Indexed generalized rewriting

Joshua Gancher (Jul 31 2021 at 15:51):

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!

Paolo Giarrusso (Jul 31 2021 at 16:27):

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.

Joshua Gancher (Jul 31 2021 at 20:07):

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.

Paolo Giarrusso (Aug 01 2021 at 14:44):

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

Paolo Giarrusso (Aug 01 2021 at 14:44):

I _think_ you can still give instances for Reflexive (EqT 0) and Symmetric (EqT e), right?

Paolo Giarrusso (Aug 01 2021 at 14:45):

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

Joshua Gancher (Aug 01 2021 at 15:53):

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

Joshua Gancher (Aug 02 2021 at 16:58):

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

Notification Bot (Aug 02 2021 at 16:58):

Joshua Gancher has marked this topic as resolved.

Paolo Giarrusso (Aug 03 2021 at 00:35):

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

Jason Gross (Aug 03 2021 at 09:09):

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: Sep 26 2023 at 12:02 UTC