Stream: Coq users

Topic: ✔ Threading context between sections


view this post on Zulip Vincent Siles (Dec 09 2021 at 13:25):

Hi ! I have a section with some context:

Section Foo.
  Context (X: T).
  ...
End Foo.

Now I'd like to do another section (in another file) with the same context, so I don't have to pass X by hand all the time.

view this post on Zulip Karl Palmskog (Dec 09 2021 at 13:30):

people have used Load for this purpose, e.g.,

However, Dune does not like this at all, since you don't compile hCoefStructure.v into a .vo file

view this post on Zulip Vincent Siles (Dec 09 2021 at 13:32):

Not sure I undersand. If I have

Section Foo.
  Variable (X: T).
  Definition f ....
End Foo.

Section Bar.
  Variable (X: T).
   Definition  g := f. (* I don't want to write f X *)
End.

Is Load doing some magic to make this work ?

view this post on Zulip Karl Palmskog (Dec 09 2021 at 13:33):

Section Foo.
  Load "XT.v".
  Definition f ....
End Foo.

Section Bar.
  Load "XT.v".
   Definition  g := f. (* I don't want to write f X *)
End.

view this post on Zulip Karl Palmskog (Dec 09 2021 at 13:33):

and then in XT.v you put simply:

Variable (X: T).

view this post on Zulip Vincent Siles (Dec 09 2021 at 13:34):

that's magic :D We don't compile with dune (yet?) so it should work for us. I'll try that right away thank you

view this post on Zulip Karl Palmskog (Dec 09 2021 at 13:34):

note that this only solves the problem of having the "same" X in both places

view this post on Zulip Enrico Tassi (Dec 09 2021 at 13:35):

I'd recommend not using Load in new code.

view this post on Zulip Pierre-Marie Pédrot (Dec 09 2021 at 13:35):

Please refrain from using Load.

view this post on Zulip Pierre-Marie Pédrot (Dec 09 2021 at 13:35):

@Enrico Tassi synchronous grievance

view this post on Zulip Karl Palmskog (Dec 09 2021 at 13:35):

I just said what people use, what is then the official recommendation for use case above?

view this post on Zulip Pierre-Marie Pédrot (Dec 09 2021 at 13:36):

I think typeclasses?

view this post on Zulip Pierre-Marie Pédrot (Dec 09 2021 at 13:36):

Loading still doesn't prevent you from having to define aliases inside sections not to have to explicitly apply the constants to the context.

view this post on Zulip Pierre-Marie Pédrot (Dec 09 2021 at 13:36):

Not very scalable if you ask me.

view this post on Zulip Enrico Tassi (Dec 09 2021 at 13:36):

We know you can't re-use, re-open sections. This is bad. But Load brings other problems (dependencies are wrong even with coq_makefile for example).

view this post on Zulip Pierre-Marie Pédrot (Dec 09 2021 at 13:37):

And also it stresses weirds parts of the STM.

view this post on Zulip Karl Palmskog (Dec 09 2021 at 13:37):

I think it's harsh to say: "just design your own typeclass hierarchy" when someone just wants to have the same section variables in several places

view this post on Zulip Vincent Siles (Dec 09 2021 at 13:38):

I guess it is time to learn how to use type classes in Coq ;)

view this post on Zulip Enrico Tassi (Dec 09 2021 at 13:38):

one hack would be to use Context `{hack V1 V2 V3}.

view this post on Zulip Pierre-Marie Pédrot (Dec 09 2021 at 13:38):

@Karl Palmskog Yeah, Coq sucks at abstraction. But a workaround with a footgun is still not recommended.

view this post on Zulip Enrico Tassi (Dec 09 2021 at 13:39):

hack would be a term that has as arguments all the variables you want, and the backtick think will postulate them for you

view this post on Zulip Enrico Tassi (Dec 09 2021 at 13:39):

together with a dummy one of type hack...

view this post on Zulip Enrico Tassi (Dec 09 2021 at 13:39):

Does my explanation make sense?

view this post on Zulip Vincent Siles (Dec 09 2021 at 13:40):

not really :D

view this post on Zulip Enrico Tassi (Dec 09 2021 at 13:42):

Look here https://coq.inria.fr/refman/language/core/sections.html#coq:cmd.Context and replace EqDec with something that depends on arguments of the types you need.

view this post on Zulip Enrico Tassi (Dec 09 2021 at 13:42):

also https://coq.inria.fr/refman/language/extensions/implicit-arguments.html#implicit-generalization
you need to make hack a class, but not really to use any type class resolution on it.

view this post on Zulip Kenji Maillard (Dec 09 2021 at 13:44):

So something like the following ?

Axiom T : Type.

Inductive hack (X: T) := | Hack.

Section Foo.
  (* Variable (X: T). *)
  Context X `(hack X).
  Definition f : T := X.
End Foo.

Section Bar.
  (* Variable (X: T). *)
  Context X `(hack X).
  Definition  g := f. (* I don't want to write f X *)
End Bar.

Print f.
(* f = fun X : T => X *)
(*      : T -> T *)

Print g.
(* g = f *)
(*      : T -> T *)

view this post on Zulip Enrico Tassi (Dec 09 2021 at 13:44):

Class hack (T : Type) (x : T).

Section foo.
Generalizable All Variables.
Context `(_dummy_ : hack T x).
Goal True.

view this post on Zulip Kenji Maillard (Dec 09 2021 at 13:45):

I don't understand how Coq figure out which X to use for f in the second section (since f does not take any hack argument after generalization)...

view this post on Zulip Enrico Tassi (Dec 09 2021 at 13:45):

You were close, but you don't really need an inductive

view this post on Zulip Vincent Siles (Dec 09 2021 at 13:46):

I can work with that, thank you

view this post on Zulip Enrico Tassi (Dec 09 2021 at 13:46):

And yes, you can drop the Generalize All Variables directive at the cost of repeating the names.

view this post on Zulip Notification Bot (Dec 09 2021 at 13:48):

Enrico Tassi has marked this topic as resolved.

view this post on Zulip Kenji Maillard (Dec 09 2021 at 13:48):

Wait, actually the code I wrote above does not do the right thing

view this post on Zulip Enrico Tassi (Dec 09 2021 at 13:48):

Mine does ;-)

view this post on Zulip Kenji Maillard (Dec 09 2021 at 13:48):

in the second section f has type T -> T instead of T

view this post on Zulip Kenji Maillard (Dec 09 2021 at 13:50):

@Enrico Tassi not so sure... Did I make a mistake ?

Axiom T : Type.

Class hack (x : T).

Section foo.
Generalizable All Variables.
Context `(_dummy_ : hack x).
Definition f : T := x.
End foo.

Section Bar.
Generalizable All Variables.
Context `(_dummy_ : hack x).
Fail Definition  g : T := f. (* I don't want to write f X *)
(* - ?x: Cannot infer the implicit parameter x of f whose type is  *)
(*   "T" in environment: *)
(*   x : T *)
(*   _dummy_ : hack x *)
End Bar.

view this post on Zulip Enrico Tassi (Dec 09 2021 at 13:51):

It should have type T -> T, since you closed the first section, no?

view this post on Zulip Kenji Maillard (Dec 09 2021 at 13:52):

I was hoping that the hack would simulate a reopening of section, just got fooled ^^'

view this post on Zulip Enrico Tassi (Dec 09 2021 at 13:52):

I see, there are 2 things:

view this post on Zulip Enrico Tassi (Dec 09 2021 at 13:52):

my hack solves 1, not 2

view this post on Zulip Karl Palmskog (Dec 09 2021 at 13:52):

yes, not even Load solves 2.

view this post on Zulip Enrico Tassi (Dec 09 2021 at 13:52):

for that, we would need something which is not even too hard if someone has the time

view this post on Zulip Vincent Siles (Dec 09 2021 at 13:52):

I'm mostly intersting in 2 :p

view this post on Zulip Vincent Siles (Dec 09 2021 at 13:53):

It is really like I want to split an existing section with context into 2 sections or files

view this post on Zulip Enrico Tassi (Dec 09 2021 at 13:53):

We miss "default values for arguments". Today the implicit arguments machinery can pad a constant with _ standing for arguments to be inferred. If we could say: "pad it with variable A", we would get 2.

view this post on Zulip Karl Palmskog (Dec 09 2021 at 13:54):

people use stuff like local notations and the like for this today I think

view this post on Zulip Enrico Tassi (Dec 09 2021 at 13:54):

@Vincent Siles this is not really possible. You can use modules/functors for that, if you want (I'm not in love with them, since they are not first class).

view this post on Zulip Enrico Tassi (Dec 09 2021 at 13:55):

Yes, that would do, but it is not super nice either :-/

view this post on Zulip Enrico Tassi (Dec 09 2021 at 13:55):

@Vincent Siles why do you need to split? Usually people need to close a section to get the things generalized. But you talk about 2 files...

view this post on Zulip Vincent Siles (Dec 09 2021 at 13:58):

So in our context, we have a bunch of definitions that assume a program description (like a list of classes for examples). And the file is getting quite big, so I wanted to split it into multiple files, and each of them expect this global "program definition". So each section/file would have a Context (Prog : list ClassDef). I wanted to avoid having to explicitly pass his Prog to definition that come from a previous section/file

view this post on Zulip Enrico Tassi (Dec 09 2021 at 14:00):

Instead of abstracting over a section, you can abstract over a module with a field Prog, and in the second file do Module Import F1(Prog)

view this post on Zulip Enrico Tassi (Dec 09 2021 at 14:00):

it may work for you

view this post on Zulip Yannick Forster (Dec 09 2021 at 16:37):

Here's an old feature request by me asking for essentially the same thing Vincent asked for: https://github.com/coq/coq/issues/10737

view this post on Zulip Paolo Giarrusso (Dec 09 2021 at 19:51):

can’t you just solve to by making _dummy_ an implicit argument?

view this post on Zulip Paolo Giarrusso (Dec 09 2021 at 19:52):

ah no, I see the problem. For this you don’t want x to be an index of the typeclass, it should be a member.

view this post on Zulip Paolo Giarrusso (Dec 09 2021 at 19:53):

Class hack := { x : T }.
Section foo.
Context `{!hack}.
Definition f : T := x.
End foo.

Section bar.
Context `{!hack}.
Definition g : T := f.
End foo.

view this post on Zulip Paolo Giarrusso (Dec 09 2021 at 19:54):

with these identifiers, this is a terrible example — but this kind of thing is used throughout Iris…

view this post on Zulip Paolo Giarrusso (Dec 09 2021 at 19:56):

however, I would not recommend trying this if you haven’t mastered the key rules of type classes — eg, learned to use Hint Mode. There’s definitely a learning curve, and I don’t think I’ve seen a sufficient manual anywhere…

view this post on Zulip Paolo Giarrusso (Dec 09 2021 at 19:57):

let’s just say that https://arxiv.org/abs/1102.1323 is necessary but not sufficient.

view this post on Zulip Paolo Giarrusso (Dec 09 2021 at 19:58):

with modules, you avoid having to control type inference, and I’ve used this, but then you’re dealing with Coq modules.

view this post on Zulip Karl Palmskog (Dec 09 2021 at 20:17):

what's the meaning of the ! again?

view this post on Zulip Gaëtan Gilbert (Dec 09 2021 at 20:20):

don't implicitly generalize the typeclass arguments

view this post on Zulip Karl Palmskog (Dec 09 2021 at 20:27):

but in the example, his typeclass doesn't have arguments?

view this post on Zulip Gaëtan Gilbert (Dec 09 2021 at 20:27):

then ! does nothing

view this post on Zulip Paolo Giarrusso (Dec 09 2021 at 20:29):

Must have been muscle memory. stdpp has Generalizable All Variables, so Context without ! is dangerous.

view this post on Zulip Paolo Giarrusso (Dec 09 2021 at 20:30):

(you need it, but with care)

view this post on Zulip Karl Palmskog (Dec 09 2021 at 20:30):

argh/sigh/etc.

view this post on Zulip Paolo Giarrusso (Dec 09 2021 at 20:31):

But I swear, I had to check my code above to see that, indeed, I had used !.

view this post on Zulip Paolo Giarrusso (Dec 09 2021 at 20:31):

I think the interjection you're looking for is "Coq :frown:"

view this post on Zulip Karl Palmskog (Dec 09 2021 at 20:32):

I mean seriously, we need typeclass consultants at this point

view this post on Zulip Gaëtan Gilbert (Dec 09 2021 at 20:34):

Paolo Giarrusso said:

Must have been muscle memory. stdpp has Generalizable All Variables, so Context without ! is dangerous.

how does Generalizable makes lack of ! more dangerous?

view this post on Zulip Paolo Giarrusso (Dec 09 2021 at 20:35):

I'm not as familiar with the semantics without, but is there any generalization without changing that setting?

view this post on Zulip Paolo Giarrusso (Dec 09 2021 at 20:36):

I have next to no PTSD ^W experience with classes without that setting, so not sure

view this post on Zulip Gaëtan Gilbert (Dec 09 2021 at 20:36):

Generalizable No Variables.

Class C := {}.

Class D (x:C) := {}.

Check forall `{D}, _.
(* forall (x : C) (H : D x), ?T *)

view this post on Zulip Paolo Giarrusso (Dec 09 2021 at 22:02):

I see: Generalizable affects the variables you name explicitly, not the ones you aren't naming.

Fail Check forall `{!D c}, _.

Last updated: Sep 28 2023 at 10:01 UTC