coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Stefan Monnier" <monnier+lists.coq/news/ AT rum.cs.yale.edu>
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club] Discriminate tactic on big inductive definitions
- Date: 10 Dec 2002 09:51:54 -0500
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
- Newsgroups: lists.coq
When I try the Discriminate' tactic on something like
Int=(Exist k t)
it fails because Int and Exist are constructors of a non-small inductive
definition, so it says:
Error: Incorrect elimination of ee in the inductive type
Omega
The elimination predicate Prop has type Type
It should be one of :
Prop, Set
Elimination of an inductive object of sort : Set
is not allowed on a predicate in sort : Type
because
strong elimination on non-small inductive types leads to paradoxes.
This happens because the `Discriminate' tactic basically uses a Cases
elimination that either returns False or True.
When I do the proof "manually" I simply use a `Cases' elimination that
returns a boolean and then lift this boolean to Prop, thus avoiding
the strong elimination issue.
Since I have to do that often, I was wondering if someone has already
written a `Discriminate++' that does it for me.
Stefan
- [Coq-Club] Discriminate tactic on big inductive definitions, Stefan Monnier
Archive powered by MhonArc 2.6.16.