#gadt — Public Fediverse posts
Live and recent posts from across the Fediverse tagged #gadt, aggregated by home.social.
-
Red-black tree in Lean 4 prover.
I proved all needed properties, for example that resulting tree is sorted.
I implemented one operation only: insertion. And I "cheat" by assuming that original tree is always black. My goal was not implementing everything, I just wanted to implement one simple operation and prove really everything about it.
Proof of sorting (
insert_sorted) turned out to be rather big. If someone knows how to make it smaller (possibly using mathlib), then, please, tell me that.