Stream: math-comp devs

Topic: Is subst idiomatic to math-comp


view this post on Zulip Yves Bertot (Mar 29 2024 at 07:47):

Hello, I would think that the subst tactic should be avoided in math-comp development, because it has implicit effects in all hypotheses, which is a weakness with respect to long term maintenance.

There is currently a PR under review https://github.com/math-comp/math-comp/pull/1191/files/c7f7ae57f333da67eadbd89b7efaabe628450b41..7b124c96229fc896daa5403ddcac007b4cdcf77b#diff-7bdcaab656106c271b7e9284ed02a35c9d0de4163af1efbe73cb8d189db9bd3fR1048, where this tactic is being used, and I was wondering whether the substusage should be replace with more explicit rewriting in hypotheses to comply with code style.

view this post on Zulip Pierre Roux (Mar 29 2024 at 07:51):

Pinging @Quentin VERMANDE

view this post on Zulip Pierre Roux (Mar 29 2024 at 07:52):

Maybe we should document this in CONTRIBUTING.md?

view this post on Zulip Yves Bertot (Mar 29 2024 at 08:01):

The remember tactic also feels "non-idiomatic" to me, but I am not sure this is as important.

view this post on Zulip Yves Bertot (Mar 29 2024 at 08:11):

I just looked at the CONTRIBUTING.md and it could do with a facelift. For our current discussion, the problem is that there is no section explaining why some tactics should be avoided in math-comp coding style.

Another remark that pops in my head is that the naming conventions have evolved, but this is not reflected there.

view this post on Zulip Quentin VERMANDE (Mar 29 2024 at 08:55):

subst does exactly what I want, namely getting rid of a variable by replacing it with something it is equal to everywhere. I can of course do the same thing by hand with rewrite (and I will if it is decided to be the way to go), but I think it just makes things less readable.
Regarding remember, I know that move: {1}(term) (eq_refl term) => x xE does what I want, but this is the only alternative I know and it is ugly, so I would be very interested in a reasonable idiomatic way to do it.

view this post on Zulip Enrico Tassi (Mar 29 2024 at 10:01):

This last idiom is explained here: https://coq.inria.fr/doc/V8.19.0/refman/proof-engine/ssreflect-proof-language.html#generation-of-equations-ssr

view this post on Zulip Cyril Cohen (Mar 29 2024 at 10:23):

subst is fragile and is indeed forbidden in the main mathcomp repos for the sake of long term maintainance.
That being said it is indeed way more concise than the existing, so we could have a {x in H1 H2 Hn}-> intro pattern to explain the substitution should happen and have a clean alternative.

view this post on Zulip Cyril Cohen (Mar 29 2024 at 10:25):

One additional way to document allowed tactics we could implement today is to shell "forbidden tactics" with a warning message explaining available replacements.

view this post on Zulip Pierre-Yves Strub (Mar 29 2024 at 10:26):

I never really understood why subst is considered fragile (if you give the equation to use). It seems to me that it has then a clear semantic.

view this post on Zulip Pierre-Yves Strub (Mar 29 2024 at 10:28):

In EC, we have the ->> intro-pattern that does a substitution of the top-level assumption.

view this post on Zulip Cyril Cohen (Mar 29 2024 at 10:28):

Pierre-Yves Strub said:

I never really understood why subst is considered fragile (if you give the equation to use). It seems to me that it has then a clear semantic.

It is considered fragile because it touches hypthotheses which names are absent in the proof script. There are two sources of fragility in that:

view this post on Zulip Cyril Cohen (Mar 29 2024 at 10:29):

A stable alternative is one where you inline the set of hypothesis you want to substitute in hence my suggestion
{x in H1 H2 Hn}->, where {x clears the variable in is a keyword and allows to inline a in construction, and H1 H2 Hn} are the explicit names of where the subsitution happens.

view this post on Zulip Cyril Cohen (Mar 29 2024 at 10:30):

This is analog to the difference between Coq case and ssr case: the former can decide to substitue in the context, while the second one requires an explicit discharge or in .

view this post on Zulip Pierre-Yves Strub (Mar 29 2024 at 10:56):

I would meet in the middle: this depends on your equation. When I have x = 0 for x a local variable, I use subst x (or ->>), because I find my proof script much more maintainable. Never been caught by that.

view this post on Zulip Yves Bertot (Mar 29 2024 at 12:07):

technically, the comment of @Cyril Cohen is wrong about vanilla case which does nothing in the context, it is destruct that modifies the context.

view this post on Zulip Yves Bertot (Mar 29 2024 at 12:12):

Where did we document the exclusion of subst or similar tactics (induction, destruct)?

view this post on Zulip Cyril Cohen (Mar 29 2024 at 14:11):

Yves Bertot said:

Where did we document the exclusion of subst or similar tactics (induction, destruct)?

I guess no-one ever documented it. But we should!

view this post on Zulip Cyril Cohen (Mar 29 2024 at 14:11):

And provide suitable replacements when required.

view this post on Zulip Pierre-Yves Strub (Mar 29 2024 at 14:11):

Only when x is equal to 0 :grinning_face_with_smiling_eyes:

view this post on Zulip Cyril Cohen (Mar 29 2024 at 19:00):

FYI here is one weird behaviour of subst:

Lemma test1 x (a : 1 <= x) : x = 0 -> False.
Proof.
intro b.
subst x. (* remaing hypothesis: a *)
now inversion a.
Qed.

Lemma test x (a : x = 1) : x = 0 -> False.
Proof.
intro b.
subst x. (* remaing hypothesis: b *)
Fail now inversion a. (* hence a does not exist anymore *)
now inversion b.
Abort.

view this post on Zulip Pierre-Yves Strub (Mar 29 2024 at 19:04):

Yes, this, I agree, hence the "if you give the equation to use" in my message.

view this post on Zulip Pierre-Yves Strub (Mar 29 2024 at 19:04):

Having the tactic deciding which equation to use is indeed a no-go

view this post on Zulip Enrico Tassi (Mar 29 2024 at 20:43):

I still don't get why listing the context is needed. If I say subst: E and E : variable = term then all occurrences of variable in all hyps and goal are replaced by term. if term uses one of these hyps, we fail (so you have to do subst: E in bla bla bla). If variable occurs in a section var, we fail. If the shape of E is not the one above, we fail. E is cleared, unless stated otherwise. Variants subst., move: E => ->>. Sugar subst: -E = subst: (esym E). The implementation is "revert all hyps mentioning x but for E, rewrite E, undo the revert"

I know it is not in the usual style of context management, but I fail to see why this is fragile.

view this post on Zulip Enrico Tassi (Mar 29 2024 at 20:49):

In a way the question "is term t occurring in s" is hard (how do you look for t, etc). But "is variable x occurring in s" seems to be way better defined.

view this post on Zulip Pierre-Yves Strub (Mar 29 2024 at 20:50):

In EC, ->> only works for variables, indeed. Otherwise, this is a rewriting and we expect people to use rewrite

view this post on Zulip Cyril Cohen (Mar 29 2024 at 21:47):

Well it breaks the invariant that only named hypotheses are touched, the new invariant is: if an hyp changed either it is named somewhere in the proof script -- and that's where it changed -- or it was updated by a subst.
In particular this means that on file update, certain proofs can now break for reasons that cannot be investigated easily from the proof script alone.

By looking very hard I figured out one example so far (I'm not sure it occurs in existing proof scripts though) :

Require Import NArith.
Fixpoint fact n := match n with S n => S n * fact n | _ => 1 end.
Definition oddb n := Nat.eqb (Nat.modulo n 2) 1.

Section stuff1.
Variables (m : nat) (Pm : oddb m = true).

(* a lot of stuff *)

Lemma test1 : m = 1000 -> False.
Proof.
intro mE; subst m.
discriminate. (* terminates fast *)
Qed.
End stuff1.

Section stuff2.
Variables (m : nat) (Pm : oddb m = true).
(* stuff *)

Variables (k : nat) (Pm': fact (fact m) = k).
(* a lot of stuff *)

Lemma test2 : m = 1000 -> False.
Proof.
intro mE; subst m.
discriminate. (* same proof script, does not terminate anymore *)
Abort.

End stuff2.

view this post on Zulip Cyril Cohen (Mar 29 2024 at 21:48):

Now I guess it is a matter of balance, do we want to forbid the (safer version of) subst, in order to save ourselves some pain on too few examples. Maybe not?

view this post on Zulip Cyril Cohen (Mar 29 2024 at 22:02):

And I realize this example relies on success when rewriting in section variables... which Enrico proposes to forbid anyway.

view this post on Zulip Cyril Cohen (Mar 29 2024 at 22:03):

I guess I am short on examples, I won't oppose the introduction of this new intro pattern and tactic

view this post on Zulip Cyril Cohen (Mar 29 2024 at 22:04):

Still it would be nice to also have a syntax where we can give explicit names in an intro pattern.

view this post on Zulip Pierre-Yves Strub (Mar 29 2024 at 22:04):

I think that the proposed syntax (with { ... }) is good.

view this post on Zulip Cyril Cohen (Mar 29 2024 at 22:05):

Like => {x in H1 .. Hn}->>. At least if we realize one day it was a bad idea to allow general subst, at least we can easily piggyback on the explicit version

view this post on Zulip Pierre-Yves Strub (Mar 29 2024 at 22:05):

Yes

view this post on Zulip Cyril Cohen (Mar 29 2024 at 22:06):

We could also go lean-like and have {x in ?}->> print the auto-completion of ?

view this post on Zulip Cyril Cohen (Mar 29 2024 at 22:07):

(Lean heuristic tactics that end with a ? print a non-heuristic version of themselves)

view this post on Zulip Pierre-Yves Strub (Mar 29 2024 at 22:07):

Ok, I have to admit that I don't know Lean very well :)

view this post on Zulip Cyril Cohen (Mar 29 2024 at 22:08):

In Lean:

view this post on Zulip Enrico Tassi (Mar 30 2024 at 21:18):

Cyril Cohen said:

(Lean heuristic tactics that end with a ? print a non-heuristic version of themselves)

Matita's auto by _ ? so sad...

view this post on Zulip Hugo Herbelin (Mar 31 2024 at 08:25):

This is an interesting discussion, and, maybe, as members of the Coq development team, you would be interested to move the discussion at a larger level. In particular:

view this post on Zulip Cyril Cohen (Apr 02 2024 at 07:46):

let's discuss subst in the next mathcomp meeting

view this post on Zulip Cyril Cohen (Apr 02 2024 at 07:55):

Hugo Herbelin said:

This is an interesting discussion, and, maybe, as members of the Coq development team, you would be interested to move the discussion at a larger level. In particular:

I think we should have global reflection about tactics in Coq in general indeed.

view this post on Zulip Cyril Cohen (Apr 02 2024 at 08:00):

But it is good to have a the reflection at both level, because it might take some time to converge at the broader level.

view this post on Zulip Pierre Roux (Apr 02 2024 at 08:40):

I have mixed feelings about adding options to tactics we consider dangerous:

Maybe adding a warning to the dangerous behavior could help. But this may be too noisy and just risk being ignored?

view this post on Zulip Cyril Cohen (Apr 02 2024 at 08:46):

Pierre Roux said:

I have mix feelings about adding options to tactics we consider dangerous:

Maybe adding a warning to the dangerous behavior could help. But this may be too noisy and just risk being ignored?

I think this is exactly the kind of discussion that have to happen at Coq level.

view this post on Zulip Hugo Herbelin (Apr 02 2024 at 11:46):

I think this is exactly the kind of discussion that has to happen at Coq level.

Yes, it is about making explicit the methodologies and we need to take decisions.

view this post on Zulip Cyril Cohen (Apr 02 2024 at 11:49):

The issue with Coq level decisions compared to mathcomp level is that consensus is harder and longer to reach.

view this post on Zulip Hugo Herbelin (Apr 02 2024 at 11:51):

A simple way to get consensus would also be to provide different modes and to explain which mode is useful for which application.

view this post on Zulip Cyril Cohen (Apr 02 2024 at 12:10):

I think no mode needs unpredictible tactics... still it would break many user developments


Last updated: Jul 23 2024 at 20:01 UTC