Merge remote-tracking branch 'origin/amethyst' into amethyst

theories/type_systems/stlc/cbn_logrel.v

@@ -143,12 +143,13 @@ Proof.
   - intros y e'. rewrite lookup_insert_Some.
     intros [[-> <-]|[Hne Hlook]].
     + by eapply expr_rel_closed.
-    + eapply IHsem_context_rel; last done.
+    + eapply IHsem_context_rel.
+      exact Hlook.
 Qed.
 
 
 (* This is essentially an inversion lemma for 𝒢 *)
-Lemma sem_context_rel_exprs Γ θ x A :
+Lemma sem_context_rel_exprs {Γ θ x A} :
   sem_context_rel Γ θ →
   Γ !! x = Some A →
   ∃ e, θ !! x = Some e ∧ ℰ A e.
@@ -170,15 +171,249 @@ Proof.
   - rewrite !dom_insert. congruence.
 Qed.
 
+Ltac specialize_all' θ H_ctx := repeat (
+  match goal with
+  | [ H: ∀ θ, ∀ (_: sem_context_rel ?G θ), ?e |- ?goal ] =>
+    specialize (H θ H_ctx)
+  | [ H: ?G ⊨ ?e : ?T |- ?goal ] =>
+    destruct H as [? H];
+    specialize (H θ H_ctx)
+  end
+).
+
+Ltac specialize_all_closed := repeat (
+  match goal with
+  | [ H: ?G ⊨ ?e : ?T |- ?goal ] =>
+    destruct H as [H _]
+  end
+).
+
+Ltac specialize_all θ H_ctx :=
+  match goal with
+  | [ |- ∀ θ, ∀ (_: sem_context_rel ?G θ), ?e ] => intros θ H_ctx; specialize_all' θ H_ctx
+  | [ |- ?G ⊨ ?e : ?T ] => econstructor; first (specialize_all_closed); last (intros θ H_ctx; specialize_all' θ H_ctx)
+  end.
+
+Ltac break_expr_rel H val Hcl Hval :=
+  simp type_interp in H;
+  destruct H as (val & H & Hcl & Hval).
+
+Ltac split3 := split; last split.
+
+(* Search (?A !! ?B = Some ?C) (?B ∈ ?D). *)
+(* Search (?x ∈ elements ?y). *)
+
+Lemma compat_var Γ x A:
+  Γ !! x = Some A →
+  Γ ⊨ (Var x): A.
+Proof.
+  intro H_some.
+  split.
+  - simpl.
+    apply bool_decide_pack.
+    rewrite elem_of_elements.
+    exact (elem_of_dom_2 Γ x A H_some).
+  - specialize_all θ H_ctx.
+    destruct (sem_context_rel_exprs H_ctx H_some) as (e & Hθ_some & He).
+    simpl.
+    rewrite Hθ_some.
+    exact He.
+Qed.
 
+Search (elem_of ?x (cons ?x ?y)).
+
+(* Compatibility for [lam] unfortunately needs a very technical helper lemma. *)
+Lemma lam_closed Γ θ (x : string) A e :
+  closed (elements (dom (<[x:=A]> Γ))) e →
+  𝒢 Γ θ →
+  closed [] (Lam x (subst_map (delete x θ) e)).
+Proof.
+  intros Hcl Hctxt.
+  eapply subst_map_closed'_2.
+  - eapply closed_weaken; first done.
+    rewrite dom_delete dom_insert (sem_context_rel_dom Γ θ) //.
+    (* The [set_solver] tactic is great for solving goals involving set
+    inclusion and union. However, when set difference is involved, it can't
+    always solve the goal -- we need to help it by doing a case distinction on
+    whether the element we are considering is [x] or not. *)
+    intros y. destruct (decide (x = y)); set_solver.
+  - eapply subst_closed_weaken, sem_context_rel_closed; last done.
+    + set_solver.
+    + apply map_delete_subseteq.
+Qed.
+
+Lemma lam_closed' {Γ θ x A e}:
+  closed (elements (dom (<[x:=A]> Γ))) e →
+  𝒢 Γ θ →
+  closed [x] (subst_map (delete x θ) e).
+Proof.
+  intros Hcl H_ctx.
+  eapply closed_subst_weaken.
+  eapply subst_closed_weaken; first reflexivity.
+  by apply map_delete_subseteq.
+  exact (sem_context_rel_closed _ _ H_ctx).
+  2: exact Hcl.
+
+  rewrite dom_insert.
+  intros y Hy_in Hy_notin.
+
+  rewrite (sem_context_rel_dom _ _ H_ctx) in Hy_in.
+  rewrite dom_delete in Hy_notin.
+  rewrite not_elem_of_difference in Hy_notin.
+  rewrite elem_of_elements in Hy_in.
+  set_solver.
+Qed.
+the internship
+Lemma compat_lam Γ x e A B:
+  (<[x:=A]> Γ ⊢ e : B)%ty →
+  <[x:=A]> Γ ⊨ e : B →
+  Γ ⊨ (λ: (BNamed x), e) : (A → B).
+Proof.
+  intros He_ty IHe.
+
+  specialize_all θ H_ctx.
+  - simpl.
+    rename IHe into IHcl.
+    eapply closed_weaken.
+    exact IHcl.
+
+    rewrite dom_insert.
+
+    induction (decide (x ∈ (dom Γ))) as [Hin | Hnotin]; set_solver.
+  - destruct IHe as [Hcl IHe].
+
+    simp type_interp.
+    eexists.
+    simpl; split3.
+    {
+      constructor.
+    }
+    {
+      by eapply lam_closed.
+    }
+
+    simp type_interp.
+    exists x.
+    eexists.
+    simpl; split3.
+    {
+      reflexivity.
+    }
+    {
+      by eapply lam_closed'.
+    }
+    intros e_arg He_arg.
+
+    rewrite subst_subst_map.
+    {
+      eapply IHe.
+      econstructor.
+      assumption.
+      assumption.
+    }
+    {
+      exact (sem_context_rel_closed _ _ H_ctx).
+    }
+Qed.
+
+Lemma compat_int Γ z:
+  Γ ⊨ LitInt z : Int.
+Proof.
+  econstructor.
+  1: eauto.
+  simpl; intros; simp type_interp.
+  exists z.
+  split; last split; eauto.
+  simp type_interp.
+  exists z; reflexivity.
+Qed.
+
+Lemma compat_plus Γ e1 e2:
+  Γ ⊨ e1 : Int →
+  Γ ⊨ e2 : Int →
+  Γ ⊨ (e1 + e2) : Int.
+Proof.
+  intros H1 H2.
+  destruct H1 as [Hcl1 He1].
+  destruct H2 as [Hcl2 He2].
+  econstructor.
+  1: naive_solver.
+  specialize_all θ H_ctx.
+  break_expr_rel He1 v1 Hcl1' Hv1.
+  break_expr_rel He2 v2 Hcl2' Hv2.
+  simp type_interp in Hv1; destruct Hv1 as [z1 ->].
+  simp type_interp in Hv2; destruct Hv2 as [z2 ->].
+
+  simpl.
+  simp type_interp.
+  exists (z1 + z2)%Z.
+  split3.
+  - econstructor; assumption.
+  - naive_solver.
+  - simp type_interp.
+    eauto.
+Qed.
+
+Lemma compat_app Γ e1 e2 A B:
+  Γ ⊨ e1 : (A → B) →
+  Γ ⊨ e2 : A →
+  Γ ⊨ App e1 e2 : B.
+Proof.
+  intros Hsem_fn Hsem_e2.
+
+  specialize_all θ H_ctx.
+  - simpl; rewrite andb_True; split; assumption.
+  - simpl.
+    simp type_interp; simpl; eauto.
+    break_expr_rel Hsem_fn v_fn Hcl_fn Hv_fn.
+    break_expr_rel Hsem_e2 v_e2 Hcl_e2 Hv_e2.
+    simp type_interp in Hv_fn.
+    simpl in Hv_fn; destruct Hv_fn as (x & e_body & -> & Hcl_e & IHe_subst).
+
+    assert (ℰ A (subst_map θ e2)) as Hsem_subst.
+    {
+      simp type_interp.
+      eauto.
+    }
+    specialize (IHe_subst (subst_map θ e2) Hsem_subst).
+    break_expr_rel IHe_subst v_target Hcl_target Hv_target.
+
+    exists v_target; split3.
+    {
+      econstructor.
+      exact v_target.
+      exact Hsem_fn.
+      exact IHe_subst.
+    }
+    apply andb_True; split; eauto.
+    assumption.
+Qed.
+
+Lemma sem_soundness {Γ e A}:
+  (Γ ⊢ e: A)%ty →
+  Γ ⊨ e: A.
+Proof.
+  induction 1.
+  - by apply compat_var.
+  - by apply compat_lam.
+  - by apply compat_int.
+  - by eapply compat_app.
+  - by apply compat_plus.
+Qed.
 
 
 Lemma termination e A :
   (∅ ⊢ e : A)%ty →
   ∃ v, big_step e v.
 Proof.
-  (* You may want to add suitable intermediate lemmas, like we did for the cbv
-     logical relation as seen in the lecture. *)
-  (* TODO: exercise *)
-Admitted.
-
+  intro H_step.
+  remember (sem_soundness H_step) as H_sem.
+  destruct H_sem as [H_closed H_e].
+  clear HeqH_sem.
+  specialize (H_e ∅ sem_context_rel_empty).
+  simp type_interp in H_e.
+  destruct H_e as (target & Hbs_subst & _ & _).
+  exists target.
+  rewrite subst_map_empty in Hbs_subst.
+  assumption.
+Qed.

theories/type_systems/stlc_extended/bigstep.v

@@ -32,7 +32,7 @@ Inductive big_step : expr → val → Prop :=
     big_step (Fst e) v1
   | bs_snd (e : expr) (v1 v2: val):
     big_step e (PairV v1 v2) →
-    big_step (Fst e) v1
+    big_step (Snd e) v2
   (* Inj *)
   | bs_inj_l e v :
     big_step e v →

theories/type_systems/stlc_extended/ctxstep.v

@@ -12,24 +12,20 @@ Inductive base_step : expr → expr → Prop :=
      e2 = (LitInt n2) →
      (n1 + n2)%Z = n3 →
      base_step (Plus e1 e2) (LitInt n3)
-  | FstS e v1 v2:
+  | FstS v1 v2:
     is_val v1 →
     is_val v2 →
-    e = (Pair v1 v2) →
-    base_step (Fst e) v1
-  | SndS e v1 v2:
+    base_step (Fst (Pair v1 v2)) v1
+  | SndS v1 v2:
     is_val v1 →
     is_val v2 →
-    e = (Pair v1 v2) →
-    base_step (Snd e) v2
-  | CaseLS v_inj v e1 e2:
-    is_val v_inj →
-    v_inj = (InjL v) →
-    base_step (Case v_inj e1 e2) (App e1 v)
-  | CaseRS v_inj v e1 e2:
-    is_val v_inj →
-    v_inj = (InjR v) →
-    base_step (Case v_inj e1 e2) (App e2 v)
+    base_step (Snd (Pair v1 v2)) v2
+  | CaseLS v e1 e2:
+    is_val v →
+    base_step (Case (InjL v) e1 e2) (App e1 v)
+  | CaseRS v e1 e2:
+    is_val v →
+    base_step (Case (InjR v) e1 e2) (App e2 v)
 .
 
 #[export] Hint Constructors base_step : core.

theories/type_systems/stlc_extended/logrel.v

@@ -35,11 +35,14 @@ Equations type_interp (ve : val_or_expr) (t : type) : Prop by wf (mut_measure ve
   type_interp (inj_val v) Int =>
     ∃ z : Z, v = #z ;
   type_interp (inj_val v) (A × B) =>
-    (* TODO: add type interpretation *) 
-    False;
+    ∃ v₁ v₂,
+      v = @PairV v₁ v₂
+      ∧ type_interp (inj_val v₁) A
+      ∧ type_interp (inj_val v₂) B
+    ;
   type_interp (inj_val v) (A + B) =>
-    (* TODO: add type interpretation *)
-    False;
+    (∃ v₁, v = @InjLV v₁ ∧ type_interp (inj_val v₁) A)
+    ∨ (∃ v₂, v = @InjRV v₂ ∧ type_interp (inj_val v₂) B);
   type_interp (inj_val v) (A → B) =>
     ∃ x e, v = @LamV x e ∧ closed (x :b: nil) e ∧
       ∀ v',
@@ -58,12 +61,11 @@ Next Obligation.
 Qed.
 (* Uncomment the following once you have amended the type interpretation to
    solve the new obligations: *)
-(*
+
 Next Obligation. repeat simp mut_measure; simp type_size; lia. Qed.
 Next Obligation. repeat simp mut_measure; simp type_size; lia. Qed.
 Next Obligation. repeat simp mut_measure; simp type_size; lia. Qed.
 Next Obligation. repeat simp mut_measure; simp type_size; lia. Qed.
-*)
 
 
 Notation sem_val_rel t v := (type_interp (inj_val v) t).
@@ -115,8 +117,18 @@ Proof.
   induction A in v |-*; simp type_interp.
   - intros [z ->]. done.
   - intros (x & e & -> & Hcl & _). done.
-  (* TODO: exercise *)
-Admitted.
+  - intros (v1 & v2 & -> & Hv1 & Hv2).
+    unfold closed.
+    simpl.
+    apply andb_True.
+    split.
+    by apply (IHA1 _ Hv1).
+    by apply (IHA2 _ Hv2).
+  - intro H.
+    case H; intros (v' & -> & Hv').
+    + exact (IHA1 _ Hv').
+    + exact (IHA2 _ Hv').
+Qed.
 
 Lemma sem_context_rel_closed Γ θ:
   𝒢 Γ θ → subst_closed [] θ.
@@ -202,8 +214,8 @@ Qed.
 
 (* Compatibility for [lam] unfortunately needs a very technical helper lemma. *)
 Lemma lam_closed Γ θ (x : string) A e :
-  closed (elements (dom (<[x:=A]> Γ))) e → 
-  𝒢 Γ θ → 
+  closed (elements (dom (<[x:=A]> Γ))) e →
+  𝒢 Γ θ →
   closed [] (Lam x (subst_map (delete x θ) e)).
 Proof.
   intros Hcl Hctxt.
@@ -234,6 +246,7 @@ Proof.
   apply Hbody.
   apply sem_context_rel_insert; done.
 Qed.
+
 Lemma compat_lam_anon Γ e A B :
   Γ ⊨ e : B →
   Γ ⊨ (Lam BAnon e) : (A → B).
@@ -274,8 +287,119 @@ Proof.
 
 Qed.
 
+Lemma compat_pair Γ e_lhs e_rhs A B:
+  Γ ⊨ e_lhs: A →
+  Γ ⊨ e_rhs: B →
+  Γ ⊨ (e_lhs, e_rhs): A × B.
+Proof.
+  intros [Hcl_lhs He_lhs].
+  intros [Hcl_rhs He_rhs].
+  split.
+  (* The closedness can be handled by naive_solver *)
+  {
+    unfold closed.
+    naive_solver.
+  }
+
+  (* Use the same θ and H_ctx everywhere: *)
+  intros θ H_ctx.
+  specialize (He_lhs _ H_ctx).
+  specialize (He_rhs _ H_ctx).
+  (* Apply the definition of E[A × B] and E[A], E[B] *)
+  simp type_interp in *.
+  destruct He_lhs as (v_lhs & Hbs_lhs & Hv_lhs).
+  destruct He_rhs as (v_rhs & Hbs_rhs & Hv_rhs).
+
+  (* We now just need to provide a value satisfying our requirements *)
+  exists (PairV v_lhs v_rhs).
+  split.
+  - (* Prove that our expression steps towards the value *)
+    simpl.
+    econstructor.
+    assumption.
+    assumption.
+  - (* Next prove that our value is a correct member of V[A × B] *)
+    simp type_interp. (* Can't just split here :> *)
+    eauto. (* Trivial from then on *)
+Qed.
 
+Lemma compat_fst_snd {Γ e_pair A B}:
+  Γ ⊨ e_pair: A × B →
+  Γ ⊨ (Fst e_pair): A ∧ Γ ⊨ (Snd e_pair): B.
+Proof.
+  intros [Hcl He].
+  split.
+  all: split; first (unfold closed; naive_solver).
+  all: intros θ H_ctx; specialize (He _ H_ctx).
+  all: simp type_interp in *; destruct He as (v & Hbs & Hv).
+  all: simp type_interp in Hv; destruct Hv as (v₁ & v₂ & -> & Hv₁ & Hv₂).
+  1: exists v₁.
+  2: exists v₂.
+  (* Solve the big_step *)
+  all: simpl; split; first (econstructor; eauto).
+  all: assumption.
+Qed.
 
+Lemma compat_inj {Γ e_inj} A B:
+  Γ ⊨ e_inj: A →
+  Γ ⊨ (InjL e_inj): A + B ∧ Γ ⊨ (InjR e_inj): B + A.
+Proof.
+  intros [Hcl He].
+  split.
+  all: split; first (unfold closed; naive_solver).
+  all: intros θ H_ctx; specialize (He _ H_ctx).
+  all: simp type_interp in *; destruct He as (v & Hbs & Hv).
+  1: exists (InjLV v).
+  2: exists (InjRV v).
+
+  all: simpl; split; first (econstructor; eauto).
+  - simp type_interp; left; eauto.
+  - simp type_interp; right; eauto.
+Qed.
+
+Lemma compat_case {Γ e_inj e_lhs e_rhs A B C}:
+  Γ ⊨ e_inj: A + B →
+  Γ ⊨ e_lhs: (A → C) →
+  Γ ⊨ e_rhs: (B → C) →
+  Γ ⊨ (Case e_inj e_lhs e_rhs): C.
+Proof.
+  intros [Hcl_inj He_inj] [Hcl_lhs He_lhs] [Hcl_rhs He_rhs].
+  split; first (unfold closed; naive_solver).
+
+  intros θ H_ctx;
+    specialize (He_inj _ H_ctx);
+    specialize (He_lhs _ H_ctx);
+    specialize (He_rhs _ H_ctx).
+
+  (* All the hypotheses! *)
+  simp type_interp in *;
+    destruct He_inj as (v_inj & Hbs_inj & Hv_inj);
+    destruct He_lhs as (v_lhs & Hbs_lhs & Hv_lhs);
+    destruct He_rhs as (v_rhs & Hbs_rhs & Hv_rhs).
+  simp type_interp in *;
+    destruct Hv_lhs as (x_lhs & fn_lhs & -> & Hcl_lhs2 & IHe_lhs);
+    destruct Hv_rhs as (x_rhs & fn_rhs & -> & Hcl_rhs2 & IHe_rhs).
+
+  case Hv_inj as [[v_lhs [-> Hv_lhs]] | [v_rhs [-> Hv_rhs]]].
+  1: specialize (IHe_lhs _ Hv_lhs);
+    simp type_interp in IHe_lhs;
+    destruct IHe_lhs as (v_res & Hbs_res & Hv_res).
+  2: specialize (IHe_rhs _ Hv_rhs);
+    simp type_interp in IHe_rhs;
+    destruct IHe_rhs as (v_res & Hbs_res & Hv_res).
+
+  all: exists v_res.
+  all: simpl; split; last assumption.
+
+  - eapply bs_case_l.
+    exact Hbs_inj.
+    econstructor; eauto.
+    apply big_step_of_val; reflexivity.
+  - eapply bs_case_r.
+    exact Hbs_inj.
+    econstructor; eauto.
+    apply big_step_of_val; reflexivity.
+Qed.
 
 Lemma sem_soundness Γ e A :
   (Γ ⊢ e : A)%ty →
@@ -288,9 +412,14 @@ Proof.
   - apply compat_int.
   - by eapply compat_app.
   - by apply compat_add.
-  (* add compatibility lemmas for the new rules here. *)
-  (* TODO: exercise *)
-Admitted.
+  - by apply compat_pair.
+  - (* "Cool theorem prover you got" — this comment was made by the Lean gang *)
+    exact (proj1 (compat_fst_snd IHsyn_typed)).
+  - exact (proj2 (compat_fst_snd IHsyn_typed)).
+  - exact (proj1 (compat_inj _ _ IHsyn_typed)).
+  - exact (proj2 (compat_inj _ _ IHsyn_typed)).
+  - by eapply compat_case.
+Qed.
 
 
 Lemma termination e A :
@@ -304,4 +433,3 @@ Proof.
   destruct Hsem as (v & Hbs & _); last eauto.
   constructor.
 Qed.
-

theories/type_systems/stlc_extended/types.v

@@ -47,7 +47,27 @@ Inductive syn_typed : typing_context → expr → type → Prop :=
       Γ ⊢ e1 : Int →
       Γ ⊢ e2 : Int →
       Γ ⊢ e1 + e2 : Int
-  (* TODO: provide the new typing rules *)
+  | typed_pair Γ e_lhs e_rhs A B:
+      Γ ⊢ e_lhs : A →
+      Γ ⊢ e_rhs : B →
+      Γ ⊢ (Pair e_lhs e_rhs) : A × B
+  | typed_fst Γ e_pair A B:
+      Γ ⊢ e_pair: A × B →
+      Γ ⊢ (Fst e_pair): A
+  | typed_snd Γ e_pair A B:
+      Γ ⊢ e_pair: A × B →
+      Γ ⊢ (Snd e_pair): B
+  | typed_injl Γ e_inj A B:
+      Γ ⊢ e_inj : A →
+      Γ ⊢ (InjL e_inj) : A + B
+  | typed_injr Γ e_inj A B:
+      Γ ⊢ e_inj : B →
+      Γ ⊢ (InjR e_inj) : A + B
+  | typed_case Γ e_inj e_lhs e_rhs A B C:
+      Γ ⊢ e_inj: A + B →
+      Γ ⊢ e_lhs: (A → C) →
+      Γ ⊢ e_rhs: (B → C) →
+      Γ ⊢ (Case e_inj e_lhs e_rhs): C
 where "Γ ⊢ e : A" := (syn_typed Γ e%E A%ty).
 #[export] Hint Constructors syn_typed : core.
 
@@ -60,8 +80,7 @@ Lemma syn_typed_closed Γ e A X :
   (∀ x, x ∈ dom Γ → x ∈ X) →
   is_closed X e.
 Proof.
-  (* TODO: you will need to add the new cases, i.e. "|"'s to the intro pattern. The proof then should go through *)
-  induction 1 as [ | ?????? IH | | | | ] in X |-*; simpl; intros Hx; try done.
+  induction 1 as [ | ?????? IH | | | | | | | | | | ] in X |-*; simpl; intros Hx; try done.
   { (* var *) apply bool_decide_pack, Hx. apply elem_of_dom; eauto. }
   { (* lam *) apply IH.
     intros y. rewrite elem_of_dom lookup_insert_is_Some.
@@ -81,8 +100,7 @@ Lemma typed_weakening Γ Δ e A:
   Γ ⊆ Δ →
   Δ ⊢ e : A.
 Proof.
-  (* TODO: here you will need to add the new cases to the intro pattern as well. The proof then should go through *)
-  induction 1 as [| Γ x e A B Htyp IH | | | | ] in Δ |-*; intros Hsub; eauto.
+  induction 1 as [| Γ x e A B Htyp IH | | | | | | | | | | ] in Δ |-*; intros Hsub; eauto.
   - (* var *) econstructor. by eapply lookup_weaken.
   - (* lam *) econstructor. eapply IH; eauto. by eapply insert_mono.
 Qed.
@@ -115,13 +133,54 @@ Proof. inversion 1; subst; eauto. Qed.
   They will be very useful for the proofs below!
 *)
 
+Lemma pair_inversion Γ e_lhs e_rhs C:
+  Γ ⊢ (Pair e_lhs e_rhs) : C →
+  ∃ A B, C = (A × B)%ty ∧ Γ ⊢ e_lhs : A ∧ Γ ⊢ e_rhs : B.
+Proof.
+  inversion 1; subst; eauto.
+Qed.
+
+Lemma fst_inversion Γ e_pair A:
+  Γ ⊢ (Fst e_pair) : A →
+  ∃ B, Γ ⊢ e_pair : A × B.
+Proof.
+  inversion 1; subst; eauto.
+Qed.
+
+Lemma snd_inversion Γ e_pair B:
+  Γ ⊢ (Snd e_pair) : B →
+  ∃ A, Γ ⊢ e_pair : A × B.
+Proof.
+  inversion 1; subst; eauto.
+Qed.
+
+Lemma injl_inversion Γ e_inj C:
+  Γ ⊢ (InjL e_inj): C →
+  ∃ A B, C = (A + B)%ty ∧ Γ ⊢ e_inj: A.
+Proof.
+  inversion 1; subst; eauto.
+Qed.
+
+Lemma injr_inversion Γ e_inj C:
+  Γ ⊢ (InjR e_inj): C →
+  ∃ A B, C = (A + B)%ty ∧ Γ ⊢ e_inj: B.
+Proof.
+  inversion 1; subst; eauto.
+Qed.
+
+Lemma case_inversion Γ e_inj e_lhs e_rhs C:
+  Γ ⊢ (Case e_inj e_lhs e_rhs): C →
+  ∃ A B, Γ ⊢ e_inj: (A+B)%ty ∧ Γ ⊢ e_lhs: (A → C)%ty ∧ Γ ⊢ e_rhs: (B → C)%ty.
+Proof.
+  inversion 1; subst; eauto.
+Qed.
 
 Lemma typed_substitutivity e e' Γ (x: string) A B :
   ∅ ⊢ e' : A →
   (<[x := A]> Γ) ⊢ e : B →
   Γ ⊢ lang.subst x e' e : B.
 Proof.
-  intros He'. revert B Γ; induction e as [y | y | | | | | | |  | | ]; intros B Γ; simpl.
+  intros He'. revert B Γ; induction e as [y | y | | | | | | | | | ]; intros B Γ; simpl.
   - intros Hp % var_inversion.
     destruct (decide (x = y)).
     + subst. rewrite lookup_insert in Hp. injection Hp as ->.
@@ -140,13 +199,23 @@ Proof.
   - intros (C & Hty1 & Hty2) % app_inversion. eauto.
   - inversion 1; subst; auto.
   - intros (-> & Hty1 & Hty2)%plus_inversion; eauto.
-  - (* TODO *) admit.
-  - (* TODO *) admit.
-  - (* TODO *) admit.
-  - (* TODO *) admit.
-  - (* TODO *) admit.
-  - (* TODO *) admit.
-Admitted.
+  - intros Hty%pair_inversion.
+    destruct Hty as (A' & B' & -> & Hty1 & Hty2).
+    eauto.
+  - intros (A' & Hty)%fst_inversion.
+    econstructor.
+    exact (IHe _ _ Hty).
+  - intros (B' & Hty)%snd_inversion; eauto.
+  - intros (A' & B' & -> & Hty)%injl_inversion.
+    econstructor.
+    exact (IHe _ _ Hty).
+  - intros (A' & B' & -> & Hty)%injr_inversion; eauto.
+  - intros (A' & B' & Hty_inj & Hty_lhs & Hty_rhs)%case_inversion.
+    econstructor.
+    apply IHe1; exact Hty_inj.
+    apply IHe2; exact Hty_lhs.
+    apply IHe3; exact Hty_rhs.
+Qed.
 
 (** Canonical values *)
 Lemma canonical_values_arr Γ e A B:
@@ -165,15 +234,37 @@ Proof.
   inversion 1; simpl; naive_solver.
 Qed.
 
-(* TODO: add canonical forms lemmas for the new types *)
+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 canonical_values_prod Γ e A B :
+  Γ ⊢ e : A × B →
+  is_val e →
+  ∃ e1 e2, e = (e1, e2)%E ∧ is_val e1 ∧ is_val e2.
+Proof.
+  inversion 1; simpl; naive_solver.
+Qed.
+
+Lemma canonical_values_sum Γ e A B :
+  Γ ⊢ e : A + B →
+  is_val e →
+  (∃ e', e = InjL e' ∧ is_val e') ∨ (∃ e', e = InjR e' ∧ is_val e').
+Proof.
+  inversion 1; simpl; naive_solver.
+Qed.
 
 (** Progress *)
 Lemma typed_progress e A:
   ∅ ⊢ e : A → is_val e ∨ reducible e.
 Proof.
   remember ∅ as Γ.
-  (* TODO: you will need to extend the intro pattern *)
-  induction 1 as [| | | | Γ e1 e2 A B Hty IH1 _ IH2 | Γ e1 e2 Hty1 IH1 Hty2 IH2].
+  induction 1 as [| | | | Γ e1 e2 A B Hty IH1 _ IH2 | Γ e1 e2 Hty1 IH1 Hty2 IH2 | Γ ? ? ? ? Hty_lhs IH_lhs Hty_rhs IH_rhs |
+    Γ e A B Hty IH |
+    Γ e A B Hty IH |
+    Γ e A B Hty IH |
+    Γ e A B Hty IH |
+    Γ e e1 e2 A B C Htye IHe Htye1 IHe1 Htye2 IHe2
+  ].
   - subst. naive_solver.
   - left. done.
   - left. done.
@@ -194,13 +285,47 @@ Proof.
       subst. eexists; eapply base_contextual_step. eauto.
     + right. destruct H1 as [e1' Hstep]. eexists. eauto.
     + right. destruct H2 as [e2' H2]. eexists. eauto.
-
-(* FIXME: prove the new cases *)
-Admitted.
+  - destruct (IH_rhs HeqΓ) as [Hval_rhs | Hval_rhs];
+    first destruct (IH_lhs HeqΓ) as [Hval_lhs | Hval_lhs].
+    + left. constructor; assumption.
+    + right.
+      destruct Hval_lhs as [e_lhs' Hstep].
+      eexists; eapply contextual_step_pair_l.
+      assumption.
+      exact Hstep.
+    + right.
+      destruct Hval_rhs as [e_rhs' Hstep].
+      eexists; exact (contextual_step_pair_r _ _ _ Hstep).
+  - (* fst *)
+    destruct (IH HeqΓ) as [H | H].
+    + eapply canonical_values_prod in Hty as (e1 & e2 & -> & ? & ?); last done.
+      right. eexists. eapply base_contextual_step. eapply FstS; assumption.
+    + right. destruct H as [e' H]. eexists. eauto.
+  - (* snd *)
+    destruct (IH HeqΓ) as [H | H].
+    + eapply canonical_values_prod in Hty as (e1 & e2 & -> & ? & ?); last done.
+      right. eexists. eapply base_contextual_step. eapply SndS; assumption.
+    + right. destruct H as [e' H]. eexists. eauto.
+  - (* injl *)
+    destruct (IH HeqΓ) as [H | H].
+    + left. done.
+    + right. destruct H as [e' H]. eexists. eauto.
+  - (* injr *)
+    destruct (IH HeqΓ) as [H | H].
+    + left. done.
+    + right. destruct H as [e' H]. eexists. eauto.
+  - (* case *)
+    right. destruct (IHe HeqΓ) as [H1|H1].
+    + eapply canonical_values_sum in Htye as [(e' & -> & ?) | (e' & -> & ?)]; last done.
+      * eexists. eapply base_contextual_step. econstructor. done.
+      * eexists. eapply base_contextual_step. econstructor. done.
+    + destruct H1 as [e' H1]. eexists. eauto.
+Qed.
 
 Definition ectx_typing (K: ectx) (A B: type) :=
   ∀ e, ∅ ⊢ e : A → ∅ ⊢ (fill K e) : B.
 
+(* This is actually a pretty strong lemma: if ⊢ K[e]: A, then ∃B, ⊢e:B and ∀e',⊢e':B→K[e']: A *)
 Lemma fill_typing_decompose K e A:
   ∅ ⊢ fill K e : A →
   ∃ B, ∅ ⊢ e : B ∧ ectx_typing K B A.
@@ -231,9 +356,27 @@ Proof.
     injection Heq as -> ->.
     eapply typed_substitutivity; eauto.
   - eapply plus_inversion in Hty as (-> & Hty1 & Hty2). constructor.
-
-(* TODO: extend this for the new cases *)
-Admitted.
+  - eapply fst_inversion in Hty as (B & Hty).
+    eapply pair_inversion in Hty as (A' & B' & H_inj & H1 & H2).
+    injection H_inj; intros HA HB; subst.
+    assumption.
+  - eapply snd_inversion in Hty as (B & Hty).
+    eapply pair_inversion in Hty as (A' & B' & H_inj & H1 & H2).
+    injection H_inj; intros HA HB; subst.
+    assumption.
+  - eapply case_inversion in Hty as (A' & B' & Hty_inj & Hty_lhs & Hty_rhs).
+    eapply injl_inversion in Hty_inj as (A'' & B'' & Heq & Hty_inj).
+    injection Heq as -> ->.
+    eapply typed_app.
+    exact Hty_lhs.
+    exact Hty_inj.
+  - eapply case_inversion in Hty as (A' & B' & Hty_inj & Hty_lhs & Hty_rhs).
+    eapply injr_inversion in Hty_inj as (A'' & B'' & Heq & Hty_inj).
+    injection Heq as -> ->.
+    eapply typed_app.
+    exact Hty_rhs.
+    exact Hty_inj.
+Qed.
 
 Lemma typed_preservation e e' A:
   ∅ ⊢ e : A →

theories/type_systems/systemf/exercises03.v

@@ -18,51 +18,57 @@ From semantics.ts.systemf Require Import lang notation types tactics.
 (** Exercise 3 (LN Exercise 22): Universal Fun *)
 
 Definition fun_comp : val :=
-  #0 (* TODO *).
+  Λ, Λ, Λ, (λ: "f" "g" "x", "g" ("f" "x")).
 Definition fun_comp_type : type :=
-  #0 (* TODO *).
+  (∀: ∀: ∀: (#0 → #1) → (#1 → #2) → (#0 → #2)).
 Lemma fun_comp_typed :
   TY 0; ∅ ⊢ fun_comp : fun_comp_type.
 Proof.
-  (* should be solved by solve_typing. *)
-  (* TODO: exercise *)
-Admitted.
+  solve_typing.
+Qed.
+
 
 
 Definition swap_args : val :=
-  #0 (* TODO *).
+  Λ, Λ, Λ, (λ: "f", (λ: "x" "y", "f" "y" "x")).
 Definition swap_args_type : type :=
-  #0 (* TODO *).
+  (∀: ∀: ∀: (#0 → #1 → #2) → (#1 → #0 → #2)).
 Lemma swap_args_typed :
   TY 0; ∅ ⊢ swap_args : swap_args_type.
 Proof.
-  (* should be solved by solve_typing. *)
-  (* TODO: exercise *)
-Admitted.
+  solve_typing.
+Qed.
+
 
 
 Definition lift_prod : val :=
-  #0 (* TODO *).
+  Λ, Λ, Λ, Λ, (λ: "f" "g", (λ: "pair",
+    (Pair ("f" (Fst "pair")) ("g" (Snd "pair")))
+  )).
 Definition lift_prod_type : type :=
-  #0 (* TODO *).
+  (∀: ∀: ∀: ∀: (#0 → #1) → (#2 → #3) → ((#0 × #2) → (#1 × #3))).
 Lemma lift_prod_typed :
   TY 0; ∅ ⊢ lift_prod : lift_prod_type.
 Proof.
-  (* should be solved by solve_typing. *)
-  (* TODO: exercise *)
-Admitted.
+  solve_typing.
+Qed.
 
 
 Definition lift_sum : val :=
-  #0 (* TODO *).
+  Λ, Λ, Λ, Λ, (λ: "f" "g", (λ: "inj",
+    (match: "inj" with
+      InjL "x" => (InjL ("f" "x"))
+      | InjR "x" => (InjR ("g" "x"))
+    end)
+  )).
 Definition lift_sum_type : type :=
-  #0 (* TODO *).
+  (∀: ∀: ∀: ∀: (#0 → #1) → (#2 → #3) → ((#0 + #2) → (#1 + #3))).
 Lemma lift_sum_typed :
   TY 0; ∅ ⊢ lift_sum : lift_sum_type.
+
 Proof.
-  (* should be solved by solve_typing. *)
-  (* TODO: exercise *)
-Admitted.
+  solve_typing.
+Qed.
 
 
 (** Exercise 5 (LN Exercise 18): Named to De Bruijn *)
@@ -86,26 +92,84 @@ Notation "∃:  x , τ" :=
     (PTExists x τ%pty)
     (at level 100, τ at level 200) : PType_scope.
 
+(*
+De Bruijn representation of the following types:
+∀α. α:
+  ∀.#0
+∀α. α → α:
+  ∀.#0->#0
+∀α, β. α → (β → α) → α:
+  ∀.∀. #1 -> (#0 -> #1) -> #1
+∀α. (∀β. β → α) → (∀β, δ. β → δ → α):
+  ∀. (∀. #0 -> #1) -> (∀. ∀. #1 -> #0 -> #2)
+∀α, β. (β → (∀α. α → β)) → α:
+  ∀. ∀. (#0 -> (∀. #0 -> #1)) -> #1
+
+Named representation of the following types:
+∀. ∀. #0:
+  ∀α,β. β
+∀. (∀. #1 → #0):
+  ∀α. ∀β. α→β
+∀. ∀. (∀. #1 → #0):
+  ∀α,β,γ. β→γ
+∀. (∀. #0 → #1) → ∀. #0 → #1 → #0:
+  ∀α. (∀δ. δ→α) → ∀γ. γ → α → γ
+*)
+
+(* Imagine being a coq standard library author *)
+Definition merge {A B C: Type} (f: A → B → C):
+  option A → option B → option C
+  := fun oa ob => match oa, ob with
+    | Some a, Some b => Some (f a b)
+    | _, _ => None
+  end.
+
+Definition gmap_inc_insert (m: gmap string nat) (key: string): gmap string nat :=
+  <[ key := 0 ]> (Nat.succ <$> m).
+
 Fixpoint debruijn (m: gmap string nat) (A: ptype) : option type :=
-  None (* FIXME *).
+  match A with
+  | PTVar ty_name => TVar <$> (m !! ty_name)
+  | PInt => Some Int
+  | PBool => Some Bool
+  | PTForall ty_name body => TForall <$> (debruijn (gmap_inc_insert m ty_name) body)
+  | PTExists ty_name body => TExists <$> (debruijn (gmap_inc_insert m ty_name) body)
+  | PFun lhs rhs =>
+    merge Fun (debruijn m lhs) (debruijn m rhs)
+  end.
 
 (* Example *)
 Goal debruijn ∅ (∀: "x", ∀: "y", "x" → "y")%pty = Some (∀: ∀: #1 → #0)%ty.
 Proof.
-  (* Should be solved by reflexivity. *)
-  (* TODO: exercise *)
-Admitted.
+  reflexivity.
+Qed.
 
 
 Goal debruijn ∅ (∀: "x", "x" → ∀: "y", "y")%pty = Some (∀: #0 → ∀: #0)%ty.
 Proof.
-  (* Should be solved by reflexivity. *)
-  (* TODO: exercise *)
-Admitted.
+  reflexivity.
+Qed.
 
 
 Goal debruijn ∅ (∀: "x", "x" → ∀: "y", "x")%pty = Some (∀: #0 → ∀: #1)%ty.
 Proof.
-  (* Should be solved by reflexivity. *)
-  (* TODO: exercise *)
-Admitted.
+  reflexivity.
+Qed.
+
+Theorem debruijn_inv_multiple: ∃ (T1 T2: ptype), T1 ≠ T2 ∧ debruijn ∅ T1 = debruijn ∅ T2.
+Proof.
+  exists (∀: "x", "x")%pty.
+  exists (∀: "y", "y")%pty.
+  split.
+  discriminate.
+  reflexivity.
+Qed.
+
+(*
+  The issue with our naive implementation of ⤉σ is that any non-primitive type can cause unwanted behavior if that type refers to something from the higher context:
+  ∀. (∀.∀. #0 → #1)<∀.#0→#1> => ∀. (∀. (∀.#0→#1) → #1) and not what we expect, ie ∀. (∀. (∀.#0→#2) → #1)
+
+  In the lecture, we also saw `A[id] = (∀. #0 -> #1)[id] = ∀. (#0 -> #1)[⤉id] = ∀. (#0 -> (id(0))) = ∀. #0 -> #0`
+
+  To fix this, we would have to carefully tweak each value in our substitution map to increment all the free type variables
+*)