#829 Autorewriter generates invalid proof rule
In some cases, when simplifying expressions with comprehenion sets, the auto rewriter returns an invalid proof rule. It then causes an infinite loop in the prover that keeps trying to apply this erroneous rule. A simple example, provided by Yannis Benabbi, is attached.
Implementation details:
The auto rewriter has two rules related to comprehension sets: SIMP_COMPSET_IN ({x · x∈S ∣ x} == S) and SIMP_COMPSET_SUBSETEQ ({x · x⊆S ∣ x} == ℙ(S)).
In 2011, a bug was found and fixed by Laurent Voisin in SIMP_COMPSET_IN: it did not handle bound identifiers correctly when extracting the expression S from the comprehension set.
Alas, there was the same bug in SIMP_COMPSET_SUBSETEQ but no one noticed at the time; Yannis Benabbi just found it out. The fix is the same: add a call to shiftBoundIdentifiers(-nbBound) on S.
It has been fixed and merged in commit [67fd5a].
Related
Commit: [67fd5a]