exercises 02 sol

theories/stlc/exercises02_sol.v

+From stdpp Require Import gmap base relations tactics.
+From iris Require Import prelude.
+From semantics.stlc Require Import lang notation.
+From semantics.stlc Require untyped types.
+
+
+(** ** 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. *)
+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: Define a function on Scott-encoded numbers that returns the identity for 0 and diverges for every other number. *)
+Section zero_or_diverge.
+  Import semantics.stlc.untyped.
+  Definition zero_or_diverge : val := λ: "n", "n" "n" (λ: "m", Ω).
+
+  Lemma zero_or_diverge_zero :
+    rtc step (zero_or_diverge (enc_nat 0)) (enc_nat 0).
+  Proof.
+    eapply rtc_l.
+    { econstructor. done. }
+    simpl. eapply rtc_l.
+    { econstructor; first done.
+      econstructor. done.
+    }
+    simpl. eapply rtc_l.
+    { econstructor. done. }
+    simpl. reflexivity.
+  Qed.
+
+  Lemma zero_or_diverge_nonzero n :
+    rtc step (zero_or_diverge (enc_nat (S n))) Ω.
+  Proof.
+    eapply rtc_l.
+    { econstructor. done. }
+    simpl. eapply rtc_l.
+    { econstructor; first done.
+      econstructor. done.
+    }
+    simpl. eapply rtc_l.
+    { econstructor. done. }
+    simpl. eapply rtc_l.
+    { econstructor.
+      rewrite !(subst_closed_nil (enc_nat _)); [by auto | | ].
+      all: apply enc_nat_closed.
+    }
+    simpl. reflexivity.
+  Qed.
+End zero_or_diverge.
+
+(** ** Exercise 3: Scott encodings *)
+Section scott.
+  Import semantics.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_enc (v1 v2 : val) : val := λ: "d", "d" v1 v2.
+  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.stlc.types.
+
+(** ** Exercise 4: 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 5: 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.
+
+(** 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 6: 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.
+
+Fixpoint infer_type (Γ: gmap string type) E :=
+  match E with
+  | EVar x => Γ !! x
+  | 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 (BNamed x) A E =>
+    match infer_type (<[x := A]> Γ) E with
+    | Some B => Some (Fun A B)
+    | None => None
+    end
+  | ELam BAnon A E => None
+  end.
+
+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 7: untypable, safe term *)
+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.