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 you`remember`

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: Jun 23 2024 at 23:01 UTC