Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Smart case analysis in Coq.

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Smart case analysis in Coq.


Chronological Thread 
  • From: Kirill Taran <kirill.t256 AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Smart case analysis in Coq.
  • Date: Sat, 19 Jul 2014 14:32:31 +0400

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



Archive powered by MHonArc 2.6.18.

Top of Page