Stream: Coq users

Topic: [non-]reversible tactics


view this post on Zulip yder (Feb 16 2021 at 00:58):

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?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 16 2021 at 00:59):

That's an interesting question, are you thinking of something like focusing / invertible rules?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 16 2021 at 00:59):

Keep in mind that in HO languages, you could argue that beta destroys information, that is to say (\x -> 3) 4 -> 3

view this post on Zulip yder (Feb 16 2021 at 01:02):

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?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 16 2021 at 01:03):

I see what you mean, and I'd dare to say that it's an art!

view this post on Zulip Emilio Jesús Gallego Arias (Feb 16 2021 at 01:05):

Good advice is to avoid induction, sounds weird but you can read some reasoning on why here https://hal.inria.fr/hal-00805966/document

view this post on Zulip yder (Feb 16 2021 at 01:07):

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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 16 2021 at 01:09):

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.

view this post on Zulip yder (Feb 16 2021 at 01:10):

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?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 16 2021 at 01:20):

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

view this post on Zulip Paolo Giarrusso (Feb 16 2021 at 09:47):

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.

view this post on Zulip Paolo Giarrusso (Feb 16 2021 at 09:47):

so e.g. reflexivity isn't generally safe (but I suspect lia is)

view this post on Zulip Pierre-Marie Pédrot (Feb 16 2021 at 10:24):

Lia is probably not safe without proof irrelevance. You could get into a situation where the shape of the proof matters.

view this post on Zulip Théo Winterhalter (Feb 16 2021 at 10:34):

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.

view this post on Zulip Théo Winterhalter (Feb 16 2021 at 10:35):

And induction should be fine if you are dealing with non-nested inductive types and if you remember the specialised indices.

view this post on Zulip Pierre-Marie Pédrot (Feb 16 2021 at 10:39):

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

view this post on Zulip Pierre-Marie Pédrot (Feb 16 2021 at 10:40):

That's about it.

view this post on Zulip Guillaume Melquiond (Feb 16 2021 at 11:13):

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.

view this post on Zulip Guillaume Melquiond (Feb 16 2021 at 11:18):

(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.)

view this post on Zulip Théo Winterhalter (Feb 16 2021 at 11:21):

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.

view this post on Zulip Tej Chajed (Feb 16 2021 at 13:49):

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

view this post on Zulip Paolo Giarrusso (Feb 16 2021 at 19:06):

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