The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

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