The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

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.”.

 

 

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 J

 

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