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.
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
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 ?
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.
and then in XT.v
you put simply:
Variable (X: T).
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
note that this only solves the problem of having the "same" X
in both places
I'd recommend not using Load in new code.
Please refrain from using Load.
@Enrico Tassi synchronous grievance
I just said what people use, what is then the official recommendation for use case above?
I think typeclasses?
Loading still doesn't prevent you from having to define aliases inside sections not to have to explicitly apply the constants to the context.
Not very scalable if you ask me.
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).
And also it stresses weirds parts of the STM.
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
I guess it is time to learn how to use type classes in Coq ;)
one hack would be to use Context `{hack V1 V2 V3}.
@Karl Palmskog Yeah, Coq sucks at abstraction. But a workaround with a footgun is still not recommended.
hack
would be a term that has as arguments all the variables you want, and the backtick think will postulate them for you
together with a dummy one of type hack...
Does my explanation make sense?
not really :D
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.
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.
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 *)
Class hack (T : Type) (x : T).
Section foo.
Generalizable All Variables.
Context `(_dummy_ : hack T x).
Goal True.
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)...
You were close, but you don't really need an inductive
I can work with that, thank you
And yes, you can drop the Generalize All Variables
directive at the cost of repeating the names.
Enrico Tassi has marked this topic as resolved.
Wait, actually the code I wrote above does not do the right thing
Mine does ;-)
in the second section f
has type T -> T
instead of T
@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.
It should have type T -> T
, since you closed the first section, no?
I was hoping that the hack would simulate a reopening of section, just got fooled ^^'
I see, there are 2 things:
my hack solves 1, not 2
yes, not even Load
solves 2.
for that, we would need something which is not even too hard if someone has the time
I'm mostly intersting in 2 :p
It is really like I want to split an existing section with context into 2 sections or files
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.
people use stuff like local notations and the like for this today I think
@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).
Yes, that would do, but it is not super nice either :-/
@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...
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
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)
it may work for you
Here's an old feature request by me asking for essentially the same thing Vincent asked for: https://github.com/coq/coq/issues/10737
can’t you just solve to by making _dummy_
an implicit argument?
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.
Class hack := { x : T }.
Section foo.
Context `{!hack}.
Definition f : T := x.
End foo.
Section bar.
Context `{!hack}.
Definition g : T := f.
End foo.
with these identifiers, this is a terrible example — but this kind of thing is used throughout Iris…
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…
let’s just say that https://arxiv.org/abs/1102.1323 is necessary but not sufficient.
with modules, you avoid having to control type inference, and I’ve used this, but then you’re dealing with Coq modules.
what's the meaning of the !
again?
don't implicitly generalize the typeclass arguments
but in the example, his typeclass doesn't have arguments?
then ! does nothing
Must have been muscle memory. stdpp has Generalizable All Variables, so Context without ! is dangerous.
(you need it, but with care)
argh/sigh/etc.
But I swear, I had to check my code above to see that, indeed, I had used !.
I think the interjection you're looking for is "Coq :frown:"
I mean seriously, we need typeclass consultants at this point
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?
I'm not as familiar with the semantics without, but is there any generalization without changing that setting?
I have next to no PTSD ^W experience with classes without that setting, so not sure
Generalizable No Variables.
Class C := {}.
Class D (x:C) := {}.
Check forall `{D}, _.
(* forall (x : C) (H : D x), ?T *)
I see: Generalizable affects the variables you name explicitly, not the ones you aren't naming.
Fail Check forall `{!D c}, _.
Last updated: Oct 13 2024 at 01:02 UTC