is there any place that gives a comprehensive list of which tactics do/don't destroy information, or a better discussion of this aspect of using coq?
That's an interesting question, are you thinking of something like focusing / invertible rules?
Keep in mind that in HO languages, you could argue that beta destroys information, that is to say (\x -> 3) 4 -> 3
from a formal perspective, I think invertibility is along these lines, yes. but I'm more asking from a practical perspective--how can (particularly beginning) users of Coq determine when they've painted themselves into a corner, e.g. with a too-weak induction principle?
I see what you mean, and I'd dare to say that it's an art!
Good advice is to avoid induction, sounds weird but you can read some reasoning on why here https://hal.inria.fr/hal-00805966/document
it's an art to say precisely (because you may not start with a provable claim in the first place), but an overapproximation (or just indication that certain tactics are "risky") seems like it would be helpful and possible--e.g., induction is "risky" but intros can be undone
Something that helped me was using case:
and elim:
from ssreflect, as they are more strict w.r.t. scoping, and in general you become more aware of information loss, but YMMV.
Emilio Jesús Gallego Arias said:
Good advice is to avoid induction, sounds weird but you can read some reasoning on why here https://hal.inria.fr/hal-00805966/document
what part here is relevant? I see they say they avoided induction by subsuming their applications of it into gaussian elimination in their domain, but is there a generalization of that technique that's widely/universally applicable?
The part here is that similar libraries used many many calls to induction, which is always a complex tactic as you have to guess a IH, however in this approach, induction is not used, but you are in the realm of lemma manimpulation
Can somebody name a safe tactic? Revert is safe, intros is only safe if you don't use it to apply lemmas... And then closing tactics are safe if they don't instantiate evars.
so e.g. reflexivity isn't generally safe (but I suspect lia is)
Lia is probably not safe without proof irrelevance. You could get into a situation where the shape of the proof matters.
For lia
we have in any case proof irrelevance for nat
equality don't we? Sure you might end up with stuck terms, but that's not a question of provability.
If you go that way, then maybe only idtac
?
I think you're going off-topic, the question is about "mostly-safe" uses. Which tactics usually don't make you lose generality.
And induction
should be fine if you are dealing with non-nested inductive types and if you remember
the specialised indices.
@Théo Winterhalter invertible rules are fine if they preserve conversions. Since we have η it means that intro is OK and split as well assuming the goal is a primitive record.
That's about it.
Théo Winterhalter said:
And
induction
should be fine [...] if youremember
the specialised indices.
I don't quite follow. If the inferred induction principle is not inductive, I do not see how you can be safe, even by remembering things.
(Thinking about it, "inductive" does not matter, since you can always restart the proof from scratch. But, if the induction principle is not an invariant of the property, the new goal is just false.)
Again, I stress the "mostly". But you're right that the induction principle might not be general enough so I guess I still have to retract my statement.
@yder that is a great question and I wish there were an introductory explanation somewhere. When we teach Coq in courses, we generally highlight exists
, left
, and right
as being the "unsafe" tactics. Tactics that solve the goal, like reflexivity
, can become unsafe when they solve evars, which is a little like exists
. induction
is also quite unsafe as you point out because if you set up the goal incorrectly you can end up with an insufficiently general inductive hypothesis. Many tactics are in the middle: for example with apply
and rewrite
it depends on the lemmas you're using; rewrite H by ...
is a good way to make it safe, and apply
on bidirectional (iff) lemmas is also safe.
Ah, your point on rewrite by is that you're sure the extra goals are solved, and you're assuming that "rewrite <-H" could invert the rewrite (indeed true when rewriting by symmetric relations like equality)
Last updated: Mar 28 2024 at 14:01 UTC