Zulip Chat Archive

Stream: general

Topic: simp, tauto


Sean Leather (May 31 2018 at 11:11):

So close and yet so far:

error: done tactic failed, there are unsolved goals
state:
...
a : b₁ = b₂
 b₂ = b₁

Kevin Buzzard (May 31 2018 at 19:02):

eq.symm is not a good simp lemma :-)

Simon Hudon (May 31 2018 at 19:12):

What is the goal before you call tauto?

Reid Barton (May 31 2018 at 19:36):

I made a version of tauto that calls cc (which is how I discovered that cc bug I mentioned here a while ago)

Reid Barton (May 31 2018 at 19:36):

instead of done

Sean Leather (Jun 01 2018 at 06:16):

The goal is rather complicated (but seems like it should be automatically solvable), and I don't have it around anymore. The proof doesn't involve eq.symm. But I've noticed this same pattern a few times when trying tauto. Here's another example that I just tried. It seems that tauto can't solve this (which is just or.inr)?

 s  tl  s = hd  s  tl

Last updated: Dec 20 2023 at 11:08 UTC