Stream: Coq devs & plugin devs

Topic: quiz


view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Oct 15 2020 at 13:13):

s/c/t/ ?

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Oct 15 2020 at 13:42):

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

view this post on Zulip Théo Zimmermann (Oct 15 2020 at 13:42):

What you are looking for is encompassed in the term_generalizing nonterminal.

view this post on Zulip Théo Zimmermann (Oct 15 2020 at 13:43):

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

view this post on Zulip 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?

view this post on Zulip Ralf Jung (Oct 15 2020 at 14:51):

wow how is that even legal syntax^^

view this post on Zulip 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 ;)

view this post on Zulip 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")

view this post on Zulip 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.~~

view this post on Zulip Paolo Giarrusso (Oct 15 2020 at 19:31):

Wait a sec

view this post on Zulip Paolo Giarrusso (Oct 15 2020 at 19:31):

How is x unbound in the goal?

view this post on Zulip Paolo Giarrusso (Oct 15 2020 at 19:33):

I see two bound occurrences, but both are bound

view this post on Zulip Paolo Giarrusso (Oct 15 2020 at 19:34):

x used to be unbound until the parent commit

view this post on Zulip Paolo Giarrusso (Oct 15 2020 at 19:35):

(see https://gitlab.mpi-sws.org/iris/stdpp/-/commit/c8bb51b2dae2fb03ace3d35c95b406cbb7a53aa6#bea97b576dbfb634e878d29fe3430ae55d29b731_299_299 )

view this post on Zulip Gaëtan Gilbert (Oct 15 2020 at 19:37):

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

view this post on Zulip 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).

view this post on Zulip 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).

view this post on Zulip Gaëtan Gilbert (Oct 15 2020 at 19:51):

it has an invisible `{} around the type (see https://github.com/coq/coq/issues/6042)
replacing it with forall {x}, ... fails

view this post on Zulip Paolo Giarrusso (Oct 15 2020 at 22:08):

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

view this post on Zulip Gaëtan Gilbert (Oct 16 2020 at 08:00):

what do you mean?

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip Paolo Giarrusso (Oct 16 2020 at 22:56):

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

view this post on Zulip 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...

view this post on Zulip Paolo Giarrusso (Oct 16 2020 at 22:58):

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

view this post on Zulip 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..

view this post on Zulip Paolo Giarrusso (Oct 16 2020 at 23:00):

and for this issue, Lemma foo x : c. is enough (implicit _arguments_ are irrelevant here).

view this post on Zulip 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)

view this post on Zulip Gaëtan Gilbert (Oct 17 2020 at 10:07):

yes it's about the command in its home context
renaming x works


Last updated: Oct 16 2021 at 03:02 UTC