Stream: Coq users

Topic: is there a tactic for automating left/right.

walker (Feb 14 2023 at 15:52):

I have nested disjunctions, and I want something that automates only left/right choices.

I have things like this:

        right.
        left.
        left.
        by right.

in many places, and I want to avoid having to pick the path every single time ( Also I don't want to use auto because I prefer to have verbose proof control when it comes to applying lemmas and solving non trivial goals)

Gaëtan Gilbert (Feb 14 2023 at 15:55):

by repeat (left + right)?

walker (Feb 14 2023 at 15:57):

perfect, I didn't know about adding two tactics trick!

Alexander Gryzlov (Feb 14 2023 at 21:25):

do !constructor maybe too?

Last updated: Oct 13 2024 at 01:02 UTC