Fix bug with Iff elimination.

ufmg-smite / lean-smt

Tactics for discharging Lean goals into SMT solvers.

Apache License 2.0

89 stars 18 forks source link

Fix bug with Iff elimination. #123

Closed abdoo8080 closed 1 month ago

abdoo8080 commented 1 month ago

The rewrite tactic we use to eliminate Iff does not work properly inside quantifiers (as in #121). This PR changes Iff elimination to use simp instead. This PR also optimizes the code to avoid executing the tactic if it's not needed.