From ad5f832f96efe4cd05edfeefa2f03b1a6862c218 Mon Sep 17 00:00:00 2001
From: Adrien Burgun <adrien.burgun@orange.fr>
Date: Wed, 6 Dec 2023 15:17:43 +0100
Subject: [PATCH] Giving up on exercises 6

---
 .../type_systems/systemf_mu/exercises06.v     | 376 +++++++++++++++++-
 theories/type_systems/systemf_mu/pure.v       |  60 ++-
 2 files changed, 418 insertions(+), 18 deletions(-)

diff --git a/theories/type_systems/systemf_mu/exercises06.v b/theories/type_systems/systemf_mu/exercises06.v
index a3b27d6..4aa6373 100644
--- a/theories/type_systems/systemf_mu/exercises06.v
+++ b/theories/type_systems/systemf_mu/exercises06.v
@@ -13,6 +13,9 @@ Implicit Types
   (A B : type)
 .
 
+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.
+
 (** ** Exercise 5: Keep Rollin' *)
 (** This exercise is slightly tricky.
   We strongly recommend you to first work on the other exercises.
@@ -56,9 +59,6 @@ Section recursion_combinator.
     tauto.
   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.
-
   (*
 (Rec t) e = (λx. (unroll (rec' t)) (rec' t) x) e
 ~> (unroll (rec' t)) (rec' t) e
@@ -123,7 +123,6 @@ Do not attempt to understand what is going on in the proof, this clearly isn't m
     reflexivity.
   Qed.
 
-  Search (?A ⊆ <[?f := ?x]> ?A).
   Lemma rec_body_typing n Γ (A B: type) t :
     Γ !! x = None →
     Γ !! f = None →
@@ -157,9 +156,30 @@ Do not attempt to understand what is going on in the proof, this clearly isn't m
     TY n; Γ ⊢ (Rec t) : (A → B).
   Proof.
     intros.
-
-    (* TODO: exercise *)
-  Admitted.
+    econstructor.
+    solve_typing.
+    - unfold rec_body.
+      eapply typed_unroll'.
+      eapply (typed_weakening n _ Γ).
+      apply rec_body_typing; try assumption.
+      3: exact H3.
+      all: try eauto.
+      apply insert_subseteq; assumption.
+      asimpl.
+      reflexivity.
+    - asimpl.
+      solve_typing.
+      eapply (typed_weakening n _ Γ).
+      assumption.
+      etrans; [ apply insert_subseteq | apply insert_subseteq ].
+      assumption.
+      rewrite lookup_insert_ne.
+      assumption.
+      symmetry.
+      assumption.
+      reflexivity.
+    - assumption.
+  Qed.
 
 
 End recursion_combinator.
@@ -194,8 +214,57 @@ Lemma fix_red (f x: string) (e e': expr):
   f ≠ x →
   rtc contextual_step ((fix: f x := e) e')%V (sub x e' (sub f (fix: f x := e)%V e)).
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  intros.
+  rewrite Fix_eq.
+
+  unfold Fix.
+
+  eapply rtc_l.
+  apply base_contextual_step.
+
+  eapply BetaS; [ assumption | reflexivity ].
+
+  simpl.
+  repeat rewrite bnamed_eq.
+  repeat (rewrite (decide_False (P := x = f)); last auto).
+  repeat (rewrite (decide_True (P := x = x)); last reflexivity).
+
+  is_val_to_val v H1; subst.
+
+  eapply rtc_l.
+  eapply (Ectx_step _ _ [
+    AppLCtx (RollV (λ: (BNamed f),
+      App (λ: (BNamed f) (BNamed x), e) (λ: (BNamed x),
+        App (App (unroll Var f) (Var f)) (Var x)
+      ))
+    );
+    AppLCtx v
+  ]); [reflexivity | reflexivity | econstructor; eauto].
+
+  eapply rtc_l.
+  eapply (Ectx_step _ _ [
+    AppLCtx v
+  ]); [reflexivity | reflexivity | econstructor; eauto].
+  simpl.
+  repeat rewrite bnamed_eq.
+  repeat (rewrite (decide_False (P := f = x)); last auto).
+  repeat (rewrite (decide_True (P := f = f)); last reflexivity).
+
+  eapply rtc_l.
+  eapply (Ectx_step _ _ [
+    AppLCtx v
+  ]); [reflexivity | reflexivity | econstructor; eauto].
+  simpl.
+  repeat rewrite bnamed_eq.
+  repeat (rewrite (decide_False (P := f = x)); last auto).
+
+  eapply rtc_l.
+  eapply base_contextual_step.
+  econstructor; [eauto | reflexivity].
+  simpl.
+
+  reflexivity.
+Qed.
 
 
 Lemma fix_typing n Γ (f x: string) (A B: type) (e: expr):
@@ -205,7 +274,7 @@ Lemma fix_typing n Γ (f x: string) (A B: type) (e: expr):
   TY n; <[x := A]> (<[f := (A → B)%ty]> Γ) ⊢ e : B →
   TY n; Γ ⊢ (fix: f x := e) : (A → B).
 Proof.
-  (* TODO: exercise *)
+  (* Weee, let's do everything from scratch again! *)
 Admitted.
 
 
@@ -289,22 +358,299 @@ Definition list_t (A : type) : type :=
 
 Definition mylist_impl : val := PackV (
   (#0, (LitV LitUnit)),
-  (λ: "a" "l", (#1 + (Fst "l"), ("a", (Snd "")))),
+  (λ: "a" "l", (#1 + (Fst "l"), ("a", (Snd "l")))),
   (Λ, λ: "l" "zero" "cb",
     (* (fix "rec" "l" := *)
       if: (Fst "l") = #0 then
         "zero"
       else
-        "cb" (Fst (Snd "l")) (Snd (Snd "l"))
+        "cb" (Fst (Snd "l")) ((Fst "l") - #1, Snd (Snd "l"))
     (* ) "l1" *)
   )
 ).
 
+Inductive list_sem_type {A : type} : nat → val → Prop :=
+| empty k : list_sem_type k (PairV (LitV (LitInt 0)) (LitV LitUnit))
+| push k (n : nat) rest head :
+  is_closed [] (of_val head)
+  → list_sem_type k (PairV (LitV (LitInt n)) rest)
+  → 𝒱 A δ_any k head
+  → list_sem_type k (PairV (LitV (LitInt (1 + n))) (PairV head rest)).
 
-
+(* I'm not gonna reiterate my beliefs on what constitute bad pedagogy. *)
 Lemma mylist_impl_sem_typed A :
   type_wf 0 A →
   ∀ k, 𝒱 (list_t A) δ_any k mylist_impl.
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  intros A_wf k.
+  unfold list_t.
+  simp type_interp.
+  eexists; split; [ reflexivity | ].
+
+  pose_sem_type (list_sem_type (A := A)) as τ.
+  {
+    intros l v sem.
+    induction sem.
+    eauto.
+    simpl.
+    simpl in IHsem.
+    apply andb_True; split; assumption.
+  }
+  {
+    intros l l' v sem l'_le_l.
+    induction sem.
+    econstructor.
+    econstructor.
+    assumption.
+    exact (IHsem l'_le_l).
+    eapply val_rel_mono.
+    2: exact H0.
+    assumption.
+  }
+  exists τ.
+  simp type_interp; eexists; eexists; split; last split; first reflexivity.
+  simp type_interp; eexists; eexists; split; last split; first reflexivity.
+
+  - simp type_interp; simpl.
+    constructor.
+  - simp type_interp; eexists; eexists; split; last split; [reflexivity | eauto | ].
+    intros arg₁ j j_le_k Hsem₁.
+    simpl.
+    eapply sem_val_expr_rel'; eauto.
+
+    simp type_interp; eexists; eexists; split; last split; [reflexivity | simpl; apply andb_True; split; eauto | ].
+    apply is_closed_weaken_nil.
+    apply val_rel_is_closed in Hsem₁.
+    assumption.
+
+    intros arg₂ i i_le_k Hsem₂.
+    simpl.
+    rewrite subst_is_closed_nil.
+    2: apply val_rel_is_closed in Hsem₁; assumption.
+
+    simp type_interp in Hsem₂; simpl in Hsem₂.
+    induction Hsem₂.
+    + eapply expr_det_step_closure.
+      apply det_step_pair_r.
+      apply det_step_pair_r.
+      apply det_step_snd; eauto.
+
+      eapply expr_det_step_closure.
+      apply det_step_pair_l; eauto.
+      apply det_step_binop_r.
+      apply det_step_fst; eauto.
+
+      eapply expr_det_step_closure.
+      apply det_step_pair_l; eauto.
+
+      eapply sem_val_expr_rel'; eauto.
+      simpl.
+      simplify_val.
+      eauto.
+
+      simp type_interp; simpl.
+      have h₁ : 0%Z = Z.of_nat 0.
+      reflexivity.
+      rewrite h₁.
+      econstructor.
+      apply val_rel_is_closed in Hsem₁; assumption.
+      econstructor.
+      rewrite <-sem_val_rel_cons in Hsem₁.
+      eapply val_rel_mono.
+      2: exact Hsem₁.
+      lia.
+    + eapply expr_det_step_closure.
+      apply det_step_pair_r.
+      apply det_step_pair_r.
+      apply det_step_snd; eauto.
+      fold of_val.
+
+      eapply expr_det_step_closure.
+      apply det_step_pair_l; eauto.
+      apply det_step_binop_r.
+      apply det_step_fst; eauto.
+
+      eapply expr_det_step_closure.
+      apply det_step_pair_l; eauto.
+
+      eapply sem_val_expr_rel'; eauto.
+      simpl.
+      simplify_val.
+      eauto.
+
+      simp type_interp; simpl.
+      have h₂ : (1 + Z.of_nat n)%Z = Z.of_nat (1 + n).
+      lia.
+      rewrite h₂.
+      econstructor.
+      apply val_rel_is_closed in Hsem₁; assumption.
+      rewrite <-h₂.
+      econstructor.
+      apply val_rel_is_closed in Hsem₁; assumption.
+      eapply __p2.
+      exact Hsem₂.
+      lia.
+
+      (* Little annoying buggers: *)
+      eapply val_rel_mono.
+      2: exact H0.
+      lia.
+      rewrite <-sem_val_rel_cons in Hsem₁.
+      eapply val_rel_mono.
+      2: exact Hsem₁.
+      lia.
+  - simp type_interp.
+    eexists; split; last split; [ reflexivity | eauto | ].
+    intro τ₂.
+    eapply sem_val_expr_rel'; eauto.
+
+    simp type_interp; eexists; eexists; split; last split; [reflexivity | eauto | ].
+    intros arg₁ j j_le_k Hsem₁.
+    have Hcl₁ := (val_rel_is_closed _ _ _ _ Hsem₁).
+    simpl.
+
+    eapply sem_val_expr_rel'; eauto.
+    simp type_interp; eexists; eexists; split; last split; [reflexivity | eauto | ].
+    simpl.
+    repeat (apply andb_True; split); eauto; apply is_closed_weaken_nil; assumption.
+
+    intros arg₂ i i_le_j Hsem₂.
+    simpl.
+    have Hcl₂ := (val_rel_is_closed _ _ _ _ Hsem₂).
+
+    eapply sem_val_expr_rel'; eauto.
+    simp type_interp; eexists; eexists; split; last split; [reflexivity | eauto | ].
+    (* Big closedness detour *)
+    simpl.
+    repeat (apply andb_True; split); eauto; apply is_closed_weaken_nil;
+    try assumption;
+    rewrite subst_is_closed_nil; assumption.
+
+    intros arg₃ l l_le_i Hsem₃.
+    simpl.
+    have Hcl₃ := (val_rel_is_closed _ _ _ _ Hsem₃).
+    rewrite subst_is_closed_nil.
+    2: rewrite subst_is_closed_nil; assumption.
+    rewrite subst_is_closed_nil.
+    2: assumption.
+
+    simp type_interp in Hsem₁; simpl in Hsem₁.
+    destruct Hsem₁.
+    + eapply expr_det_step_closure.
+      apply det_step_if.
+      apply det_step_binop_l; eauto.
+      apply det_step_fst; eauto.
+
+      eapply expr_det_step_closure.
+      apply det_step_if.
+      eauto.
+
+      simpl.
+
+      eapply expr_det_step_closure.
+      apply det_step_if_true.
+
+      rewrite subst_is_closed_nil.
+      2: assumption.
+
+      eapply sem_val_expr_rel'; eauto.
+      rewrite to_of_val; reflexivity.
+      simp type_interp; simpl.
+      eapply sem_type_mono.
+      simp type_interp in Hsem₂; simpl in Hsem₂.
+      lia.
+    + eapply expr_det_step_closure.
+      apply det_step_if.
+      apply det_step_binop_l; eauto.
+      apply det_step_fst; eauto.
+
+      eapply expr_det_step_closure.
+      apply det_step_if.
+      eauto.
+
+      simpl.
+      have h₂ : bool_decide ((1 + n)%Z = 0%Z) = false.
+      apply bool_decide_false.
+      lia.
+      rewrite h₂.
+
+      eapply expr_det_step_closure.
+      apply det_step_if_false.
+
+      eapply expr_det_step_closure.
+      apply det_step_app_r.
+      apply det_step_pair_r.
+      apply det_step_snd_lift.
+      apply det_step_snd; eauto.
+
+      eapply expr_det_step_closure.
+      apply det_step_app_r.
+      apply det_step_pair_r.
+      apply det_step_snd; eauto.
+
+      eapply expr_det_step_closure.
+      apply det_step_app_r.
+      apply det_step_pair_l; eauto.
+
+      eapply expr_det_step_closure.
+      apply det_step_app_r.
+      apply det_step_pair_l; eauto.
+
+      have h₀ : (1 + Z.of_nat n - 1)%Z = Z.of_nat n.
+      lia.
+      rewrite h₀.
+
+      eapply expr_det_step_closure.
+      apply det_step_app_l; eauto.
+      apply det_step_app_r.
+      apply det_step_fst_lift.
+      apply det_step_snd; eauto.
+
+      eapply expr_det_step_closure.
+      apply det_step_app_l; eauto.
+
+      simp type_interp in Hsem₃.
+      destruct Hsem₃ as (x & e & -> & Hcl₄ & Hsem₃).
+
+      eapply expr_det_step_closure.
+      apply det_step_app_l; eauto.
+      apply det_step_beta; eauto.
+
+      have h₃ : 𝒱 A.[ren (+2)] (τ₂ .: τ .: δ_any) l head.
+      {
+        have h₄ : A.[ren (+2)] = A.[ren (+1)].[ren (+1)].
+        asimpl; reflexivity.
+        rewrite h₄.
+        rewrite <-sem_val_rel_cons.
+        rewrite <-sem_val_rel_cons.
+        eapply val_rel_mono.
+        2: exact H0.
+        lia.
+      }
+      have h₄ : l ≤ l.
+      lia.
+      specialize (Hsem₃ _ _ h₄ h₃).
+
+      eapply (bind [AppLCtx (LitV (Z.of_nat n), rest)]).
+      eapply expr_rel_mono.
+      2: exact Hsem₃.
+      lia.
+
+      intros j v j_le_funny Hsem₄.
+      simpl.
+      simp type_interp in Hsem₄.
+      destruct Hsem₄ as (x' & e' & -> & Hcl₅ & Hsem₅).
+
+      eapply expr_det_step_closure.
+      apply det_step_beta; eauto.
+      have h₆ : (#(LitInt (Z.of_nat n)), of_val rest)%E = of_val (PairV (LitV n) rest).
+      reflexivity.
+      rewrite h₆.
+      apply Hsem₅.
+      lia.
+
+      simp type_interp; simpl.
+      eapply __p2.
+      exact Hsem₁.
+      lia.
+Qed.
diff --git a/theories/type_systems/systemf_mu/pure.v b/theories/type_systems/systemf_mu/pure.v
index d7c942a..e773d39 100644
--- a/theories/type_systems/systemf_mu/pure.v
+++ b/theories/type_systems/systemf_mu/pure.v
@@ -3,12 +3,56 @@ From iris Require Import prelude.
 From semantics.lib Require Import maps.
 From semantics.ts.systemf_mu Require Import lang notation.
 
+Print base_reducible_contextual_step_ectx.
+
+
+
+Lemma contextual_ectx_step_case' {a e e'} :
+  contextual_step (fill_item a e) e' →
+  (∃ e'', e' = fill_item a e'' ∧ contextual_step e e'') ∨ is_val e.
+Proof.
+  intro H.
+
+  admit.
+Admitted.
+
 Lemma contextual_ectx_step_case K e e' :
   contextual_step (fill K e) e' →
   (∃ e'', e' = fill K e'' ∧ contextual_step e e'') ∨ is_val e.
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  revert e e'.
+  induction K.
+  - intros e e' H.
+    simpl.
+    left. eexists. split; [reflexivity | exact H].
+  - intros e e' H.
+    simpl in H.
+    specialize (IHK _ _ H).
+    induction IHK.
+    + destruct H0 as (e'' & -> & Hctx).
+      induction (contextual_ectx_step_case' Hctx).
+      destruct H0 as (e''' & -> & Hctx').
+      left.
+      eexists.
+      split.
+      reflexivity.
+      exact Hctx'.
+      right.
+      exact H0.
+    + induction a; simpl in H0; try (exfalso; exact H0); right; tauto.
+  (* Restart.
+  revert e e'.
+  induction K using rev_ind.
+  - intros e e' H.
+    simpl.
+    left. eexists. split; [reflexivity | exact H].
+  - intros e e' H.
+    have h₁ : K ++ [x] = comp_ectx [x] K.
+    reflexivity.
+    rewrite h₁.
+    rewrite h₁ in H. *)
+
+Qed.
 
 
 (** ** Deterministic reduction *)
@@ -162,7 +206,17 @@ Lemma red_nsteps_fill K k e e' :
     red_nsteps j e e'' ∧
     red_nsteps (k - j) (fill K e'') e'.
 Proof.
-  (* TODO: exercise *)
+  (* revert e e'.
+  induction K.
+  {
+    admit.
+    (* trivial *)
+  }
+  intros e e' H.
+  induction a.
+  specialize (IHK (fill [a] e)).
+
+  TODO: exercise *)
 Admitted.