feat(Boole): Bring Boole sandbox to Lean 4.29 and add queue examples#539
feat(Boole): Bring Boole sandbox to Lean 4.29 and add queue examples#539Robertboy18 wants to merge 2 commits intoleanprover:Boole-sandboxfrom
Conversation
Robertboy18
force-pushed
the
feat/boole-queue-deque-examples
branch
from
0ad4c54 to
5df3164
Compare
| // `NextIndex(i, n)` is `(i + 1) mod n`, axiomatized without using `mod`. | ||
| function NextIndex(i : int, n : int) : int; | ||
|
|
||
| axiom (∀ i : int, n : int :: | ||
| n > 0 && 0 <= i && i < n ==> 0 <= NextIndex(i, n) && NextIndex(i, n) < n); | ||
| axiom (∀ n : int :: n > 0 ==> NextIndex(n - 1, n) == 0); | ||
| axiom (∀ i : int, n : int :: | ||
| n > 0 && 0 <= i && i + 1 < n ==> NextIndex(i, n) == i + 1); |
There was a problem hiding this comment.
This seems to be the same as if i + 1 == n then 0 else i + 1, is there a reason why the axiomatic definition is preferred?
There was a problem hiding this comment.
Yes, that’s exactly the intended meaning! I originally wrote it axiomatically because the direct Boole conditional version currently triggers a VC-generation/elaboration issue for integer-valued if branches: the generated VC contains something like ite (tail + 1 = n) 0 ..., and Lean reports that the 0 has type Int but a Prop was expected. So NextIndex is just a workaround for expressing the same circular successor while keeping the example verifiable. I agree the conditional version is clearer, and I’m happy to switch once that VC issue is fixed or add a short comment explaining the helper.
There was a problem hiding this comment.
Thanks! I understand now. Maybe it would be helpful if you added a quick bit about that in the comment too, because it explains why mod doesn't work but not the issue with the if/else, which seems to be the other obvious non-axiomatic approach (compared to mod).
There was a problem hiding this comment.
I just pushed the comment! Thanks
I wanted to keep building out the Boole examples, but noticed the sandbox was still pinned to Lean 4.27 while newer Strata support for old(...) and global modifies had landed upstream. This PR updates the Boole sandbox to Lean 4.29.1 and adds/finishes verified data-structure examples: stack, FIFO queue, circular queue, and array-backed deque!
Let me know if you have any questions: )!