Stream: Coq users

Topic: Non-recursive injection


view this post on Zulip Ralf Jung (Nov 18 2020 at 14:35):

Is there any way to use injection or the [= ...] pattern to apply one one level of injectivity? I am still working on a minimal example, but comments I saw before and behavior in our complex codebase indicate that currently, this will recursively apply injectivity as often as it can, which is not very modular and causes hard-to-handle side-effects in some of our tactics.

view this post on Zulip Ralf Jung (Nov 18 2020 at 14:37):

yeah, this:

Lemma test n m : S (S n) = S (S m) -> n = m.
Proof.
intros [= HS].

leads to a context n = m, but if you imagine the inner S being a constructor of a totally different inductive type than this can be very much not what you want. it seems strange that recursing is the default, and this is inconsistent with destruct where only the top-level inductive type is pattern matched.

view this post on Zulip Ralf Jung (Nov 18 2020 at 14:38):

unfortunately, ssreflect's move=>-[= HS] does the same thing.

view this post on Zulip Pierre-Marie Pédrot (Nov 18 2020 at 14:40):

Not that I know of. I was rereading this code half an hour ago and it seems to be recursive without a way to deactivate it.

view this post on Zulip Kenji Maillard (Nov 18 2020 at 14:51):

so destruct is using another codepath ?

view this post on Zulip Pierre-Marie Pédrot (Nov 18 2020 at 14:57):

No, I think @Ralf Jung was referring to the semantics of brackets in destruct.

view this post on Zulip Kenji Maillard (Nov 18 2020 at 14:59):

ah indeed, my bad

view this post on Zulip Enrico Tassi (Nov 18 2020 at 16:30):

You can also peel 1 constructor by using a lemma as a view, eg injective_S : forall x y, S x = S y -> x = y and then move=> /injective_S HS.

view this post on Zulip Paolo Giarrusso (Nov 18 2020 at 18:55):

stdpp has a typeclass for those lemmas, so move /inj. (or move => /inj) might work

view this post on Zulip Paolo Giarrusso (Nov 18 2020 at 18:56):

@Ralf Jung in ssreflect, why move=> -[= HS] instead of move=>[HS]?

view this post on Zulip Paolo Giarrusso (Nov 18 2020 at 18:56):

does ssreflect really do [= ?] patterns?

view this post on Zulip Ralf Jung (Nov 18 2020 at 19:27):

Enrico Tassi said:

You can also peel 1 constructor by using a lemma as a view, eg injective_S : forall x y, S x = S y -> x = y and then move=> /injective_S HS.

sure, if such a lemma has been proven that works (but is more verbose to type). stdpp's inj means I don't even have to remember the lemma name.
but this requries manually proving such a lemma for each injective Inductive constructor.

view this post on Zulip Ralf Jung (Nov 18 2020 at 19:28):

Paolo Giarrusso said:

Ralf Jung in ssreflect, why move=> -[= HS] instead of move=>[HS]?

defensive programming^^ I recall solving strange problems with ssreflect by adding that -, and my mental model is not solidified enough to be sure when it is needed and when not.

view this post on Zulip Paolo Giarrusso (Nov 18 2020 at 21:39):

Confused by the = as well

view this post on Zulip Paolo Giarrusso (Nov 18 2020 at 21:42):

Re -, I think it switches [] from "different actions for different goals" to "destruct/inject", but for move, you get destruct/inject by default (maybe because you never get multiple goals from move?)

view this post on Zulip Ralf Jung (Nov 19 2020 at 08:48):

Paolo Giarrusso said:

Confused by the = as well

that's just an injectivity pattern, no?

view this post on Zulip Enrico Tassi (Nov 19 2020 at 09:36):

Paolo Giarrusso said:

does ssreflect really do [= ?] patterns?

SSR should accept [= ... ] as a synonym of [...] when doing injection. [] is overloaded in SSR, and when Coq added an intro pattern for injection I suggested to use a different syntax, and I then I added the same syntax to SSR as well IIRC.

view this post on Zulip Ralf Jung (Nov 19 2020 at 10:05):

well, move=>[HS] also strips of both layers of injection, so this does not really help


Last updated: Feb 06 2023 at 13:03 UTC