Stream: Coq users

Topic: Local Definition ignored by `Import`?!?


view this post on Zulip Paolo Giarrusso (Nov 14 2020 at 01:40):

IMHO, making Definition foo local should prevent it from being _imported_. That works.
However, as soon as the containing module bar is required, bar.foo should IMHO work. That doesn't always work.

inside a file, Local Definition works as I'd expect:

Module Import A.
Local Definition test1 := 1.
Definition test2 := 1.
End A.
Local Definition test2 := A.test1.
Definition test3 := A.test1.

I'm more confused by the semantics wrt Require:

Require Import D.testLocalDefA.

(* OK *)
Definition test3' := test3.
Definition test3'a := testLocalDefA.test3.

(* OK *)
Fail Definition test3 := test2.
Definition test3 := testLocalDefA.test2.

(* WAT? *)
Fail Definition test4 := A.test1.
Definition test4 := testLocalDefA.A.test1.

Definition test5 := A.test2.
Definition test5' := testLocalDefA.A.test2.

AFAICS, using A.test1 requires one more qualification than I'd expect. I have no idea why.

view this post on Zulip Paolo Giarrusso (Nov 14 2020 at 01:44):

Possible explanation: Import skips local definitions recursively?

view this post on Zulip Paolo Giarrusso (Nov 14 2020 at 01:45):

so Import A skips making test1 available, correctly, but when Import D.testLocalDefA imports testLocalDefA, and it makes A globally available, it recursively filters out test1.

view this post on Zulip Li-yao (Nov 14 2020 at 01:46):

Local makes it so the only way to use a name is to qualify it completely.

view this post on Zulip Paolo Giarrusso (Nov 14 2020 at 01:46):

"qualify it completely" is not true

view this post on Zulip Paolo Giarrusso (Nov 14 2020 at 01:46):

see above

view this post on Zulip Paolo Giarrusso (Nov 14 2020 at 01:47):

I can skip the initial prefix D for some reason, and however many levels appear there.

view this post on Zulip Paolo Giarrusso (Nov 14 2020 at 01:48):

so if D.testLocalDefA. where instead A.B.C.D.testLocalDefA., I'd just need to repeat testLocalDefA

view this post on Zulip Paolo Giarrusso (Nov 14 2020 at 01:48):

(as if Require ignored local instead? dunno)

view this post on Zulip Paolo Giarrusso (Nov 14 2020 at 01:48):

(this assumes that Import works by deep-copying dictionaries, instead of linking them, which is a pretty weird idea, but you can ignore that part if it doesn't help)

view this post on Zulip Paolo Giarrusso (Nov 14 2020 at 01:49):

@Li-yao but would that semantics be useful/desirable/predictable?

view this post on Zulip Paolo Giarrusso (Nov 14 2020 at 01:51):

things work as I'd expect without nested modules... so I noticed because I failed to make sense of the behavior

view this post on Zulip Li-yao (Nov 14 2020 at 01:52):

Okay I thought it was a little stricter than that. :shrug:

view this post on Zulip Paolo Giarrusso (Nov 14 2020 at 01:53):

Well you weren't alone:

They [Definition and Example] can take the local attribute, which makes the defined ident accessible by Import and its variants only through their fully qualified names.

https://coq.github.io/doc/v8.12/refman/language/core/definitions.html#coq:cmd.definition

view this post on Zulip Li-yao (Nov 14 2020 at 01:57):

Modulo the prefix D, your examples seem to work as described by that sentence, don't they?

view this post on Zulip Paolo Giarrusso (Nov 14 2020 at 01:58):

Sorta. In another example, after From bedrock.lang.cpp.logic Require Import simple_pointers., I can just start from simple_pointers.

view this post on Zulip Paolo Giarrusso (Nov 14 2020 at 02:00):

that is, if simple_pointers contains Module A with local def test1, you must write simple_pointers.A.test1

view this post on Zulip Paolo Giarrusso (Nov 14 2020 at 02:01):

so, my theory works if simple_pointers is bound into the top-level by Require (which ignores the Local attribute), while A is bound by Import (which discards definitions marked Local).

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

Probably worth an issue, to decide whether the documentation should be fixed or the behavior changed.

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

Local Definition means Import does nothing, but Require still has an effect
Require Foo makes Foo available without needing to prefix it
so for instance after Require List. you can do Import List. instead of having to do Import Coq.Lists.List.


Last updated: Feb 04 2023 at 22:29 UTC