The Coq mailing list

[Beta Ziliani <bziliani AT famaf.unc.edu.ar>]

If you don’t mind using plugins, you might consider MetaCoq[1], where
such type of programming is quite natural.

Here is a function that takes a type and filters the hypotheses of
that type. I made the function a tactic that only prints the filtered
list since you asked for a tactic and a function.

Definition filter_hyps (T: Type) : tactic :=
  l <- hypotheses;
  l <- MCListUtils.mfilter
    (fun h=>
       mmatch h with
       | [? (x: T) d] ahyp x d => ret true
       | _ => ret false
       end) l;
  print_term l;;
  exact I.

To run the example using the MProof environment:

Example filter_ex (a: bool) (x y z : nat) (c: x > y) : True.
MProof.
  filter_hyps nat.
Qed.

Or to do it inside a normal Coq Proof:

Notation "'evalT' t" := (eval (run_tac t)) (at level 0).

Example filter_ex_no_mproof (a: bool) (x y z : nat) (c: x > y) : True.
Proof.
  refine (evalT (filter_hyps nat)).
Qed.

Best,
Beta

[1] https://github.com/MetaCoq/MetaCoq

On Wed, Sep 14, 2016 at 1:43 PM, Jonathan Leivent 
<jonikelee AT gmail.com>
 wrote:
>
>
> 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
>>
>