Modules and notations · Coq users

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.

Quentin VERMANDE (Nov 01 2023 at 18:05):

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 *)

Pierre Rousselin (Nov 01 2023 at 18:25):

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

Quentin VERMANDE (Nov 01 2023 at 18:32):

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.

Julio Di Egidio (Nov 01 2023 at 18:54):

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.

Gaëtan Gilbert (Nov 01 2023 at 19:01):

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

Julio Di Egidio (Nov 02 2023 at 13:02):

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.

Pierre Rousselin (Nov 02 2023 at 13:04):

You would need to write the lemma as one <> zero. IIUC the Include part must come after the complete instantiation of TwoEltsT.

Pierre Rousselin (Nov 02 2023 at 13:06):

Module BitTwoElts : TwoEltsT.

Julio Di Egidio (Nov 02 2023 at 13:07):

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

Pierre Rousselin (Nov 02 2023 at 13:07):

Pierre Rousselin (Nov 02 2023 at 13:08):

Julio Di Egidio (Nov 02 2023 at 13:15):

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.

Gaëtan Gilbert (Nov 02 2023 at 13:22):

Julio Di Egidio (Nov 02 2023 at 13:23):

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....

Julio Di Egidio (Nov 02 2023 at 13:25):

@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.

Stream: Coq users

Topic: Modules and notations

Pierre Rousselin (Nov 01 2023 at 17:00):