 # Asymmetric variant of program equivalence : Program approximation

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)

``````(* 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.
``````

Thank you very much.

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

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

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!

Thank you! So encouraging!