search

epfl-lara / lisa

Proof assistant based on first-order logic and set theory
Apache License 2.0
33 stars 18 forks source link

Fix: proper renaming of bound substitutions #159

Closed sankalpgambhir closed 1 year ago

sankalpgambhir commented 1 year ago

Added a fix for a bug discovered recently by usage of Tautology.

When a substitution is made inside a formula with a binder, the bound variable is not taken into account for further recursive generation of new identifiers. This is now fixed by tracking a set of extra taken IDs.

It was failing in the following example (minified):

Substitute with formula variable s, s -> (z = y) (trivial substitution that does nothing here, but has a free variable y):

Original:
∧(∀'y_1. ¬(∀'y. ¬('y = 'y_1)))
Expected:
∧(∀'y_1. ¬(∀'y. ¬('y = 'y_1)))
Output:
∧(∀'y_1. ¬(∀'y_1. ¬('y_1 = 'y_1)))

Added this test case as well.