From 9f2a8302e9d0543c7e828c17c9bcb11759ee19f3 Mon Sep 17 00:00:00 2001
From: Adrien Burgun <adrien.burgun@orange.fr>
Date: Sun, 5 Nov 2023 16:15:42 +0100
Subject: [PATCH] :sparkles: Solve exercises02 :3

---
 _CoqProject                              |   2 +-
 theories/type_systems/stlc/exercises02.v | 412 ++++++++++++++++++++---
 2 files changed, 358 insertions(+), 56 deletions(-)

diff --git a/_CoqProject b/_CoqProject
index 5ae0220..12baf82 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -30,4 +30,4 @@ theories/type_systems/warmup/warmup.v
 #theories/type_systems/warmup/warmup_sol.v
 theories/type_systems/stlc/exercises01.v
 #theories/type_systems/stlc/exercises01_sol.v
-#theories/type_systems/stlc/exercises02.v
+theories/type_systems/stlc/exercises02.v
diff --git a/theories/type_systems/stlc/exercises02.v b/theories/type_systems/stlc/exercises02.v
index a759308..15d9f80 100644
--- a/theories/type_systems/stlc/exercises02.v
+++ b/theories/type_systems/stlc/exercises02.v
@@ -12,44 +12,63 @@ From semantics.ts.stlc Require untyped types.
 (** You will find it very helpful to separately derive the structural rules of the
   structural semantics for the contextual semantics. *)
 
+
+Ltac ectx_step K :=
+  eapply (Ectx_step _ _ K); subst; eauto.
+
 Lemma contextual_step_beta x e e':
   is_val e' → contextual_step ((λ: x, e) e') (subst' x e' e).
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  intro H_val.
+  ectx_step HoleCtx.
+Qed.
 
 
 Lemma contextual_step_app_r (e1 e2 e2': expr) :
   contextual_step e2 e2' →
   contextual_step (e1 e2) (e1 e2').
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  intro H_step.
+  inversion H_step.
+  induction K eqn:H_K.
+  (* I am a smart foxxo >:3 *)
+  all: ectx_step (AppRCtx e1 K).
+Qed.
 
+Ltac is_val_to_val v H :=
+  rewrite (is_val_spec _) in H; destruct H as [v H]; apply of_to_val in H; symmetry in H.
 
 Lemma contextual_step_app_l (e1 e1' e2: expr) :
   is_val e2 →
   contextual_step e1 e1' →
   contextual_step (e1 e2) (e1' e2).
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  intros H_val H_step.
+  is_val_to_val v H_val.
+  subst.
 
+  inversion H_step.
+  induction K eqn:H_K.
+  all: ectx_step (AppLCtx K v).
+Qed.
 
 Lemma contextual_step_plus_red (n1 n2 n3: Z) :
   (n1 + n2)%Z = n3 →
   contextual_step (n1 + n2)%E n3.
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  intro H_plus.
+  ectx_step HoleCtx.
+Qed.
 
 
 Lemma contextual_step_plus_r e1 e2 e2' :
   contextual_step e2 e2' →
   contextual_step (Plus e1 e2) (Plus e1 e2').
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  intro H_step.
+  inversion H_step.
+  ectx_step (PlusRCtx e1 K).
+Qed.
 
 
 Lemma contextual_step_plus_l e1 e1' e2 :
@@ -57,18 +76,32 @@ Lemma contextual_step_plus_l e1 e1' e2 :
   contextual_step e1 e1' →
   contextual_step (Plus e1 e2) (Plus e1' e2).
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  intro H_val.
+  is_val_to_val v H_val.
+  intro H_step.
+  inversion H_step.
+  ectx_step (PlusLCtx K v).
+Qed.
 
 
 (** We register these lemmas as hints for [eauto]. *)
 #[global]
 Hint Resolve contextual_step_beta contextual_step_app_l contextual_step_app_r contextual_step_plus_red contextual_step_plus_l contextual_step_plus_r : core.
 
+Ltac step_ind H := induction H as [
+  name e_λ e_v
+  | e_fn e_fn' e_v H_val H_fn_step IH
+  | e_fn e_arg e_arg' H_arg_step IH
+  | n1 n2 n_sum H_plus
+  | e_l e_l' e_r H_val H_l_step IH
+  | e_l e_r e_r' H_r_step IH
+].
+
 Lemma step_contextual_step e1 e2: step e1 e2 → contextual_step e1 e2.
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  intro H_step.
+  step_ind H_step; eauto.
+Qed.
 
 
 (** Now the other direction. *)
@@ -78,8 +111,19 @@ Admitted.
 Lemma contextual_step_step e1 e2:
   contextual_step e1 e2 → step e1 e2.
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  intro H_cstep.
+  inversion H_cstep as [K e1' e2' H_eq1 H_eq2 H_bstep]; subst.
+  inversion H_bstep as [
+    name body arg H_val H_eq1 H_eq2 H_eq3
+    | e1 e2 n1 n2 n_sum H_n1 H_n2 H_sum H_eq1 H_eq2
+  ]; subst.
+  (*
+    Here we do an induction on K, and we let eauto solve it for us.
+    In practice, each case of the induction on K can be solved quite easily,
+    as the induction hypothesis has us prove a `contextual_step`, for which we have plenty of useful lemmas.
+  *)
+  all: induction K; unfold fill; eauto.
+Qed.
 
 
 
@@ -89,51 +133,147 @@ Section scott.
   Import semantics.ts.stlc.untyped.
 
   (** Scott encoding of Booleans *)
-  Definition true_scott : val := 0(* TODO *).
-  Definition false_scott : val := 0(* TODO *).
+  Definition true_scott : val := (λ: "t" "f", "t").
+  Definition false_scott : val := (λ: "t" "f", "f").
+
+  (* Lemma steps_beta e_λ e_arg *)
+  Ltac rtc_single step_cons := eapply rtc_l; last reflexivity; eapply step_cons; auto.
 
   Lemma true_red (v1 v2 : val) :
     closed [] v1 →
     closed [] v2 →
     rtc step (true_scott v1 v2) v1.
   Proof.
-    (* TODO: exercise *)
-  Admitted.
+    intros H_cl1 H_cl2.
+    unfold true_scott.
+    etransitivity.
+    eapply steps_app_l; auto.
+    rtc_single StepBeta.
+    simpl.
+    etransitivity.
+    rtc_single StepBeta.
+    simpl.
+    rewrite subst_closed_nil; auto.
+    reflexivity.
+  Qed.
+
+  Lemma steps_plus_r (e1 e2 e2': expr) :
+    rtc step e2 e2' → rtc step (e1 + e2)%E (e1 + e2')%E.
+  Proof.
+    induction 1; subst.
+    reflexivity.
+    etransitivity; last exact IHrtc.
+    rtc_single StepPlusR.
+  Qed.
+
+  Lemma steps_plus_l (e1 e1' e2: expr) :
+    is_val e2 →
+    rtc step e1 e1' →
+    rtc step (e1 + e2)%E (e1' + e2)%E.
+  Proof.
+    induction 2; subst.
+    reflexivity.
+    etransitivity; last exact IHrtc.
+    rtc_single StepPlusL.
+  Qed.
+
+  Lemma lam_is_val name e_body :
+    is_val (Lam name e_body).
+  Proof.
+    unfold is_val.
+    intuition.
+  Qed.
 
+  Lemma int_is_val n :
+    is_val (LitInt n).
+  Proof.
+    unfold is_val.
+    intuition.
+  Qed.
+
+  Hint Resolve lam_is_val int_is_val: core.
+
+  (* TODO: recursively traverse the goal for subst instances? *)
+  Ltac auto_subst :=
+    (rewrite subst_closed_nil; last assumption) ||
+    (unfold subst'; unfold subst; simpl; fold subst).
+
+  (* This is ridiculously powerful, although it only works when you know all the terms *)
+  Ltac auto_step :=
+    match goal with
+      | [ |- rtc step (App ?e_l ?e_v) ?e_target ] =>
+        etransitivity;
+        first eapply steps_app_r;
+        first auto_step;
+        simpl;
+        etransitivity;
+        first eapply steps_app_l;
+        first auto;
+        first auto_step;
+        simpl;
+        repeat auto_subst;
+        rtc_single StepBeta;
+        simpl;
+        done
+      | [ |- rtc step (of_val ?v) ?e_target ] => reflexivity
+      | [ |- rtc step (Lam ?name ?body) ?e_target ] => reflexivity
+      | [ |- rtc step (LitInt ?n) ?e_target ] => reflexivity
+      | [ |- rtc step (Plus ?e1 ?e2) ?e_target ] =>
+        etransitivity;
+        first eapply steps_plus_r;
+        first auto_step;
+        etransitivity;
+        first eapply steps_plus_l;
+        first auto;
+        first auto_step;
+        rtc_single StepPlusRed;
+        done
+      | [ |- rtc step (subst ?var ?thing) ?e_target ] =>
+        repeat auto_subst;
+        auto_step
+    end
+  .
+
+  Ltac multi_step :=
+    repeat (reflexivity || (
+      etransitivity;
+      first auto_step;
+      first repeat auto_subst
+    )).
 
   Lemma false_red (v1 v2 : val) :
     closed [] v1 →
     closed [] v2 →
     rtc step (false_scott v1 v2) v2.
   Proof.
-    (* TODO: exercise *)
-  Admitted.
+    intros H_cl1 H_cl2.
+    auto_step.
+  Qed.
 
 
   (** Scott encoding of Pairs *)
-  Definition pair_scott : val := 0(* TODO *).
+  Definition pair_scott : val := (λ: "lhs" "rhs" "f", ("f" "lhs" "rhs")).
 
-  Definition fst_scott : val := 0(* TODO *).
-  Definition snd_scott : val := 0(* TODO *).
+  Definition fst_scott : val := (λ: "pair", ("pair" (λ: "lhs" "rhs", "lhs"))).
+  Definition snd_scott : val := (λ: "pair", ("pair" (λ: "lhs" "rhs", "rhs"))).
 
   Lemma fst_red (v1 v2 : val) :
     is_closed [] v1 →
     is_closed [] v2 →
     rtc step (fst_scott (pair_scott v1 v2)) v1.
   Proof.
-    (* TODO: exercise *)
-  Admitted.
-
+    intros H_cl1 H_cl2.
+    multi_step.
+  Qed.
 
   Lemma snd_red (v1 v2 : val) :
     is_closed [] v1 →
     is_closed [] v2 →
     rtc step (snd_scott (pair_scott v1 v2)) v2.
   Proof.
-    (* TODO: exercise *)
-  Admitted.
-
-
+    intros H_cl1 H_cl2.
+    multi_step.
+  Qed.
 End scott.
 
 Import semantics.ts.stlc.types.
@@ -151,7 +291,13 @@ Inductive src_expr :=
 
 (** The erasure function *)
 Fixpoint erase (E: src_expr) : expr :=
-0 (* TODO *).
+  match E with
+  | ELitInt n => LitInt n
+  | EVar x => Var x
+  | ELam x A e => Lam x (erase e)
+  | EApp e1 e2 => App (erase e1) (erase e2)
+  | EPlus e1 e2 => Plus (erase e1) (erase e2)
+  end.
 
 Reserved Notation "Γ '⊢S' e : A" (at level 74, e, A at next level).
 Inductive src_typed : typing_context → src_expr → type → Prop :=
@@ -177,20 +323,51 @@ where "Γ '⊢S' E : A" := (src_typed Γ E%E A%ty) : FType_scope.
 Lemma type_erasure_correctness Γ E A:
   (Γ ⊢S E : A)%ty → (Γ ⊢ erase E : A)%ty.
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  intro H_styped.
+  induction H_styped; unfold erase; eauto.
+Qed.
 
 
 (** ** Exercise 4: Unique Typing *)
 Lemma src_typing_unique Γ E A B:
   (Γ ⊢S E : A)%ty → (Γ ⊢S E : B)%ty → A = B.
 Proof.
-  (* TODO: exercise *)
-Admitted.
-
-
-(** TODO: Is runtime typing (Curry-style) also unique? Prove it or give a counterexample. *)
+  intro H_typed.
+  revert B.
+  induction H_typed as [
+    Γ x A H_x_ty
+    | Γ x e_body A1 A2 H_body_ty IH
+    | Γ n
+    | Γ e_fn e_arg A1 A2 H_fn_ty H_arg_ty IH
+    | Γ e1 e2 H_e1_ty H_e2_ty
+  ]; intro B; intro H_typed'.
+  all: inversion H_typed' as [
+    Γ' y B' H_y_ty
+    | Γ' y e_body' B1 B2 H_body_ty'
+    | Γ' n'
+    | Γ' e_fn' e_arg' B1 B2 H_fn_ty' H_arg_ty'
+    | Γ' e3 e4 H_e3_ty H_e4_ty
+  ]; subst; try auto.
+  - rewrite H_y_ty in H_x_ty; injection H_x_ty.
+    intuition.
+  - rewrite (IH B2); eauto.
+  - remember (H_arg_ty _ H_fn_ty') as H_eq.
+    injection H_eq.
+    intuition.
+Qed.
 
+Lemma syn_typing_not_unique:
+  ∃ (Γ: typing_context) (e: expr) (A B: type),
+  (Γ ⊢ e: A)%ty ∧ (Γ ⊢ e: B)%ty ∧ A ≠ B.
+Proof.
+  exists ∅.
+  exists (λ: "x", "x")%E.
+  exists (Int → Int)%ty.
+  exists ((Int → Int) → (Int → Int))%ty.
+  repeat split.
+  3: discriminate.
+  all: apply typed_lam; eauto.
+Qed.
 
 (** ** Exercise 5: Type Inference *)
 
@@ -216,25 +393,90 @@ Fixpoint infer_type (Γ: ctx) E :=
     | None => None
     end
   (* TODO: complete the definition for the remaining cases *)
-  | ELitInt l => None (* TODO *)
-  | EApp E1 E2 => None (* TODO *)
-  | EPlus E1 E2 => None (* TODO *)
+  | ELitInt l => Some (Int) (* TODO *)
+  | EApp E1 E2 => match infer_type Γ E1, infer_type Γ E2 with
+    | Some (Fun A B), Some A' => (if type_eq A A' then Some B else None)
+    | _, _ => None
+    end
+  | EPlus E1 E2 => match infer_type Γ E1, infer_type Γ E2 with
+    | Some Int, Some Int => Some Int
+    | _, _ => None
+    end
   | ELam BAnon A E => None
   end.
 
+Ltac destruct_match H H_eq :=
+  repeat match goal with
+  | [H: match ?matcher with _ => _ end = Some _ |- _] =>
+    induction matcher eqn:H_eq; try discriminate H
+  end.
+
 (** Prove both directions of the correctness theorem. *)
 Lemma infer_type_typing Γ E A:
   infer_type Γ E = Some A → (Γ ⊢S E : A)%ty.
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  revert Γ A.
+  induction E; intros Γ B H_infer; inversion H_infer; subst; eauto.
+  - destruct_match H0 H_x.
+    destruct_match H0 H_eq.
+    injection H0; intro H_eq'.
+    subst.
+    eapply src_typed_lam.
+    exact (IHE _ _ H_eq).
+  - destruct_match H0 H_E1.
+    destruct_match H0 H_a.
+    destruct_match H0 H_E2.
+    destruct_match H0 H_eq.
+    clear IHt1 IHt2.
+    apply Is_true_eq_left in H_eq.
+    rewrite type_eq_iff in H_eq.
+    injection H0; intro H_eq'.
+    subst.
+    eapply src_typed_app.
+    exact (IHE1 _ _ H_E1).
+    exact (IHE2 _ _ H_E2).
+  - destruct_match H0 H_E1.
+    destruct_match H0 H_a.
+    destruct_match H0 H_E2.
+    rename a0 into b.
+    destruct_match H0 H_b.
+    injection H0; intro H_eq.
+    subst.
+    eapply src_typed_add.
+    exact (IHE1 _ _ H_E1).
+    exact (IHE2 _ _ H_E2).
+Qed.
 
 
 Lemma typing_infer_type Γ E A:
   (Γ ⊢S E : A)%ty → infer_type Γ E = Some A.
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  intro H_typed.
+  induction H_typed; simpl; try eauto.
+  - induction (infer_type (<[x := A]> Γ) E) eqn:H1; try discriminate IHH_typed.
+    rewrite H1.
+    injection IHH_typed; intro H_eq.
+    rewrite H_eq.
+    intuition.
+  - induction (infer_type Γ E1) eqn:H1; try discriminate IHH_typed1.
+    injection IHH_typed1; intro H_eq; subst.
+    induction (infer_type Γ E2) eqn:H2; try discriminate IHH_typed2.
+    injection IHH_typed2; intro H_eq; subst.
+    destruct (type_eq A A) eqn:H_AA.
+    + reflexivity.
+    + (* idk why I struggled so much to manipulate H_AA *)
+      assert (A = A) as H_AA_true by reflexivity.
+      rewrite <-type_eq_iff in H_AA_true.
+      apply Is_true_eq_true in H_AA_true.
+      rewrite H_AA_true in H_AA.
+      discriminate H_AA.
+  - induction (infer_type Γ E1) eqn:H1; try discriminate IHH_typed.
+    injection IHH_typed1; intro H_eq; subst.
+    induction (infer_type Γ E2) eqn:H2; try discriminate IHH_typed2.
+    injection IHH_typed2; intro H_eq; subst.
+    + reflexivity.
+    + discriminate IHH_typed1.
+Qed.
 
 
 
@@ -246,28 +488,88 @@ Admitted.
 *)
 
 Section give_example.
-  Definition ust : expr := 0 (* TODO *).
+  Definition omega : expr := (λ: "x", "x" "x").
+  (* This is simply binding Ω to a variable, without using it. *)
+  Definition ust : expr := ((λ: "x" "y", "y") (λ: "_", omega omega) 1)%E.
 
   Lemma ust_safe e':
     rtc step ust e' → is_val e' ∨ reducible e'.
   Proof.
-    (* TODO: exercise *)
-  Admitted.
 
+    intro H_steps.
+    assert (e' = 1 ∨ e' = ((λ: "y", "y") 1)%E ∨ e' = ust).
+    {
+      refine (rtc_ind_r (λ (e: expr), e = 1 ∨ e = ((λ: "y", "y") 1)%E ∨ e = ust) ust _ _ _ H_steps).
+      - right; right; reflexivity.
+      - intros y z H_steps' H_step_yz H_y.
+        destruct H_y; subst; try val_no_step.
+        destruct H; subst.
+        + inversion H_step_yz; subst; try val_no_step; simpl.
+          left; reflexivity.
+        + inversion H_step_yz; subst; try val_no_step; simpl.
+          inversion H3; subst; try val_no_step; simpl.
+          right; left; reflexivity.
+    }
+    destruct H as [ H | [ H | H ]].
+    - left.
+      rewrite H.
+      unfold is_val; intuition.
+    - right.
+      exists 1.
+      subst.
+      apply StepBeta.
+      unfold is_val; intuition.
+    - right.
+      exists ((λ: "y", "y") 1)%E.
+      subst.
+      apply StepAppL.
+      unfold is_val; intuition.
+      apply StepBeta.
+      unfold is_val; intuition.
+  Qed.
+
+  Lemma rec_type_contra A B:
+    (A → B)%ty = A -> False.
+  Proof.
+    revert B.
+    induction A.
+    - intros B H_eq.
+      discriminate H_eq.
+    - intros B H_eq.
+      injection H_eq.
+      intros H_eqb H_eqA1.
+      eapply IHA1.
+      exact H_eqA1.
+  Qed.
 
   Lemma ust_no_type Γ A:
     ¬ (Γ ⊢ ust : A)%ty.
   Proof.
-    (* TODO: exercise *)
-  Admitted.
+    intro H_typed.
+    inversion H_typed; subst; rename H2 into H_typed_let_omega.
+    inversion H_typed_let_omega; subst; rename H5 into H_typed_lambda_omega.
+    inversion H_typed_lambda_omega; subst; rename H5 into H_typed_omega_omega.
+    inversion H_typed_omega_omega; subst; rename H6 into H_typed_omega.
+    inversion H_typed_omega; subst; rename H6 into H_typed_omega_inner.
+    inversion H_typed_omega_inner; subst.
+    rename H5 into H_typed_x.
+    rename H7 into H_typed_x'.
+    inversion H_typed_x; subst; clear H_typed_x; rename H1 into H_typed_x.
+    inversion H_typed_x'; subst; clear H_typed_x'; rename H1 into H_typed_x'.
+    rewrite lookup_insert in H_typed_x.
+    rewrite lookup_insert in H_typed_x'.
+    injection H_typed_x; intro H_eq1.
+    injection H_typed_x'; intro H_eq2.
+    rewrite H_eq1 in H_eq2.
+    exact (rec_type_contra _ _ H_eq2).
+  Qed.
 
 End give_example.
 
-Section prove_non_existence.
+(* Section prove_non_existence.
   Lemma no_ust :
   ∀ e, (∀ e', rtc step e e' → is_val e' ∨ reducible e') → ∃ A, (∅ ⊢ e : A)%ty.
   Proof.
-    (* TODO: exercise *)
   Admitted.
 
-End prove_non_existence.
\ No newline at end of file
+End prove_non_existence. *)