walker (Sep 21 2022 at 18:58): 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 ?
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/
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).
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 :\
Paolo Giarrusso (Sep 21 2022 at 19:44):That's fair enough, please ignore that part of the answer
Last updated: Apr 19 2024 at 04:02 UTC