Stream: VsCoq devs & users

Topic: impredicative set


view this post on Zulip Bas Spitters (Nov 12 2020 at 14:19):

What is the most convenient way to enable impredicative-set in vscoq. I assume using Coqproject works, but there may be easier ways.

view this post on Zulip Yannick Forster (Nov 12 2020 at 14:30):

Interesting, I was about to say "There should be a command similar to the command which displays implicit arguments", but there isn't. I don't know an answer, but maybe the easiest way is to add a "Set Impredicative Set" command to vscoq. Once you know what you're doing (@Fabian Kunze, can you help?) that might even be easy and universally helpful

view this post on Zulip Gaëtan Gilbert (Nov 12 2020 at 14:34):

coqproject is your best bet
for unclear reasons impredicative set may not be enabled except by the command line argument

view this post on Zulip Yannick Forster (Nov 12 2020 at 14:35):

Oh, so it's not a vscoq issue, you can also not enable it in Proof General?

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

@Gaëtan Gilbert rather, for unclear reason we allow to set some flags that don't get along together from inside a Coq file.

view this post on Zulip Théo Zimmermann (Nov 12 2020 at 14:42):

In PG, you can do exactly the same (use -arg -impredicative-set in _CoqProject) or use one of the special custom PG configuration variables.

view this post on Zulip Théo Zimmermann (Nov 12 2020 at 14:42):

Pierre-Marie Pédrot said:

Gaëtan Gilbert rather, for unclear reason we allow to set some flags that don't get along together from inside a Coq file.

Like?

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

Like type-in-type.

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

This breaks SR and currently one can fool the checker that way.

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

I am not saying it's a fundamental problem, but being able to locally change the flags governing the kernel rules requires some serious changes in the checker architecture.

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

Also, it's a footgun.

view this post on Zulip Gaëtan Gilbert (Nov 12 2020 at 14:53):

flags that don't get along together

What doe that mean? They start a Coq fight?

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

Or you beat the kernel up.

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

And get random anomalies (in the best case).

view this post on Zulip Gaëtan Gilbert (Nov 12 2020 at 14:54):

the checker already understands declaration-local flags though
(although it gets confused if you change the flag between a section variable and a definition using it)

view this post on Zulip Gaëtan Gilbert (Nov 12 2020 at 14:55):

ty-in-ty is more about nontermination than anomalies

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

If you set it then unset it, you'll have a hard time when unfolding type-in-type defs inside non-type-in-type ones.

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

The only reasonable use of local type-in-type is for stuff that is not unfoldable, e.g. inductive types and axioms.

view this post on Zulip Gaëtan Gilbert (Nov 12 2020 at 14:56):

so you get some type errors, isn't that the user's problem?

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

Or anomalies.

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

Maybe loops, who knows.

view this post on Zulip Gaëtan Gilbert (Nov 12 2020 at 14:57):

what anomalies?

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

I don't have a reproducible example right here but essentially both the checker and the kernel rely implicitly on SR in various parts.

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

Since locally tweaking the kernel rules breaks SR, it's definitely a problem.

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

(And I wouldn't bet on the absence of soundness issues in the checker from this kind of tricks either.)

view this post on Zulip Gaëtan Gilbert (Nov 12 2020 at 15:10):

do they really? I've tried to find anomalies from lack of SR but couldn't figure out how to do it

view this post on Zulip Pierre-Marie Pédrot (Nov 12 2020 at 15:11):

With SProp it should be even easier, shouldn't it?

view this post on Zulip Pierre-Marie Pédrot (Nov 12 2020 at 15:12):

Like, if you can postulate SProp : SProp, you're breaking one of the assumptions of conversion

view this post on Zulip Pierre-Marie Pédrot (Nov 12 2020 at 15:12):

That sorts are always proof relevant

view this post on Zulip Pierre-Marie Pédrot (Nov 12 2020 at 15:12):

now you hide that SProp under a definition

view this post on Zulip Gaëtan Gilbert (Nov 12 2020 at 15:12):

you can get errors easily, but not anomalies

view this post on Zulip Pierre-Marie Pédrot (Nov 12 2020 at 15:13):

I had a few theoretical POCs from type-in-type at a point

view this post on Zulip Pierre-Marie Pédrot (Nov 12 2020 at 15:13):

But it's stuff that is really hard to exploit because you need to hit right in the blind spots of UGraph and friends.

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

I guess I could have crafted a vo but that's kind of heavyweight

view this post on Zulip Paolo Giarrusso (Nov 12 2020 at 16:00):

wait I can enable type-in-type and get past the checker?

view this post on Zulip Paolo Giarrusso (Nov 12 2020 at 16:01):

you know that the French certification authority gives some official trust on the checker :-P

view this post on Zulip Pierre-Marie Pédrot (Nov 12 2020 at 16:02):

See https://github.com/coq/coq/issues/11477

view this post on Zulip Pierre-Marie Pédrot (Nov 12 2020 at 16:04):

in this case it's closer to Pollack-inconsistency than actual inconsistency

view this post on Zulip Pierre-Marie Pédrot (Nov 12 2020 at 16:04):

(but there are ways to build handcrafted vos proving False that the checker happily accepts.)

view this post on Zulip Théo Winterhalter (Nov 12 2020 at 16:17):

And Print Assumptions doesn't track definitions that use local type in type I suppose?

view this post on Zulip Kenji Maillard (Nov 12 2020 at 16:25):

It does

Unset Universe Checking.
Definition a : Type := nat.
Set Universe Checking.
Print Assumptions a.
(* Axioms: *)
(* a relies on an unsafe hierarchy. *)

view this post on Zulip Théo Winterhalter (Nov 12 2020 at 16:26):

So the proof of False Pierre-Marie mentions would not be marked as safe then.

view this post on Zulip Pierre-Marie Pédrot (Nov 12 2020 at 16:27):

It's not safe by unfolding.

view this post on Zulip Pierre-Marie Pédrot (Nov 12 2020 at 16:27):

Also Print Assumption is literal piece of garbage.

view this post on Zulip Pierre-Marie Pédrot (Nov 12 2020 at 16:28):

It's a pile of hacks that tries to pierce opacity information in modules, with a bit of duct tape here and there to convince ourselves that we're not doing batshit crazy stuff.

view this post on Zulip Pierre-Marie Pédrot (Nov 12 2020 at 16:29):

The checker is slightly saner but even there it's an approximation (hopefully a sound one, but it's not even clear)

view this post on Zulip Pierre-Marie Pédrot (Nov 12 2020 at 16:37):

Here is a proof that print assumptions is not working:

Universe i j.
Monomorphic Constraint i < j.

Module Type S.

Parameter Inline T : Type@{i}.

End S.

Module F (X : S).

Include X.

End F.

Module LOL <: S.

Unset Universe Checking.

Definition T : Type@{i} := Type@{j}.

Set Universe Checking.

End LOL.

Module PROFIT := F(LOL).

Print PROFIT.T.
Print Assumptions PROFIT.T.

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

Similar hack without functors but with sections:

Universe i j.
Monomorphic Constraint i < j.

Section Foo.

Unset Universe Checking.

Let T : Type@{i} := Type@{j}.

Set Universe Checking.

Definition S : Type@{i} := T.

End Foo.

Print S.
Print Assumptions S.

view this post on Zulip Paolo Giarrusso (Nov 12 2020 at 17:28):

On https://github.com/coq/coq/issues/11477, how hard would it be to change --output-context’s default for coqchk?

view this post on Zulip Paolo Giarrusso (Nov 12 2020 at 17:29):

It sounds like it should be easy enough, even for contributors?

view this post on Zulip Bas Spitters (Nov 13 2020 at 09:27):

Coqproject is a workable solution. In PG one can do this:

(* Remember to reload the buffer in Emacs for Proof General to take the local variables into account. *)
(*
 *** Local Variables: ***
 *** coq-prog-args: ("-impredicative-set") ***
 *** End: ***
 *)

Last updated: Jan 30 2023 at 19:04 UTC