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.
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.
If feel like my definition of cmin is meaningless… please advice
Thank you very much.