https://github.com/digama0/mizar-rs
Revision 4655c8bdf3c24ac8769f61d9a1f0e4e8e5b29938 authored by Mario Carneiro on 15 February 2023, 08:05:31 UTC, committed by Mario Carneiro on 15 February 2023, 08:08:39 UTC
I was planning to do this eventually anyway, but it turns out that the existing representation actually has a soundness bug, in addition to the sketchy unpacking code in `expand()`, because it is not true that equality of the endpoints implies equality of the FlexAnd expressions. For example, `P[1+1] /\ ... /\ P[n]` represents `P[x]` for `x in 1..=n` but if you substitute `n = 2+2` then you get the expression `P[1+1] /\ ... /\ P[2+2]`, which if re-parsed actually results in `P[x+x]` for `x in 1..=2`. These two expressions are not equivalent despite having the same endpoints and this can be used to prove false.
1 parent f498ae7
Tip revision: 4655c8bdf3c24ac8769f61d9a1f0e4e8e5b29938 authored by Mario Carneiro on 15 February 2023, 08:05:31 UTC
change FlexAnd representation
change FlexAnd representation
Tip revision: 4655c8b
| File | Mode | Size |
|---|---|---|
| .vscode | ||
| src | ||
| .gitignore | -rw-r--r-- | 8 bytes |
| Cargo.lock | -rw-r--r-- | 8.7 KB |
| Cargo.toml | -rw-r--r-- | 399 bytes |
| rustfmt.toml | -rw-r--r-- | 288 bytes |
Computing file changes ...
