The final bit is in
Падабаецца 0
Рэпосты 0
@vitaut Is this a whole proof, or only the new functions you need for your proof?
Падабаецца 0
Рэпосты 0
@jgrg I have a proof of Roundtrips and Shortest for yy and it's ~2 kLOC o_O
https://github.com/vitaut/zmij/blob/main/test/verify.lean
Падабаецца 0
Рэпосты 0
@vitaut Right, so these are three conditions of correctness which you want to prove your algorithms satisfy? And you've done it for yy for two of them, but not zmij?
Падабаецца 0
Рэпосты 0
@jgrg Exactly. I picked yy because it is simple and it is used in zmij, just not for double. It should be straightforward to adapt the proof to another algorithm of a similar kind.
Падабаецца 0
Рэпосты 0