Hi all! I was wondering if anybody has insights for the following:

I have a type T with a predicate EqT : T -> T -> Prop, which I have registered with Add Relation to be an equivalence. I have an operation op : T -> T -> T which is a Morphism EqT ==> EqT ==> EqT with identity t0, and I have the notation: ops (ts : list T) := foldr op t0 ts. (where here, foldr comes from mathcomp)

Is there a way for me to easily lift EqT to lists, using ops? I.e., if I have

ops ( x :: y :: nil), and have EqT x z, then I can rewrite this to ops (z :: y :: nil)

Thanks!

You can try adding a Morphism for `foldr`

For posterity: I figured out how to do this, inspired by std++. I created an Inductive list_EqT which lifts EqT to lists point wise, showed it was an equivalence with Add Relation, and then I just needed to add morphisms for ops : list_EqT ==> EqT, and cons : EqT ==> list_EqT ==> list_eqT. No morphism for folds was needed.

Last updated: Jan 29 2023 at 01:02 UTC