Try (and fail) the first exercise

closes #1

README.md

@@ -49,6 +49,9 @@ make -j4
 ```
 **IMPORTANT:** You will have to compile to interactively do proofs. You will have to recompile if the dependencies of the file your editing change.
 
+By default, the exercise proofs won't be compiled by the above command.
+You can still work on them interactively, but if you want `make` to check them, you can uncomment the respective lines in the `_CoqProject` file. (We do not add them by default, so `make' will not complain if your proofs of an old exercise do not work.)
+
 
 ## Editing the Coq code
 To edit the Coq code and complete the exercises, you will need an editor. We recommend you use [CoqIDE](https://coq.inria.fr/refman/practical-tools/coqide.html) or [VsCoq](https://github.com/coq-community/vscoq) ([VSCode](https://code.visualstudio.com/)).

_CoqProject

@@ -12,5 +12,11 @@
 theories/lib/maps.v
 theories/lib/sets.v
 
+# STLC
+theories/type_systems/stlc/lang.v
+theories/type_systems/stlc/notation.v
+
 # By removing the # below, you can add the exercise sheets to make
 theories/type_systems/warmup/warmup.v
+#theories/type_systems/warmup/warmup_sol.v
+#theories/type_systems/stlc/exercises01.v

theories/type_systems/stlc/exercises01.v

@@ -0,0 +1,321 @@
+From stdpp Require Import gmap base relations tactics.
+From iris Require Import prelude.
+From semantics.ts.stlc Require Import lang notation.
+
+(** Exercise 2 (LN Exercise 1): Deterministic Operational Semantics *)
+
+Lemma val_no_step e e':
+  step e e' → is_val e → False.
+Proof.
+  by destruct 1.
+Qed.
+
+(* Note how the above lemma is another way to phrase the statement "values
+ * cannot step" that doesn't need inversion. It can also be used to prove the
+ * phrasing we had to use inversion for in the lecture: *)
+Lemma val_no_step' (v : val) (e : expr) :
+  step v e -> False.
+Proof.
+  intros H. eapply val_no_step; first eassumption.
+  apply is_val_val.
+Qed.
+
+
+(* You might find the following tactic useful,
+   which derives a contradiction when you have a [step e1 e2] assumption and
+   [e1] is a value.
+
+   Example:
+   H1: step e e'
+   H2: is_val e
+   =====================
+   ???
+
+   Then [val_no_step.] will solve the goal by applying the [val_no_step] lemma.
+
+   (We neither expect you to understand how exactly the tactic does this nor to
+   be able to write such a tactic yourself. Where useful, we will always
+   provide you with custom tactics and explain in a comment what they do.) *)
+Ltac val_no_step :=
+  match goal with
+  | [H: step ?e1 ?e2 |- _] =>
+    solve [exfalso; eapply (val_no_step _ _ H); done]
+  end.
+
+(* Lemma app_eq e1 e2 e3 e4:
+  (App e1 e2) = (App e3 e4) → e1 = e3 ∧ e2 = e4.
+Proof.
+
+  intro h.
+  split.
+  injection h as hnm.
+  assumption.
+  injection h as hnm.
+  assumption.
+Qed. *)
+
+Lemma step_det e e' e'':
+  step e e' → step e e'' → e' = e''.
+Proof.
+  intros H_step H_step'.
+
+  (*
+    `induction` here seems to introduce incorrect induction hypothesis for IH_λ, IH_v, IH_a, IH_b. Those try to prove that e' = e'', when I need them to prove other equalities later introduced by `inversion H_step`.
+
+    When swapping `inversion H_step` and `induction e`,
+    the number of things to prove jumps to 30, and I do not know how to quickly prove the incorrect ones.
+    `inversion e` doesn't introduce any induction hypothesis, so it is also out of the question.
+  *)
+  induction e as [
+    name |
+    name body |
+    e_λ IH_λ e_v IH_v |
+    n |
+    a IH_a b IH_b
+  ].
+  - inversion H_step.
+  - inversion H_step.
+  - inversion H_step.
+    {
+      rewrite <-H in H_step'.
+      inversion H_step'.
+      - reflexivity.
+      - inversion H7.
+      - val_no_step.
+    }
+    {
+      inversion H_step'.
+      - rewrite <-H4 in H3.
+        inversion H3.
+      - admit.
+      - val_no_step.
+    }
+    {
+      inversion H_step'.
+      - val_no_step.
+      - val_no_step.
+      - admit.
+    }
+  - inversion H_step.
+  - inversion H_step.
+    {
+      rewrite <-H in H_step'.
+      rewrite <-H1 in H_step'.
+      inversion H_step'.
+      - rewrite <-H6.
+        rewrite <-H2.
+        reflexivity.
+      - val_no_step.
+      - val_no_step.
+    }
+    {
+      inversion H_step'.
+      - rewrite <-H4 in H3.
+        val_no_step.
+      - admit.
+      - val_no_step.
+    }
+    {
+      inversion H_step'.
+      - rewrite <-H5 in H2.
+        val_no_step.
+      - val_no_step.
+      - admit.
+    }
+Admitted.
+
+
+(** Exercise 3 (LN Exercise 2): Call-by-name Semantics *)
+Inductive cbn_step : expr → expr → Prop :=
+  | CBNStepBeta x e e'  :
+      cbn_step (App (Lam x e) e') (subst' x e' e)
+      (* TODO: add more constructors *)
+.
+
+(* We make the eauto tactic aware of the constructors of cbn_step *)
+#[global] Hint Constructors cbn_step : core.
+
+Lemma different_results :
+  ∃ (e: expr) (e1 e2: expr), rtc cbn_step e e1 ∧ rtc step e e2 ∧ is_val e1 ∧ is_val e2 ∧ e1 ≠ e2.
+Proof.
+  (* TODO: exercise *)
+Admitted.
+
+
+Lemma val_no_cbn_step e e':
+  cbn_step e e' → is_val e →  False.
+Proof.
+  (* TODO: exercise *)
+Admitted.
+
+
+(* Same tactic as [val_no_step] but for cbn_step.*)
+Ltac val_no_cbn_step :=
+  match goal with
+  | [H: cbn_step ?e1 ?e2 |- _] =>
+    solve [exfalso; eapply (val_no_cbn_step _ _ H); done]
+  end.
+
+Lemma cbn_step_det e e' e'':
+  cbn_step e e' → cbn_step e e'' → e' = e''.
+Proof.
+  (* TODO: exercise *)
+Admitted.
+
+
+
+(** Exercise 4 (LN Exercise 3): Reflexive Transitive Closure *)
+Section rtc.
+  Context {X : Type}.
+
+  Inductive rtc (R : X → X → Prop) : X → X → Prop :=
+    | rtc_base x : rtc R x x
+    | rtc_step x y z : R x y → rtc R y z → rtc R x z.
+
+  Lemma rtc_reflexive R : Reflexive (rtc R).
+  Proof.
+    unfold Reflexive.
+    (* TODO: exercise *)
+  Admitted.
+
+  Lemma rtc_transitive R : Transitive (rtc R).
+  Proof.
+    unfold Transitive.
+    (* TODO: exercise *)
+  Admitted.
+
+
+  Lemma rtc_subrel (R: X → X → Prop) (x y : X): R x y → rtc R x y.
+  Proof.
+    (* TODO: exercise *)
+  Admitted.
+
+
+  Section typeclass.
+    (* We can use Coq's typeclass mechanism to enable the use of the [transitivity] and [reflexivity] tactics on our goals.
+       Typeclasses enable easy extensions of existing mechanisms -- in this case, by telling Coq to use the knowledge about our definition of [rtc].
+     *)
+    (* [Transitive] is a typeclass. With [Instance] we provide an instance of it. *)
+    Global Instance rtc_transitive_inst R : Transitive (rtc R).
+  Proof.
+    apply rtc_transitive.
+  Qed.
+  Global Instance rtc_reflexive_inst R : Reflexive (rtc R).
+  Proof.
+    apply rtc_reflexive.
+  Qed.
+  End typeclass.
+End rtc.
+
+(* Let's put this to the test! *)
+Goal rtc step (LitInt 42) (LitInt 42).
+Proof.
+  (* this uses the [rtc_reflexive_inst] instance we registered. *)
+  reflexivity.
+Qed.
+Goal rtc step (LitInt 32 + (LitInt 5 + LitInt 5)%E)%E (LitInt 42).
+Proof.
+  (* this uses the [rtc_transitive_inst] instance we registered. *)
+  etransitivity.
+  + eapply rtc_step; eauto. reflexivity.
+  + eapply rtc_step; eauto. reflexivity.
+Qed.
+
+Section stdpp.
+  (* In fact, [rtc] is so common that it is already provided by the [stdpp] library! *)
+  Import stdpp.relations.
+  Print rtc.
+
+  (* The typeclass instances are also already registered. *)
+  Goal rtc step (LitInt 42) (LitInt 42).
+  Proof. reflexivity. Qed.
+End stdpp.
+
+(* Start by proving these lemmas. Understand why they are useful. *)
+Lemma plus_right e1 e2 e2':
+  rtc step e2 e2' → rtc step (Plus e1 e2) (Plus e1 e2').
+Proof.
+  (* TODO: exercise *)
+Admitted.
+
+
+Lemma plus_left e1 e1' n:
+  rtc step e1 e1' → rtc step (Plus e1 (LitInt n)) (Plus e1' (LitInt n)).
+Proof.
+  (* TODO: exercise *)
+Admitted.
+
+
+(* The exercise: *)
+Lemma plus_to_consts e1 e2 n m:
+  rtc step e1 (LitInt n) → rtc step e2 (LitInt m) → rtc step (e1 + e2)%E (LitInt (n + m)%Z).
+Proof.
+  (* TODO: exercise *)
+Admitted.
+
+
+
+
+(* Now that you have an understanding of how rtc works, we can make eauto aware of it. *)
+#[local] Hint Constructors rtc : core.
+
+(* See its power here: *)
+Lemma plus_right_eauto e1 e2 e2':
+  rtc step e2 e2' → rtc step (Plus e1 e2) (Plus e1 e2').
+Proof.
+  induction 1; eauto.
+Abort.
+
+(** Exercise 5 (LN Exercise 4): Big-step vs small-step semantics *)
+
+
+Lemma big_step_steps e v :
+  big_step e v → rtc step e (of_val v).
+Proof.
+  (* TODO: exercise *)
+Admitted.
+
+
+
+Lemma steps_big_step e (v: val):
+  rtc step e v → big_step e v.
+Proof.
+  (* Note how there is a coercion (automatic conversion) hidden in the
+   * statement of this lemma: *)
+  Set Printing Coercions.
+  (* It is sometimes very useful to temporarily print coercions if rewrites or
+   * destructs do not behave as expected. *)
+  Unset Printing Coercions.
+  (* TODO: exercise *)
+Admitted.
+
+
+
+(** Exercise 6 (LN Exercise 5): left-to-right evaluation *)
+Inductive ltr_step : expr → expr → Prop := .
+
+#[global] Hint Constructors ltr_step : core.
+
+Lemma different_steps_ltr_step :
+  ∃ (e: expr) (e1 e2: expr), ltr_step e e1 ∧ step e e2 ∧ e1 ≠ e2.
+Proof.
+  (* TODO: exercise *)
+Admitted.
+
+
+
+
+Lemma big_step_ltr_steps e v :
+  big_step e v → rtc ltr_step e (of_val v).
+Proof.
+  (* TODO: exercise *)
+Admitted.
+
+
+
+
+Lemma ltr_steps_big_step e (v: val):
+  rtc ltr_step e v → big_step e v.
+Proof.
+  (* TODO: exercise *)
+Admitted.

theories/type_systems/stlc/lang.v

@@ -0,0 +1,320 @@
+From stdpp Require Export binders strings.
+From stdpp Require Import options.
+From semantics.lib Require Import maps.
+
+(** * Simply Typed Lambda Calculus *)
+
+(** ** Expressions and values. *)
+(** [Z] is Coq's version of the integers.
+    All the standard operations, like [+], are defined on it.
+
+    The type [binder] is defined as [x ::= BNamed (s: string) | BAnon]
+    where BAnon can be used if we don't want to use the variable in
+    the function.
+*)
+Inductive expr :=
+  (* Base lambda calculus *)
+  | Var (x : string)
+  | Lam (x : binder) (e : expr)
+  | App (e1 e2 : expr)
+  (* Base types and their operations *)
+  | LitInt (n: Z)
+  | Plus (e1 e2 : expr).
+
+Inductive val :=
+  | LitIntV (n: Z)
+  | LamV (x : binder) (e : expr).
+
+(* Injections into expr *)
+Definition of_val (v : val) : expr :=
+  match v with
+  | LitIntV n => LitInt n
+  | LamV x e => Lam x e
+  end.
+
+(* try to make an expr into a val *)
+Definition to_val (e : expr) : option val :=
+  match e with
+  | LitInt n => Some (LitIntV n)
+  | Lam x e => Some (LamV x e)
+  | _ => None
+  end.
+
+Lemma to_of_val v : to_val (of_val v) = Some v.
+Proof.
+  destruct v; simpl; reflexivity.
+Qed.
+
+Lemma of_to_val e v : to_val e = Some v → of_val v = e.
+Proof.
+  destruct e; simpl; try congruence.
+  all: injection 1 as <-; simpl; reflexivity.
+Qed.
+
+(* Inj is a type class for injective functions.
+   It is defined as:
+    [Inj R S f := ∀ x y, S (f x) (f y) → R x y]
+*)
+#[export] Instance of_val_inj : Inj (=) (=) of_val.
+Proof. by intros ?? Hv; apply (inj Some); rewrite <-!to_of_val, Hv. Qed.
+
+(* A predicate which holds true whenever an
+   expression is a value. *)
+Definition is_val (e : expr) : Prop :=
+  match e with
+  | LitInt n => True
+  | Lam x e => True
+  | _ => False
+  end.
+Lemma is_val_spec e : is_val e ↔ ∃ v, to_val e = Some v.
+Proof.
+  destruct e; simpl.
+  (* naive_solver is an automation tactic like intuition, firstorder, auto, ...
+     It is provided by the stdpp library. *)
+  all: naive_solver.
+Qed.
+
+(* values are values *)
+Lemma is_val_of_val v : is_val (of_val v).
+Proof.
+  destruct v; simpl; done.
+  Restart.
+  apply is_val_spec. rewrite to_of_val. eauto.
+Qed.
+
+Definition is_val_val := is_val_of_val.
+
+(* A small tactic that simplifies handling values. *)
+Ltac simplify_val :=
+  repeat match goal with
+  | H: to_val (of_val ?v) = ?o |- _ => rewrite to_of_val in H
+  | H: is_val ?e |- _ => destruct (proj1 (is_val_spec e) H) as (? & ?); clear H
+  end.
+
+(* we tell eauto to use the lemma is_val_of_val *)
+#[global]
+Hint Immediate is_val_of_val : core.
+
+
+(** ** Operational Semantics *)
+
+(** *** Substitution *)
+Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
+  match e with
+  | LitInt n => LitInt n
+  (* The function [decide] can be used to decide propositions.
+    [decide P] is of type {P} + {¬ P}.
+    It can only be applied to propositions for which, by type class inference,
+    it can be determined that the proposition is decidable. *)
+  | Var y => if decide (x = y) then es else Var y
+  | Lam y e =>
+      Lam y $ if decide (BNamed x = y) then e else subst x es e
+  | App e1 e2 => App (subst x es e1) (subst x es e2)
+  | Plus e1 e2 => Plus (subst x es e1) (subst x es e2)
+  end.
+
+(* We lift substitution to binders. *)
+Definition subst' (mx : binder) (es : expr) : expr → expr :=
+  match mx with BNamed x => subst x es | BAnon => id end.
+
+
+(** *** Small-Step Semantics *)
+(* We use right-to-left evaluation order,
+   which means in a binary term (e.g., e1 + e2),
+   the left side can only be reduced once the right
+   side is fully evaluated (i.e., is a value). *)
+Inductive step : expr → expr → Prop :=
+  | StepBeta x e e' :
+      is_val e' →
+      step (App (Lam x e) e') (subst' x e' e)
+  | StepAppL e1 e1' e2 :
+    is_val e2 →
+    step e1 e1' →
+    step (App e1 e2) (App e1' e2)
+  | StepAppR e1 e2 e2' :
+    step e2 e2' →
+    step (App e1 e2) (App e1 e2')
+  | StepPlusRed (n1 n2 n3: Z) :
+    (n1 + n2)%Z = n3 →
+    step (Plus (LitInt n1) (LitInt n2)) (LitInt n3)
+  | StepPlusL e1 e1' e2 :
+    is_val e2 →
+    step e1 e1' →
+    step (Plus e1 e2) (Plus e1' e2)
+  | StepPlusR e1 e2 e2' :
+    step e2 e2' →
+    step (Plus e1 e2) (Plus e1 e2').
+
+(* We make the tactic eauto aware of the constructors of [step].
+   Then it can automatically solve goals where we want to prove a step. *)
+#[global] Hint Constructors step : core.
+
+
+(* A term is reducible, if it can take a step. *)
+Definition reducible (e : expr) :=
+  ∃ e', step e e'.
+
+
+(** *** Big-Step Semantics *)
+Inductive big_step : expr → val → Prop :=
+  | bs_lit (n : Z) :
+      big_step (LitInt n) (LitIntV n)
+  | bs_lam (x : binder) (e : expr) :
+      big_step (Lam x e) (LamV x e)
+  | 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
+    .
+#[export] Hint Constructors big_step : core.
+
+
+Lemma big_step_vals (v: val): big_step (of_val v) v.
+Proof.
+  induction v; econstructor.
+Qed.
+
+Lemma big_step_inv_vals (v w: val): big_step (of_val v) w → v = w.
+Proof.
+  destruct v; inversion 1; eauto.
+Qed.
+
+
+(** *** Contextual Semantics *)
+(** Base reduction *)
+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).
+
+Inductive ectx :=
+  | HoleCtx
+  | AppLCtx (K: ectx) (v2 : val)
+  | AppRCtx (e1 : expr) (K: ectx)
+  | PlusLCtx (K: ectx) (v2 : val)
+  | PlusRCtx (e1 : expr) (K: ectx).
+
+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)
+  end.
+
+(* filling a context with another context *)
+Fixpoint comp_ectx (Ko Ki: ectx) :=
+  match Ko with
+  | HoleCtx => Ki
+  | AppLCtx K v2 => AppLCtx (comp_ectx K Ki) v2
+  | AppRCtx e1 K => AppRCtx e1 (comp_ectx K Ki)
+  | PlusLCtx K v2 => PlusLCtx (comp_ectx K Ki) v2
+  | PlusRCtx e1 K => PlusRCtx e1 (comp_ectx K Ki)
+  end.
+
+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.
+
+Definition contextual_reducible (e : expr) :=
+  ∃ e', contextual_step e e'.
+
+#[export] Hint Constructors base_step : core.
+#[export] Hint Constructors contextual_step : core.
+(* Lemmas about the contextual semantics *)
+Definition empty_ectx := HoleCtx.
+
+Lemma fill_empty e : fill empty_ectx e = e.
+Proof. done. 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_comp (K1 K2 : ectx) e : fill K1 (fill K2 e) = fill (comp_ectx K1 K2) e.
+Proof. induction K1; simpl; congruence. 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.
+
+
+(** Open and closed expressions *)
+Fixpoint is_closed (X : list string) (e : expr) : bool :=
+  match e with
+  | Var x => bool_decide (x ∈ X)
+  | Lam x e => is_closed (x :b: X) e
+  | LitInt _ => true
+  | App e1 e2
+  | Plus e1 e2 => is_closed X e1 && is_closed X e2
+  end.
+
+Notation closed X e := (Is_true (is_closed X e)).
+#[export] Instance closed_proof_irrel X e : ProofIrrel (closed X e).
+Proof. unfold closed. apply _. Qed.
+#[export] Instance closed_dec X e : Decision (closed X e).
+Proof. unfold closed. apply _. Defined.
+
+Lemma closed_weaken X Y e : closed X e → X ⊆ Y → closed Y e.
+Proof. revert X Y; induction e; naive_solver (eauto; set_solver). Qed.
+
+Lemma closed_weaken_nil X e : closed [] e → closed X e.
+Proof. intros. by apply closed_weaken with [], list_subseteq_nil. Qed.
+
+Lemma closed_subst X Y e x es :
+  closed Y es → closed (x :: X) e → closed (X ++ Y) (subst x es e).
+Proof.
+  induction e as [y|y e IH|e1 e2|n|e1 e2]in X |-*; simpl; intros Hc1 Hc2; eauto.
+  - eapply bool_decide_unpack, elem_of_cons in Hc2 as [->|Hc2].
+    + destruct decide; try congruence. eapply closed_weaken; eauto with set_solver.
+    + destruct decide.
+      * eapply closed_weaken; eauto with set_solver.
+      * simpl. eapply bool_decide_pack. set_solver.
+  - destruct y as [|y]; simpl in *; eauto.
+    destruct decide as [Heq|].
+    + injection Heq as ->. eapply closed_weaken; eauto. set_solver.
+    + rewrite app_comm_cons. eapply IH; eauto.
+      eapply closed_weaken; eauto. set_solver.
+  - eapply andb_True. eapply andb_True in Hc2 as [H1 H2].
+    split; eauto.
+  - eapply andb_True. eapply andb_True in Hc2 as [H1 H2].
+    split; eauto.
+Qed.
+
+Lemma closed_subst_nil X e x es :
+  closed [] es → closed (x :: X) e → closed X (subst x es e).
+Proof.
+  intros Hc1 Hc2. eapply closed_subst in Hc1; eauto.
+  revert Hc1. rewrite right_id; [done|apply _].
+Qed.
+
+Lemma closed_do_subst' X e x es :
+  closed [] es → closed (x :b: X) e → closed X (subst' x es e).
+Proof. destruct x; eauto using closed_subst_nil. Qed.
+
+Lemma subst_closed X e x es : closed X e → x ∉ X → subst x es e = e.
+Proof.
+  induction e in X |-*; simpl; rewrite ?bool_decide_spec, ?andb_True; intros ??;
+    repeat case_decide; simplify_eq; simpl; f_equal; intuition eauto with set_solver.
+Qed.
+
+Lemma subst_closed_nil e x es : closed [] e → subst x es e = e.
+Proof. intros. apply subst_closed with []; set_solver. Qed.

theories/type_systems/stlc/lecture2.v

@@ -0,0 +1,299 @@
+(** * This file was shown during the lecture on 26.10.2023.
+    * It contrains duplicated code that is copy-pasted from e.g. lang.v
+    *)
+
+From stdpp Require Export binders strings.
+From stdpp Require Import options.
+From semantics.lib Require Import maps.
+
+(** * Simply Typed Lambda Calculus *)
+
+(** ** Expressions and values. *)
+(** [Z] is Coq's version of the integers.
+    All the standard operations, like [+], are defined on it.
+
+    The type [binder] is defined as [x ::= BNamed (s: string) | BAnon]
+    where BAnon can be used if we don't want to use the variable in
+    the function.
+*)
+Inductive expr :=
+  (* Base lambda calculus *)
+  | Var (x : string)
+  | Lam (x : binder) (e : expr)
+  | App (e1 e2 : expr)
+  (* Base types and their operations *)
+  | LitInt (n: Z)
+  | Plus (e1 e2 : expr).
+
+Inductive val :=
+  | LitIntV (n: Z)
+  | LamV (x : binder) (e : expr).
+
+(* Injections into expr *)
+Definition of_val (v : val) : expr :=
+  match v with
+  | LitIntV n => LitInt n
+  | LamV x e => Lam x e
+  end.
+
+(* try to make an expr into a val *)
+Definition to_val (e : expr) : option val :=
+  match e with
+  | LitInt n => Some (LitIntV n)
+  | Lam x e => Some (LamV x e)
+  | _ => None
+  end.
+
+Lemma to_of_val v : to_val (of_val v) = Some v.
+Proof.
+  destruct v; simpl; reflexivity.
+Qed.
+
+Lemma of_to_val e v : to_val e = Some v -> of_val v = e.
+Proof.
+  destruct e; simpl; try congruence.
+  all: injection 1 as <-; simpl; reflexivity.
+Qed.
+
+(* Inj is a type class for injective functions.
+   It is defined as:
+    [Inj R S f := ∀ x y, S (f x) (f y) -> R x y]
+*)
+#[export] Instance of_val_inj : Inj (=) (=) of_val.
+Proof. by intros ?? Hv; apply (inj Some); rewrite <-!to_of_val, Hv. Qed.
+
+(* A predicate which holds true whenever an
+   expression is a value. *)
+Definition is_val (e : expr) : Prop :=
+  match e with
+  | LitInt n => True
+  | Lam x e => True
+  | _ => False
+  end.
+Lemma is_val_spec e : is_val e ↔ ∃ v, to_val e = Some v.
+Proof.
+  destruct e; simpl.
+  (* naive_solver is an automation tactic like intuition, firstorder, auto, ...
+     It is provided by the stdpp library. *)
+  all: naive_solver.
+Qed.
+
+Lemma is_val_of_val v : is_val (of_val v).
+Proof.
+  apply is_val_spec. rewrite to_of_val. eauto.
+Qed.
+
+(* A small tactic that simplifies handling values. *)
+Ltac simplify_val :=
+  repeat match goal with
+  | H: to_val (of_val ?v) = ?o |- _ => rewrite to_of_val in H
+  | H: is_val ?e |- _ => destruct (proj1 (is_val_spec e) H) as (? & ?); clear H
+  end.
+
+(* values are values *)
+Lemma is_val_val (v: val): is_val (of_val v).
+Proof.
+  destruct v; simpl; done.
+Qed.
+
+(* we tell eauto to use the lemma is_val_val *)
+#[global]
+Hint Immediate is_val_val : core.
+
+
+(** ** Operational Semantics *)
+
+(** *** Substitution *)
+Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
+  match e with
+  | LitInt n => LitInt n
+  (* The function [decide] can be used to decide propositions.
+    [decide P] is of type {P} + {¬ P}.
+    It can only be applied to propositions for which, by type class inference,
+    it can be determined that the proposition is decidable. *)
+  | Var y => if decide (x = y) then es else Var y
+  | Lam y e =>
+      Lam y $ if decide (BNamed x = y) then e else subst x es e
+  | App e1 e2 => App (subst x es e1) (subst x es e2)
+  | Plus e1 e2 => Plus (subst x es e1) (subst x es e2)
+  end.
+
+(* We lift substitution to binders. *)
+Definition subst' (mx : binder) (es : expr) : expr -> expr :=
+  match mx with BNamed x => subst x es | BAnon => id end.
+
+
+(** *** Small-Step Semantics *)
+(* We use right-to-left evaluation order,
+   which means in a binary term (e.g., e1 + e2),
+   the left side can only be reduced once the right
+   side is fully evaluated (i.e., is a value). *)
+Inductive step : expr -> expr -> Prop :=
+  | StepBeta x e e'  :
+      is_val e' ->
+      step (App (Lam x e) e') (subst' x e' e)
+  | StepAppL e1 e1' e2 :
+    is_val e2 ->
+    step e1 e1' ->
+    step (App e1 e2) (App e1' e2)
+  | StepAppR e1 e2 e2' :
+    step e2 e2' ->
+    step (App e1 e2) (App e1 e2')
+  | StepPlusRed (n1 n2 n3: Z) :
+    (n1 + n2)%Z = n3 ->
+    step (Plus (LitInt n1) (LitInt n2)) (LitInt n3)
+  | StepPlusL e1 e1' e2 :
+    is_val e2 ->
+    step e1 e1' ->
+    step (Plus e1 e2) (Plus e1' e2)
+  | StepPlusR e1 e2 e2' :
+    step e2 e2' ->
+    step (Plus e1 e2) (Plus e1 e2').
+
+(* We make the tactic eauto aware of the constructors of [step].
+   Then it can automatically solve goals where we want to prove a step. *)
+#[global] Hint Constructors step : core.
+
+
+(* A term is reducible, if it can take a step. *)
+Definition reducible (e : expr) :=
+  ∃ e', step e e'.
+
+
+(** *** Big-Step Semantics *)
+Inductive big_step : expr -> val -> Prop :=
+  | bs_lit (n : Z) :
+      big_step (LitInt n) (LitIntV n)
+  | bs_lam (x : binder) (e : expr) :
+      big_step (Lam x e) (LamV x e)
+  | 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
+    .
+#[export] Hint Constructors big_step : core.
+
+
+Lemma big_step_vals (v: val): big_step (of_val v) v.
+Proof.
+  induction v; econstructor.
+Qed.
+
+
+
+
+
+
+(*** Inversion ***)
+
+
+
+(* We might want to show the following lemma about small step semantics: *)
+Lemma val_no_step (v : val) (e : expr) :
+  step (of_val v) e -> False.
+Proof.
+  (* destructing doesn't work: the different cases don't have enough information *)
+  destruct 1.
+  - admit.
+  - admit.
+    Restart.
+  remember (of_val v) as e' eqn:Heq.
+  destruct 1.
+  - (* Aha! Coq remembered that we had a value on the left-hand sidde of the
+       step *)
+    destruct v; discriminate.
+  - destruct v; discriminate.
+  - destruct v; discriminate.
+  - destruct v; discriminate.
+  - destruct v; discriminate.
+  - destruct v; discriminate.
+  Restart.
+  (* there's a tactic that does this for us: inversion *)
+  inversion 1.
+  all: destruct v; discriminate.
+Qed.
+
+
+(* The (non-recursive) eliminator for step in Coq *)
+Lemma step_elim (P : expr -> expr -> Prop) :
+           (∀ (x : binder) (e1 e2 : expr), is_val e2 ->               
+                                             P (App (Lam x e1) e2) (subst' x e2 e1))
+         -> (∀ e1 e1' e2 : expr,           is_val e2 -> step e1 e1' -> 
+                                             P (App e1 e2) (App e1' e2))
+         -> (∀ e1 e2 e2' : expr,           step e2 e2' -> 
+                                             P (App e1 e2) (App e1 e2'))
+         -> (∀ n1 n2 n3 : Z,               (n1 + n2)%Z = n3 ->        
+                                             P (Plus (LitInt n1) (LitInt n2)) (LitInt n3))
+         -> (∀ e1 e1' e2 : expr,           is_val e2 -> step e1 e1' -> 
+                                             P (Plus e1 e2) (Plus e1' e2))
+         -> (∀ e1 e2 e2' : expr,           step e2 e2' -> P (Plus e1 e2) (Plus e1 e2'))
+         
+  
+         -> ∀ e e' : expr, step e e' -> P e e'.
+Proof.
+  destruct 7; eauto.
+Qed.
+
+
+(* An inversion operator for step in Coq *)
+Lemma step_inversion (P : expr -> expr -> Prop) (e e' : expr) :
+           (∀ (x : binder) (e1 e2 : expr), e = App (Lam x e1) e2 -> e' = subst' x e2 e1 -> 
+                                             is_val e2 ->               
+                                             P (App (Lam x e1) e2) (subst' x e2 e1))
+         -> (∀ e1 e1' e2 : expr,           e = App e1 e2 -> e' = App e1' e2 -> 
+                                             is_val e2 -> step e1 e1' -> 
+                                             P (App e1 e2) (App e1' e2))
+         -> (∀ e1 e2 e2' : expr,           e = App e1 e2 -> e' = App e1 e2' ->
+                                             step e2 e2' -> 
+                                             P (App e1 e2) (App e1 e2'))
+         -> (∀ n1 n2 n3 : Z,               e = Plus (LitInt n1) (LitInt n2) -> e' = LitInt n3 -> 
+                                             (n1 + n2)%Z = n3 ->        
+                                             P (Plus (LitInt n1) (LitInt n2)) (LitInt n3))
+         -> (∀ e1 e1' e2 : expr,           e = Plus e1 e2 -> e' = Plus e1' e2 ->
+                                             is_val e2 -> step e1 e1' -> 
+                                             P (Plus e1 e2) (Plus e1' e2))
+         -> (∀ e1 e2 e2' : expr,           e = Plus e1 e2 -> e' = Plus e1 e2' -> 
+                                             step e2 e2' -> 
+                                             P (Plus e1 e2) (Plus e1 e2'))
+         -> step e e' -> P e e'.
+Proof.
+  intros H1 H2 H3 H4 H5 H6.
+  destruct 1.
+  { eapply H1. all: easy. }
+  { eapply H2. all: easy. }
+  (* All the other cases are similar. *)
+  all: eauto.
+Qed.
+
+
+(* We can use the inversion operator to show that values cannot step. *)
+Lemma val_no_step' (v : val) (e : expr) :
+  step (of_val v) e -> False.
+Proof.
+  intros H. eapply step_inversion. 7: eauto.
+  all: intros; destruct v; discriminate.
+Qed.
+
+
+
+(* The following is another kind of inversion operator, as taught in the ICL lecture. *)
+Definition step_inv (e e' : expr) :  step e e' -> 
+  (match e with
+   | App e1 e2 => 
+       (∃ x f, e1 = (Lam x f) ∧ e' = subst' x e2 f) ∨ 
+       (∃ e1', is_val e2 ∧ step e1 e1') ∨ 
+       (∃ e2', step e2 e2')
+   | Plus e1 e2 => 
+       (∃ n1 n2, e1 = LitInt n1 ∧ e2 = LitInt n2 ∧ LitInt (n1 + n2) = e') ∨ 
+       (∃ e1', is_val e2 ∧ step e1 e1') ∨ 
+       (∃ e2', step e2 e2')
+   | _ => False
+                                        end).
+Proof.
+  intros H. destruct H; naive_solver.
+Qed.

theories/type_systems/stlc/notation.v

@@ -0,0 +1,49 @@
+From semantics.ts.stlc Require Export lang.
+Set Default Proof Using "Type".
+
+
+(* We declare two notation scopes, one for values and one for expressions.
+   Afterwards, we add notations to them, which then do not interfere with
+   any existing Coq notations. *)
+Declare Scope expr_scope.
+Declare Scope val_scope.
+Delimit Scope expr_scope with E.
+Delimit Scope val_scope with V.
+Bind Scope expr_scope with expr.
+Bind Scope val_scope with val.
+
+(* Values can be embedded into expressions with of_val
+   and integers into expressions with LitInt. The following
+   coercions allow us to omit the embeddings. With them
+   (e1 v2 n3) desugars to (e3 (of_val v2) (LitInt n1)). *)
+Coercion of_val : val >-> expr.
+Coercion LitInt : Z >-> expr.
+Coercion LitIntV : Z >-> val.
+Coercion App : expr >-> Funclass.
+Coercion Var : string >-> expr.
+
+Notation "e1 + e2" := (Plus e1%E e2%E) : expr_scope.
+
+(* The breaking point '/  ' makes sure that the body of the λ: is indented
+by two spaces in case the whole λ: does not fit on a single line. *)
+Notation "λ: x , e" := (Lam x%binder e%E)
+  (at level 200, x at level 1, e at level 200,
+   format "'[' 'λ:'  x ,  '/  ' e ']'") : expr_scope.
+Notation "λ: x y .. z , e" := (Lam x%binder (Lam y%binder .. (Lam z%binder e%E) ..))
+  (at level 200, x, y, z at level 1, e at level 200,
+   format "'[' 'λ:'  x  y  ..  z ,  '/  ' e ']'") : expr_scope.
+
+Notation "λ: x , e" := (LamV x%binder e%E)
+  (at level 200, x at level 1, e at level 200,
+   format "'[' 'λ:'  x ,  '/  ' e ']'") : val_scope.
+Notation "λ: x y .. z , e" := (LamV x%binder (Lam y%binder .. (Lam z%binder e%E) .. ))
+  (at level 200, x, y, z at level 1, e at level 200,
+   format "'[' 'λ:'  x  y  ..  z ,  '/  ' e ']'") : val_scope.
+
+Notation "'let:' x := e1 'in' e2" := (Lam x%binder e2%E e1%E)
+  (only parsing, at level 200, x at level 1, e1, e2 at level 200
+  (*, format "'[' 'let:'  x  :=  '[' e1 ']'  'in'  '/' e2 ']'" *)
+  ) : expr_scope.
+Notation "e1 ;; e2" := (Lam BAnon e2%E e1%E)
+  (at level 100, e2 at level 200,
+   format "'[' '[hv' '[' e1 ']' ;;  ']' '/' e2 ']'") : expr_scope.

theories/type_systems/warmup/warmup_sol.v

@@ -0,0 +1,166 @@
+(* Throughout the course, we will be using the [stdpp] library to provide
+   some useful and common features.
+   We will introduce you to its features as we need them.
+ *)
+From stdpp Require Import base tactics numbers strings.
+From stdpp Require relations.
+From semantics.lib Require Import maps.
+
+(** * Exercise sheet 0 *)
+
+(* We are using Coq's notion of integers, [Z].
+   All the standard operations, like [+] and [*], are defined on it.
+ *)
+Inductive expr :=
+  | Const (z : Z)
+  | Plus (e1 e2 : expr)
+  | Mul (e1 e2 : expr).
+
+(** Exercise 1: Arithmetics *)
+Fixpoint expr_eval (e : expr) : Z :=
+  match e with
+  | Const z => z
+  | Plus e1 e2 => (expr_eval e1) + (expr_eval e2)
+  | Mul e1 e2 => (expr_eval e1) * (expr_eval e2)
+  end.
+
+(** Now let's define some notation to make it look nice! *)
+(* We declare a so-called notation scope, so that we can still use the nice notations for addition on natural numbers [nat] and integers [Z]. *)
+Declare Scope expr.
+Delimit Scope expr with E.
+Notation "e1 + e2" := (Plus e1%Z e2%Z) : expr.
+Notation "e1 * e2" := (Mul e1%Z e2%Z) : expr.
+
+ 
+
+Lemma expr_eval_test: expr_eval (Plus (Const (-4)) (Const 5)) = 1%Z.
+Proof.
+  (* should be solved by:  simpl. lia. *)
+  simpl. lia.
+Qed.
+
+Lemma plus_eval_comm e1 e2 :
+  expr_eval (Plus e1 e2) = expr_eval (Plus e2 e1).
+Proof.
+  simpl. lia.
+Qed.
+Lemma plus_syntax_not_comm :
+  Plus (Const 0) (Const 1) ≠ Plus (Const 1) (Const 0).
+Proof.
+  (* [done] is an automation tactic provided by [stdpp] to solve simple goals. *)
+  intros Heq. injection Heq. done.
+Qed.
+
+(** Exercise 2: Open arithmetical expressions *)
+
+(* Finally, we introduce variables into our arithmetic expressions.
+   Variables are of Coq's [string] type.
+ *)
+Inductive expr' :=
+  | Var (x: string)
+  | Const' (z : Z)
+  | Plus' (e1 e2 : expr')
+  | Mul' (e1 e2 : expr').
+
+(* We call an expression closed under the list X,
+  if it only contains variables in X *)
+Fixpoint is_closed (X: list string) (e: expr') : bool :=
+  match e with
+    | Var x => bool_decide (x ∈ X)
+    | Const' z => true
+    | Plus' e1 e2 => is_closed X e1 && is_closed X e2
+    | Mul' e1 e2 => is_closed X e1 && is_closed X e2
+  end.
+
+Definition closed X e := is_closed X e = true.
+
+
+(* Some examples of closed terms. *)
+Lemma example_no_vars_closed:
+  closed [] (Plus' (Const' 3) (Const' 5)).
+Proof.
+  unfold closed. simpl. done.
+Qed.
+
+
+Lemma example_some_vars_closed:
+  closed ["x"; "y"] (Plus' (Var "x") (Var "y")).
+Proof.
+  unfold closed. simpl. done.
+Qed.
+
+Lemma example_not_closed:
+  ¬ closed ["x"] (Plus' (Var "x") (Var "y")).
+Proof.
+  unfold closed. simpl. done.
+Qed.
+
+Lemma closed_mono X Y e:
+  X ⊆ Y → closed X e → closed Y e.
+Proof.
+  unfold closed. intros Hsub; induction e as [ x | z | e1 IHe1 e2 IHe2 | e1 IHe1 e2 IHe2]; simpl.
+  - (* bool_decide is an stdpp function, which can be used to decide simple decidable propositions.
+      Make a search for it to find the right lemmas to complete this subgoal. *)
+    (* Search bool_decide. *)
+    intros ?%bool_decide_eq_true_1. eapply bool_decide_eq_true_2.
+    naive_solver.
+  - done.
+  - (* Locate the notation for && by typing: Locate "&&". Then search for the right lemmas.*)
+    intros [H1 H2]%andb_prop. rewrite IHe1, IHe2; done.
+  - intros [H1 H2]%andb_prop. rewrite IHe1, IHe2; done.
+Qed.
+
+(* we define a substitution operation on open expressions *)
+Fixpoint subst (e: expr') (x: string) (e': expr') : expr' :=
+  match e with
+  | Var y => if (bool_decide (x = y)) then e' else Var y
+  | Const' z => Const' z
+  | Plus' e1 e2 => Plus' (subst e1 x e') (subst e2 x e')
+  | Mul' e1 e2 => Mul' (subst e1 x e') (subst e2 x e')
+  end.
+
+Lemma subst_closed e e' x X:
+  closed X e → ¬ (x ∈ X) → subst e x e' = e.
+Proof.
+  unfold closed. induction e as [ y | z | e1 IHe1 e2 IHe2 | e1 IHe1 e2 IHe2]; simpl.
+  - intros Hel%bool_decide_eq_true_1 Hnel.
+    destruct bool_decide eqn: Heq.
+    + eapply bool_decide_eq_true_1 in Heq. subst.
+      congruence.
+    + done.
+  - done.
+  - intros [Hcl1 Hcl2]%andb_prop Hnel.
+    rewrite IHe1; eauto.
+    rewrite IHe2; eauto.
+  - intros [Hcl1 Hcl2]%andb_prop Hnel.
+    rewrite IHe1; eauto.
+    rewrite IHe2; eauto.
+Qed.
+
+(* To evaluate an arithmetic expression, we define an evaluation function [expr_eval], which maps them to integers.
+   Since our expressions contain variables, we pass a finite map as the argument, which is used to look up variables.
+   The type of finite maps that we use is called [gmap].
+ *)
+Fixpoint expr_eval' (m: gmap string Z) (e : expr') : Z :=
+  match e with
+  | Var x => default 0%Z (m !! x) (* this is the lookup operation on gmaps *)
+  | Const' z => z
+  | Plus' e1 e2 => (expr_eval' m e1) + (expr_eval' m e2)
+  | Mul' e1 e2 => (expr_eval' m e1) * (expr_eval' m e2)
+  end.
+
+(* Prove the following lemma which explains how substitution interacts with evaluation *)
+Lemma eval_subst_extend (m: gmap string Z) e x e':
+  expr_eval' m (subst e x e') = expr_eval' (<[x := expr_eval' m e']> m) e.
+Proof.
+  induction e as [ y | z | e1 IHe1 e2 IHe2 | e1 IHe1 e2 IHe2]; simpl.
+  - destruct bool_decide eqn: Heq.
+    + eapply bool_decide_eq_true_1 in Heq. subst.
+      rewrite lookup_insert. done.
+    + eapply bool_decide_eq_false_1 in Heq.
+      rewrite lookup_insert_ne; [|done].
+      simpl. done.
+  - done.
+  - rewrite IHe1, IHe2. done.
+  - rewrite IHe1, IHe2. done.
+Qed.