Ssreflect Users Discussion List

[Benjamin Werner <>]

Hello,

You are probably aware of it, but the generic (non ssr) match
goal command of Coq allows
some distribution of tactics over the hypotheses. Here is
something for a very simple case:


Variable a  : nat.

Definition d := a.

Variable al : nat -> Prop.

Goal al a -> al a -> al a.
move => h1 h2.
repeat (match goal with | h :  context [a] |- _ => rewrite -/d in h
end).


Problems :

1) you have to write the body of the definition once in your command.

2) it is not a rewrite item for ssr. But you can put it in a tactic  
abreviation.


There are indeed two possibly desirable extensions:

- having a tactical combinator in order to appply a given command for
every hypothesis.

- a ssr entry "in *" to do the same of one rewrite item.

Sorry not to be of more help !


Best,

Benjamin


Le 20 juin 08 à 11:23, Assia Mahboubi a écrit :

> Dear Keiko,
>
>   to  my knowledge, this is indeed not possible. The 'set' tactic  
> folds the abbreviation in the goal, and you need to rewrite the  
> definition explicitly in the context if needed. More generally there  
> is no way to provide a "universal" argument to an ssreflect  
> tactical, I mean an argument representing "all the  facts in the  
> context".
>
>   I would tend to think that if you define the abbreviation early  
> enough in your script, i.e. as soon as the subterm to be captured by  
> the definition appears in your goal, the problem should not arise.
> But may be I am wrong or may be you are in a situation where this is  
> not convenient? In this case I would be happy to see an example if  
> possible.
>
> Hope this helps,
>
> assia
>
>
>  a écrit :
> > Hello again and thank you for the reply yesterday.
> >
> > Is it possible to define an abbreviation and fold it in all the  
> > facts appearing
> > in the context without enumerating all their names?
> > I could not find out how to do it with set + in tacticals.
> >
> > Best regards,
> > Keiko