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