3 ms·

This would be the classical proof via strong induction, without Σ-types: https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAZRgEwHQBECGNOoBKYDOAFgLKZgBQokscAggKaE

This would be the classical proof via strong induction, without Σ-types: https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAZRgEwHQBECGNOoBKYDOAFgLKZgBQokscAggKaERWuMB2iKlvyjAMzghMAD3QQANpMxRCAfUJhGAYzgAKLgC44AOWwBKODv3wtAXkpw4wIV0AmRHAAccGMU5W4AWi9wAQkSMcCqBOgLQcAAGDs6RADQ2MADkhHAARowwMIxQrhBwhIzSru7BEMBcyMBQqjCSAJ6ontYcnkWFnj5wAEqqAK5ywABuQSGFOirEEBCFJUEioqB9IOmZAO6MnAVFkhUA5nNlFXBVNSp19XCYHMhwjKKT13v7iU3W1gtwXOoLEtKyCiUqg0XAA9HAAExGADUwjEfxkckUyjUmjg4IAzDC4eIpIjASiQei4AAWAwGXiUfhCdySZRQUiMED5EzYOCAJMI4AQSOQwHo2aYOfz4AB1rlEMgUYXCzwAHy+CRATPy5gAfM04TBJsJlag9pkAPxfOBrYBuDXylhKuBDOBqjRDRXKozeXyYSQ1TDIS4hSaMZAWr4QDhBNUa6y2Y2OFxuLbvePWLppQLBULbYoqcqVaq1Brh96STI65lJYzmYsQVAVQp0LitBPvTROksUhvtRj5xO+M4DQjDRgTCDgPrZVaEeD3R4cfU2919RjN8oALxe7uDB1jJsw9U7cEL8HUQwAjIuj0YLHBafTGcyieCoRXd/uHRDFw+L1ecjf8mjMUYlcyR5PkWh4YouWJlpeRTXsqd6kv+yoQsB8AZOOkGfN8x5wLCQwQthNpYshFalheAEQBiVYcDW8BcKhMC7uodGLkkFJUoIOIIgC35EqyMDntKFieOon4MrB3zcpKYCoEyYAwPUADqZrEAAwhQmAqGa9TkqgAjjpS1IVvIIhgPImZQGcB4gDoEm8tKpgGDoAAKUCsJBgAARMajrCHqhrGuWVpBLaXiqhxeIAsiwJcOWQy8LG0BMnc4ByUZyqmdAFk6GRRkUGl5m1BoNkUNJSUKUpqlgOpmnnuWaSXH24BwAA2llxm5RZAC6sXuPFKxmRZ8jVjkMDZRUODVm1tQhoQqQ/EYwmZalrV9flIBzcQEI6La5a/GFSJAmoADWDmGUt6X5T8lHUXAB02tV6Q7tYfQcOEki3C1OXLecnijS5nnBJ4T0vW9i0fWd5xXPAxCePtwDusAS5BMQXzQzQ8jupIcDBg0TWFVJ+owAa8iMAAjvI+MAKKFiABqddYUBrDjEq8j5MCU0yhODbA7UQ/91hKLs8Bsionjo2TEDuqk9UmejlKUHFNQrCJ34TeDmi8XNq0aMQC3MtlJmffAmsAN62iASQAL5a1AOhK2Jwh2g6ioscdW2hf8e2ElwgDkRCdoN5eDZuQbV303H05zAMGxp9H207Cqg44udOvQqAA8lw+ohlAcMrrHKym0knhjEEFS3FwwBI2G8aA1Ity27ebLEFAGr82aPON66BRgALhxkZqky8PGReXvIR5wPI13BHaIVS2jxSNUjXBDLT7xD8Q8h4UMpZqPaXRKK3m4xC4tj5i3guQ03DZD8AhAACpQPOl7b+qDZ0wzjXORAaAgAdlEAFbk8TbmDcL4v3pk1QACYSN1QCeOAkCoCoAhEA+AAAqAeL9iCYBGMYPybt8QRTUNoGqD0X6PWejXXB4V9q7j5qjdGmMODY0arjFmhMSZk0yGzamCQKZU1YaTDgwZGADQEAIBIgBkwhqMgMOjAACS2ROq7kzFRGA99zjQF3AAdruKIdS8A3DX00do3RZR/bDU5sNEQo1MDjQNlNVI48kb6MILufMV9CAADEJaIyfruU+bcoAAG4vj3D0V3UeWEyKjxJqPSuL8/HAKCSGUQoTJAbzwmRPCJM8KxIbPE8+iSQmuC7hiAiFYSkkxKWGXcGCsHl1HhecucEHyMUuEORgexMD/kvHcYmQESE1OLutSCjTfxwAgi0zGSoOkIUAjYYgR4EE9KQv0zBgySkNKRqMskGhaqTPaZ0iseFy4QkWRUtBDYwHvxcl/H+FR/6AP8buS5cDoEJBeYgnmqDqmrOwTiY0h5R44TwjhCC214S7QJJFIOxCSHV1ehQj2qhqEFBoE1YgKgEh1NeXMk5MDy4USPAokhSiE5hxgOokhWj7jGKcYY6l4MDYDSokNEaHAxpURVjAOxY85kUTwrSrqjAeqGQNtgjyaJ1aKnBe7Qg3EooIshQQ6FIcVH5HrHAOFb1pX4m/IXQIqQVA6GEtBL8dtmEyTkopNw5VKpyVbKmWY384C6XgIQG4U9PADJKNfSCdcICcv+eakqVqVJqQ0naxKsl6gpV1qK4WNDwCz0kJQIAA https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAZRgEwHQBECGN... Doing the proof inside the algorithm (i.e. doing inline induction over the algorithm recursion structure) has the advantage that the branching structure doesn't have to be duplicated as in an external proof like the one I did. In my proof I didn't struggle so much with induction, but much more with basic Lean stuff, such as not getting lost in the amount of variables, dealing with r.fst/r.snd vs r=(fst, snd) and the confusing difference of .get? k and [k]?.

duve02 1y ago
Nice job. My attempt at the initial strong induction proof was a long time ago so I don't remember the details. It definitely followed a similar structure as yours (but this was before `omega` im pretty sure). Can't quite remember where I got stuck but your proof is good. Thanks!

duve02 1y ago

Nice job. My attempt at the initial strong induction proof was a long time ago so I don't remember the details. It definitely followed a similar structure as yours (but this was before `omega` im pretty sure). Can't quite remember where I got stuck but your proof is good. Thanks!