Stream: Coq users

Topic: Modules and notations


view this post on Zulip Pierre Rousselin (Nov 01 2023 at 17:00):

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?

view this post on Zulip 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 *)

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Nov 01 2023 at 19:01):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Pierre Rousselin (Nov 02 2023 at 13:06):

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

Module BitTwoElts : TwoEltsT.

view this post on Zulip 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...

view this post on Zulip Pierre Rousselin (Nov 02 2023 at 13:07):

Not in the last module.

view this post on Zulip Pierre Rousselin (Nov 02 2023 at 13:08):

That's why Coq's complaining.

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Nov 02 2023 at 13:22):

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

view this post on Zulip 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....

view this post on Zulip 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.

view this post on Zulip Julio Di Egidio (Nov 02 2023 at 14:44):

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