Non terminal tauto?

Stream: Is there code for X?

[Siddharth Bhat]

I'd like to have a version of tauto that simplifies tautologies as much as possible, leaving me with the final goal state. In order to avoid an XY problem, I have some bitvector reasoning:

I start with:

w : Nat
x y : BitVec w
h✝² : ¬y = 0#w
h✝¹ : ¬((¬w = 1 ∧ x = intMin w) ∧ y = -1#w)
h✝ : y = 0#w ∨ x = intMin w ∧ y = -1#w
⊢ False

and I want to end with the state:

w : Nat
x y : BitVec w
h✝¹ : ¬y = 0#w
em✝ : (a : Prop) → Decidable a
left✝ : x = intMin w
right✝ : y = -1#w
h✝ : w = 1
⊢ False

where the subsingleton property of bitvectors of width 1 creates a contradiction between right✝ : y = -1#w and h✝¹ : ¬y = 0#w.

Currently, tauto from the starting goal ends with "unsolved goal <END GOAL STATE>". I want a version of tauto that leaves me there interactively (ie, a version of tauto that is not a finishing tactic).

[Anand Rao Tadipatri]

It seems like Mathlib.Tactic.Tauto.Config is currently empty, so it's unlikely that the tactic can be configured to do this.

However, the aesop tactic has a configuration option to make it non-terminal: aesop (options := { terminal := False }).

It might be possible to use aesop as a replacement for tauto, but it probably depends on the specifics of the use-case.

[Siddharth Bhat]

Alternatively. I could PR mathlib adding a config, correct?

[Anand Rao Tadipatri]

Yes

[Siddharth Bhat]

Great, thanks!