Is subst idiomatic to math-comp · math-comp devs

Stream: math-comp devs

Topic: Is subst idiomatic to math-comp

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.

Pierre Roux (Mar 29 2024 at 07:51):

Pinging @Quentin VERMANDE

Pierre Roux (Mar 29 2024 at 07:52):

Maybe we should document this in CONTRIBUTING.md?

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.

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.

The D modifier is mentioned only for set difference, but it is now also used for addition, as in mulrDr

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.

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

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.

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.

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.

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.

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:

it may capture variables unintentionally and make it harder to find where in the script this capture happened
it may alter section variables, and this is a hard source of bugs AFAIK

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.

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 .

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.

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.

Yves Bertot (Mar 29 2024 at 12:12):

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

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!

Cyril Cohen (Mar 29 2024 at 14:11):

And provide suitable replacements when required.

Pierre-Yves Strub (Mar 29 2024 at 14:11):

Only when x is equal to 0 :grinning_face_with_smiling_eyes:

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.

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.

Pierre-Yves Strub (Mar 29 2024 at 19:04):

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

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.

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.

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

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.

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?

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.

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

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.

Pierre-Yves Strub (Mar 29 2024 at 22:04):

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

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

Pierre-Yves Strub (Mar 29 2024 at 22:05):

Yes

Cyril Cohen (Mar 29 2024 at 22:06):

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

Cyril Cohen (Mar 29 2024 at 22:07):

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

Pierre-Yves Strub (Mar 29 2024 at 22:07):

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

Cyril Cohen (Mar 29 2024 at 22:08):

In Lean:

If you do simp it's a full heureustic rewriting tactic with a huge db and thus very fragile and it might break in subsequent versions of the library
If you do simp? instead it does the same but prints a stable replacement simp only [h1, ..., hn] that you can copy-paste. (This replacement uses the explicit db of equations that is inside the brackets, so it is predictible again.)

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

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:

it is many years that I'd love to have a kind of auto? as you describe and I'd be happy to see a consensus emerging in this direction;
about subst: the "vanilla" tactics are not in stone and if there is some interest in a variant of subst x that makes explicit the name of the hypothesis stating the equality, that would be easy to implement (say e.g. with syntax subst x with H).
about intropattens, I'd love to see the ideas from ssreflect usable in Coq Vanilla (and possibly reciprocally), for a collective benefice.

Cyril Cohen (Apr 02 2024 at 07:46):

let's discuss subst in the next mathcomp meeting

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:

it is many years that I'd love to have a kind of auto? as you describe and I'd be happy to see a consensus emerging in this direction;

about subst: the "vanilla" tactics are not in stone and if there is some interest in a variant of subst x that makes explicit the name of the hypothesis stating the equality, that would be easy to implement (say e.g. with syntax subst x with H).

about intropattens, I'd love to see the ideas from ssreflect usable in Coq Vanilla (and possibly reciprocally), for a collective benefice.

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

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.

Pierre Roux (Apr 02 2024 at 08:40):

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

it gives users a way to avoid the danger
but if the dangerous behavior remains the default, the tactics keeps "pushing to the crime" (a good example of this is intros whose default is to introduce automatically named variables, I've seen it leading to very bad behaviors while teaching, induction is probably another example).

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

Cyril Cohen (Apr 02 2024 at 08:46):

Pierre Roux said:

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

it gives users a way to avoid the danger

but if the dangerous behavior remains the default, the tactics keeps "pushing to the crime" (a good example of this is intros whose default is to introduce automatically named variables, I've seen it leading to very bad behaviors while teaching, induction is probably another example).

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.

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.

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.

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.

Cyril Cohen (Apr 02 2024 at 12:10):

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

Last updated: Oct 13 2024 at 01:02 UTC