带有coq的自动机的建模

Question

我在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")

感谢您的关注。

Answer 1

当您执行模式匹配时，模式中有两种可能性:构造函数或充当绑定器的自由变量。例如，匹配的第一个例子读作"如果q是用q0构造的，并且对于x的任何值将在分支中命名为a，执行…"

这个分支中的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 b和c的定义替换为:

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

，那么你的代码就会像你想的那样运行。我建议你阅读Coq手册的这一部分来学习符号。

最好的,v .