Stream: Coq users

Topic: Injection intro patterns

Ralf Jung (Oct 15 2020 at 16:16):

Is there a deep reason why [= ...] as intro pattern does not work in destruct? I end up writing silly things like revert Hlookup'. intros [= <-]. because destruct Hlookup' as [= <-]. does not work...

Théo Zimmermann (Oct 15 2020 at 16:35):

Hum. What is it you are trying to do? Only an injection? Or a destruct + an injection?

Maxime Dénès (Oct 15 2020 at 16:36):

a destruct, an injection and a rewrite

Théo Zimmermann (Oct 15 2020 at 16:37):

If that's the case, then I would expect to see something like destruct Hlookup' as [ [= <- ] ]. (which should work)

Maxime Dénès (Oct 15 2020 at 16:37):

what do the first brackets mean?

Théo Zimmermann (Oct 15 2020 at 16:38):

They are for the destructing intro-pattern. But note that I'm talking without testing because I don't know the precise example.

Maxime Dénès (Oct 15 2020 at 16:39):

if the brackets are for destructuring, what is destruct for?

Théo Zimmermann (Oct 15 2020 at 16:39):

Well, you always end up repeating the tactic in the intro pattern when you use vanilla as clauses.

Maxime Dénès (Oct 15 2020 at 16:39):

said otherwise, what's the difference between destruct H as x y and destruct H as [x y]?

Théo Zimmermann (Oct 15 2020 at 16:40):

destruct H as x y is not supported AFAICT

Maxime Dénès (Oct 15 2020 at 16:40):

Théo Zimmermann said:

repeating the tactic in the intro pattern when you use vanilla as clauses.

Does that even make sense? How do you repeat inversion for example?

Théo Zimmermann (Oct 15 2020 at 16:41):

And if @Ralf Jung did not want to do a destruct, but just an injection + a rewrite, then the way to do it would be injection as [= <- ].

Théo Zimmermann (Oct 15 2020 at 16:41):

How do you repeat inversion for example?

Théo Zimmermann (Oct 15 2020 at 16:41):

WDYM?

Théo Zimmermann (Oct 15 2020 at 16:42):

Oh, I see!

Maxime Dénès (Oct 15 2020 at 16:42):

you say destruct H as [x y], injection H as [= x y], inversion H as ... ?

Théo Zimmermann (Oct 15 2020 at 16:42):

Well, let's say this is an exception because there is no inversion intro-pattern.

Maxime Dénès (Oct 15 2020 at 16:42):

lol

Maxime Dénès (Oct 15 2020 at 16:43):

I hadn't realized this design, thanks for the explanation anyway

Théo Zimmermann (Oct 15 2020 at 16:43):

Note that injection also used to be like inversion but Hugo changed it to be like destruct (but it still support the old way)

Ralf Jung (Oct 15 2020 at 16:58):

I don't think I understand the disucssion here... but by expectation is that destruct X as pat and revert X; intros pat are the same thing

Ralf Jung (Oct 15 2020 at 16:58):

and that mostly works except for = patterns

Ralf Jung (Oct 15 2020 at 16:58):

which seems rather odd

Ralf Jung (Oct 15 2020 at 16:58):

however, injection Hlookup' as [= <-] works :)

Maxime Dénès (Oct 15 2020 at 16:58):

IIUC, your expectation is "wrong" (or the design is)

Théo Zimmermann (Oct 15 2020 at 16:59):

Well, the design is what it is.

Maxime Dénès (Oct 15 2020 at 16:59):

destruct X as [pat] is revert X; intros pat

Ralf Jung (Oct 15 2020 at 16:59):

Maxime Dénès said:

destruct X as [pat] is revert X; intros pat

no that's not true

Théo Zimmermann (Oct 15 2020 at 16:59):

hum, no.

Maxime Dénès (Oct 15 2020 at 16:59):

ah?

Maxime Dénès (Oct 15 2020 at 16:59):

then I didn't understand

Théo Zimmermann (Oct 15 2020 at 16:59):

destruct X as [pat] is really revert X; intros [pat].

Ralf Jung (Oct 15 2020 at 16:59):

destruct X as [A B] is the same as revert X; intros [A B]

Théo Zimmermann (Oct 15 2020 at 16:59):

Yes

Maxime Dénès (Oct 15 2020 at 16:59):

ah yes, sorry

Ralf Jung (Oct 15 2020 at 16:59):

but it doesnt work for other patterns

Théo Zimmermann (Oct 15 2020 at 17:00):

destruct only allows destructuring intro-patterns

Ralf Jung (Oct 15 2020 at 17:00):

there seems to be some arbirary restriction then that the top-level pattern must not be = or so

Maxime Dénès (Oct 15 2020 at 17:00):

yes, injection X as [= A B] is the same as revert X; intros [= A B]

Ralf Jung (Oct 15 2020 at 17:00):

(I seem to recall it actually works in nested places which confused me even more)

Théo Zimmermann (Oct 15 2020 at 17:01):

What would destruct even mean if you could use it with any pattern?

Théo Zimmermann (Oct 15 2020 at 17:01):

Note that Hugo has proposed a neutral tactic to use the as clause.

Théo Zimmermann (Oct 15 2020 at 17:01):

I think the proposed name was onto

Théo Zimmermann (Oct 15 2020 at 17:01):

let me dig up the PR

Ralf Jung (Oct 15 2020 at 17:01):

Théo Zimmermann said:

destruct only allows destructuring intro-patterns

that's not true either, this works:

Lemma foo (a b : nat) : (True ∧ Some a = Some b) → a = b.
Proof. intros HX.
destruct HX as [_ [= ->]].

Maxime Dénès (Oct 15 2020 at 17:02):

I guess this is still a destructuring intro-pattern, isn't it ?

Ralf Jung (Oct 15 2020 at 17:02):

Théo Zimmermann said:

What would destruct even mean if you could use it with any pattern?

it means "apply a destruct pattern". that's what the patterns you just called "intro patterns" are called in my head.

Ralf Jung (Oct 15 2020 at 17:03):

or maybe you could say, since intro patterns "destruct" a value (in the wider sense of taking it apart, including injectivity), destruct is jsut a way to let you apply intro patterns to things that are already introduced

Ralf Jung (Oct 15 2020 at 17:03):

Maxime Dénès said:

I guess this is still a destructuring intro-pattern, isn't it ?

I mean at that point the definition of "destructuring intro-pattern" seems to be "whatever destruct accepts" which is somewhat circular

Théo Zimmermann (Oct 15 2020 at 17:04):

Maxime Dénès said:

I guess this is still a destructuring intro-pattern, isn't it ?

It is

Ralf Jung (Oct 15 2020 at 17:04):

to me it seems like the pattern engine clearly can handle product, sum and injection patterns with arbitrary nesting. but there is a totally arbitrary-seeming restricting that with destruct, the top-level pattern must be product or sum pattern but not injection pattern.

Ralf Jung (Oct 15 2020 at 17:05):

I can learn this restriction but I cannot make sense of it.

Ralf Jung (Oct 15 2020 at 17:05):

Théo Zimmermann said:

Maxime Dénès said:

I guess this is still a destructuring intro-pattern, isn't it ?

It is

it clearly uses injection though

Théo Zimmermann (Oct 15 2020 at 17:06):

Yes, but nested.

Théo Zimmermann (Oct 15 2020 at 17:06):

You can put whatever you want if you nest it inside a destruct intro-pattern.

Ralf Jung (Oct 15 2020 at 17:06):

yes so what? basic compositionality demands that this should make no difference

Théo Zimmermann (Oct 15 2020 at 17:06):

And it's easy to explain why it only accepts destruct intro-pattern at top-level.

Maxime Dénès (Oct 15 2020 at 17:06):

Ralf Jung said:

basic compositionality

ah ah

Ralf Jung (Oct 15 2020 at 17:06):

I think this is what that is so surprising to me

Ralf Jung (Oct 15 2020 at 17:07):

Théo Zimmermann said:

Théo Zimmermann said:

And it's easy to explain why it only accepts destruct intro-pattern at top-level.

This is just so that as doesn't extend the expressive power of destruct.

but it does. without as it'll never use injection, with as it can, but only nested

Ralf Jung (Oct 15 2020 at 17:08):

I'd buy this argument if destruct would not allow any nesting

Théo Zimmermann (Oct 15 2020 at 17:08):

OK anyway, please open an issue to propose to remove this limitation.

Ralf Jung (Oct 15 2020 at 17:09):

I'll do, thanks :)

Théo Zimmermann (Oct 15 2020 at 17:09):

This would basically mean that the generic as tactic proposed by @Hugo Herbelin would be named destruct instead of what he was proposing.

Théo Zimmermann (Oct 15 2020 at 17:09):

(I cannot retrieve the PR anymore.)

Maxime Dénès (Oct 15 2020 at 17:09):

I don't think it would be the same

Maxime Dénès (Oct 15 2020 at 17:10):

or maybe it would

Théo Zimmermann (Oct 15 2020 at 17:10):

I think it would

Maxime Dénès (Oct 15 2020 at 17:10):

hum no

Maxime Dénès (Oct 15 2020 at 17:10):

destruct H as [= x y] should do two things

Maxime Dénès (Oct 15 2020 at 17:10):

right?

Maxime Dénès (Oct 15 2020 at 17:11):

a destruction and an injection

Maxime Dénès (Oct 15 2020 at 17:11):

or not?

Maxime Dénès (Oct 15 2020 at 17:11):

anyway, @Ralf Jung we could also add a variant of the arrow to ssr that rewrites everywhere

Maxime Dénès (Oct 15 2020 at 17:12):

I thought we had it at some point let me look in my notes

Ralf Jung (Oct 15 2020 at 17:12):

Maxime Dénès said:

a destruction and an injection

looks like you think there is an implicit outer [...] with destruct?

Ralf Jung (Oct 15 2020 at 17:12):

but there isn't, so I am confused

Ralf Jung (Oct 15 2020 at 17:12):

Maxime Dénès said:

anyway, Ralf Jung we could also add a variant of the arrow to ssr that rewrites everywhere

that seems very un-ssreflect-like, given e.g. behavior of case

Maxime Dénès (Oct 15 2020 at 17:13):

Easycrypt (which has an extension of ssr's tactics essentially) has it, I believe

Maxime Dénès (Oct 15 2020 at 17:13):

substituting an equation everywhere is not so fragile

Ralf Jung (Oct 15 2020 at 17:13):

Ralf Jung said:

Maxime Dénès said:

a destruction and an injection

looks like you think there is an implicit outer [...] with destruct?

i.e. that statement would hold if destruct X as pat was revert X; intros [pat]. but it's not.

Théo Zimmermann (Oct 15 2020 at 17:17):

Maxime Dénès said:

or not?

It wouldn't. You would still need to provide an explicit [ ] to destruct.

Théo Zimmermann (Oct 15 2020 at 17:17):

I.e. the as clause would still be fully explicit.

Ralf Jung (Oct 15 2020 at 17:26):

Théo Zimmermann said:

OK anyway, please open an issue to propose to remove this limitation.

https://github.com/coq/coq/issues/13205

Hugo Herbelin (Oct 15 2020 at 17:43):

As I was pinged:

there is no inversion intro-pattern

There is no reason per se not to have an inversion intro-pattern. I did not do it because I don't consider inversion as nicely designed enough to do it.

But I have for instance a branch somewhere with an induction intro-pattern. I did not insist because I felt so many resistance about intro-pattern extensions from various developers without actually being able to understand well why there was a resistance that I renounced. I would however remain delighted to have design discussions about introduction patterns with developers, because we could clearly do much better that what we have now with a bit of collaboration.

I will reply at https://github.com/coq/coq/issues/13205 too.

Paolo Giarrusso (Oct 15 2020 at 17:47):

interesting discussion. Seems ssreflect's more compositional here?

Paolo Giarrusso (Oct 15 2020 at 17:49):

(indeed move supports both injection and destruct, and case => pats just adds an extra destruction step — it seems equivalent to move => [] pats)

Hugo Herbelin (Oct 15 2020 at 19:03):

For the record, the discussion on a generic on was there.

(indeed move supports both injection and destruct, and case => pats just adds an extra destruction step — it seems equivalent to move => [] pats)

Technically, it is => and not move which supports different patterns. move in itself is basically idtac together with (IIRC) an extra hack so that move => [...] is interpreted as a destruct rather than as a dispatch.

To feed the discussion, see also #136 which incidentally gives a hint at how Coq developers are good at dispersing their energy about tactics, even though there are many interesting tactic features to develop though.

Paolo Giarrusso (Oct 15 2020 at 19:09):

That’s a huge discussion! And a hybrid between “Wadler’s law” and fundamental research problems such as “how to evaluate a language design”.

Paolo Giarrusso (Oct 15 2020 at 19:10):

and for extra fun, this is a language for controlling program synthesis — tho honestly intro patterns seem basically a different take on pattern matching.

Paolo Giarrusso (Oct 15 2020 at 19:11):

(Scala, Haskell, Agda all have different takes on “views” via pattern synonyms, extractors, etc.).

Ralf Jung (Oct 16 2020 at 11:35):

It seems to me that introduction patterns users are currently split. If they want to use specialization on the fly, or apply in on the fly with generalization, or simpl on the fly, or easy/done on the fly, they have to use ssreflect => but if they want Coq's style [=], or Coq 's style ->, or Coq's structured patterns, then they cannot use what ssreflect proposes. This is suboptimal and something should be done to improve the situation.

:+1:

Ralf Jung (Oct 16 2020 at 11:35):

indeed I quite often wanted "simpl on the fly" in an otherwise coq-style pattern recently

Ralf Jung (Oct 16 2020 at 11:36):

OTOH, I find ssreflect's special treatment of the first pattern in => [...] to mean "dispatch over the subgoals" very surprising and somewhat inconsistent... it also necessitates a strange syntax to opt-out of that, which IIRC is =>- [...] or so, but I can never remember

Enrico Tassi (Oct 16 2020 at 15:14):

The irregularity in SSR is a bit unfortunate, I know, but case: x => [a|b] making 2 case split would be worse, since one would need to opt out more often than not. As an alternative, we tried to have a syntax for "only branching" here https://github.com/coq/coq/pull/9195

Enrico Tassi (Oct 16 2020 at 15:15):

With that syntax for non-case branching, one could make [] more regular and do always case.
But we would also need a tool to apply a silly replacement to all existing SSR scripts...

Ralf Jung (Oct 16 2020 at 17:05):

Enrico Tassi said:

The irregularity in SSR is a bit unfortunate, I know, but case: x => [a|b] making 2 case split would be worse, since one would need to opt out more often than not. As an alternative, we tried to have a syntax for "only branching" here https://github.com/coq/coq/pull/9195

yeah I am sure it is a well-motivated non-uniformity, and I cannot really come up with a better proposal.

I am wondering, why can't the | here itself be "the thing that does the splitting"? that's more like how it works with Coq's and Iris' intro patterns I believe.

Pierre Courtieu (Oct 16 2020 at 17:38):

I have been pleading for real as tactical applicable on the resulting goals of any tactic? Why has it to be a per-tactic thing?
I know this would be very incompatible with current as but it would be so much easier to use...

Pierre Courtieu (Oct 16 2020 at 17:41):

and semi-automatically generate too.

Hugo Herbelin (Oct 16 2020 at 19:01):

Ralf Jung said:

It seems to me that introduction patterns users are currently split. If they want to use specialization on the fly, or apply in on the fly with generalization, or simpl on the fly, or easy/done on the fly, they have to use ssreflect => but if they want Coq's style [=], or Coq 's style ->, or Coq's structured patterns, then they cannot use what ssreflect proposes. This is suboptimal and something should be done to improve the situation.

:+1:

That's a big issue and that would be great to get help to resolve this split!

As far as I'm concerned, when ssreflect was integrated to Coq 3½ years ago, I had the hope that this would eventually help getting a convergence between the best of ssreflect features and the best of Vanilla Coq features. Having a convergence of introduction patterns was part of this hope. I made a couple of tentatives to go in this direction, with various reactions from the other developers. For instance, I started at some time to implement a support for arbitrary introduction patterns so that it'll be easy for any user to add a short notation for simpl, or auto, or ring, or any other tactics producing 0 or 1 goals. Unfortunately, I got a very strong resistance from some developers. At another time, I proposed to make the two introduction pattern interpretation engines of ssr and Coq converge and I got again a resistance from some (other) developpers. (Of course, I could also have tried to work alone in this direction but this was not my expectations. There are so many many interesting things to implement in Coq that my current priority is not to fight but rather to form a consensus so that we can make our energies go in the same direction, even if this is not easy.)

Technical solutions exist to resolve the split. In particular, adding specialization on the fly to vanilla patterns, or providing a variant of % that generalizes, or supporting custom patterns abbreviating any 0-or-1-goal producing tactic so as to allow an equivalent to // and /= would be relatively easy. But I don't want to repeat what happened when I implemented the %foo pattern and I don't think that it makes sense that I contribute to resolving the split alone without a clear support of the development team or, at least, of the users.

I'm otherwise pretty sure that, in their heart, the ssreflect maintainers would also be happy, even if it requires a bit of technical and human efforts, that the split is resolved, because this split is good for noone. But it is probably not good either that I talk in their place, so maybe do they want to comment by themselves.

Hugo Herbelin (Oct 16 2020 at 19:06):

Pierre Courtieu said:

I have been pleading for real as tactical applicable on the resulting goals of any tactic? Why has it to be a per-tactic thing?
I know this would be very incompatible with current as but it would be so much easier to use...

I agree, and, somehow, isn't ssreflect => what you are asking for? Providing a => Vanilla side would be easy (there is actually already the PR #136 that I mentioned above). Providing a => which at the same time subsumes ssreflect => and provides Vanilla-style introduction patterns would be more challenging but not out of reach.

Pierre Courtieu (Oct 16 2020 at 21:35):

I agree, and, somehow, isn't ssreflect => what you are asking for? Providing a => Vanilla side would be easy (there is actually already the PR #136 that I mentioned above).

Yes => is what we want. But its vanilla version: it would apply directly to an hypothesis of the context.

Yannick Forster (Oct 17 2020 at 08:50):

I didn't follow the detailed discussion, but wanted to mention that I often do specialize H as pat which should be completely equivalent to revert H; intros H as pat. It's counterintuitive for readers, but that way I don't have to remember which tactic accepts which pattern.

Ralf Jung (Oct 21 2020 at 08:01):

Technical solutions exist to resolve the split. In particular, adding specialization on the fly to vanilla patterns, or providing a variant of % that generalizes, or supporting custom patterns abbreviating any 0-or-1-goal producing tactic so as to allow an equivalent to // and /= would be relatively easy. But I don't want to repeat what happened when I implemented the %foo pattern and I don't think that it makes sense that I contribute to resolving the split alone without a clear support of the development team or, at least, of the users.

FWIW, the things that surprised me most about %foo is how different it is from the ssreflect /foo, and in particular the strange effects it has on evaluation order: H%foo has foo applied before H is evaluated (right-to-left order) except that H%foo%bar still has these two lemmas applied in left-to-right order... so there is not even a way to describe the semantics of %foo by just traversing the syntax tree of patterns, at least not if the syntax tree looks as one would intuitively expected: pat ::= ... | pat%lemma. One instead needs a more complicated syntax tree where pat%lemma1...%lemmaN is a single production rule and pat itself must not have a top.level %... that is very counterintuitive.

I wonder what the reasons were to not just copy ssreflect syntax unchanged? It has proven to work very well, after all.

Maxime Dénès (Oct 21 2020 at 08:40):

I wonder what the reasons were to not just copy ssreflect syntax unchanged? It has proven to work very well, after all.

IIRC, this was more or less the feedback that was given by the development team at the time.

Théo Zimmermann (Oct 21 2020 at 09:35):

It was introduced in 8.5 though, so before proper reviewing happened through pull requests. The changelog notes that "The feature and syntax are in experimental stage". I wonder what impact would have a change to the semantic of this intro pattern.

Last updated: Oct 03 2023 at 02:34 UTC