coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Marianna Rapoport <mrapoport AT uwaterloo.ca>
- To: Abhishek Anand <abhishek.anand.iitg AT gmail.com>, "coq-club" <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Overloading notation for different types in Coq
- Date: Sat, 20 May 2017 21:28:42 -0400
- Authentication-results: mail3-smtp-sop.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 v4L1ShOl032197
- Ironport-phdr: 9a23:KlfPTRVM9VS7IpbvLbUSJ2mxU/bV8LGtZVwlr6E/grcLSJyIuqrYbB2Et8tkgFKBZ4jH8fUM07OQ6PG+HzFfqdbZ6TZZIcMKD0dEwewt3CUeQ+e9SnfHZMbwaCI7GMkQHHRExFqcdXZvJcDlelfJqWez5zNBUj/2NA5yO/inUtWK15f/2O+94YDcbBtVjzShf7xyMA+2rQLMvcUKnIduMKg8xx/Ir3dSe+lbx35jKVaPkxrh/Mu98ppu/iZKt/4968JMVLjxcrglQ7BfEDkpPGc56dHxuxXEUQWB+GYXXH8MkhpPDQjF7RX6UYn0vyDnqOdz2zSUMNPvQ7wsVjus86lkSBnziCcaLDE5633YitZxjK1Avh2soQF0zpPOb4GUMPp+eb7dfc8fSGFcUMtdSzBND4WhZIYJEuEPP/tXr5PlqlUNrRWwGwajCuzzxTFPhHD406M63fk6HA7c3gEtBcgDvW7IoNj3MqoZTOC7zLPPzTXGd/5Y3i3y6JLJch87p/GMW6h/etfNx0Y1DwPFiU2QqYv/PzOJy+8AtG2b7/B6WuK3jG4nswZxoiKzxso3l4nIiJgaykza+iVjxIY1Itq4RFRnbtG+CZZdsTyROYVxQsMnWW5ouSA6x6Uatp68ZigKzoooxxrba/CdbYeH/w/jWeCMKjl7nHJoYK+ziwi2/ES6zuDxVNO43EtUoidGiNXBtHMA2wTS58WGUPdx41qt1SuV2w3c8O1IP144mKjdJpU82LA/jIATvl7GHiLumEX5kquWdkI89+it6uTnZLLmpoSGO49phADxKLguldKlAeQ8NQgOWHKX9vim27H7/E35RqtFjuEun6XErpzXId4Xq6q7DgNPz4ov9RWyAy2k3dkbhXUHKUhKeBODj4jnIVHOJ/X4AO+6g1S2ijhr3/fGPqXmApXXMnjOi6rhfLhn5E5A1gUz19Rf55VTCr0bPP38QFf9tMbEAR8hLwy03+HnBc1h2YMZQGKDG7OWMKfPsVCT/e8vOOmNZIoNuDnnMfQl5vjujWU4mVAHZ6Wp04EXOziEGaFPKUWYenrhgZ8oF24MskJqRebqiUaCXD0VbnC7Wa565zAnB6qpCI7CQsamh7nXmG/xFZpPI2tCF1rGWSPjcJzBUPMRYgqTJNVgm3oKT+7yZZUm0ESLvRX7wrxhJ6Lu8zUfrZX5yJAh4vfajRYq8iZoJ9mC2n2AVWVzmSUDTmllj+hEvUVhxwLbguBDiPtCGIkL6g==
What you suggest does indeed work for that little example; it was my fault to simplify it too much. If I try to apply level 999 to the definition of the "less minimal" minimal example (please see below), I get the error "Syntax error: '.' expected after [vernac:gallina] (in [vernac_aux])."
Inductive type : Type :=
| TBool : type.
Inductive term1 : Type :=
| tvar1 : term1.
Inductive term2 : Type :=
| tvar2 : term2.
Definition context := nat -> (option type).
Class VDash (A B C : Type) := vdash : A -> B -> C -> Prop.
Notation "G '|-' t '::' T" := (vdash G t T) (at level 999, t at level 59).
Inductive typing1 : VDash context term1 type :=
| T_Var1 : forall G T,
G |- tvar1 :: T
with typing2 : VDash context term2 type :=
| T_Var2 : forall G T,
G |- tvar2 :: T.
Ltac tactic :=
solve [match goal with
| H: _ |- _ => auto
end].
On Fri, May 19, 2017, at 10:44 PM, Abhishek Anand wrote:
Increasing the level of your notation (thereby reducing its "priority") helps:Class VDash (A B C : Type) := vdash : A -> B -> C -> Prop.Notation "G '|-' e '::' T" := (vdash G e T) (at level 999, e at level 59).Ltac tactic :=solve [match goal with| H: _ |- _ => autoend].Global Instance vd : VDash nat nat nat := fun a b c => True.Check (0 |- 0::0).(* The manual says that levels are supposed to be 200 or less, so I have no idea why 999 is allowed. 200 isn't high enough for the last Check to check*)-- AbhishekOn Fri, May 19, 2017 at 4:59 PM, Marianna Rapoport <mrapoport AT uwaterloo.ca> wrote:As a follow up on the turnstile notation, is it possible to avoid a parse conflict with the match notation of Ltac?Minimal example:Class VDash (A B C : Type) := vdash : A -> B -> C -> Prop.Notation "G '|-' e '::' T" := (vdash G e T) (at level 40, e at level 59).Ltac tactic :=solve [match goal with| H: _ |- _ => autoend].The error I get is:Syntax error: '::' expected after [constr:operconstr level 59] (in [constr:operconstr]).On Thu, May 18, 2017, at 03:27 PM, Marianna Rapoport wrote:> That's exactly what I was looking for. Thanks a lot!>> Marianna>> On Thu, May 18, 2017, at 02:05 PM, Gaetan Gilbert wrote:> > With typeclasses you can do something like see attached file.> >> > Gaëtan Gilbert> >> > On 18/05/2017 19:57, 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?> >> > Email had 1 attachment:> > + tc_notas.v> > 1k (text/x-verilog)
- [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
- 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/19/2017
- Re: [Coq-Club] Overloading notation for different types in Coq, Marianna Rapoport, 05/18/2017
Archive powered by MHonArc 2.6.18.