Gaëtan Gilbert (Oct 15 2020 at 12:49): Gaëtan Gilbert (Oct 15 2020 at 12:49):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
Paolo Giarrusso (Oct 15 2020 at 13:13):s/c/t/ ?
Paolo Giarrusso (Oct 15 2020 at 13:14):And are there docs on backticks in conclusions, as opposed to assumptions? Never saw it before your PR
Théo Zimmermann (Oct 15 2020 at 13:42):https://coq.inria.fr/refman/language/extensions/implicit-arguments.html#implicit-generalization
Théo Zimmermann (Oct 15 2020 at 13:42):What you are looking for is encompassed in the term_generalizing nonterminal.
Théo Zimmermann (Oct 15 2020 at 13:43):And it's described in the third paragraph in the text.
Tej Chajed (Oct 15 2020 at 14:49):What if x's type requires an additional typeclass? Doesn't the former generalize that, too, while the latter doesn't?
Ralf Jung (Oct 15 2020 at 14:51):wow how is that even legal syntax^^
Gaëtan Gilbert (Oct 15 2020 at 14:53):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 ;)
Paolo Giarrusso (Oct 15 2020 at 17:51):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")
Gaëtan Gilbert (Oct 15 2020 at 18:01):~~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.~~
Paolo Giarrusso (Oct 15 2020 at 19:31):Wait a sec
Paolo Giarrusso (Oct 15 2020 at 19:31):How is x unbound in the goal?
Paolo Giarrusso (Oct 15 2020 at 19:33):I see two bound occurrences, but both are bound
Paolo Giarrusso (Oct 15 2020 at 19:34):x used to be unbound until the parent commit
Paolo Giarrusso (Oct 15 2020 at 19:35): Gaëtan Gilbert (Oct 15 2020 at 19:37):I didn't notice the commit had changed after I encountered the issue
Paolo Giarrusso (Oct 15 2020 at 19:38):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).
Gaëtan Gilbert (Oct 15 2020 at 19:38):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
Paolo Giarrusso (Oct 15 2020 at 22:08):Uh wait. I saw an issue. What if you annotate the type of x?
Gaëtan Gilbert (Oct 16 2020 at 08:00):what do you mean?
Paolo Giarrusso (Oct 16 2020 at 21:20):What if you write forall {x:A}, (if that's the right type) does that still fail?
Paolo Giarrusso (Oct 16 2020 at 21:24):(ah I think I saw https://github.com/coq/coq/issues/13170, but then I should retract my guess)
Gaëtan Gilbert (Oct 16 2020 at 21:39):that issue is unrelated
writing x:B (the type is B not A) works (command succeeds)
Paolo Giarrusso (Oct 16 2020 at 22:56):Wait. Is the issue about the command as-is in that context?
Paolo Giarrusso (Oct 16 2020 at 22:57):I cheated by trying this out, but IIUC, the problem cannot be reproduced with these 3 lines in isolation...
Paolo Giarrusso (Oct 16 2020 at 22:58):(and posting the minimized context would defeat the point of the quiz)
Paolo Giarrusso (Oct 16 2020 at 22:59):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..
Paolo Giarrusso (Oct 16 2020 at 23:00):and for this issue, Lemma foo x : c. is enough (implicit _arguments_ are irrelevant here).
Paolo Giarrusso (Oct 16 2020 at 23:02):what about Lemma foo y : c[x/y] :smiling_devil: (where c[x/y] is metanotation for substitution, not Coq notation)
Gaëtan Gilbert (Oct 17 2020 at 10:07):yes it's about the command in its home context
renaming x works
Last updated: Apr 20 2024 at 00:02 UTC