liao zhang (Jul 04 2020 at 01:24): 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: Sep 23 2023 at 08:01 UTC