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 ?

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/

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).

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 :\

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

Last updated: Oct 03 2023 at 20:01 UTC