search

vprover / vampire

The Vampire Theorem Prover
https://vprover.github.io/
Other
302 stars 52 forks source link

avoid sortedness errors with polymorphically let-bound constants #544

Closed MichaelRawson closed 6 months ago

MichaelRawson commented 7 months ago

Fixes bug 1 of #542 by providing a fast path for constants in getResultSort that also does not assert a condition that isn't true for let-bound constants.

A TFX1 $let might capture sort variables. Consider e.g. polymorphic lists and the following axiom.

tff(bug, axiom, ![A: $tType]: $let(x: list(A), x := nil(A), e)).

In the expression e, x: list(A). But this is a non-polymorphic constant (both term and type arity 0) with a variable in its result sort, which SortHelper doesn't like. It seems to be eliminated just fine in later FOOLing around.

MichaelRawson commented 6 months ago

A completely different solution, should be ready for re-review. Thanks @mezpusz !