Work around #334 in definition of allperms

[oskgo]

Ref #972

@alleystoughton Does this work for your proofs?

[fdupress]

Perhaps it's worth pushing this encoding trick into Why3's encoder instead of counting on our collective memory?

[strub]

This is again the termination checker of Why3 complaining?

[alleystoughton]

smt is no longer failing with that bug, but some uses of smt that worked before are now failing. E.g., I had to clear the assumption

ms_perm_len: ms \in allperms range_len

in order for smt(...) to work with something not related to allperms.

[strub]

And anyway, the definition should then be opaque, the 2 definitional lemmas reproven and added as a hint simplify.

[oskgo]

@fdupress Perhaps. I can't tell right now whether doing so would be a patchwork hack or a proper fix.

[alleystoughton]

And anyway, the definition should then be opaque, the 2 definitional lemmas reproven and added as a hint simplify.

maybe smt_opaque too.

[alleystoughton]

I think you want

op [opaque smt_opaque] allperms = ...

That way smt doesn't complain about your original definition. You just have to prove things by explicit unfolding.

[alleystoughton]

My proofs check again.

[oskgo]

That's what I get for touching such an old theory I suppose. I've changed the recursively defined operator to be opaque and smt_opaque, re-proven definitional equalities and added them as rewrite hints like before. I've also kept my hack around on the opaque definition just in case, while using the non-hacked definition for the lemmas.

[fdupress]

smt is no longer failing with that bug, but some uses of smt that worked before are now failing. E.g., I had to clear the assumption

ms_perm_len: ms \in allperms range_len

in order for smt(...) to work with something not related to allperms.

Did this accidentally root-cause #918? This would be due to why3's SMT encoding behaving differently on the context and on goals, and specifically so on inductive operators whose definition uses a higher-order op.

[alleystoughton]

smt is no longer failing with that bug, but some uses of smt that worked before are now failing. E.g., I had to clear the assumption

ms_perm_len: ms \in allperms range_len

in order for smt(...) to work with something not related to allperms.

Did this accidentally root-cause #918? This would be due to why3's SMT encoding behaving differently on the context and on goals, and specifically so on inductive operators whose definition uses a higher-order op.

I think so. But all is good now.

[strub]

Did this accidentally root-cause #918? This would be due to why3's SMT encoding behaving differently on the context and on goals, and specifically so on inductive operators whose definition uses a higher-order op.

#918 is due to goal being simplified before being sent to SMT, not the context, nor the general facts.

IMO, #918 is not a bug. We could make the behavior configurable if needed.