Stream: Coq users

Topic: Generalized rewrite in list fold

view this post on Zulip Joshua Gancher (Nov 24 2020 at 19:05):

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)


view this post on Zulip Li-yao (Nov 24 2020 at 19:10):

You can try adding a Morphism for foldr

view this post on Zulip Joshua Gancher (Jan 05 2021 at 20:29):

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: Jun 20 2024 at 12:02 UTC