Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Discriminate tactic on big inductive definitions

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Discriminate tactic on big inductive definitions


chronological Thread 
  • 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




Archive powered by MhonArc 2.6.16.

Top of Page