The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 09/14/2016 12:34 PM, Soegtrop, Michael wrote:
> 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?

There is Gregory Malecha's plugin, which can be used to iterate over 
hypotheses: https://github.com/gmalecha/coq-ltac-iter

Without plugins, I have a set of tactics that can get a list of the 
current hypotheses and iterate over them, including filtering by type.  
But, they're somewhat kludgey - depending on tactic-in-term behaviors.

Also, there is a way that an Ltac tactic can both return a value and 
manipulate the goal - using a dummy let that is assigned a trivial match 
where the branch does the manipulation:

  let dummy := match goal with _ => manipulating_tac end in
  let result := ... in result.

-- Jonathan


> 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