## Stream: Coq users

### Topic: Describing the relation between two tactics

#### liao zhang (Jul 04 2020 at 01:24):

Hi, I meet some problems with describing the relation between some Coq tactics.
There are two tactics `unfold A, B in H`, and `unfold A in H`.
It easy to manually judge that the effect of `unfold A in H` is a part of that of `unfold A, B in H`.
However, “effect” is so informal that I want to describe the relation more precisely, for example,
an argument of `unfold A in H` is a subset of the corresponding argument of `unfold A, B in H`

But I have two puzzles:
1: Could I say `A` is a subset of `A, B`? I think `A` and `A, B` are all arguments, I do not know whether one argument can be a subset of another argument.
2: How could I describe `A` and `A, B` are in the corresponding position? Because there is also an argument `H` in `unfold A, B in H`. If I just say an argument of `unfold A in H` is a subset of the argument of `unfold A, B in H`, without the word "corresponding", it is wrong because `A` in `unfold A in H` is not a subset of `H` in `unfold A, B in H`

#### Paolo Giarrusso (Jul 04 2020 at 01:36):

Unfold takes a list of identifiers (well, it's more complex, see the manual); so "unfold A, B" passes to unfold a bigger indentifier list than "unfold A".

#### Paolo Giarrusso (Jul 04 2020 at 01:41):

I guess similar jargon generalizes to any tactic which takes a list of something as an argument. E.g. "unfold foo in H1, H2" takes a bigger hypothesis list than "unfold foo in H1".

#### liao zhang (Jul 04 2020 at 02:04):

After more consideration, I guess it is fine to say the argument `A` is a sublist of the argument `A, B`. Is there any problem?

Last updated: Jun 18 2024 at 09:02 UTC