The Coq mailing list

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

> If you are instead asking for a tactic to replace the above assertion such that it determines the type of H' for you, I agree that such a tactic would be nice to have.

This and plus that with some matches we need more than one destruct (when patterns have variables e.g.), but the latter can be fixed with plain repeat.

Maybe there are other difficulties with complex pattern matches, yesterday I had some specific notes, but I have forgotten them already =/

Sincerely,
Kirill Taran

On Sat, Jul 19, 2014 at 8:55 PM, Jonathan <jonikelee AT gmail.com> wrote:

On 07/19/2014 06:32 AM, Kirill Taran wrote:

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

Why not just revert H; destruct x?  For instance, given the following:

Inductive Foo := foo1|foo2|foo3.

Goal forall x, match x with
                 | foo1 => true
                 | foo2 => false
                 | foo3 => false
               end = false -> x <> foo1.
intros x H.
revert H. (*obviously not needed if only did intro x*)
destruct x.

after destructing, you get 3 goals, one for each branch, and the match is gone in all of them.  If you want to see the equation for x in each subgoal, change destruct x to destruct x eqn:E.

Alternatively, if you want to get H' : x = foo2 \/ x = foo3, you can assert it and prove the assertion:

Inductive Foo := foo1|foo2|foo3.

Goal forall x, match x with
                 | foo1 => true
                 | foo2 => false
                 | foo3 => false
               end = false -> x <> foo1.
intros x H.
assert (x=foo2 \/ x=foo3) as H' by (destruct x; intuition discriminate).

If you are instead asking for a tactic to replace the above assertion such that it determines the type of H' for you, I agree that such a tactic would be nice to have.

-- Jonathan