A minimal example of my issue looks as follows:
Goal let x := True in x.
This is immediately solved by simpl. auto., but auto. does not work.
In my actual case, the search tree is a bit bigger than that. It involves many intermediate steps in which auto would be able to proceed, but it bails out scared off by some zeta-reducible let expressions. Even if I wanted to, I can’t even make it stop there and let me manually insert that simpl (because auto either solves or leaves the goal unchanged).
What is the proper way of dealing with that? If possible, I want to avoid adding an Extern Hint simpl to brutally apply simpl on every let everywhere in my program. I don’t need to stick to auto; any other tactic which would do the job in a non-superfluous way is fine by me.
1
You can tell auto to try arbitrary tactics with Hint extern.
E.g.
Hint Extern 5 => progress simpl : core.
would work. But this is dangerous and might lead to slow auto. The number (5) is a cost – auto will first try all hints with lower cost. The progress ensures that the hint does not apply in case it doesn’t change anything, so that simpl won’t loop.