Coq：多个构造函数的单一符号

Question

是否可以在 Coq 中为多个构造函数定义一个符号？如果构造函数的参数类型不同，则可以从中推断出它们。一个最小的（非）工作示例：

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*)

在这种情况下，构造函数推断不起作用。也许还有另一种方法可以将构造函数指定为变量？

Answer 1

显然，这很简单：

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

Answer 2

您可以创建一个以构造函数作为实例的类型类，让实例解析机制为您推断构造函数来调用：

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.

顺便说一句，对于 Coq 8.5，如果您真的想要一个符号 ' x 来生成应用于 x 的确切构造函数，而不是例如@a_const C A_const_c c1，那么你可以使用 ltac-terms 来完成：

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 *)

Answer 3

事实上，使用 ltac 术语的想法导致了与我发布的另一个完全不同的解决方案：

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 *)

（这里的 eval hnf 部分允许它工作，即使参数的类型在语法上不等于 C 或 D，但它确实减少到其中之一.)

Coq：多个构造函数的单一符号

Coq: a single notation for multiple constructors

constructor

coq