Coq：依赖模式匹配有问题

Question

我想知道是否可以实现这种依赖模式匹配。如您所见，我正在尝试将多个值映射到 nul（并指示输出具有带有 return 子句的所需类型）。类型 N 是一个垃圾收集器，我只是想摆脱

之后的所有值

| P, c => phy
| P, b => phy
| Ii, b => inf

（在这个特定的设置中，使用 option 类型似乎非常笨拙。）请注意，如果 Coercion 在这里是不可能的，我也会很高兴 w/ Definition

Inductive R := P | Ii | S | N.
Parameter rp:> R -> Prop.
Inductive X: Type := | c {z:P} :> X | b {z:P} {y:Ii} :> X.
Parameter (phy:P) (inf:Ii) (sen:S) (nul:N).

Check phy: id P.
Fail Coercion xi(y:R)(x:X): id y := match y, x with
| P, c => phy
| P, b => phy
| Ii, b => inf
| _, _ => match _ return N with _ => nul end end.
(* The term "nul" has type "rp N" while it is expected to have type "rp Ii". *)

Answer 1

你说 "I'm simply trying to get rid of all the values after ..."，我有点担心有多个没有显着特征的默认值，我怀疑你的代码不会像你想的那样，但你可以这样做:

Inductive R := P | Ii | S | N.
Parameter rp:> R -> Prop.
Inductive X: Type := | c {z:P} :> X | b {z:P} {y:Ii} :> X.
Parameter (phy:P) (inf:Ii) (sen:S) (nul:N).

Check phy: id P.
Definition xi(y:R)(x:X): id y
  := match y, x with
     | P, c => phy
     | P, b => phy
     | Ii, b => inf
     | Ii, _ => inf
     | S, _ => sen
     | N, _ => nul
     end.

请注意，您也可以这样做：

Definition xi(y:R)(x:X): id y
  := match y with
     | P => phy
     | Ii => inf
     | S => sen
     | N => nul
     end.

您不能将其设为强制转换，因为无法从 x.

推断出 y

如果您关心的是值而不是类型，则可以使用依赖类型来获取每种情况下您想要的 return 类型：

Inductive R := P | Ii | S | N.
Parameter rp:> R -> Prop.
Inductive X: Type := | c {z:P} :> X | b {z:P} {y:Ii} :> X.
Parameter (phy:P) (inf:Ii) (sen:S) (nul:N).

Check phy: id P.
Definition xi_type(y:R)(x:X)
  := match y, x return Type with
     | P, c
     | P, b
     | Ii, b
       => y
     | _, _
       => N
     end.
Definition xi(y:R)(x:X): xi_type y x
  := match y, x return xi_type y x with
     | P, c => phy
     | P, b => phy
     | Ii, b => inf
     | _, _ => nul
     end.

Answer 2

带有定义返回 "match type":

的较短解决方案

Inductive R := P | Ii | S | N. Fail Check N: Type.
Parameter rp:> R -> Prop. Check N: Type.
Inductive X: Type := | c {z:P} :> X | b {z:P} {y:Ii} :> X.
Parameter (phy:P) (inf:Ii) (sen:S) (nul:N).

Definition xi (y:R) := match y return (match y with (P|Ii) => y | _ => N end) with
     | P => phy
     | Ii => inf
     | _ => nul end.

Eval hnf in xi S. (* = nul *)

找到想法here

Coq：依赖模式匹配有问题

Coq: Trouble w/ a dependent pattern match

pattern-matching

coq