Stream: Coq users

Topic: Intro vs intros ?


view this post on Zulip Thomas Lamiaux (May 17 2024 at 22:12):

I have been asking myself a question for a while. What is the point of intro considering we have intros ?

view this post on Zulip Joomy Korkut (May 17 2024 at 23:58):

https://stackoverflow.com/a/50038115/2016295

view this post on Zulip Thomas Lamiaux (May 18 2024 at 00:11):

Thanks for the link that provides some information. According to the link the thing that is not supported by intros compared to intro is that intros do not support the options after / before / at top / at bottom.
But do we really care (even barely) about that ? Why was that even implemented ?

view this post on Zulip Ali Caglayan (May 18 2024 at 01:52):

I believe at some point there was only intro and you had to repeat that for intros. "some point" being 20 years ago. This was the folklore I picked up.

view this post on Zulip Pierre Roux (May 18 2024 at 08:18):

I'd also say intro is an historical artefact (Ltac1 is decades old and it is probably inevitable to have plenty of those). It should also be noted that intro and intros without arguments introduce automatically named variables, with the risk of explicitly referencing them, which is one of the most well known recipe for brittle proofs. Ssreflect on the other hand offers move=> ? that introduces an automatically named variable that cannot be explicitly referenced. The option -mangle-names can also be used to check for that issue.

view this post on Zulip Thomas Lamiaux (May 18 2024 at 13:42):

That is my understanding too. I find it very confusing for beginners to have two tactics intro and intros. It is literally introducing a difficulty right at the beginning.

view this post on Zulip Thomas Lamiaux (May 18 2024 at 13:45):

without arguments introduce automatically named variables, with the risk of explicitly referencing them,

it is not necessarily bad ?I many proofs you have stuffs like

induction n; intro m; destruct m; intros; auto using ...`

view this post on Zulip Théo Winterhalter (May 18 2024 at 15:48):

Yes I agree and also move => ? should just be the equivalent of intros ? so I don't think there's an actual mechanism (besides mangle names) which prevents you from using automatically generated names.

view this post on Zulip Pierre Roux (May 18 2024 at 17:24):

Théo Winterhalter said:

Yes I agree and also move => ? should just be the equivalent of intros ?

Unfortunately, it isn't, intros ? is pretty useless as it introduces a regular, unprotected, variable.
Théo Winterhalter said:

so I don't think there's an actual mechanism (besides mangle names) which prevents you from using automatically generated names.

Well, move=> ? does: it introduces a specially named variable _Hyp_ that cannot be explicitly referenced in the proof script.

view this post on Zulip Pierre Roux (May 18 2024 at 17:25):

Thomas Lamiaux said:

without arguments introduce automatically named variables, with the risk of explicitly referencing them,

it is not necessarily bad ?I

Yes, that's what I wrote, what's bad is explicitly referencing it (I would also argue that keeping it in the proof for multiple lines is also not so nice).

view this post on Zulip Théo Winterhalter (May 19 2024 at 11:46):

I see I was not aware of reserved identifiers. That's nice.

view this post on Zulip Pierre Courtieu (May 19 2024 at 12:33):

intro and ˋintros` have a different behaviour with respect to unfolding , don’t they?

view this post on Zulip Gaëtan Gilbert (May 19 2024 at 12:36):

isn't intro equivalent to intros ??

view this post on Zulip Pierre Courtieu (May 20 2024 at 12:10):

IMHO no: intro tries to unfold the head constant if no product is found.

view this post on Zulip Pierre Courtieu (May 20 2024 at 12:12):

Ho yes these two are equivalent (with the question mark).

view this post on Zulip Meven Lennon-Bertrand (May 20 2024 at 12:54):

Pierre Courtieu said:

Ho yes these two are equivalent (with the question mark).

Yes, that's the trick, having the question mark forces Coq to head-reduce to expose a product.

view this post on Zulip Thomas Lamiaux (May 20 2024 at 15:20):

So simple! :face_palm: I can't wait for @Pierre Rousselin to make a tuto about that :smile:

view this post on Zulip Thomas Lamiaux (May 20 2024 at 15:21):

But otherwise, I still think that in future version of coq that would be good to keep only intros

view this post on Zulip Thomas Lamiaux (May 20 2024 at 15:27):

It shouldn't be hard to make intro depreciated if intro x = intros x and intro. = intros ? ?
If it is used in the code of intros and hence we don't to remove it but make it unacessible it can always be renamed to sth like intros_aux ?

view this post on Zulip Théo Winterhalter (May 20 2024 at 15:29):

But also, it doesn't harm to have it if you don't advertise it?

view this post on Zulip Gaëtan Gilbert (May 20 2024 at 15:29):

it is entirely trivial to deprecate intro or remove, it's just about if we want to do it

view this post on Zulip Pierre Roux (May 20 2024 at 15:31):

The thing is that it's probably used a whole lot, so users could have to modify quite a lot of code (although you could provide a script to help them). You can open a pull request removing it if you want to assess the impact on the CI.

view this post on Zulip Pierre Roux (May 20 2024 at 15:33):

I'm not sure it's really worth deprecating intro knowing that intros is about just as bad in making introduction of unnamed variables easier than naming them.

view this post on Zulip Pierre Roux (May 20 2024 at 15:33):

FWIW, the long term plan rather seems to be deprecating ltac1 in favor of ltac2, although it seems we are not there yet.

view this post on Zulip Gaëtan Gilbert (May 20 2024 at 15:35):

ltac2 intros has the same behaviour, the ltac1 -> ltac2 change is irrelevant to this discussion IMO

view this post on Zulip Thomas Lamiaux (May 20 2024 at 15:38):

It seems to me that the issue is that they are too close together. So even if you want to use intros and always teach that, as a user you will at a point or another forget the s and end up using intro and getting confuse. If it was intros and intros_aux it wouldn't be an issue, same it is there is a warning depreciated on intro.

view this post on Zulip Théo Winterhalter (May 20 2024 at 15:42):

I feel like it's ok, it's intros without the s so it's singular, so exactly one introduction.

view this post on Zulip Gaëtan Gilbert (May 20 2024 at 15:45):

if you want to try making a PR, this patch should do it

modified   plugins/ltac/coretactics.mlg
@@ -195,17 +195,28 @@ TACTIC EXTEND intros_until
 | [ "intros" "until" quantified_hypothesis(h) ] -> { Tactics.intros_until h }
 END

+{
+
+let warn_deprecated_intro = CWarnings.create ~name:"deprecated-intro" ~category:Deprecation.Version.v8_20
+    Pp.(fun () -> str "\"intro\" is deprecated, use \"intros\" instead.")
+
+let intro_move a b =
+  warn_deprecated_intro ();
+  Tactics.intro_move a b
+
+}
+
 TACTIC EXTEND intro
-| [ "intro" ] -> { Tactics.intro_move None MoveLast }
-| [ "intro" ident(id) ] -> { Tactics.intro_move (Some id) MoveLast }
-| [ "intro" ident(id) "at" "top" ] -> { Tactics.intro_move (Some id) MoveFirst }
-| [ "intro" ident(id) "at" "bottom" ] -> { Tactics.intro_move (Some id) MoveLast }
-| [ "intro" ident(id) "after" hyp(h) ] -> { Tactics.intro_move (Some id) (MoveAfter h) }
-| [ "intro" ident(id) "before" hyp(h) ] -> { Tactics.intro_move (Some id) (MoveBefore h) }
-| [ "intro" "at" "top" ] -> { Tactics.intro_move None MoveFirst }
-| [ "intro" "at" "bottom" ] -> { Tactics.intro_move None MoveLast }
-| [ "intro" "after" hyp(h) ] -> { Tactics.intro_move None (MoveAfter h) }
-| [ "intro" "before" hyp(h) ] -> { Tactics.intro_move None (MoveBefore h) }
+| [ "intro" ] -> { intro_move None MoveLast }
+| [ "intro" ident(id) ] -> { intro_move (Some id) MoveLast }
+| [ "intro" ident(id) "at" "top" ] -> { intro_move (Some id) MoveFirst }
+| [ "intro" ident(id) "at" "bottom" ] -> { intro_move (Some id) MoveLast }
+| [ "intro" ident(id) "after" hyp(h) ] -> { intro_move (Some id) (MoveAfter h) }
+| [ "intro" ident(id) "before" hyp(h) ] -> { intro_move (Some id) (MoveBefore h) }
+| [ "intro" "at" "top" ] -> { intro_move None MoveFirst }
+| [ "intro" "at" "bottom" ] -> { intro_move None MoveLast }
+| [ "intro" "after" hyp(h) ] -> { intro_move None (MoveAfter h) }
+| [ "intro" "before" hyp(h) ] -> { intro_move None (MoveBefore h) }
 END

 (** Move *)

view this post on Zulip Thomas Lamiaux (May 20 2024 at 15:46):

As I was way saying originally, I think it is introducing a difficulty right at the beginning for nothing, but It is a valid point of view to say it is not worth the effort and clear enough like that

view this post on Zulip Théo Winterhalter (May 20 2024 at 15:49):

Have you ever been confused by this, like it caused you problems when learning? It was never a problem for me, I was more like "cool, there is an even stronger intro", and I never saw anyone struggle because of this.
If it turns out people are struggling because of it, then it might be worth the effort.

view this post on Zulip Pierre Roux (May 20 2024 at 16:27):

Gaëtan Gilbert said:

ltac2 intros has the same behaviour, the ltac1 -> ltac2 change is irrelevant to this discussion IMO

Indeed, damn, forgot that.

view this post on Zulip Pierre Roux (May 20 2024 at 16:30):

Théo Winterhalter said:

Have you ever been confused by this, like it caused you problems when learning? It was never a problem for me, I was more like "cool, there is an even stronger intro", and I never saw anyone struggle because of this.
If it turns out people are struggling because of it, then it might be worth the effort.

My small experience of teaching Coq also seems to indicate that intro/intros is not a big issue. The actual issue being that it's way to easy to write it without arguments, leading students to introduce too many things without thinking about it.

view this post on Zulip Pierre Rousselin (May 20 2024 at 16:52):

There are many ways to introduce many things without thinking anyway...

view this post on Zulip Pierre Rousselin (May 20 2024 at 16:53):

In class I only ever use intros with names.

view this post on Zulip Pierre Roux (May 20 2024 at 16:56):

Pierre Rousselin said:

There are many ways to introduce many things without thinking anyway...

Sure, I'm not saying this is the only bad thing in ltac.

view this post on Zulip Pierre Rousselin (May 20 2024 at 16:58):

I also think there are other problems which are bigger by some orders of magnitude, so deprecating intro would not be my priority (even though, I'm always in favour of a bit of clean-up).

About why, I think it was a trend in the 90's 2000's for formal specification languages to try to stick to real languages. Coq has some of it: plurals, vernacular where we actually write (imperative) complete sentences. I would guess that could be an explanation about intros and intro, like Parameter and Parameters, etc...

view this post on Zulip Thomas Lamiaux (May 20 2024 at 17:02):

I don't know if it's confusing for general audience, but it is a bit for me.

view this post on Zulip Thomas Lamiaux (May 20 2024 at 17:03):

So I guess my point of view would be: I don't see any good reasons not to remove it as the cost seems low and automatable with a script (that needs to be provided)

view this post on Zulip Pierre Rousselin (May 20 2024 at 17:08):

@Thomas Lamiaux, you are very welcome to try it. There needs to be a deprecation phase of at least 2 versions before it is removed. Then, if one is bold enough to proceed with the removal, the CI will show which external library (which are part of the CI) will break and proceed to repair them with PRs on these libraries.
Repairing them should not be very hard, but the amount of build/repair/try to read some 50-line broken tactic could be scary.

view this post on Zulip Pierre-Marie Pédrot (May 20 2024 at 17:14):

If one is strictly included in the other why would there be two?

one is shorter than the other, I think this is the only advantage

view this post on Zulip Pierre Rousselin (May 20 2024 at 17:23):

Then, I suggest:

Tactic Notation "intr" := intros.

to remove the only advantage.

view this post on Zulip Théo Winterhalter (May 20 2024 at 17:35):

I think some people like that it's more "atomic".

view this post on Zulip Gaëtan Gilbert (May 20 2024 at 17:52):

Pierre Rousselin said:

Then, I suggest:

Tactic Notation "intr" := intros.

to remove the only advantage.

https://github.com/coq-contribs/cats-in-zfc/blob/master/tactics.v#L26

view this post on Zulip Pierre-Marie Pédrot (May 20 2024 at 18:10):

A little bit more effort, and we'll get to the level of Perl: https://www.mcmillen.dev/sigbovik/


Last updated: Jun 13 2024 at 19:02 UTC