将PVS转换为Coq

Question

我想将以下PVS翻译成Coq：

其中type trans的类型为env - > env - > bool，我按如下方式编写Coq代码：

Definition trans := env -> env -> bool.

Definition dseq (P Q : trans) : trans :=
  fun s1 s2 => andb (P s1 s') (Q s' s2).

但是，我不知道在Coq中代表存在（s：env）。该定义的目标是存在满足（P s1 s）和（P s s2）的值s。我不想使用逻辑，因为我想证明以下定理：

Theorem dseq_comm:
  forall (F G H : trans), dseq (desq F G) H = dseq F (dseq G H).

Answer 1

你有可能想用Prop而不是bool。然后你可以写：

Parameter env : Type.

Definition trans := env -> env -> Prop.

Definition dseq (P Q : trans) : trans :=
  fun s1 s2 => exists s', P s1 s' /\ Q s' s2.

你将能够证明

Theorem dseq_assoc:
  forall (F G H : trans), dseq (desq F G) H = dseq F (dseq G H).

如果你愿意承担Proposition extensionality。