Coq: a single notation for multiple constructors

Question

Is it possible to define a single notation for multiple constructors in Coq? If the constructors differ by their argument types, they might be inferrable from them. A minimal (non-)working example:

Inductive A : Set := a | b | c: C -> A | d: D -> A
with C: Set := c1 | c2
with D: Set := d1 | d2.

Notation "' x" := (_ x) (at level 19).
Check 'c1. (*?6 c1 : ?8*)

In this case, constructor inference doesn't work. Maybe there's another way to specify a constructor as a variable?

Daniel Schepler · Accepted Answer · 2016-06-27T21:13:33.740

You can create a typeclass with the constructors as instances and let the instance resolution mechanism infer the constructor to call for you:

Class A_const (X:Type) : Type :=
  a_const : X -> A.
Instance A_const_c : A_const C := c.
Instance A_const_d : A_const D := d.

Check a_const c1.
Check a_const d2.

By the way, with Coq 8.5, if you really want a notation ' x to result in the exact constructor applied to x, rather than e.g. @a_const C A_const_c c1, then you can use ltac-terms to accomplish that:

Notation "' x" := ltac:(match constr:(a_const x) with
                        | @a_const _ ?f _ =>
                          let unfolded := (eval unfold f in f) in
                          exact (unfolded x)
                        end) (at level 0).
Check 'c1. (* c c1 : A *)
Check 'd2. (* d d2 : A *)

Indeed; depending on the particular application using a Canonical Structure could work very well here too. — ejgallego, Jun 27 '16 at 20:30

score 1 · Answer 2 · answered Jun 28 '16 at 01:06

In fact, the idea of using an ltac-term leads to an entirely different solution from the other one I posted:

Notation "' x" := ltac:(let T := (type of x) in
                        let T' := (eval hnf in T) in
                        match T' with
                        | C => exact (c x)
                        | D => exact (d x)
                        end) (at level 0).
Check 'c1. (* c c1 : A *)
Check 'd2. (* d d2 : A *)

(Here the eval hnf part lets it work even if the type of the argument isn't syntactically equal to C or D, but it does reduce to one of them.)

Unfortunately, [Coq 8.5 isn't working](http://stackoverflow.com/questions/37901837/coqide-8-5-no-syntax-highlighting-on-linux) for me (so I'll probably accept another answer) — jaam, Jun 28 '16 at 07:05

score 0 · Answer 3 · answered Jun 27 '16 at 18:31

0

Apparently, it's easy:

Notation "' x" := ((_:_->A) x) (at level 19).
Check 'c1. (*' c1 : A*)

answered Jun 27 '16 at 18:31

jaam

900
4
23

But the constructor (`c`) wasn't inferred. If you `Unset Printing Notations.` you'll see `(?a : forall _ : C, A) c1: A where ?a : [ |- forall _ : C, A]`. – Anton Trunov Jun 27 '16 at 18:54
@AntonTrunov True. I'll accept an answer that can, in addition, infer the constructor. Ow. we'll have to be content w/ a specification of a constructor as a variable – jaam Jun 27 '16 at 19:03

Coq: a single notation for multiple constructors

3 Answers3

Linked