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 `subst`

usage should be replace with more explicit rewriting in hypotheses to comply with code style.

Pinging @Quentin VERMANDE

Maybe we should document this in CONTRIBUTING.md?

The `remember`

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

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`

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

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

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

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

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.

In EC, we have the `->>`

intro-pattern that does a substitution of the top-level assumption.

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

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.

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`

.

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.

technically, the comment of @Cyril Cohen is wrong about vanilla `case`

which does nothing in the context, it is `destruct`

that modifies the context.

Where did we document the exclusion of `subst`

or similar tactics (`induction`

, `destruct`

)?

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!

And provide suitable replacements when required.

Only when `x`

is equal to `0`

:grinning_face_with_smiling_eyes:

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

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

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

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.

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.

In EC, `->>`

only works for variables, indeed. Otherwise, this is a rewriting and we expect people to use `rewrite`

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

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?

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

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

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

I think that the proposed syntax (with `{ ... }`

) is good.

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

Yes

We could also go lean-like and have `{x in ?}->>`

print the auto-completion of `?`

(Lean heuristic tactics that end with a `?`

print a non-heuristic version of themselves)

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

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

Cyril Cohen said:

(Lean heuristic tactics that end with a

`?`

print a non-heuristic version of themselves)

Matita's `auto by _`

? so sad...

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.

let's discuss subst in the next mathcomp meeting

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.

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

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?

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.

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.

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

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

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

Last updated: Jul 23 2024 at 20:01 UTC