coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Overloading notation for different types in Coq

From: Marianna Rapoport <mrapoport AT uwaterloo.ca>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Overloading notation for different types in Coq
Date: Thu, 18 May 2017 14:01:15 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mrapoport AT uwaterloo.ca; spf=Pass smtp.mailfrom=mrapoport AT uwaterloo.ca; spf=None smtp.helo=postmaster AT minos.uwaterloo.ca
Dkim-filter: OpenDKIM Filter v2.11.0 minos.uwaterloo.ca v4II1Fnd032564
Ironport-phdr: 9a23:Y8JOGh/pF50Mv/9uRHKM819IXTAuvvDOBiVQ1KB42ugcTK2v8tzYMVDF4r011RmSDNudtq0My7KP9fuxBipYudfJmUtBWaIPfidGs/lepxYnDs+BBB+zB9/RRAt+Iv5/UkR49WqwK0lfFZW2TVTTpnqv8WxaQU2nZkJ6KevvB4Hdkdm82fys9J3PeQVIgye2ba9vIBmsowjcssgbjZFiJ6sz1xDFpmdEd/lMyW5mIV+enQzw6tus8JJm7i9dp+8v+8lcXKr1eKg1UaZWADM6PW4r+cblrwPDTQyB5nsdVmUZjB9FCBXb4R/5Q5n8rDL0uvJy1yeGM8L2S6s0WSm54KdwVBDokiYHOCUn/2zRl8d9kbhUoBOlpxx43o7UfISYP+dwc6/BYd8XQ3dKU8BMXCJDH4y8dZMCAekBM+hGoIbzqEcBoxywBQauGe3hxCRFiWX00KAgyeksCx3K0Q4mEtkTsHrUttL1NKIKXO6y1qbI1zTDYOlQ2Tf78ofDbwwvruuUXbJ3acrRzlMvFx/YhViXrIzlJSma1vwKs2iD6OpgT/6vhnU6qwB/uDev2tkjipPNhoISzVDI7zl2z5wsKNC+VUV1YsakHYNNuy2EM4Z6WMcvTmNytCon1LELuoS3cSoJxZg/xhPSauaLf5WV7h7+TuqcLi10iGx7dL+9gRu57FKuxffmVsau1VZHtipFncfItnAKzxHT78mHSv16/ke6wzqPyg7S5ftYIU8qj6rbL5khwrkqmpUPq0vPBi72mEPog6+Kbkgo5/ak5uD9brjipJKQLZJ4hh/9P6g0mMGyAvw0Mg0UUGia/eS82qfj/Ur8QLhSi/02iLPWsIjdJcQDoa65GRNV350+6xexFTimzMoXnWMDLFJCfxKLlZTmNEvWLPDiEfi/m0iskCtsx/3eIrLhBYzNImHfn7flYLZy8FVRyBEzzNBa/5JbEKsNIPP1Wk/rtdzXFAU1MwKuw7WvNNIo3YQHHGmLH6WxMaXIsFbO6Ph8DfOLYdowsSz8Iv4j7rbUhGc+gVgHYeH92IEecHegGe56C1iGaGbhmNMGFiEBt1xtH6TRlFSeXGsLND6JVKUm62RjBQ==

Sorry, the actual error is: The term "tvar1" has type "term1" while it is expected to have type "term2".

On Thu, May 18, 2017, at 01:57 PM, Marianna Rapoport wrote:

I would like to be able to define the same Coq notations for different inductive definitions, and distinguish the notations based on the types of their arguments.

Here is a minimal example:

    Inductive type : Type :=

    | TBool : type.

    Inductive term1 : Type :=

    | tvar1 : term1.

    Inductive term2 : Type :=

    | tvar2 : term2.

    Definition context := nat -> (option type).

    Reserved Notation "G '⊢' t '::' T" (at level 40, t at level 59).

    Inductive typing1 : context -> term1 -> type -> Prop :=

     | T_Var1 : forall G T,

          G ⊢ tvar1 :: T

    where "G '⊢' t1 '::' T" := (typing1 G t1 T)

    with typing2 : context -> term2 -> type -> Prop :=

     | T_Var2 : forall G x T,

          G ⊢ tvar2 :: T

    where "G '⊢' t2 '::' T" := (typing2 G t2 T).

As you see, there is a mutually inductive definition, in which I'd like to be able to use the same notation for different types of terms (`term1` and `term2`).

The error I get when trying to compile this is `Error: Illegal application (Non-functional construction): The _expression_ "tvar1" of type "term1" cannot be applied to the term "x" : "?T"`.

Is there a way to get this to work, maybe by using type classes?

[Coq-Club] Overloading notation for different types in Coq, Marianna Rapoport, 05/18/2017
- Re: [Coq-Club] Overloading notation for different types in Coq, Marianna Rapoport, 05/18/2017
- Re: [Coq-Club] Overloading notation for different types in Coq, Gaetan Gilbert, 05/18/2017
  - Re: [Coq-Club] Overloading notation for different types in Coq, Marianna Rapoport, 05/18/2017
    - Re: [Coq-Club] Overloading notation for different types in Coq, Marianna Rapoport, 05/19/2017
      - Re: [Coq-Club] Overloading notation for different types in Coq, Abhishek Anand, 05/20/2017
        
        Re: [Coq-Club] Overloading notation for different types in Coq, Marianna Rapoport, 05/21/2017