0

我在 coq 证明助手中定义自动机时遇到问题，创建此代码时显示错误：

(*automate*)

Record automaton :Type:=
mk_auto {
   states : Set;
   actions :Set;
   initial : states;
   transitions : states -> actions -> list states
}.
(*States*)
Inductive st :Set:= q0 | q1 |q2 .
Inductive acts:Set:=pred(p:nat)|event(e:bool).
Definition a :acts:=pred(0).
Definition b:acts:=pred(1).
Definition c:acts:=event(true).
Function trans (q:st)(x:acts) :list st :=
match q, x with
  | q0, a =>  cons q1 nil
  | q1, b =>  cons q0 nil
  | q1, c =>  cons q2 nil
  | _,_ =>    nil (A:=_)
end.

错误是：错误：此子句是多余的。（在本条款下划线“| q1, c => cons q2 nil”）

感谢您的关注。

4

1 回答 1

1

当您执行模式匹配时，模式中有两种可能性：构造函数或充当绑定器的自由变量。例如，匹配的第一个案例读作 ''ifq已用 构造，并且对于将在分支中命名q0的任何值，do ...'''xa

a此分支中的 与您之前所做的定义之间没有关系Definition a。

因此，第 2 行和第 3 行是多余的，它们都捕获了q已构造q1并x具有任何值的情况。

我猜你想写这样的东西：

match q, x with
  | q0, pred 0 => cons q1 nil
  | q1, pred 1 => cons q0 nil
  | q1, event true => cons q2 nil
  | _, _ => nil (A := _)
end.

您可以Definition在模式匹配分支中使用别名。据我所知，做这样一个别名的唯一方法是使用Notation.

如果将a band的定义替换为c：

Notation "'a'" := (pred 0).
Notation "'b'" := (pred 1).
Notation "'c'" := (event true).

那么您的代码将表现得像（我认为）您想要的那样。我建议你阅读Coq 手册的这一部分来了解符号。

最好的，V.

于 2014-03-18T09:49:36.360 回答