I'm new to Coq and to learn formal semantics I'm following the book Software Foundations. Currently I'm in the chapter: https://softwarefoundations.cis.upenn.edu/lf-current/Imp.html. Where it defines the commands for a simple imperative language. As an exercise I've tried to add a repeat command to the language defined as follows:
Inductive ceval : com -> state -> state -> Prop :=
(* ...same as in the book *)
| E_RepeatTrue : forall st st' b c,
[ c, st ] ~> st' ->
beval st' b = true ->
[ repeat c until b end, st ] ~> st'
| E_RepeatFalse : forall st st' st'' b c,
[ c, st ] ~> st'' ->
beval st'' b = false ->
[ repeat c until b end, st'' ] ~> st' ->
[ repeat c until b end, st ] ~> st'
where "'[' c ',' st ']' '~>' st'" := (ceval c st st').
But I'm stuck trying to prove that the command repeat c until b end is equivalent to c; while ~b do c end, in the following sense:
Definition cequiv (c1 c2 : com) : Prop :=
forall (st st' : state),
([ c1, st ] ~> st') <-> ([ c2, st ] ~> st').
I defined the theorem in Coq as follows:
Theorem repeat_equiv_while : forall b c,
cequiv <{repeat c until b end}> <{c; while ~b do c end}>.
Proof.
intros.
split; intros.
- inversion H; subst.
+ apply E_Concat with st'. assumption.
apply E_WhileFalse. apply bev_not_true_iff_false.
rewrite <- H5. apply bev_negb_involutive.
+ (* infinite loop? *)
admit.
- inversion H. subst.
inversion H5. subst.
+ apply E_RepeatTrue. assumption.
apply bev_not_true_iff_false in H6.
rewrite <- H6. symmetry.
apply bev_negb_involutive.
+ admit.
Admitted.
I've managed to prove the cases where the evaluation ends in the next step but when I try to prove the other case I get stuck in a loop. I would like to apply the induction hypothesis to solve it, but I don't know how to do it. I think maybe dependent induction can help me but I couldn't manage to prove it either using it.
You have solved the easy case, in which both loops terminate. In the more interesting case that they don't, you need to use an inductive hypothesis that will claim that the loops are equivalent for the remaining iterations. This induction is well founded because the remaining iterations are fewer by one than the ones we started with. Therefore, in principle, you need to do induction on the number of iterations that the loops will make.
Now, a problem that is inherent in big-step semantics is that this number of iterations is not explicit. Therefore, the easiest way to prove your theorem is by induction on the derivation of your big-step semantics. This has to be done carefully; it has to be a dependent induction in Coq, as otherwise you will miss information in the proofs. Furthermore, in the proof of the inverse, you need to carefully generalize your goal after the inversion, otherwise the inductive hypothesis will not be strong enough to be applied.
I'm writing down the skeleton, which shows the Coq technicalities, but I'm leaving the rest admitted because I don't want to spoil the exercise. Happy proving!
Theorem repeat_equiv_while_fixed : forall b c,
cequiv <{repeat c until b end}> <{c; while ~b do c end}>.
Proof.
intros; split; intros.
- dependent induction H.
+ admit.
+ admit.
- inversion H; subst; clear H.
generalize st H2; clear st H2.
dependent induction H5; intros st0 H2.
+ admit.
+ admit.
Qed.