Stream: Coq users

Topic: "Import" Sections with a specifix context

view this post on Zulip Thomas Lamiaux (May 12 2024 at 19:33):

Hi everyone,
I have a bunch of definitions with commons arguments so I put them in a section, something like

Section Foo.
  Context (a : A).
  Context (b : B).
  Definition def1 := ...
  Definition def2 := ...
  Definition def3 := ...
End Foo.

Later on, in a file, I would like to use many of these functions instantiated with the same context.
So I would like to be able to write something like the following:

Import Foo a1 b1

Do you know how / if I can do that ?

view this post on Zulip Li-yao (May 12 2024 at 19:52):

There's no good way to do this. Depending on the use case, I would either copy-paste, use type classes, or use modules.

view this post on Zulip Pierre Rousselin (May 13 2024 at 09:14):

Dear Thomas,
This was the best I could come up with:

Module Type HasABab.
  Parameter Inline A : Type.
  Parameter Inline B : Type.
  Context (a : A) (b : B).
End HasABab.

Module Foo (Import M : HasABab).
  Definition def1 : nat -> A := fun _ => a.
  Definition def2 : A * B := (a, b).
  Definition def3 (x : bool) :=
    match x as y return if y then A else B with
    | true => a
    | false => b
End Foo.

Module HasABab42true <: HasABab.
  Definition A := nat.
  Definition B := bool.
  Definition a : nat := 42.
  Definition b : bool := true.
End HasABab42true.

Module Import F := Foo HasABab42true.

Check def1.
Print def1. (* you may inline a as well if you want 42 instead of a *)
Check def2.
Check def3.

view this post on Zulip Thomas Lamiaux (May 14 2024 at 10:14):

Thanks @Pierre Roux . In my particular case, it is too complicated but if I had more functions I think It could be agood solution.

Last updated: Jun 13 2024 at 21:01 UTC