Asymmetric variant of program equivalence : Program approximation

Using Coq
1

Dear friends,
I solved exercise, but I feel like my definition is not what was expected by authors.
It is a very last exercise in this chapter.
https://softwarefoundations.cis.upenn.edu/current/plf-current/Equiv.html

Exercise: 4 stars, advanced, optional (capprox)

Second task:

(* Find a program cmin that approximates every other program. 

Definition capprox (c1 c2 : com) : Prop := forall (st st' : state),
    st =[ c1 ]-> st' -> st =[ c2 ]-> st'.

Theorem skip_left : forall c,
  cequiv
    (SKIP;; c)
    c.

*)

Definition cmin c : com := SKIP ;; c.

Theorem cmin_minimal : forall c, capprox (cmin c) c.
Proof. unfold capprox.
       unfold cmin.
       intros.
       induction c; apply skip_left; apply H.
Qed.

If feel like my definition of cmin is meaningless… please advice
Thank you very much.

2

Hello,

Indeed you have “cheated” in that your program cmin is parameterized by a program c, while the goal of the exercise is to find a constant program. You should have:
Definition cmin : com := ??? (* Fill the solution in here *).
Theorem cmin_minimal : forall c, capprox cmin c.
Hope it helps.

Best,
Yannick

3

Thanks… yeah.
I’ll keep thinking.

Oh, I have an idea: definition of capprox is the next:

“program c1 approximates a program c2 when, for each of the initial states for which c1 terminates, c2 also terminates”

what if c1 (cmin) never terminates? it is not cheating this time, right?

Definition cmin : com := WHILE BTrue DO SKIP END.

Theorem cmin_minimal : forall c, capprox cmin c.
Proof. unfold capprox.
       unfold cmin.
       intros.
       induction c; apply WHILE_true_nonterm in H; inversion H; unfold bequiv; intros; auto.
Qed.
1 Like
4

That is definitely not cheating, that was indeed the expected answer: the goal of the exercise is to understand the subtlety of partial correctness/refinement, that only constraints terminating executions.

Well done!

5

Thank you! So encouraging!