✨ Start exercises 6

theories/type_systems/systemf_mu/exercises06.v

@@ -19,18 +19,20 @@ Implicit Types
   You may use the results from this exercise, in particular the fixpoint combinator and its typing, in other exercises, however (which is why it comes first in this Coq file).
  *)
 Section recursion_combinator.
-  Variable (f x: string). (* the template of the recursive function *)
+  Variable (f F x: string). (* the template of the recursive function *)
   Hypothesis (Hfx: f ≠ x).
+  Hypothesis (HFx: F ≠ x).
+  Hypothesis (HfF: f ≠ F).
 
   (** Recursion Combinator *)
   (* First, setup a definition [Rec] satisfying the reduction lemmas below. *)
 
   (** You may find an auxiliary definition [rec_body] helpful *)
-  Definition rec_body (t: expr) : expr :=
-    roll (λ: f x, #0). (* TODO *)
+  Definition rec_body (t : expr): expr :=
+    roll (λ: f, t (λ: x, (unroll f) f x)).
 
   Definition Rec (t: expr): val :=
-    λ: x, rec_body t. (* TODO *)
+    λ: x, (unroll (rec_body t)) (rec_body t) x.
 
   Lemma closed_rec_body t :
     is_closed [] t → is_closed [] (rec_body t).
@@ -42,19 +44,86 @@ Section recursion_combinator.
     is_val (Rec t).
   Proof. done. Qed.
 
-  
-
-   Lemma Rec_red (t e: expr):
+  Lemma bnamed_eq {A : Type} {a b : string} {g h : A} :
+    (if decide (BNamed a = BNamed b) then g else h) = if decide (a = b) then g else h.
+  Proof.
+    induction (decide (a = b)) as [H | H].
+    rewrite H.
+    rewrite decide_True; reflexivity.
+    rewrite decide_False; first reflexivity.
+    intro H2.
+    injection H2.
+    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
+~> (λ f, t (λ x, (unroll f) f x)) (rec' t) e
+~> (t (λ x, (unroll (rec' t)) (rec' t) x)) e
+= (t (Rec t) e)
+
+Do not attempt to understand what is going on in the proof, this clearly isn't meant to be solved by humans.
+  *)
+  Lemma Rec_red (t e: expr):
     is_val e →
     is_val t →
     is_closed [] e →
     is_closed [] t →
     rtc contextual_step ((Rec t) e) (t (Rec t) e).
   Proof.
-    (* TODO: exercise *)
-  Admitted.
-
-
+    have Hxf : x ≠ f.
+    symmetry; assumption.
+    intros.
+
+    eapply rtc_l.
+    eapply base_contextual_step.
+    econstructor; [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).
+    rewrite subst_is_closed_nil; last assumption.
+
+    is_val_to_val v H; subst.
+
+    eapply rtc_l.
+    eapply (Ectx_step _ _ [
+      AppLCtx (RollV (λ: (BNamed f),
+        App t (λ: (BNamed x),
+          App (App (unroll Var f) (Var f)) (Var x)
+        ))
+      );
+      AppLCtx v
+    ]).
+    reflexivity.
+    reflexivity.
+    econstructor.
+    eauto.
+    simpl.
+
+    eapply rtc_l.
+    eapply (Ectx_step _ _ [
+      AppLCtx v
+    ]).
+    reflexivity.
+    reflexivity.
+    econstructor.
+    eauto.
+    reflexivity.
+
+    simpl.
+    repeat rewrite bnamed_eq.
+    repeat (rewrite (decide_False (P := f = x)); last auto).
+    repeat (rewrite (decide_True (P := f = f)); last reflexivity).
+    rewrite subst_is_closed_nil; last assumption.
+    reflexivity.
+  Qed.
+
+  Search (?A ⊆ <[?f := ?x]> ?A).
   Lemma rec_body_typing n Γ (A B: type) t :
     Γ !! x = None →
     Γ !! f = None →
@@ -63,8 +132,20 @@ Section recursion_combinator.
     TY n; Γ ⊢ t : ((A → B) → (A → B)) →
     TY n; Γ ⊢ rec_body t : (μ: #0 → rename (+1) A → rename (+1) B).
   Proof.
-    (* TODO: exercise *)
-  Admitted.
+    intros x_notin_Γ f_notin_Γ A_wf B_wf Hty_t.
+    unfold rec_body.
+    solve_typing.
+    simpl.
+    asimpl.
+    eapply typed_weakening; [exact Hty_t | simplify_list_subseteq | reflexivity ].
+
+    (* Love the consistency in the naming here: *)
+    apply insert_subseteq; assumption.
+    asimpl; apply lookup_insert.
+
+    apply type_wf_rename; [ assumption | intros; simpl; lia ].
+    apply type_wf_rename; [ assumption | intros; simpl; lia ].
+  Qed.
 
 
   Lemma Rec_typing n Γ A B t:
@@ -75,6 +156,8 @@ Section recursion_combinator.
     TY n; Γ ⊢ t : ((A → B) → (A → B)) →
     TY n; Γ ⊢ (Rec t) : (A → B).
   Proof.
+    intros.
+
     (* TODO: exercise *)
   Admitted.
 
@@ -128,24 +211,34 @@ Admitted.
 
 (** ** Exercise 1: Encode arithmetic expressions *)
 
-Definition aexpr : type := #0 (* TODO *).
+(*
+  int, addition, multiplication:
+  (int + (aexpr × aexpr) + (aexpr × aexpr))
+
+  (int + ((μα. α × α) + (μα. α × α)))
+*)
+Definition aexpr : type := (μ:
+  (Int + (
+    (#0 × #0)
+    + (#0 × #0)
+  )))
+.
 
-Definition num_val (v : val) : val := #0 (* TODO *).
-Definition num_expr (e : expr) : expr := #0 (* TODO *).
+Definition num_val (v : val) : val := RollV (InjLV v).
+Definition num_expr (e : expr) : expr := Roll (InjL e).
 
-Definition plus_val (v1 v2 : val) : val := #0 (* TODO *).
-Definition plus_expr (e1 e2 : expr) : expr := #0 (* TODO *).
+Definition plus_val (v1 v2 : val) : val := RollV (InjRV (InjLV (PairV v1 v2))).
+Definition plus_expr (e1 e2 : expr) : expr := Roll (InjR (InjL (Pair e1 e2))).
 
-Definition mul_val (v1 v2 : val) : val := #0 (* TODO *).
-Definition mul_expr (e1 e2 : expr) : expr := #0 (* TODO *).
+Definition mul_val (v1 v2 : val) : val := RollV (InjRV (InjRV (PairV v1 v2))).
+Definition mul_expr (e1 e2 : expr) : expr := Roll (InjR (InjR (Pair e1 e2))).
 
 Lemma num_expr_typed n Γ e :
   TY n; Γ ⊢ e : Int →
   TY n; Γ ⊢ num_expr e : aexpr.
 Proof.
   intros. solve_typing.
-  (* TODO: exercise *)
-Admitted.
+Qed.
 
 
 Lemma plus_expr_typed n Γ e1 e2 :
@@ -153,9 +246,8 @@ Lemma plus_expr_typed n Γ e1 e2 :
   TY n; Γ ⊢ e2 : aexpr →
   TY n; Γ ⊢ plus_expr e1 e2 : aexpr.
 Proof.
-  (*intros; solve_typing.*)
-  (* TODO: exercise *)
-Admitted.
+  intros; solve_typing.
+Qed.
 
 
 Lemma mul_expr_typed n Γ e1 e2 :
@@ -163,19 +255,27 @@ Lemma mul_expr_typed n Γ e1 e2 :
   TY n; Γ ⊢ e2 : aexpr →
   TY n; Γ ⊢ mul_expr e1 e2 : aexpr.
 Proof.
-  (*intros; solve_typing.*)
-  (* TODO: exercise *)
-Admitted.
+  intros; solve_typing.
+Qed.
 
 
-Definition eval_aexpr : val :=
-  #0. (* TODO *)
+Definition eval_aexpr : val := (fix: "eval" "x" := (
+  match: (Unroll "x") with
+  InjL "int" => "int"
+  | InjR "bin" => (match: "bin" with
+    InjL "add" => "eval" (Fst "add") + "eval" (Snd "add")
+    | InjR "mul" => "eval" (Fst "mul") * "eval" (Snd "mul")
+    end
+  )
+  end
+)).
 
 Lemma eval_aexpr_typed Γ n :
   TY n; Γ ⊢ eval_aexpr : (aexpr → Int).
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  apply fix_typing; [solve_typing | solve_typing | auto | ].
+  solve_typing.
+Qed.
 
 
 
@@ -187,9 +287,18 @@ Definition list_t (A : type) : type :=
     × (∀: #1 → #0 → (A.[ren (+2)] → #1 → #0) → #0)) (* mylistcase *)
   .
 
-Definition mylist_impl : val :=
-  #0 (* TODO *)
-  .
+Definition mylist_impl : val := PackV (
+  (#0, (LitV LitUnit)),
+  (λ: "a" "l", (#1 + (Fst "l"), ("a", (Snd "")))),
+  (Λ, λ: "l" "zero" "cb",
+    (* (fix "rec" "l" := *)
+      if: (Fst "l") = #0 then
+        "zero"
+      else
+        "cb" (Fst (Snd "l")) (Snd (Snd "l"))
+    (* ) "l1" *)
+  )
+).
 
 
 
@@ -199,4 +308,3 @@ Lemma mylist_impl_sem_typed A :
 Proof.
   (* TODO: exercise *)
 Admitted.
-

theories/type_systems/systemf_mu/logrel.v

@@ -572,7 +572,7 @@ Qed.
 
 Lemma compat_int Δ Γ z : TY Δ; Γ ⊨ (Lit $ LitInt z) : Int.
 Proof.
-  split; first done. 
+  split; first done.
   intros θ δ k _.
   eapply (sem_val_expr_rel _ _ _ #z).
   simp type_interp. eauto.
@@ -580,14 +580,14 @@ Qed.
 
 Lemma compat_bool Δ Γ b : TY Δ; Γ ⊨ (Lit $ LitBool b) : Bool.
 Proof.
-  split; first done. 
+  split; first done.
   intros θ δ k _.
   eapply (sem_val_expr_rel _ _ _ #b). simp type_interp. eauto.
 Qed.
 
 Lemma compat_unit Δ Γ : TY Δ; Γ ⊨ (Lit $ LitUnit) : Unit.
 Proof.
-  split; first done. 
+  split; first done.
   intros θ δ k _.
   eapply (sem_val_expr_rel _ _ _ #LitUnit). simp type_interp. eauto.
 Qed.
@@ -983,20 +983,72 @@ Proof.
   eapply sem_val_expr_rel. eapply val_rel_mono; last done. lia.
 Qed.
 
+(*
+
+*)
 Lemma compat_injl Δ Γ e A B :
   TY Δ; Γ ⊨ e : A →
   TY Δ; Γ ⊨ InjL e : A + B.
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  intro Hty.
+  destruct Hty as (Hcl₁ & Hty).
+  econstructor.
+  simpl; assumption.
+
+  intros θ δ k Hctx.
+  specialize (Hty θ δ k Hctx).
+
+  simpl.
+  eapply (bind [InjLCtx]).
+  exact Hty.
 
+  intros j v j_le_k Hv.
+  simpl.
+
+  have h₁ : of_val (InjLV v) = InjL (of_val v).
+  {
+    reflexivity.
+  }
+  rewrite <-h₁.
+  eapply sem_val_expr_rel.
+
+  simp type_interp.
+  left.
+  eexists; split; first reflexivity.
+  exact Hv.
+Qed.
 
 Lemma compat_injr Δ Γ e A B :
   TY Δ; Γ ⊨ e : B →
   TY Δ; Γ ⊨ InjR e : A + B.
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  intro Hty.
+  destruct Hty as (Hcl₁ & Hty).
+  econstructor.
+  simpl; assumption.
+
+  intros θ δ k Hctx.
+  specialize (Hty θ δ k Hctx).
+
+  simpl.
+  eapply (bind [InjRCtx]).
+  exact Hty.
+
+  intros j v j_le_k Hv.
+  simpl.
+
+  have h₁ : of_val (InjRV v) = InjR (of_val v).
+  {
+    reflexivity.
+  }
+  rewrite <-h₁.
+  eapply sem_val_expr_rel.
+
+  simp type_interp.
+  right.
+  eexists; split; first reflexivity.
+  exact Hv.
+Qed.
 
 
 Lemma compat_case Δ Γ e e1 e2 A B C :
@@ -1005,8 +1057,71 @@ Lemma compat_case Δ Γ e e1 e2 A B C :
   TY Δ; Γ ⊨ e2 : (C → A) →
   TY Δ; Γ ⊨ Case e e1 e2 : A.
 Proof.
-  (* TODO: exercise *)
-Admitted.
+  intros Hty₁ Hty₂ Hty₃.
+  destruct Hty₁ as (Hcl₁ & Hty₁).
+  remember Hty₂ as Hty₂'; clear HeqHty₂'.
+  destruct Hty₂ as (Hcl₂ & Hty₂).
+  destruct Hty₃ as (Hcl₃ & Hty₃).
+  econstructor.
+  simpl.
+  apply andb_True; split; [ apply andb_True; split | ]; assumption.
+
+  intros θ δ k Hctx.
+  specialize (Hty₁ _ _ _ Hctx).
+  simpl.
+
+  eapply (bind [CaseCtx _ _]).
+  exact Hty₁.
+  simpl.
+  intros j v₁ j_le_k Hty₁'.
+
+  have Hctx' : 𝒢 δ (j-1) Γ θ.
+  eapply sem_context_rel_mono; last exact Hctx; lia.
+
+  simp type_interp in Hty₁'.
+  induction Hty₁' as [(v₁' & -> & Hty₁') | (v₁' & -> & Hty₁')].
+
+  - eapply expr_det_step_closure.
+    {
+      eapply det_step_casel.
+      eauto.
+    }
+    fold of_val.
+
+    specialize (Hty₂ θ δ _ Hctx').
+    eapply (bind [AppLCtx _]); first exact Hty₂.
+    intros i v i_lt_j Hty₄.
+    simpl.
+
+    simp type_interp in Hty₄; destruct Hty₄ as (x & e₄ & -> & Hcl₄ & Hty₄).
+    eapply expr_det_step_closure.
+    {
+      eapply det_step_beta; apply is_val_of_val.
+    }
+    apply Hty₄.
+    lia.
+    eapply val_rel_mono; last exact Hty₁'; lia.
+  - eapply expr_det_step_closure.
+    {
+      eapply det_step_caser.
+      eauto.
+    }
+    fold of_val.
+
+    specialize (Hty₃ θ δ _ Hctx').
+    eapply (bind [AppLCtx _]); first exact Hty₃.
+    intros i v i_lt_j Hty₄.
+    simpl.
+
+    simp type_interp in Hty₄; destruct Hty₄ as (x & e₄ & -> & Hcl₄ & Hty₄).
+    eapply expr_det_step_closure.
+    {
+      eapply det_step_beta; apply is_val_of_val.
+    }
+    apply Hty₄.
+    lia.
+    eapply val_rel_mono; last exact Hty₁'; lia.
+Qed.
 
 
 Lemma compat_roll n Γ e A :