How can I prove 'deterministic step' cleverly?

[seohongpark]

I think proving deterministic step (step from MoreStlc chapter) directly is too complex...

Is there alternative way to prove deterministic step more cleverly? (using previously proven lemmas, etc ...)

[jaewooklee93]

This is my solution. You may be able to test this proof after copying it on Assignment12_01.v or other assignment files. (But it doesn't work on MoreStlc.v file itself, because operational semantic is not fully provided in that file. The professor filled it in our Assignment12_00.v file.)

Theorem MoreStlc_value_is_nf: forall v t,
  value v -> v ==> t -> False.
Proof with eauto.
  intros; generalize dependent t; assert (normal_form step v)...
  unfold normal_form; intros; induction H; intros contra; destruct contra;
  try solve by inversion; try inversion H0; try inversion H1; subst...
Qed.

Hint Resolve MoreStlc_value_is_nf.

Theorem MoreStlc_deterministic:
  deterministic step.
Proof with eauto.
  unfold deterministic; intros; generalize dependent y2;
  induction H as [| |? ? ? ? P| | | | | |? ? ? ? P| | | | | |? ? ? ? P| |? ? ? P|
  |? ? ? P| | | | | | | | |? ? ? ? P| | | ? ? ? ? ? ? P| |? ? ? P]; intros;
  inversion H0; subst; try solve by inversion;
  try replace t0'0 with t0';
  try replace t1'0 with t1';
  try replace t2'0 with t2';
  eauto; exfalso...
Qed.

I think the only dirty part in this proof is the pattern introduction after induction H, but you can even remove that part if you can utilize Ltac language nicely.

[seohongpark]

Wow, I'm surprised that the automation in Coq is far more powerful than I thought. That's a wonderful solution. Thanks a lot!

[sanha]

Wow, Thank you!