Translate the PVS into Coq

Question

I want to translate the following PVS into Coq:

where type trans has type env -> env -> bool, I write the Coq code as follows:

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

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

However, I have no idea to represent the Exists (s : env) in Coq. The goal of this definition is that there exists a value s that satisfies the (P s1 s) and (P s s2). I would not like to use logic since I want to prove the following theorem:

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

gallais gallais · Accepted Answer · 2018-03-02T12:42:25

Chances are you want to use Prop instead of bool. You can then write:

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.

You will be able to prove

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

if you're willing to assume Proposition extensionality.

Translate the PVS into Coq

1 Answers