Stream: Coq users

Topic: Subst for setoids?


view this post on Zulip Roger Bosman (May 05 2021 at 10:33):

Hi all, substs eliminates hypotheses of form x = y by rewriting all occurances and then discharging the hypothesis. However, this does not work for alternate equivalence relations. Is there a setoid-based (?) variant that does this?

view this post on Zulip MackieLoeffel (May 05 2021 at 12:04):

std++ has a setoid_subst tactic that may do what you want (for the std++ equiv relation): https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/theories/tactics.v#L324


Last updated: Feb 01 2023 at 12:30 UTC