coq - 将 PVS 翻译成 Coq

Question

我想将以下 PVS 翻译成 Coq：

其中类型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中表示Exists (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).

如果你愿意假设命题外延。