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`

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".

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".

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