The Coq mailing list

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

Dear Coq Users,

 

I need a tactic to collect all hypothesis of a given type in a list. The un-elegant and restricted version below somehow works, but I am looking for something which would work for any number of hypothesis.

 

I wanted to use a recursive function and clear the hypothesis in each step (this would be ok), but as far as I know an Ltac function can either return a value or manipulate the goal but not both.

 

Does someone have something similar?

 

Alternatively an example for constructing a list in a hypothesis by keeping the tail an evar would be useful. I tried a few things but always get typing errors, when I instantiate an existing evar with something like head :: newevar.

 

Thanks & best regards,

 

Michael

 

 

Open Scope list_scope.

 

Inductive PropWrap : Prop :=

| SomeProp {P : Prop} (p : P)

| NoneProp

.

 

Ltac CollectPropWrap :=

  lazymatch goal with

  | H1 := ?h1 : PropWrap, H2 := ?h2 : PropWrap, H3 := ?h3 : PropWrap |- _ => constr:(h1::h2::h3::nil)

  | H1 := ?h1 : PropWrap, H2 := ?h2 : PropWrap                       |- _ => constr:(h1::h2::nil)

  | H1 := ?h1 : PropWrap                                             |- _ => constr:(h1::nil)

  end.

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