I'm trying to understand modules better. I have some issues with notations.

In the following snippet, I try to implement a module type.

```
Module Type HasTwoElts.
Parameters (t : Type) (zero : t) (one : t).
Notation "0" := zero.
Notation "1" := one.
Axiom ne_one_zero : 1 <> 0.
End HasTwoElts.
Variant Bit := Zero | One.
Module BitHasTwoElts : HasTwoElts.
Definition t := Bit.
Definition zero := Zero.
Definition one := One.
Lemma ne_one_zero : 1 <> 0.
Proof. Check 1. (* 1 : nat. *) Admitted.
End BitHasTwoElts.
```

How can I use the notations from HasTwoElts in BitHasTwoElts?

I am for from being an expert on the subject, but I think you have to import or include a module containing notations in order for these to take effect. If this is correct, you need a module containing the notations for `0`

and `1`

to include before stating `ne\_one\_zero`

. In other words, you would have to separate the code defining the notations from the code using them. I managed to make something work with the following code. I guess it would have been better to nest the module types, but I could not do it.

```
Module Type HasTwoEltsData.
Parameters (t : Type) (zero : t) (one : t).
Notation "0" := zero.
Notation "1" := one.
End HasTwoEltsData.
Module Type HasTwoElts.
Include HasTwoEltsData.
Axiom ne_one_zero : 1 <> 0.
End HasTwoElts.
Variant Bit := Zero | One.
Module BitHasTwoElts : HasTwoElts.
Module BitHasTwoEltsData : HasTwoEltsData.
Definition t := Bit.
Definition zero := Zero.
Definition one := One.
End BitHasTwoEltsData.
Include BitHasTwoEltsData.
Lemma ne_one_zero : 1 <> 0.
Proof. Check 1. (* 1 : t. *) Admitted.
End BitHasTwoElts.
Import BitHasTwoElts.
Check 1. (* 1 : t *)
```

Thank you! It feels a bit strange to nest a module *and*include it, but this seems to do the trick (although in a very verbose way).

You can declare the inner module outside if it is better, I nested it only to hide the duplication of the definitions that the include does.

Hi, with the premise that my understanding of the module system to this point remains minimal so I am here to learn, I have tried to adapt the above to a pattern with module hierarchies that has worked for me so far, and, despite playing with it for a couple of hours now, I just can find no way to reuse notation from the ("params") module types:

```
Module Type TwoEltsParams.
Parameters (t : Type) (zero : t) (one : t).
Axiom ne_one_zero : one <> zero.
End TwoEltsParams.
Module TwoElts (Params : TwoEltsParams).
Include Params.
Notation "0" := zero.
Notation "1" := one. Check 1 : t.
End TwoElts.
Variant Bit := Zero | One.
Module BitTwoEltsParams <: TwoEltsParams.
Definition t := Bit.
Definition zero := Zero.
Definition one := One.
Lemma ne_one_zero : one <> zero. Admitted.
End BitTwoEltsParams.
Module BitTwoElts := TwoElts BitTwoEltsParams.
Import BitTwoElts. Check 1 : t.
```

you can also do

```
Module Type TwoEltsT.
Parameters (t : Type) (zero : t) (one : t).
End TwoEltsT.
Module TwoEltsNota (Import Params : TwoEltsT).
Notation "0" := zero.
Notation "1" := one.
Check 1 : t.
End TwoEltsNota.
Variant Bit := Zero | One.
Module BitTwoElts.
Definition t := Bit.
Definition zero := Zero.
Definition one := One.
Include TwoEltsNota.
Check 0 : t.
Lemma ne_one_zero : 1 <> 0. Admitted.
End BitTwoElts.
Import BitTwoElts.
Check 1 : t.
```

Include of a partially applied functor will use the current module to produce the functor arguments if it can

Eh, but you lost the axiom, but if we put that back we get exactly what I was saying, moreover the Lemma per se is accepted while in my version that just cannot happen ("Signature components for field ne_one_zero do not match" if I write 1 <> 0 instead of one <> zero):

```
Module Type TwoEltsT.
Parameters (t : Type) (zero one : t). Fail Check 1 : t.
Axiom ne_one_zero : one <> zero.
End TwoEltsT.
Module TwoEltsNota (Import Params : TwoEltsT).
Notation "0" := zero.
Notation "1" := one. Check 1 : t.
End TwoEltsNota.
Variant Bit := Zero | One.
Module BitTwoElts.
Definition t := Bit.
Definition zero := Zero.
Definition one := One. Fail Check 1 : t.
Lemma ne_one_zero : 1 <> 0. Admitted. (*!!*)
Fail Include TwoEltsNota.
End BitTwoElts.
Import BitTwoElts. Fail Check 1 : t.
```

You would need to write the lemma as `one <> zero`

. IIUC the `Include`

part must come after the complete instantiation of `TwoEltsT`

.

Also, you can enforce the fact that BitTwoElts has type TwoEltsT with :

```
Module BitTwoElts : TwoEltsT.
```

Sorry, I was replying re @Gaëtan Gilbert's code. I did write the Lemma as one <> zero...

Not in the last module.

That's why Coq's complaining.

I was in fact commenting on the "shortcomings" I find with @Gaëtan Gilbert's code, which in turn I took was a reply to/continuation on mine, in fact not so much the code per se but as an illustration of where the difficulty here lies.

why would you want to put the axiom in the module type?

OK, @Pierre Rousselin, I think I see what you mean, the import fails so one would be stopped there. In that sense I must concede the code is "acceptable", still it seems to defeat the purpose at least of a module hierarchy, it is more like we are using a post-condition....

@Gaëtan Gilbert Because we/I are taking it to be part of the spec of TwoElts. Indeed, if you don't put it there, you are not compelled to have it in BitTwoElts either.

Pierre Rousselin said:

Also, you can enforce the fact that BitTwoElts has type TwoEltsT with :

`Module BitTwoElts : TwoEltsT.`

But I had missed the import of that one. I shall play with it later...

Last updated: Jun 13 2024 at 19:02 UTC