From mininix Require Export lambda.operational.
From stdpp Require Import options.

Module Import lambda.
Export lambda.

(** Properties of operational semantics *)
Lemma step_not_final e1 e2 : e1 --> e2 → ¬final e1.
Proof. induction 1; inv 1; naive_solver. Qed.
Lemma final_nf e : final e → nf step e.
Proof. by intros ? [??%step_not_final]. Qed.

Lemma SAppL_rtc e1 e1' e2 : e1 -->* e1' → EApp e1 e2 -->* EApp e1' e2.
Proof. induction 1; repeat (done || econstructor). Qed.

Ltac inv_step := repeat
  match goal with H : ?e --> _ |- _ => assert_fails (is_var e); inv H end.

Lemma step_det e d1 d2 :
  e --> d1 →
  e --> d2 →
  d1 = d2.
Proof.
  intros Hred1. revert d2.
  induction Hred1; intros d2 Hred2; inv Hred2; try by inv_step.
  f_equal. by apply IHHred1.
Qed.

End lambda.