Solution for exercises02

_CoqProject

@@ -22,8 +22,11 @@ theories/type_systems/stlc/types.v
 theories/type_systems/stlc_extended/lang.v
 theories/type_systems/stlc_extended/notation.v
 theories/type_systems/stlc_extended/types.v
+theories/type_systems/stlc_extended/types_sol.v
 theories/type_systems/stlc_extended/bigstep.v
+theories/type_systems/stlc_extended/bigstep_sol.v
 theories/type_systems/stlc_extended/ctxstep.v
+theories/type_systems/stlc_extended/ctxstep_sol.v
 
 # By removing the # below, you can add the exercise sheets to make
 #theories/type_systems/warmup/warmup.v
@@ -31,3 +34,4 @@ theories/type_systems/stlc_extended/ctxstep.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_sol.v

theories/type_systems/stlc/exercises02_sol.v

@@ -0,0 +1,378 @@
+From stdpp Require Import gmap base relations tactics.
+From iris Require Import prelude.
+From semantics.ts.stlc Require Import lang notation.
+From semantics.ts.stlc Require untyped types.
+
+
+(** README: Please also download the assigment sheet as a *.pdf from here:
+            https://cms.sic.saarland/semantics_ws2324/materials/
+            It contains additional explanation and excercises. **)
+
+(** ** Exercise 1: Prove that the structural and contextual semantics are equivalent. *)
+(** You will find it very helpful to separately derive the structural rules of the
+  structural semantics for the contextual semantics. *)
+
+Lemma contextual_step_beta x e e':
+  is_val e' → contextual_step ((λ: x, e) e') (subst' x e' e).
+Proof.
+  intros Hval. eapply base_contextual_step, BetaS; done.
+Qed.
+
+Lemma contextual_step_app_r (e1 e2 e2': expr) :
+  contextual_step e2 e2' →
+  contextual_step (e1 e2) (e1 e2').
+Proof.
+  intros Hval. by eapply fill_contextual_step with (K := AppRCtx e1 HoleCtx).
+Qed.
+
+Lemma contextual_step_app_l (e1 e1' e2: expr) :
+  is_val e2 →
+  contextual_step e1 e1' →
+  contextual_step (e1 e2) (e1' e2).
+Proof.
+  intros Hval. eapply is_val_spec in Hval as [v Hval].
+  eapply of_to_val in Hval as <-.
+  eapply fill_contextual_step with (K := (AppLCtx HoleCtx v)).
+Qed.
+
+Lemma contextual_step_plus_red (n1 n2 n3: Z) :
+  (n1 + n2)%Z = n3 →
+  contextual_step (n1 + n2)%E n3.
+Proof.
+  intros Hval. eapply base_contextual_step, PlusS; done.
+Qed.
+
+Lemma contextual_step_plus_r e1 e2 e2' :
+  contextual_step e2 e2' →
+  contextual_step (Plus e1 e2) (Plus e1 e2').
+Proof.
+  intros Hval. by eapply fill_contextual_step with (K := (PlusRCtx e1 HoleCtx)).
+Qed.
+
+Lemma contextual_step_plus_l e1 e1' e2 :
+  is_val e2 →
+  contextual_step e1 e1' →
+  contextual_step (Plus e1 e2) (Plus e1' e2).
+Proof.
+  intros Hval. eapply is_val_spec in Hval as [v Hval].
+  eapply of_to_val in Hval as <-.
+  eapply fill_contextual_step with (K := (PlusLCtx HoleCtx 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.
+
+Lemma step_contextual_step e1 e2: step e1 e2 → contextual_step e1 e2.
+Proof.
+  (* The hints above make sure eauto uses the right lemmas. *)
+  induction 1; eauto.
+Qed.
+
+(** Now the other direction. *)
+(* You may find it helpful to introduce intermediate lemmas. *)
+
+Lemma base_step_step e1 e2:
+  base_step e1 e2 → step e1 e2.
+Proof.
+  destruct 1; subst.
+  - eauto.
+  - by econstructor.
+Qed.
+
+Lemma fill_step K e1 e2:
+  step e1 e2 → step (fill K e1) (fill K e2).
+Proof.
+  induction K; simpl; eauto.
+Qed.
+Lemma contextual_step_step e1 e2:
+  contextual_step e1 e2 → step e1 e2.
+Proof.
+  destruct 1 as [K h1 h2 -> -> Hstep].
+  eapply fill_step, base_step_step, Hstep.
+Qed.
+
+
+(** ** Exercise 2: Scott encodings *)
+Section scott.
+  (* take a look at untyped.v for usefull lemmas and definitions *)
+  Import semantics.ts.stlc.untyped.
+
+  (** Scott encoding of Booleans *)
+  Definition true_scott : val := λ: "t" "f", "t".
+  Definition false_scott : val := λ: "t" "f", "f".
+
+  Lemma true_red (v1 v2 : val) :
+    closed [] v1 →
+    closed [] v2 →
+    rtc step (true_scott v1 v2) v1.
+  Proof.
+    intros Hcl1 Hcl2.
+    eapply rtc_l.
+    { econstructor; first auto.
+      econstructor. auto.
+    }
+    simpl.
+    eapply rtc_l.
+    { econstructor; auto. }
+    simpl.
+    rewrite subst_closed_nil; done.
+  Qed.
+
+  Lemma false_red (v1 v2 : val) :
+    closed [] v1 →
+    closed [] v2 →
+    rtc step (false_scott v1 v2) v2.
+  Proof.
+    intros Hcl1 Hcl2.
+    eapply rtc_l.
+    { econstructor; first auto.
+      econstructor. auto.
+    }
+    simpl.
+    eapply rtc_l.
+    { econstructor; auto. }
+    simpl. done.
+  Qed.
+
+  (** Scott encoding of Pairs *)
+  Definition pair_scott : val := λ: "v1" "v2", λ: "d", "d" "v1" "v2".
+
+  Definition fst_scott : val := λ: "p", "p" (λ: "a" "b", "a").
+  Definition snd_scott : val := λ: "p", "p" (λ: "a" "b", "b").
+
+  Lemma fst_red (v1 v2 : val) :
+    is_closed [] v1 →
+    is_closed [] v2 →
+    rtc step (fst_scott (pair_scott v1 v2)) v1.
+  Proof.
+    intros Hcl1 Hcl2.
+    eapply rtc_l.
+    { econstructor 3. econstructor; first auto.
+      econstructor. auto.
+    }
+    simpl. eapply rtc_l.
+    { econstructor 3. econstructor; first auto. }
+    simpl. eapply rtc_l.
+    { econstructor. done. }
+    simpl. eapply rtc_l.
+    { econstructor. done. }
+    simpl.
+    rewrite !(subst_closed_nil v1); [ | done..].
+    rewrite subst_closed_nil; last done.
+    eapply rtc_l.
+    { econstructor; first auto.
+      econstructor. auto.
+    }
+    simpl. eapply rtc_l.
+    { econstructor; first auto. }
+    simpl. rewrite subst_closed_nil; done.
+  Qed.
+
+  Lemma snd_red (v1 v2 : val) :
+    is_closed [] v1 →
+    is_closed [] v2 →
+    rtc step (snd_scott (pair_scott v1 v2)) v2.
+  Proof.
+    intros Hcl1 Hcl2.
+    eapply rtc_l.
+    { econstructor 3. econstructor; first auto.
+      econstructor. auto.
+    }
+    simpl. eapply rtc_l.
+    { econstructor 3. econstructor; first auto. }
+    simpl. eapply rtc_l.
+    { econstructor. done. }
+    simpl. eapply rtc_l.
+    { econstructor. done. }
+    simpl.
+    rewrite !(subst_closed_nil v2); [ | done..].
+    rewrite !(subst_closed_nil v1); [ | done..].
+    eapply rtc_l.
+    { econstructor; first auto.
+      econstructor. auto.
+    }
+    simpl. eapply rtc_l.
+    { econstructor; first auto. }
+    simpl. done.
+  Qed.
+
+End scott.
+
+Import semantics.ts.stlc.types.
+
+(** ** Exercise 3: type erasure *)
+(** Source terms *)
+Inductive src_expr :=
+| ELitInt (n: Z)
+(* Base lambda calculus *)
+| EVar (x : string)
+| ELam (x : binder) (A: type) (e : src_expr)
+| EApp (e1 e2 : src_expr)
+(* Base types and their operations *)
+| EPlus (e1 e2 : src_expr).
+
+(** The erasure function *)
+Fixpoint erase (E: src_expr) : expr :=
+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 :=
+| src_typed_var Γ x A :
+    Γ !! x = Some A →
+    Γ ⊢S (EVar x) : A
+| src_typed_lam Γ x E A B :
+    (<[ x := A]> Γ) ⊢S E : B →
+    Γ ⊢S (ELam (BNamed x) A E) : (A → B)
+| src_typed_int Γ z :
+    Γ ⊢S (ELitInt z) : Int
+| src_typed_app Γ E1 E2 A B :
+    Γ ⊢S E1 : (A → B) →
+    Γ ⊢S E2 : A →
+    Γ ⊢S EApp E1 E2 : B
+| src_typed_add Γ E1 E2 :
+    Γ ⊢S E1 : Int →
+    Γ ⊢S E2 : Int →
+    Γ ⊢S EPlus E1 E2 : Int
+where "Γ '⊢S' E : A" := (src_typed Γ E%E A%ty) : FType_scope.
+#[export] Hint Constructors src_typed : core.
+
+Lemma type_erasure_correctness Γ E A:
+  (Γ ⊢S E : A)%ty → (Γ ⊢ erase E : A)%ty.
+Proof.
+  induction 1; simpl; eauto.
+Qed.
+
+(** ** Exercise 4: Unique Typing *)
+Lemma src_typing_unique Γ E A B:
+  (Γ ⊢S E : A)%ty → (Γ ⊢S E : B)%ty → A = B.
+Proof.
+  induction 1 as [ | ????? H1 IH1 | | ????? H1 IH1 H2 IH2 | ??? H1 IH1 H2 IH2] in B |-*; inversion 1; subst; try congruence.
+  - f_equal. eauto.
+  - rename select (_ ⊢S _ : (_ → _))%ty into Ha.
+    eapply IH1 in Ha. by injection Ha.
+Qed.
+
+(** TODO: Is runtime typing (Curry-style) also unique? Prove it or give a counterexample. *)
+(** Runtime typing is not unique! *)
+Lemma id_int: (∅ ⊢ (λ: "x", "x") : (Int → Int))%ty.
+Proof. eauto. Qed.
+
+Lemma id_int_to_int: (∅ ⊢ (λ: "x", "x") : ((Int → Int) → (Int → Int)))%ty.
+Proof. eauto. Qed.
+
+(** ** Exercise 5: Type Inference *)
+
+Fixpoint type_eq A B :=
+  match A, B with
+  | Int, Int => true
+  | Fun A B, Fun A' B' => type_eq A A' && type_eq B B'
+  | _, _ => false
+  end.
+
+Lemma type_eq_iff A B: type_eq A B ↔ A = B.
+Proof.
+  induction A in B |-*; destruct B; simpl; naive_solver.
+Qed.
+
+Notation ctx := (gmap string type).
+Fixpoint infer_type (Γ: ctx) E :=
+  match E with
+  | EVar x => Γ !! x
+  | ELam (BNamed x) A E =>
+    match infer_type (<[x := A]> Γ) E with
+    | Some B => Some (Fun A B)
+    | None => None
+    end
+  | ELitInt l => Some Int
+  | EApp E1 E2 =>
+    match infer_type Γ E1, infer_type Γ E2 with
+    | Some (Fun A B), Some C => if type_eq A C 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.
+
+(** Prove both directions of the correctness theorem. *)
+Lemma infer_type_typing Γ E A:
+  infer_type Γ E = Some A → (Γ ⊢S E : A)%ty.
+Proof.
+  induction E as [l|x|x B E IH|E1 IH1 E2 IH2|E1 IH1 E2 IH2] in Γ, A |-*; simpl.
+  - destruct l; naive_solver.
+  - eauto.
+  - destruct x as [|x]; first naive_solver.
+    destruct infer_type eqn: Heq; last naive_solver.
+    eapply IH in Heq. injection 1 as <-. eauto.
+  - destruct infer_type as [B|] eqn: Heq1; last naive_solver.
+    destruct B as [|B1 B2]; try naive_solver.
+    destruct (infer_type Γ E2) as [C|] eqn: Heq2; last naive_solver.
+    destruct type_eq eqn: Heq3; last naive_solver.
+    injection 1 as <-. eapply Is_true_eq_left in Heq3.
+    eapply type_eq_iff in Heq3 as ->.
+    eauto.
+  - destruct infer_type as [B|] eqn: Heq1; last naive_solver.
+    destruct B; try naive_solver.
+    destruct (infer_type Γ E2) as [C|] eqn: Heq2; last naive_solver.
+    destruct C; naive_solver.
+Qed.
+
+Lemma typing_infer_type Γ E A:
+  (Γ ⊢S E : A)%ty → infer_type Γ E = Some A.
+Proof.
+  induction 1; simpl; eauto.
+  - by rewrite IHsrc_typed.
+  - rewrite IHsrc_typed1 IHsrc_typed2.
+    rewrite (Is_true_eq_true (type_eq A A)) //=.
+    by eapply type_eq_iff.
+  - by rewrite IHsrc_typed1 IHsrc_typed2.
+Qed.
+
+
+(** ** Exercise 6: untypable, safe term *)
+
+(* The exercise asks you to:
+  "Give one example if there is such an expression, otherwise prove their non-existence."
+  So either finish one section or the other.
+*)
+
+Section give_example.
+  Definition ust : expr := (λ: "f", 5) (λ: "x", 0 0)%E.
+
+  Lemma ust_safe e':
+    rtc step ust e' → is_val e' ∨ reducible e'.
+  Proof.
+    inversion 1 as [ | x y z H1 H2]; subst.
+    - right. eexists. eapply StepBeta. done.
+    - inversion H1 as [??? Ha | ??? Ha Hb | ??? Ha | | ??? Ha Hb | ??? Ha ]; subst.
+      + simpl in H2. inversion H2 as [ | ??? [] _]; subst; eauto.
+      + inversion Hb.
+      + inversion Ha.
+  Qed.
+
+  Lemma ust_no_type Γ A:
+    ¬ (Γ ⊢ ust : A)%ty.
+  Proof.
+    intros H. inversion H; subst.
+    inversion H5; subst. inversion H6; subst.
+    inversion H4.
+  Qed.
+End give_example.
+
+Section prove_non_existence.
+  Lemma no_ust :
+  ∀ e, (∀ e', rtc step e e' → is_val e' ∨ reducible e') → ∃ A, (∅ ⊢ e : A)%ty.
+  Proof.
+    (* This is not possible as shown above *)
+  Abort.
+End prove_non_existence.

theories/type_systems/stlc_extended/bigstep_sol.v

@@ -0,0 +1,69 @@
+From stdpp Require Import gmap base relations.
+From iris Require Import prelude.
+From semantics.ts.stlc_extended Require Import lang notation.
+
+(** * Big-step semantics *)
+
+Implicit Types
+  (v : val)
+  (e : expr).
+
+Inductive big_step : expr → val → Prop :=
+  | bs_lit (n : Z) :
+      big_step (LitInt n) (LitIntV n)
+  | bs_lam (x : binder) (e : expr) :
+      big_step (λ: x, e)%E (λ: x, e)%V
+  | bs_add e1 e2 (z1 z2 : Z) :
+      big_step e1 (LitIntV z1) →
+      big_step e2 (LitIntV z2) →
+      big_step (Plus e1 e2) (LitIntV (z1 + z2))%Z
+  | bs_app e1 e2 x e v2 v :
+      big_step e1 (LamV x e) →
+      big_step e2 v2 →
+      big_step (subst' x (of_val v2) e) v →
+      big_step (App e1 e2) v
+| bs_pair e1 e2 v1 v2 :
+      big_step e1 v1 →
+      big_step e2 v2 →
+      big_step (e1, e2) (v1, v2)
+  | bs_fst e v1 v2 :
+      big_step e (v1, v2) →
+      big_step (Fst e) v1
+  | bs_snd e v1 v2 :
+      big_step e (v1, v2) →
+      big_step (Snd e) v2
+  | bs_injl e v :
+      big_step e v →
+      big_step (InjL e) (InjLV v)
+  | bs_injr e v :
+      big_step e v →
+      big_step (InjR e) (InjRV v)
+  | bs_casel e e1 e2 v v' :
+      big_step e (InjLV v) →
+      big_step (e1 (of_val v)) v' →
+      big_step (Case e e1 e2) v'
+  | bs_caser e e1 e2 v v' :
+      big_step e (InjRV v) →
+      big_step (e2 (of_val v)) v' →
+      big_step (Case e e1 e2) v'
+
+    .
+#[export] Hint Constructors big_step : core.
+
+Lemma big_step_of_val e v :
+  e = of_val v →
+  big_step e v.
+Proof.
+  intros ->.
+  induction v; simpl; eauto.
+Qed.
+
+
+
+Lemma big_step_val v v' :
+  big_step (of_val v) v' → v' = v.
+Proof.
+  enough (∀ e, big_step e v' → e = of_val v → v' = v) by naive_solver.
+  intros e Hb.
+  induction Hb in v |-*; intros Heq; subst; destruct v; inversion Heq; subst; naive_solver.
+Qed.

theories/type_systems/stlc_extended/ctxstep_sol.v

@@ -0,0 +1,211 @@
+From semantics.ts.stlc_extended Require Export lang.
+
+(** The stepping relation *)
+
+Inductive base_step : expr → expr → Prop :=
+  | BetaS x e1 e2 e' :
+     is_val e2 →
+     e' = subst' x e2 e1 →
+     base_step (App (Lam x e1) e2) e'
+  | PlusS e1 e2 (n1 n2 n3 : Z):
+     e1 = (LitInt n1) →
+     e2 = (LitInt n2) →
+     (n1 + n2)%Z = n3 →
+     base_step (Plus e1 e2) (LitInt n3)
+  | FstS e1 e2 :
+    is_val e1 →
+    is_val e2 →
+    base_step (Fst (Pair e1 e2)) e1
+  | SndS e1 e2 :
+    is_val e1 →
+    is_val e2 →
+    base_step (Snd (Pair e1 e2)) e2
+  | CaseLS e e1 e2 :
+    is_val e →
+    base_step (Case (InjL e) e1 e2) (App e1 e)
+  | CaseRS e e1 e2 :
+    is_val e →
+    base_step (Case (InjR e) e1 e2) (App e2 e)
+.
+
+#[export] Hint Constructors base_step : core.
+
+(** We define evaluation contexts *)
+Inductive ectx :=
+  | HoleCtx
+  | AppLCtx (K: ectx) (v2 : val)
+  | AppRCtx (e1 : expr) (K: ectx)
+  | PlusLCtx (K: ectx) (v2 : val)
+  | PlusRCtx (e1 : expr) (K: ectx)
+  | PairLCtx (K: ectx) (v2 : val)
+  | PairRCtx (e1 : expr) (K: ectx)
+  | FstCtx (K: ectx)
+  | SndCtx (K: ectx)
+  | InjLCtx (K: ectx)
+  | InjRCtx (K: ectx)
+  | CaseCtx (K: ectx) (e1 : expr) (e2 : expr)
+.
+
+Fixpoint fill (K : ectx) (e : expr) : expr :=
+  match K with
+  | HoleCtx => e
+  | AppLCtx K v2 => App (fill K e) (of_val v2)
+  | AppRCtx e1 K => App e1 (fill K e)
+  | PlusLCtx K v2 => Plus (fill K e) (of_val v2)
+  | PlusRCtx e1 K => Plus e1 (fill K e)
+  | PairLCtx K v2 => Pair (fill K e) (of_val v2)
+  | PairRCtx e1 K => Pair e1 (fill K e)
+  | FstCtx K => Fst (fill K e)
+  | SndCtx K => Snd (fill K e)
+  | InjLCtx K => InjL (fill K e)
+  | InjRCtx K => InjR (fill K e)
+  | CaseCtx K e1 e2 => Case (fill K e) e1 e2
+  end.
+
+Fixpoint comp_ectx (K: ectx) (K' : ectx) : ectx :=
+  match K with
+  | HoleCtx => K'
+  | AppLCtx K v2 => AppLCtx (comp_ectx K K') v2
+  | AppRCtx e1 K => AppRCtx e1 (comp_ectx K K')
+  | PlusLCtx K v2 => PlusLCtx (comp_ectx K K') v2
+  | PlusRCtx e1 K => PlusRCtx e1 (comp_ectx K K')
+  | PairLCtx K v2 => PairLCtx (comp_ectx K K') v2
+  | PairRCtx e1 K => PairRCtx e1 (comp_ectx K K')
+  | FstCtx K => FstCtx (comp_ectx K K')
+  | SndCtx K => SndCtx (comp_ectx K K')
+  | InjLCtx K => InjLCtx (comp_ectx K K')
+  | InjRCtx K => InjRCtx (comp_ectx K K')
+  | CaseCtx K e1 e2 => CaseCtx (comp_ectx K K') e1 e2
+  end.
+
+(** Contextual steps *)
+Inductive contextual_step (e1 : expr) (e2 : expr) : Prop :=
+  Ectx_step K e1' e2' :
+    e1 = fill K e1' → e2 = fill K e2' →
+    base_step e1' e2' → contextual_step e1 e2.
+
+#[export] Hint Constructors contextual_step : core.
+
+Definition reducible (e : expr) :=
+  ∃ e', contextual_step e e'.
+
+Definition empty_ectx := HoleCtx.
+
+(** Basic properties about the language *)
+Lemma fill_empty e : fill empty_ectx e = e.
+Proof. done. Qed.
+
+Lemma fill_comp (K1 K2 : ectx) e : fill K1 (fill K2 e) = fill (comp_ectx K1 K2) e.
+Proof. induction K1; simpl; congruence. Qed.
+
+Lemma base_contextual_step e1 e2 :
+  base_step e1 e2 → contextual_step e1 e2.
+Proof. apply Ectx_step with empty_ectx; by rewrite ?fill_empty. Qed.
+
+Lemma fill_contextual_step K e1 e2 :
+  contextual_step e1 e2 → contextual_step (fill K e1) (fill K e2).
+Proof.
+  destruct 1 as [K' e1' e2' -> ->].
+  rewrite !fill_comp. by econstructor.
+Qed.
+
+(** We derive a few lemmas about contextual steps:
+  these essentially provide rules for structural lifting
+   akin to the structural semantics.
+ *)
+Lemma contextual_step_app_l e1 e1' e2:
+  is_val e2 →
+  contextual_step e1 e1' →
+  contextual_step (App e1 e2) (App e1' e2).
+Proof.
+  intros [v <-%of_to_val]%is_val_spec Hcontextual.
+  by eapply (fill_contextual_step (AppLCtx HoleCtx v)).
+Qed.
+
+Lemma contextual_step_app_r e1 e2 e2':
+  contextual_step e2 e2' →
+  contextual_step (App e1 e2) (App e1 e2').
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step (AppRCtx e1 HoleCtx)).
+Qed.
+
+Lemma contextual_step_plus_l e1 e1' e2:
+  is_val e2 →
+  contextual_step e1 e1' →
+  contextual_step (Plus e1 e2) (Plus e1' e2).
+Proof.
+  intros [v <-%of_to_val]%is_val_spec Hcontextual.
+  by eapply (fill_contextual_step (PlusLCtx HoleCtx v)).
+Qed.
+
+Lemma contextual_step_plus_r e1 e2 e2':
+  contextual_step e2 e2' →
+  contextual_step (Plus e1 e2) (Plus e1 e2').
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step (PlusRCtx e1 HoleCtx)).
+Qed.
+
+Lemma contextual_step_pair_l e1 e1' e2:
+  is_val e2 →
+  contextual_step e1 e1' →
+  contextual_step (Pair e1 e2) (Pair e1' e2).
+Proof.
+  intros [v <-%of_to_val]%is_val_spec Hcontextual.
+  by eapply (fill_contextual_step (PairLCtx HoleCtx v)).
+Qed.
+
+Lemma contextual_step_pair_r e1 e2 e2':
+  contextual_step e2 e2' →
+  contextual_step (Pair e1 e2) (Pair e1 e2').
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step (PairRCtx e1 HoleCtx)).
+Qed.
+
+Lemma contextual_step_fst e e':
+  contextual_step e e' →
+  contextual_step (Fst e) (Fst e').
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step (FstCtx HoleCtx)).
+Qed.
+
+Lemma contextual_step_snd e e':
+  contextual_step e e' →
+  contextual_step (Snd e) (Snd e').
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step (SndCtx HoleCtx)).
+Qed.
+
+Lemma contextual_step_injl e e':
+  contextual_step e e' →
+  contextual_step (InjL e) (InjL e').
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step (InjLCtx HoleCtx)).
+Qed.
+
+Lemma contextual_step_injr e e':
+  contextual_step e e' →
+  contextual_step (InjR e) (InjR e').
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step (InjRCtx HoleCtx)).
+Qed.
+
+Lemma contextual_step_case e e' e1 e2:
+  contextual_step e e' →
+  contextual_step (Case e e1 e2) (Case e' e1 e2).
+Proof.
+  intros Hcontextual.
+  by eapply (fill_contextual_step (CaseCtx HoleCtx e1 e2)).
+Qed.
+
+#[global]
+Hint Resolve
+  contextual_step_app_l contextual_step_app_r contextual_step_plus_l contextual_step_plus_r
+  contextual_step_case contextual_step_fst contextual_step_injl contextual_step_injr
+  contextual_step_pair_l contextual_step_pair_r contextual_step_snd : core.

theories/type_systems/stlc_extended/types_sol.v

@@ -0,0 +1,350 @@
+From stdpp Require Import base relations.
+From iris Require Import prelude.
+From semantics.lib Require Import maps.
+From semantics.ts.stlc_extended Require Import lang notation ctxstep_sol.
+
+(** ** Syntactic typing *)
+Inductive type : Type :=
+  | Int
+  | Fun (A B : type)
+  | Prod (A B : type)
+  | Sum (A B : type).
+
+Definition typing_context := gmap string type.
+Implicit Types
+  (Γ : typing_context)
+  (v : val)
+  (e : expr).
+
+Declare Scope FType_scope.
+Delimit Scope FType_scope with ty.
+Bind Scope FType_scope with type.
+Infix "→" := Fun : FType_scope.
+Notation "(→)" := Fun (only parsing) : FType_scope.
+Infix "×" := Prod (at level 70) : FType_scope.
+Notation "(×)" := Prod (only parsing) : FType_scope.
+Infix "+" := Sum : FType_scope.
+Notation "(+)" := Sum (only parsing) : FType_scope.
+
+Reserved Notation "Γ ⊢ e : A" (at level 74, e, A at next level).
+
+Inductive syn_typed : typing_context → expr → type → Prop :=
+  | typed_var Γ x A :
+      Γ !! x = Some A →
+      Γ ⊢ (Var x) : A
+  | typed_lam Γ x e A B :
+      (<[ x := A]> Γ) ⊢ e : B →
+      Γ ⊢ (Lam (BNamed x) e) : (A → B)
+  | typed_lam_anon Γ e A B :
+      Γ ⊢ e : B →
+      Γ ⊢ (Lam BAnon e) : (A → B)
+  | typed_int Γ z : Γ ⊢ (LitInt z) : Int
+  | typed_app Γ e1 e2 A B :
+      Γ ⊢ e1 : (A → B) →
+      Γ ⊢ e2 : A →
+      Γ ⊢ (e1 e2)%E : B
+  | typed_add Γ e1 e2 :
+      Γ ⊢ e1 : Int →
+      Γ ⊢ e2 : Int →
+      Γ ⊢ e1 + e2 : Int
+  | typed_pair Γ e1 e2 A B :
+      Γ ⊢ e1 : A →
+      Γ ⊢ e2 : B →
+      Γ ⊢ (e1, e2) : A × B
+  | typed_fst Γ e A B :
+      Γ ⊢ e : A × B →
+      Γ ⊢ Fst e : A
+  | typed_snd Γ e A B :
+      Γ ⊢ e : A × B →
+      Γ ⊢ Snd e : B
+  | typed_injl Γ e A B :
+      Γ ⊢ e : A →
+      Γ ⊢ InjL e : A + B
+  | typed_injr Γ e A B :
+      Γ ⊢ e : B →
+      Γ ⊢ InjR e : A + B
+  | typed_case Γ e e1 e2 A B C :
+      Γ ⊢ e : B + C →
+      Γ ⊢ e1 : (B → A) →
+      Γ ⊢ e2 : (C → A) →
+      Γ ⊢ Case e e1 e2 : A
+where "Γ ⊢ e : A" := (syn_typed Γ e%E A%ty).
+#[export] Hint Constructors syn_typed : core.
+
+(** Examples *)
+Goal ∅ ⊢ (λ: "x", "x")%E : (Int → Int).
+Proof. eauto. Qed.
+
+Lemma syn_typed_closed Γ e A X :
+  Γ ⊢ e : A →
+  (∀ 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.
+  { (* var *) apply bool_decide_pack, Hx. apply elem_of_dom; eauto. }
+  { (* lam *) apply IH.
+    intros y. rewrite elem_of_dom lookup_insert_is_Some.
+    intros [<- | [? Hy]]; first by apply elem_of_cons; eauto.
+    apply elem_of_cons. right. eapply Hx. by apply elem_of_dom.
+  }
+  { (* anon lam *) naive_solver. }
+  (* everything else *)
+  all: repeat match goal with
+              | |- Is_true (_ && _)  => apply andb_True; split
+              end.
+  all: try naive_solver.
+Qed.
+
+Lemma typed_weakening Γ Δ e A:
+  Γ ⊢ 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.
+  - (* var *) econstructor. by eapply lookup_weaken.
+  - (* lam *) econstructor. eapply IH; eauto. by eapply insert_mono.
+Qed.
+
+(** Typing inversion lemmas *)
+Lemma var_inversion Γ (x: string) A: Γ ⊢ x : A → Γ !! x = Some A.
+Proof. inversion 1; subst; auto. Qed.
+
+Lemma lam_inversion Γ (x: string) e C:
+  Γ ⊢ (λ: x, e) : C →
+  ∃ A B, C = (A → B)%ty ∧ <[x:=A]> Γ ⊢ e : B.
+Proof. inversion 1; subst; eauto 10. Qed.
+
+Lemma lam_anon_inversion Γ e C:
+  Γ ⊢ (λ: <>, e) : C →
+  ∃ A B, C = (A → B)%ty ∧ Γ ⊢ e : B.
+Proof. inversion 1; subst; eauto 10. Qed.
+
+Lemma app_inversion Γ e1 e2 B:
+  Γ ⊢ e1 e2 : B →
+  ∃ A, Γ ⊢ e1 : (A → B) ∧ Γ ⊢ e2 : A.
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma plus_inversion Γ e1 e2 B:
+  Γ ⊢ e1 + e2 : B →
+  B = Int ∧ Γ ⊢ e1 : Int ∧ Γ ⊢ e2 : Int.
+Proof. inversion 1; subst; eauto. Qed.
+
+
+(* There are the inversion lemmas for the new typing rules *)
+Lemma pair_inversion Γ e1 e2 C :
+  Γ ⊢ (e1, e2) : C →
+  ∃ A B, C = (A × B)%ty ∧ Γ ⊢ e1 : A ∧ Γ ⊢ e2 : B.
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma fst_inversion Γ e A :
+  Γ ⊢ Fst e : A →
+  ∃ B, Γ ⊢ e : A × B.
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma snd_inversion Γ e B :
+  Γ ⊢ Snd e : B →
+  ∃ A, Γ ⊢ e : A × B.
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma injl_inversion Γ e C :
+  Γ ⊢ InjL e : C →
+  ∃ A B, C = (A + B)%ty ∧ Γ ⊢ e : A.
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma injr_inversion Γ e C :
+  Γ ⊢ InjR e : C →
+  ∃ A B, C = (A + B)%ty ∧ Γ ⊢ e : B.
+Proof. inversion 1; subst; eauto. Qed.
+
+Lemma case_inversion Γ e e1 e2 A :
+  Γ ⊢ Case e e1 e2 : A →
+  ∃ B C, Γ ⊢ e : B + C ∧ Γ ⊢ e1 : (B → A) ∧ Γ ⊢ e2 : (C → A).
+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 Hp % var_inversion.
+    destruct (decide (x = y)).
+    + subst. rewrite lookup_insert in Hp. injection Hp as ->.
+      eapply typed_weakening; [done| ]. apply map_empty_subseteq.
+    + rewrite lookup_insert_ne in Hp; last done. auto.
+  - destruct y as [ | y].
+    { intros (A' & C & -> & Hty) % lam_anon_inversion.
+      econstructor. destruct decide as [Heq|].
+      + congruence.
+      + eauto.
+    }
+    intros (A' & C & -> & Hty) % lam_inversion.
+    econstructor. destruct decide as [Heq|].
+    + injection Heq as [= ->]. by rewrite insert_insert in Hty.
+    + rewrite insert_commute in Hty; last naive_solver. eauto.
+  - intros (C & Hty1 & Hty2) % app_inversion. eauto.
+  - inversion 1; subst; auto.
+  - intros (-> & Hty1 & Hty2)%plus_inversion; eauto.
+  - intros (? & ? & -> & ? & ?) % pair_inversion. eauto.
+  - intros (? & ?)%fst_inversion. eauto.
+  - intros (? & ?)%snd_inversion. eauto.
+  - intros (? & ? & -> & ?)%injl_inversion. eauto.
+  - intros (? & ? & -> & ?)%injr_inversion. eauto.
+  - intros (? & ? & ? & ? & ?)%case_inversion. eauto.
+Qed.
+
+(** Canonical values *)
+Lemma canonical_values_arr Γ e A B:
+  Γ ⊢ e : (A → B) →
+  is_val e →
+  ∃ x e', e = (λ: x, e')%E.
+Proof.
+  inversion 1; simpl; naive_solver.
+Qed.
+
+Lemma canonical_values_int Γ e:
+  Γ ⊢ e : Int →
+  is_val e →
+  ∃ n: Z, e = (#n)%E.
+Proof.
+  inversion 1; simpl; naive_solver.
+Qed.
+
+(* canonical forms lemmas for the new types *)
+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 | Γ e1 e2 A B Hty1 IH1 Hty2 IH2 | Γ 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.
+  - (* int *)left. done.
+  - (* app *)
+    destruct (IH2 HeqΓ) as [H2|H2]; [destruct (IH1 HeqΓ) as [H1|H1]|].
+    + eapply canonical_values_arr in Hty as (x & e & ->); last done.
+      right. eexists.
+      eapply base_contextual_step, BetaS; eauto.
+    + right. destruct H1 as [e1' Hstep].
+      eexists. eauto.
+    + right. destruct H2 as [e2' H2].
+      eexists. eauto.
+  - (* plus *)
+    destruct (IH2 HeqΓ) as [H2|H2]; [destruct (IH1 HeqΓ) as [H1|H1]|].
+    + right. eapply canonical_values_int in Hty1 as [n1 ->]; last done.
+      eapply canonical_values_int in Hty2 as [n2 ->]; last done.
+      subst. eexists; eapply base_contextual_step. eauto.
+    + right. destruct H1 as [e1' Hstep]. eexists. eauto.
+    + right. destruct H2 as [e2' H2]. eexists. eauto.
+- (* pair *)
+    destruct (IH2 HeqΓ) as [H2|H2]; [destruct (IH1 HeqΓ) as [H1|H1]|].
+    + left. done.
+    + right. destruct H1 as [e1' Hstep]. eexists. eauto.
+    + right. destruct H2 as [e2' H2]. eexists. eauto.
+  - (* fst *)
+    destruct (IH HeqΓ) as [H | H].
+    + eapply canonical_values_prod in Hty as (e1 & e2 & -> & ? & ?); last done.
+      right. eexists. eapply base_contextual_step. econstructor; done.
+    + 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. econstructor; done.
+    + 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.
+
+Lemma fill_typing_decompose K e A:
+  ∅ ⊢ fill K e : A →
+  ∃ B, ∅ ⊢ e : B ∧ ectx_typing K B A.
+Proof.
+  unfold ectx_typing; induction K in e,A |-*; simpl; eauto.
+  all: inversion 1; subst; edestruct IHK as [? [Hit Hty]]; eauto.
+Qed.
+
+Lemma fill_typing_compose K e A B:
+  ∅ ⊢ e : B →
+  ectx_typing K B A →
+  ∅ ⊢ fill K e : A.
+Proof.
+  intros H1 H2; by eapply H2.
+Qed.
+
+Lemma typed_preservation_base_step e e' A:
+  ∅ ⊢ e : A →
+  base_step e e' →
+  ∅ ⊢ e' : A.
+Proof.
+  intros Hty Hstep.
+  destruct Hstep as [  ]; subst.
+  - eapply app_inversion in Hty as (B & H1 & H2).
+    destruct x as [|x].
+    { eapply lam_anon_inversion in H1 as (C & D & [= -> ->] & Hty). done. }
+    eapply lam_inversion in H1 as (C & D & Heq & Hty).
+    injection Heq as -> ->.
+    eapply typed_substitutivity; eauto.
+  - eapply plus_inversion in Hty as (-> & Hty1 & Hty2). constructor.
+- by eapply fst_inversion in Hty as (B & (? & ? & [= <- <-] & ? & ?)%pair_inversion).
+  - by eapply snd_inversion in Hty as (B & (? & ? & [= <- <-] & ? & ?)%pair_inversion).
+  - eapply case_inversion in Hty as (B & C & (? & ? & [= <- <-] & Hty)%injl_inversion & ? & ?).
+    eauto.
+  - eapply case_inversion in Hty as (B & C & (? & ? & [= <- <-] & Hty )%injr_inversion & ? & ?).
+    eauto.
+Qed.
+
+
+Lemma typed_preservation e e' A:
+  ∅ ⊢ e : A →
+  contextual_step e e' →
+  ∅ ⊢ e' : A.
+Proof.
+  intros Hty Hstep. destruct Hstep as [K e1 e2 -> -> Hstep].
+  eapply fill_typing_decompose in Hty as [B [H1 H2]].
+  eapply fill_typing_compose; last done.
+  by eapply typed_preservation_base_step.
+Qed.
+
+Lemma type_safety e1 e2 A:
+  ∅ ⊢ e1 : A →
+  rtc contextual_step e1 e2 →
+  is_val e2 ∨ reducible e2.
+Proof.
+  induction 2; eauto using typed_progress, typed_preservation.
+Qed.