From b0a5c90ebb98a7c3c0ebc3674016fe0e83fd3d96 Mon Sep 17 00:00:00 2001
From: Adrien Burgun <adrien.burgun@orange.fr>
Date: Wed, 1 Nov 2023 18:48:52 +0100
Subject: [PATCH] :tada: Finish exercise sheet 1

---
 theories/type_systems/stlc/exercises01.v | 89 +++++++++++++++++++++++-
 1 file changed, 87 insertions(+), 2 deletions(-)

diff --git a/theories/type_systems/stlc/exercises01.v b/theories/type_systems/stlc/exercises01.v
index b7c755d..eef06d7 100644
--- a/theories/type_systems/stlc/exercises01.v
+++ b/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()
+  ```
+*)