Stream: Coq users

Topic: How to substitute MSets.MSetAVL that are `Equal`s


view this post on Zulip walker (Sep 21 2022 at 18:58):

So I have Equal t2 (union (singleton x) t1) equals I want do prove that

fold Nat.add t2 1 = fold Nat.add t1 1 + x (note I also have ~ In x t1 I would think I can just replace t2 with (union (singleton x) t1)) but apparently I cannot, And it makes sence why because maybe tree representations are different. But I don't know what other approaches I can try.

I tried searching for a lemma that replaces equals in fold propositions but I couldn't find any spec or property in MSetProperties.

Any suggestions for how tackle this problem ?

view this post on Zulip Paolo Giarrusso (Sep 21 2022 at 19:22):

You can either use setoid rewriting (by stating and proving the right Proper instance) or pick sets where equalities are normal equalities (e.g. from stdpp); for the first, see https://www.cis.upenn.edu/~plclub/blog/2020-05-15-Rewriting-in-Coq/

view this post on Zulip walker (Sep 21 2022 at 19:27):

I tried using stdpp, but I at the point where I have no idea what do I even ask, I tried asking once in the past if they have tutorial, but there wasn't any back then, and at this point, I have no idea how to use their sets. If you have any hints, I would just switch to stdpp (despite the time I spent proving stuff till this point).

view this post on Zulip walker (Sep 21 2022 at 19:29):

they have lia-like tactics and equals are truly equals, which will make my proofs much shorter, but I don't know how to use them :\

view this post on Zulip Paolo Giarrusso (Sep 21 2022 at 19:44):

That's fair enough, please ignore that part of the answer


Last updated: Jan 28 2023 at 05:02 UTC