🎉 Finish exercise sheet 1

theories/type_systems/stlc/exercises01.v

@@ -508,5 +508,90 @@ Qed.
 Lemma ltr_steps_big_step e (v: val):
   rtc ltr_step e v → big_step e v.
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  intro H.
+  remember (of_val v) eqn:H_val in H.
+  induction H; subst.
+  apply big_step_vals.
+  remember ((IHrtc (eq_refl (of_val v)))) as IH.
+  clear HeqIH.
+  clear IHrtc.
+  (* This is ridiculous. *)
+  revert H0.
+  revert IH.
+  revert v.
+  induction H; intros v IH H_rtc.
+  - destruct (is_val_to_of_val H) as [ e'_v H_val ].
+    rewrite H_val.
+    eapply bs_app.
+    apply bs_lam.
+    apply big_step_vals.
+    rewrite <-H_val.
+    assumption.
+  - inversion IH; subst.
+    eapply bs_app.
+    apply IHltr_step.
+    exact H2.
+    apply big_step_ltr_steps.
+    all: eauto.
+  - inversion IH; subst.
+    eapply bs_app.
+    exact H3.
+    apply IHltr_step.
+    exact H4.
+    apply big_step_ltr_steps.
+    all: eauto.
+  - inversion IH; subst.
+    eauto.
+  - inversion IH; subst.
+    assert (big_step e1 (LitIntV z1)).
+    {
+      apply IHltr_step.
+      assumption.
+      apply big_step_ltr_steps.
+      assumption.
+    }
+    eauto.
+  - inversion IH; subst.
+    assert (big_step e2 (LitIntV z2)).
+    {
+      apply IHltr_step.
+      assumption.
+      apply big_step_ltr_steps.
+      assumption.
+    }
+    eauto.
+Qed.
+
+Theorem steps_iff_ltr_steps e v :
+  rtc step e (of_val v) ↔ rtc ltr_step e (of_val v).
+Proof.
+  split.
+  - intro H.
+    apply big_step_ltr_steps.
+    apply steps_big_step.
+    assumption.
+  - intro H.
+    apply big_step_steps.
+    apply ltr_steps_big_step.
+    assumption.
+Qed.
+
+(*
+  This result is unlike languages like javascript, where mutation cause a dependence on the execution order:
+
+  ```
+  let x = 0;
+  function hof() {
+    x *= 2;
+    return (_) => x;
+  }
+  function inc() {
+    x += 1;
+    return x;
+  }
+
+  console.log((hof())(inc()));
+  // prints 1 if hof() is called before inc() (current behavior)
+  // prints 2 if inc() is called before hof()
+  ```
+*)