Coq:多个构造函数的单一表示法 [英] Coq: a single notation for multiple constructors
问题描述
是否可以在Coq中为多个构造函数定义一个符号?如果构造函数的参数类型不同,则可能无法从中推断出它们。最小(非)工作示例:
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?
推荐答案
您可以创建一个以构造函数为实例的类型类,实例解析机制推断构造函数要为您调用:
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.
顺便说一句,使用Coq 8.5,如果您真的想要一种符号' x
导致将精确的构造函数应用于 x
,而不是例如 @a_const C A_const_c c1
,则可以使用ltac术语来实现:
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 *)
这篇关于Coq:多个构造函数的单一表示法的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!