CODEWITHSUNDEEP
coq
Frank Sheng
Frank Sheng

Reputation: 205

How can I define the equality of pair in Coq?

I define a type as follows:

Definition trans := env -> env -> Prop.
Definition tripored := trans * trans * trans.
Definition qt (t : tripored) := fst (fst t).
Definition wt (t : tripored) := snd (fst t).
Definition tt (t : tripored) := snd t.
Definition II := (ttrue, tfalse, I).

Then I define a operator based on the tripored such as 

Definition seqtr (m n : tripored) : tripored :=
(
  nott (ort (nott (qt m)) (dseq (tt m) (nott (qt n)))),
  ort (wt m) (dseq (tt m) (wt n)),
  dseq (tt m) (tt n)
).

There are many operators such as ort, dseq and so on. I want to prove the following theorem:

Theorem seqtr_ii :
  forall n : tripored, seqtr n II = n.

However, since the (seqtr n II) has type trans * trans * trans, I find difficult to prove this theorem. Can anyone give some advice for this theorem?

Upvotes: 1

Views: 345

Answers (1)

eponier
eponier

Reputation: 3122

Since you did not provide all the definitions, it is hard to answer precisely, but I will try.

Since n is a triple, you can first extract its components with destruct n as ((t1, t2), t3), where t1, t2, t3 are of type trans.

Then unfold seqtr replaces seqtr with its body.

The conclusion becomes an equality of two triples. To turn it into 3 goals stating the equality of the components, you can use do 2 apply f_equal2 or just f_equal.

Upvotes: 3

Related Questions