From 4c5d54810bc939019f400cf51648df54860955f9 Mon Sep 17 00:00:00 2001
From: Adrien Burgun <adrien.burgun@orange.fr>
Date: Mon, 30 Oct 2023 22:58:59 +0100
Subject: [PATCH] Try (and fail) the first exercise

---
 theories/type_systems/stlc/exercises01.v | 82 +++++++++++++++++++++++-
 theories/type_systems/stlc/lang.v        | 17 +++--
 2 files changed, 87 insertions(+), 12 deletions(-)

diff --git a/theories/type_systems/stlc/exercises01.v b/theories/type_systems/stlc/exercises01.v
index 9268769..a4d0ea0 100644
--- a/theories/type_systems/stlc/exercises01.v
+++ b/theories/type_systems/stlc/exercises01.v
@@ -9,6 +9,7 @@ Lemma val_no_step e e':
 Proof.
   by destruct 1.
 Qed.
+
 (* Note how the above lemma is another way to phrase the statement "values
  * cannot step" that doesn't need inversion. It can also be used to prove the
  * phrasing we had to use inversion for in the lecture: *)
@@ -41,10 +42,86 @@ Ltac val_no_step :=
     solve [exfalso; eapply (val_no_step _ _ H); done]
   end.
 
+(* Lemma app_eq e1 e2 e3 e4:
+  (App e1 e2) = (App e3 e4) → e1 = e3 ∧ e2 = e4.
+Proof.
+
+  intro h.
+  split.
+  injection h as hnm.
+  assumption.
+  injection h as hnm.
+  assumption.
+Qed. *)
+
 Lemma step_det e e' e'':
   step e e' → step e e'' → e' = e''.
 Proof.
-  (* TODO: exercise *)
+  intros H_step H_step'.
+
+  (*
+    `induction` here seems to introduce incorrect induction hypothesis for IH_λ, IH_v, IH_a, IH_b. Those try to prove that e' = e'', when I need them to prove other equalities later introduced by `inversion H_step`.
+
+    When swapping `inversion H_step` and `induction e`,
+    the number of things to prove jumps to 30, and I do not know how to quickly prove the incorrect ones.
+    `inversion e` doesn't introduce any induction hypothesis, so it is also out of the question.
+  *)
+  induction e as [
+    name |
+    name body |
+    e_λ IH_λ e_v IH_v |
+    n |
+    a IH_a b IH_b
+  ].
+  - inversion H_step.
+  - inversion H_step.
+  - inversion H_step.
+    {
+      rewrite <-H in H_step'.
+      inversion H_step'.
+      - reflexivity.
+      - inversion H7.
+      - val_no_step.
+    }
+    {
+      inversion H_step'.
+      - rewrite <-H4 in H3.
+        inversion H3.
+      - admit.
+      - val_no_step.
+    }
+    {
+      inversion H_step'.
+      - val_no_step.
+      - val_no_step.
+      - admit.
+    }
+  - inversion H_step.
+  - inversion H_step.
+    {
+      rewrite <-H in H_step'.
+      rewrite <-H1 in H_step'.
+      inversion H_step'.
+      - rewrite <-H6.
+        rewrite <-H2.
+        reflexivity.
+      - val_no_step.
+      - val_no_step.
+    }
+    {
+      inversion H_step'.
+      - rewrite <-H4 in H3.
+        val_no_step.
+      - admit.
+      - val_no_step.
+    }
+    {
+      inversion H_step'.
+      - rewrite <-H5 in H2.
+        val_no_step.
+      - val_no_step.
+      - admit.
+    }
 Admitted.
 
 
@@ -129,7 +206,7 @@ Section rtc.
   Qed.
   End typeclass.
 End rtc.
- 
+
 (* Let's put this to the test! *)
 Goal rtc step (LitInt 42) (LitInt 42).
 Proof.
@@ -242,4 +319,3 @@ Lemma ltr_steps_big_step e (v: val):
 Proof.
   (* TODO: exercise *)
 Admitted.
-
diff --git a/theories/type_systems/stlc/lang.v b/theories/type_systems/stlc/lang.v
index b668d78..d147c01 100644
--- a/theories/type_systems/stlc/lang.v
+++ b/theories/type_systems/stlc/lang.v
@@ -74,11 +74,16 @@ Proof.
   all: naive_solver.
 Qed.
 
+(* values are values *)
 Lemma is_val_of_val v : is_val (of_val v).
 Proof.
+  destruct v; simpl; done.
+  Restart.
   apply is_val_spec. rewrite to_of_val. eauto.
 Qed.
 
+Definition is_val_val := is_val_of_val.
+
 (* A small tactic that simplifies handling values. *)
 Ltac simplify_val :=
   repeat match goal with
@@ -86,15 +91,9 @@ Ltac simplify_val :=
   | H: is_val ?e |- _ => destruct (proj1 (is_val_spec e) H) as (? & ?); clear H
   end.
 
-(* values are values *)
-Lemma is_val_val (v: val): is_val (of_val v).
-Proof.
-  destruct v; simpl; done.
-Qed.
-
-(* we tell eauto to use the lemma is_val_val *)
+(* we tell eauto to use the lemma is_val_of_val *)
 #[global]
-Hint Immediate is_val_val : core.
+Hint Immediate is_val_of_val : core.
 
 
 (** ** Operational Semantics *)
@@ -125,7 +124,7 @@ Definition subst' (mx : binder) (es : expr) : expr → expr :=
    the left side can only be reduced once the right
    side is fully evaluated (i.e., is a value). *)
 Inductive step : expr → expr → Prop :=
-  | StepBeta x e e'  :
+  | StepBeta x e e' :
       is_val e' →
       step (App (Lam x e) e') (subst' x e' e)
   | StepAppL e1 e1' e2 :