The Coq mailing list

[Kirill Taran <kirill.t256 AT gmail.com>]

Hello.

Is it possible to perform "clever" case analysis during a proof session?

Suppose we have hypothesis like:
    H : match x with
        | <1> => true
        | <2> => false
        | <3> => false
        end = false
And we want to filter out branch <1> (because true <> false)
and to get something like this as result:
    H' : x = <2> \/ x = <3>

I guess that it is possible, but implementation of such tactic
(polymorphic on type of branches, i.e. not only for booleans)
is not straightforward.

So, "clever" version of destruct would be very useful for this task.
By "clever" I mean the one which takes a set of expressions with
proof that this set is exhaustive (what is true for every match _expression_)
and generates one subgoal per each _expression_ with hypothesis

like x = <expr_i> in i'th subgoal.

Sincerely,
Kirill Taran