Stream: Coq users

Topic: Non-deterministic tactic application?


view this post on Zulip Joshua Grosso (Apr 30 2021 at 19:58):

I often have multiple subgoals with similar proof structures, except for some intermediate steps: e.g. foo; bar; baz and quux; bar; baz. Is there a way to introduce "non-determinism" of the form [foo; quux]; bar; baz? (Assume that (foo || quux); bar; baz might not work because foo could succeed in the second case but lead to an unsolvable goal.)

view this post on Zulip Li-yao (Apr 30 2021 at 20:01):

There is + instead of ||. (foo + quux); bar; baz; fail? or maybe solve [ (foo + quux); bar; baz ]

view this post on Zulip Joshua Grosso (Apr 30 2021 at 20:04):

Wow that's awesome, I wish I had asked this way sooner... thanks!


Last updated: Oct 13 2024 at 01:02 UTC