Release warmup_sol.v

_CoqProject

@@ -18,4 +18,5 @@ 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

@@ -95,8 +95,6 @@ Section rtc.
     | rtc_base x : rtc R x x
     | rtc_step x y z : R x y → rtc R y z → rtc R x z.
 
-  Goal rtc step ()
-
   Lemma rtc_reflexive R : Reflexive (rtc R).
   Proof.
     unfold Reflexive.

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.