Use auto unfold for some Logic operators

[oskgo]

As suggested in #431 (comment)

We do so for the following operators:

• idfun
• \o
• \o2
• pred0
• predT
• predC
• pred1
• predC1
• rel0
• relT
• relC

These all share the property that they reduce down to an expression simpler than the original and should only be used as arguments to higher order functions like those in Bigop.

I also ran across a bug where declarations such as def foo (x y: int) / = true auto-unfolded after being given only one argument rather than requiring two. This PR fixes that as well. The fix is a one-liner, so it shouldn't be necessary to split up the PR IMO.

The library changes are a breaking change since it makes simplification more powerful, which can remove bindings. The breakage in the stdlib and examples is mostly due to the use of predT in bigops. I also fixed a few spurious errors due to smt calls failing, which might only be a difference between my machine and CI.

[oskgo]

This is going go make a lot of unfolds useless. At the meeting we decided to also make a PR to warn on unfolds that don't do anything.

[fdupress]

Good from the proof maintenance side.

@strub are we good on code style? (I'd like @oskgo to merge on June 1st so I can issue the pre-release after the breaking change, but also not too late.)

[fdupress]

Note

I also ran across a bug where declarations such as def foo (x y: int) / = true auto-unfolded after being given only one argument rather than requiring two. This PR fixes that as well. The fix is a one-liner, so it shouldn't be necessary to split up the PR IMO.

I say we fold the proof fixes into the main commit, but keep this little one separate and in this PR.

[alleystoughton]

This is going go make a lot of unfolds useless. At the meeting we decided to also make a PR to warn on unfolds that don't do anything.

I guess this would also include warning about unfolds of non-existent operators. I've always found it weird that this isn't flagged.