How can I prove "command = other command"?

[rhs0266]

At homework, I need to prove "command = other command" forms. Such as SKIP = (SKIP ;; SKIP).

Since I don't have cequiv and any states, how can I prove those things? Can I get some comment?

[jaewooklee93]

Um... I already finished this week's assignment, but I've never proved something like SKIP = (SKIP ;; SKIP), no such cases there. As you said, they are equivalent (cequiv SKIP (SKIP ;; SKIP)), but they are not the same and SKIP = (SKIP ;; SKIP) is simply False in every sense, so it is not provable. Thus, I strongly believe that if you encountered such impossible goal in some situations, you may also have False assumption in your context so that you can clear the goal with contradiction.

[jaewooklee93]

Since you can prove that it is False, you cannot prove it is True, in principle.

Lemma not_the_same:
(SKIP = (SKIP ;; SKIP)) -> False.
Proof.
intros; inversion H.
Qed.

[rhs0266]

Thanks a lot.

Then, if the state is fixed as st, SKIP / st || st and (SKIP ;; SKIP) / st || st are equivalent?

[jeehoonkang]

The two propositions are true, I think.

[rhs0266]

커맨드 2개가 같은 지를 증명하고 싶은 경우에는 어떻게 해야하나요? cequiv SKIP SKIP;;c 같은 경우는 가능하다는 걸 이해했는데, SKIP = (SKIP ;; c) 같은 경우에는 어떻게 해야하나요?

[jeehoonkang]

이해를 못했는데, 한국어로 물어봐주시겠어요?

[jaewooklee93]

SKIP = (SKIP ;; c) is always False and you cannot prove it.

Theorem not_equal:
  (exists c, SKIP = (SKIP ;; c)) -> False.
Proof.
  intros; inversion H; inversion H0.
Qed.

You should be careful about difference between equality (=) and equivalence (cequiv). (SKIP) and (SKIP;;c) can be equivalent for some c, like c=SKIP, but they are never equal.

[rhs0266]

Thanks a lot!

Then what about APlus a1 a2 = APlus a2 a1? Is it also impossible to prove?

[jaewooklee93]

Yes, it is impossible, too. That's the reason why we have aequiv, bequiv and cequiv.

[rhs0266]

Oh Thanks!!