let `x`

be the only generalizable variable in the user syntax term `c`

when is `Lemma foo : `{c}.`

different from `Lemma foo : forall {x}, c.`

?

hint: it's not about forall vs fun

s/c/t/ ?

And are there docs on backticks in conclusions, as opposed to assumptions? Never saw it before your PR

https://coq.inria.fr/refman/language/extensions/implicit-arguments.html#implicit-generalization

What you are looking for is encompassed in the `term_generalizing`

nonterminal.

And it's described in the third paragraph in the text.

What if `x`

's type requires an additional typeclass? Doesn't the former generalize that, too, while the latter doesn't?

wow how is that even legal syntax^^

What if x's type requires an additional typeclass? Doesn't the former generalize that, too, while the latter doesn't?

the quiz is not typeclass related ;)

re "legal syntax", there's even an example:

`Definition sym`

(x:A) :`(x = y -> y = x) := fun _ p => eq_sym p.`

guess we just learned backticks from a source without such examples, like the math-classes paper (~"Typeclasses for mathematics in type theory")

~~since there are no guesses so far here is more info

in https://gitlab.mpi-sws.org/iris/stdpp/-/blob/c6e5d0bea614cee9a8abb2cee93070683b7debd9/theories/sets.v#L299-301.~~

Wait a sec

How is x unbound in the goal?

I see two bound occurrences, but both are bound

x *used* to be unbound until the parent commit

I didn't notice the commit had changed after I encountered the issue

Ah, I suspected. So I guess you were talking about:

Global Instance set_unfold_list_fmap {B} (f : A → B) l P :

(∀ y, SetUnfoldElemOf y l (P y)) →

SetUnfoldElemOf x (f <$> l) (∃ y, x = f y ∧ P y).

so the command is https://gitlab.mpi-sws.org/iris/stdpp/-/blob/7f934a946006b80e3c732a81ce8e7075eebebc13/theories/sets.v#L299-301

```
Global Instance set_unfold_list_fmap {B} (f : A → B) l P :
(∀ y, SetUnfoldElemOf y l (P y)) →
SetUnfoldElemOf x (f <$> l) (∃ y, x = f y ∧ P y).
```

it has an invisible ` `{} `

around the type (see https://github.com/coq/coq/issues/6042)

replacing it with `forall {x}, ...`

fails

Uh wait. I saw an issue. What if you annotate the type of x?

what do you mean?

What if you write forall {x:A}, (if that's the right type) does that still fail?

(ah I think I saw https://github.com/coq/coq/issues/13170, but then I should retract my guess)

that issue is unrelated

writing `x:B`

(the type is B not A) works (command succeeds)

Wait. Is the issue about the command as-is in that context?

I cheated by trying this out, but IIUC, the problem cannot be reproduced with these 3 lines in isolation...

(and posting the minimized context would defeat the point of the quiz)

and as you say, it’s not about `forall`

vs `fun`

— that is, `Lemma foo {x} : c.`

should behave like `Lemma foo : forall {x}, c.`

.

and for this issue, `Lemma foo x : c.`

is enough (implicit _arguments_ are irrelevant here).

what about `Lemma foo y : c[x/y]`

:smiling_devil: (where `c[x/y]`

is metanotation for substitution, not Coq notation)

yes it's about the command in its home context

renaming x works

Last updated: Dec 07 2023 at 09:01 UTC