The Coq mailing list

[Tej Chajed <tchajed AT mit.edu>]

I've run into this issue as well and found the part of the error message "the elimination of the inductive definition _ on sort {Set,Type} is probably not allowed" confusing. What I didn't understand right away when I first saw this was that "on sort Type" means "over a goal in Type". Could the error message be changed to mention that the sort of the goal is the problem?

On Mon, May 30, 2016 at 10:57 AM, Jonathan Leivent <jonikelee AT gmail.com> wrote:

On 05/30/2016 11:44 AM, Soegtrop, Michael wrote:

Dear Coq Users,

I am way stuck trying to use an existential hypothesis with elim:

1 subgoal
t : Type
p : list t -> Type
H0 : p [ ]
HS : forall (x : t) (l : list t), p (l ++ [x])
x : t
l : list t
HM : exists (x2 : t) (l2 : list t), l ++ [x] = [x2] ++ l2
______________________________________(1/1)
p ([x] ++ l)

now I want to elim HM to get the equation to rewrite the goal, so that I can use HS to solve it. But when I try "elim HM" I get the error "Error: Cannot find the elimination combinator ex_rect, the elimination of the inductive definition ex on sort Type is probably not allowed.".

Try using sig or sigT instead of ex for HM and your lemmas that produce "exists".  It's a pet peeve of mine that Coq uses the Prop ex for the "exists" notation, but doesn't have as nice a nested binding notation for the Type variants sig or sigT.  I use this:

  Notation "'specific' x .. y , p" := (sigT (fun x => .. (sigT (fun y => p)) ..))
  (at level 200, x binder, right associativity,
   format "'[' 'specific'  '/  ' x  ..  y ,  '/  ' p ']'") : type_scope.


which allows one to write "specific x y z, P x y z" to get the Type variant of "exists x y z, P x y z".

-- Jonathan

What I want to achieve macroscopically is to simplify my (educational) proofs on various induction schemes on lists, e.g.

Lemma induction_list_append_rev :
   forall (t : Type) (p : list t -> Type),
     p [] -> (forall (x : t) (l : list t), p (l ++ [x])) -> forall l : list t, p l.

I have a rather lengthy proof for this, but thought it wouldn't be complicated to derive it from

Lemma induction_list_append :
   forall (t : Type) (p : list t -> Type),
     p [] -> (forall (x : t) (l : list t), p ([x] ++ l)) -> forall l : list t, p l.

Using this lemma:

Lemma list_mirror :
   forall {t : Type} (x1 : t) (l1 : list t),
     exists (x2 : t), exists (l2 : list t), l1 ++ [x1] = [x2] ++ l2.

I get into the above situation this way:

Lemma induction_list_append_rev :
   forall (t : Type) (p : list t -> Type),
     p [] -> (forall (x : t) (l : list t), p (l ++ [x])) -> forall l : list t, p l.
Proof.
   intros t p H0 HS.
   apply induction_list_append.
   - exact H0.
   - intros x l. assert( HM := list_mirror x l ).
     elim HM.

I would appreciate some help with the mysteries of existential elimination :)

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928