coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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>
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
(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
Sincerely,
Kirill Taran
- [Coq-Club] Smart case analysis in Coq., Kirill Taran, 07/19/2014
- Re: [Coq-Club] Smart case analysis in Coq., Jonathan, 07/19/2014
- Re: [Coq-Club] Smart case analysis in Coq., Kirill Taran, 07/20/2014
- Re: [Coq-Club] Smart case analysis in Coq., Jonathan, 07/20/2014
- Re: [Coq-Club] Smart case analysis in Coq., Jason Gross, 07/20/2014
- Re: [Coq-Club] Smart case analysis in Coq., Jonathan, 07/20/2014
- Re: [Coq-Club] Smart case analysis in Coq., Jason Gross, 07/20/2014
- Re: [Coq-Club] Smart case analysis in Coq., Jonathan, 07/20/2014
- Re: [Coq-Club] Smart case analysis in Coq., Kirill Taran, 07/20/2014
- Re: [Coq-Club] Smart case analysis in Coq., Jonathan, 07/19/2014
Archive powered by MHonArc 2.6.18.