Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • 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: _ |- _ => auto
  end].
  
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*)



On 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: _ |- _ => auto
  end].

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)





Archive powered by MHonArc 2.6.18.

Top of Page