Release warmup sheet

_CoqProject

@@ -0,0 +1,16 @@
+-Q theories/lib semantics.lib
+-Q theories/type_systems semantics.ts
+# We sometimes want to locally override notation, and there is no good way to do that with scopes.
+-arg -w -arg -notation-overridden
+# Cannot use non-canonical projections as it causes massive unification failures
+# (https://github.com/coq/coq/issues/6294).
+-arg -w -arg -redundant-canonical-projection
+# we use Restart for demoing purposes, sometimes
+-arg -w -arg -undo-batch-mode
+
+# library stuff
+theories/lib/maps.v
+theories/lib/sets.v
+
+# By removing the # below, you can add the exercise sheets to make
+#theories/type_systems/warmup/warmup.v

theories/lib/maps.v

@@ -0,0 +1,284 @@
+From stdpp Require Import gmap.
+From stdpp Require Export relations orders.
+From semantics.lib Require Export sets.
+
+(** * Finite maps *)
+(** This file provides lemmas on finite maps (functions with a finite domain) [gmap].
+  The stdpp library provides a definitions and lemmas on finite maps [gmap], but states lemmas axiomatically in terms of the [FinMap] typeclass, which may make them hard to read for novice users of stdpp.
+  We therefore instantiate the most important lemmas specifically for [gmap] to make the statements easier to comprehend.
+
+  The most important operations are:
+   - the empty map ∅ contains no elements
+   - the singleton map {[ i := v ]} defines a singleton map that maps key i to value v
+   - the insert operation <[ i := v ]> m inserts the association i ↦ v to the map m, overriding any mappings for i in m
+   - the delete operatin delete i m deletes the mapping for key i from m
+   - the lookup operation m !! i lookups a key i, and yields the optional value associated with i
+   - the fmap operation f <$> m maps a function f over all values stored in the map
+   - the subset relation m1 ⊆ m2 states that all associations of map m1 are also included in map m2
+   - the dom operation dom m yields a finite set ([gset]) of the domain of the map
+
+  stdpp's maps satisfy extensional Leibniz equality -- that is, two maps X and Y are equal (X = Y) iff they represent the same finite function.
+ *)
+
+Section map.
+  (* keys need to be countable, i.e., have an injection into positive integers *)
+  Context {K} {A B : Type} `{Countable K}.
+  Implicit Types (m : gmap K A).
+
+  Definition gmap := gmap.
+  #[global]
+  Arguments gmap _ {_ _}.
+
+  Lemma lookup_empty i : (∅ : gmap K A) !! i = None.
+  Proof. apply lookup_empty. Qed.
+
+  Lemma lookup_fmap (f : A → B) (m : gmap K A) i : (f <$> m) !! i = f <$> m !! i.
+  Proof. apply lookup_fmap. Qed.
+  Lemma map_fmap_mono (f : A → B) m1 m2 : m1 ⊆ m2 → f <$> m1 ⊆ f <$> m2.
+  Proof. apply map_fmap_mono. Qed.
+  Lemma fmap_insert (f : A → B) m i x : f <$> <[i := x]> m = <[i := f x]> (f <$> m).
+  Proof. apply fmap_insert. Qed.
+  Lemma fmap_empty (f : A → B) : f <$> (∅ : gmap K A) = ∅.
+  Proof. apply fmap_empty. Qed.
+  Lemma map_fmap_compose {C} (f : A → B) (g : B → C) m : g ∘ f <$> m = g <$> (f <$> m).
+  Proof. apply map_fmap_compose. Qed.
+  Lemma map_fmap_ext (f1 f2 : A → B) m :
+    (∀ i x, m !! i = Some x → f1 x = f2 x) →
+    f1 <$> m = f2 <$> m.
+  Proof. apply map_fmap_ext. Qed.
+
+  Lemma map_eq_iff m1 m2 : m1 = m2 ↔ ∀ i, m1 !! i = m2 !! i.
+  Proof. apply map_eq_iff. Qed.
+  Lemma map_subseteq_spec m1 m2 :
+    m1 ⊆ m2 ↔ ∀ i x, m1 !! i = Some x → m2 !! i = Some x.
+  Proof. apply map_subseteq_spec. Qed.
+  Lemma lookup_weaken m1 m2 i x :
+    m1 !! i = Some x → m1 ⊆ m2 → m2 !! i = Some x.
+  Proof. apply lookup_weaken. Qed.
+  Lemma lookup_weaken_is_Some m1 m2 i :
+    is_Some (m1 !! i) → m1 ⊆ m2 → is_Some (m2 !! i).
+  Proof. apply lookup_weaken_is_Some. Qed.
+  Lemma lookup_weaken_None m1 m2 i :
+    m2 !! i = None → m1 ⊆ m2 → m1 !! i = None.
+  Proof. apply lookup_weaken_None. Qed.
+  Lemma lookup_weaken_inv m1 m2 i x y :
+    m1 !! i = Some x → m1 ⊆ m2 → m2 !! i = Some y → x = y.
+  Proof. apply lookup_weaken_inv. Qed.
+  Lemma lookup_ne m i j : m !! i ≠ m !! j → i ≠ j.
+  Proof. apply lookup_ne. Qed.
+  Lemma map_empty m : m = ∅ ↔ ∀ i, m !! i = None.
+  Proof. apply map_empty. Qed.
+  Lemma lookup_empty_is_Some i : ¬is_Some ((∅ : gmap K A) !! i).
+  Proof. apply lookup_empty_is_Some. Qed.
+  Lemma lookup_empty_Some i (x : A) : ¬(∅ : gmap K A) !! i = Some x.
+  Proof. apply lookup_empty_Some. Qed.
+  Lemma map_empty_subseteq m : ∅ ⊆ m.
+  Proof. apply map_empty_subseteq. Qed.
+
+
+  Lemma lookup_delete m i : delete i m !! i = None.
+  Proof. apply lookup_delete. Qed.
+  Lemma lookup_delete_ne m i j : i ≠ j → delete i m !! j = m !! j.
+  Proof. apply lookup_delete_ne. Qed.
+  Lemma lookup_delete_Some m i j y :
+    delete i m !! j = Some y ↔ i ≠ j ∧ m !! j = Some y.
+  Proof. apply lookup_delete_Some. Qed.
+  Lemma lookup_delete_is_Some m i j :
+    is_Some (delete i m !! j) ↔ i ≠ j ∧ is_Some (m !! j).
+  Proof. apply lookup_delete_is_Some. Qed.
+  Lemma lookup_delete_None m i j :
+    delete i m !! j = None ↔ i = j ∨ m !! j = None.
+  Proof. apply lookup_delete_None. Qed.
+  Lemma delete_empty i : delete i ∅ = (∅ : gmap K A).
+  Proof. apply delete_empty. Qed.
+  Lemma delete_commute m i j :
+    delete i (delete j m) = delete j (delete i m).
+  Proof. apply delete_commute. Qed.
+  Lemma delete_insert_ne m i j x :
+    i ≠ j → delete i (<[j:=x]>m) = <[j:=x]>(delete i m).
+  Proof. apply delete_insert_ne. Qed.
+  Lemma delete_notin m i : m !! i = None → delete i m = m.
+  Proof. apply delete_notin. Qed.
+  Lemma delete_idemp m i :
+    delete i (delete i m) = delete i m.
+  Proof. apply delete_idemp. Qed.
+  Lemma delete_insert m i x :
+    m !! i = None → delete i (<[i:=x]>m) = m.
+  Proof. apply delete_insert. Qed.
+  Lemma delete_insert_delete m i x :
+    delete i (<[i:=x]>m) = delete i m.
+  Proof. apply delete_insert_delete. Qed.
+  Lemma delete_subseteq m i : delete i m ⊆ m.
+  Proof. apply delete_subseteq. Qed.
+  Lemma delete_mono m1 m2 i : m1 ⊆ m2 → delete i m1 ⊆ delete i m2.
+  Proof. apply delete_mono. Qed.
+
+  (** ** Properties of the [insert] operation *)
+  Lemma lookup_insert m i x : <[i:=x]>m !! i = Some x.
+  Proof. apply lookup_insert. Qed.
+  Lemma lookup_insert_rev m i x y : <[i:=x]>m !! i = Some y → x = y.
+  Proof. apply lookup_insert_rev. Qed.
+  Lemma lookup_insert_ne m i j x : i ≠ j → <[i:=x]>m !! j = m !! j.
+  Proof. apply lookup_insert_ne. Qed.
+  Lemma insert_insert m i x y : <[i:=x]>(<[i:=y]>m) = <[i:=x]>m.
+  Proof. apply insert_insert. Qed.
+  Lemma insert_commute m i j x y :
+    i ≠ j → <[i:=x]>(<[j:=y]>m) = <[j:=y]>(<[i:=x]>m).
+  Proof. apply insert_commute. Qed.
+  Lemma lookup_insert_Some m i j x y :
+    <[i:=x]>m !! j = Some y ↔ (i = j ∧ x = y) ∨ (i ≠ j ∧ m !! j = Some y).
+  Proof. apply lookup_insert_Some. Qed.
+  Lemma lookup_insert_is_Some m i j x :
+    is_Some (<[i:=x]>m !! j) ↔ i = j ∨ i ≠ j ∧ is_Some (m !! j).
+  Proof. apply lookup_insert_is_Some. Qed.
+  Lemma lookup_insert_None m i j x :
+    <[i:=x]>m !! j = None ↔ m !! j = None ∧ i ≠ j.
+  Proof. apply lookup_insert_None. Qed.
+  Lemma insert_id m i x : m !! i = Some x → <[i:=x]>m = m.
+  Proof. apply insert_id. Qed.
+  Lemma insert_non_empty m i x : <[i:=x]>m ≠ ∅.
+  Proof. apply insert_non_empty. Qed.
+  Lemma insert_delete_insert m i x : <[i:=x]>(delete i m) = <[i:=x]> m.
+  Proof. apply insert_delete_insert. Qed.
+  Lemma insert_delete m i x :
+    m !! i = Some x → <[i:=x]> (delete i m) = m.
+  Proof. apply insert_delete. Qed.
+
+  Lemma insert_subseteq m i x : m !! i = None → m ⊆ <[i:=x]>m.
+  Proof. apply insert_subseteq. Qed.
+  Lemma insert_mono m1 m2 i x : m1 ⊆ m2 → <[i:=x]> m1 ⊆ <[i:=x]>m2.
+  Proof. apply insert_mono. Qed.
+  Lemma insert_subseteq_r m1 m2 i x :
+    m1 !! i = None → m1 ⊆ m2 → m1 ⊆ <[i:=x]>m2.
+  Proof. apply insert_subseteq_r. Qed.
+  Lemma insert_subseteq_l m1 m2 i x :
+    m2 !! i = Some x → m1 ⊆ m2 → <[i:=x]> m1 ⊆ m2.
+  Proof. apply insert_subseteq_l. Qed.
+
+  Lemma insert_delete_subseteq m1 m2 i x :
+    m1 !! i = None → <[i:=x]> m1 ⊆ m2 → m1 ⊆ delete i m2.
+  Proof. apply insert_delete_subseteq. Qed.
+  Lemma delete_insert_subseteq m1 m2 i x :
+    m1 !! i = Some x → delete i m1 ⊆ m2 → m1 ⊆ <[i:=x]> m2.
+  Proof. apply delete_insert_subseteq. Qed.
+
+  Lemma map_delete_subseteq (k : K) m :
+    delete k m ⊆ m.
+  Proof.
+    apply map_subseteq_spec.
+    intros i x. rewrite lookup_delete_Some. intros [ ]; done.
+  Qed.
+
+  Lemma insert_union_singleton_l (k : K) m x :
+    <[ k := x ]> m = {[ k := x ]} ∪ m.
+  Proof. apply insert_union_singleton_l. Qed.
+  Lemma insert_union_singleton_r (k : K) m x :
+    m !! k = None → <[ k := x ]> m = m ∪ {[ k := x ]}.
+  Proof. apply insert_union_singleton_r. Qed.
+
+  Lemma lookup_union_Some_l m1 m2 (k : K) x :
+    m1 !! k = Some x → (m1 ∪ m2) !! k = Some x.
+  Proof. apply lookup_union_Some_l. Qed.
+  Lemma lookup_union_r m1 m2 (k : K) :
+    m1 !! k = None → (m1 ∪ m2) !! k = m2 !! k.
+  Proof. apply lookup_union_r. Qed.
+
+  (** map disjoint *)
+  Definition map_disjoint := @map_disjoint K (gmap K) _ A.
+  Lemma map_disjoint_spec m1 m2 :
+    m1 ##ₘ m2 ↔ ∀ i x y, m1 !! i = Some x → m2 !! i = Some y → False.
+  Proof. apply map_disjoint_spec. Qed.
+  Lemma map_disjoint_alt m1 m2 :
+    m1 ##ₘ m2 ↔ ∀ i, m1 !! i = None ∨ m2 !! i = None.
+  Proof. apply map_disjoint_alt. Qed.
+  Lemma map_not_disjoint m1 m2 :
+    ¬m1 ##ₘ m2 ↔ ∃ i x1 x2, m1 !! i = Some x1 ∧ m2 !! i = Some x2.
+  Proof. apply map_not_disjoint. Qed.
+  Global Instance map_disjoint_sym : Symmetric (map_disjoint).
+  Proof. apply map_disjoint_sym. Qed.
+  Lemma map_disjoint_empty_l m : ∅ ##ₘ m.
+  Proof. apply map_disjoint_empty_l. Qed.
+  Lemma map_disjoint_empty_r m : m ##ₘ ∅.
+  Proof. apply map_disjoint_empty_r. Qed.
+
+  (** Domain *)
+  Definition dom := @base.dom (gmap K A) (gset K) _.
+
+  Lemma elem_of_dom m i : i ∈ dom m ↔ is_Some (m !! i).
+  Proof. apply elem_of_dom. Qed.
+
+
+  Lemma elem_of_dom_2 m i x : m !! i = Some x → i ∈ dom m.
+  Proof. apply elem_of_dom_2. Qed.
+  Lemma not_elem_of_dom m i : i ∉ dom m ↔ m !! i = None.
+  Proof. apply not_elem_of_dom. Qed.
+  Lemma subseteq_dom m1 m2 : m1 ⊆ m2 → dom m1 ⊆ dom m2.
+  Proof. apply subseteq_dom. Qed.
+
+  Lemma dom_empty : dom ∅ = ∅.
+  Proof. apply dom_empty_L. Qed.
+  Lemma dom_empty_iff m : dom m = ∅ ↔ m = ∅.
+  Proof. apply dom_empty_iff_L. Qed.
+
+  Lemma dom_insert m i x : dom (<[i:=x]>m) = {[ i ]} ∪ dom m.
+  Proof. apply dom_insert_L. Qed.
+  Lemma dom_insert_lookup m i x :
+    is_Some (m !! i) → dom (<[i:=x]>m) = dom m.
+  Proof. apply dom_insert_lookup_L. Qed.
+  Lemma dom_insert_subseteq m i x : dom m ⊆ dom (<[i:=x]>m).
+  Proof. apply dom_insert_subseteq. Qed.
+
+
+  Lemma dom_singleton (i : K) (x : A) : dom ({[i := x]} : gmap K A) = {[ i ]}.
+  Proof. apply dom_singleton_L. Qed.
+  Lemma dom_delete m i : dom (delete i m) = dom m ∖ {[ i ]}.
+  Proof. apply dom_delete_L. Qed.
+
+  Lemma dom_fmap f m : dom (f <$> m) = dom m.
+  Proof. apply dom_fmap_L. Qed.
+
+  (** difference *)
+  (* TODO: upstream? *)
+  Lemma map_difference_mono m1 m2 m3 :
+    m1 ⊆ m2 →
+    m1 ∖ m3 ⊆ m2 ∖ m3.
+  Proof.
+    intros ?. apply map_subseteq_spec.
+    intros i x. rewrite !lookup_difference_Some.
+    intros [? ?]; split; [ | done]. by eapply map_subseteq_spec.
+  Qed.
+
+  (* Upstream? *)
+  Lemma map_difference_union' m1 m2 m3 :
+    m1 ##ₘ m2 →
+    (m1 ∪ m2) ∖ m3 = (m1 ∖ m3) ∪ (m2 ∖ m3).
+  Proof.
+    intros Hdisj. apply map_eq.
+    intros i. destruct (((m1 ∪ m2) ∖ m3) !! i) as [ s | ] eqn:Hlook.
+    - apply lookup_difference_Some in Hlook as [Hlook1 Hlook2].
+      apply lookup_union_Some in Hlook1; [ | done].
+      symmetry. apply lookup_union_Some.
+      { eapply map_disjoint_weaken; [ done | | ]; apply map_subseteq_difference_l; done. }
+      destruct Hlook1 as [ Hlook1 | Hlook1]; [left | right]; apply lookup_difference_Some; done.
+    - symmetry. apply lookup_difference_None in Hlook as [ Hlook | Hlook].
+      + apply lookup_union_None in Hlook as [ ? ?].
+        apply lookup_union_None; split; apply lookup_difference_None; eauto.
+      + apply lookup_union_None; split; apply lookup_difference_None; eauto.
+  Qed.
+
+  (* TODO: upstream the first inclusion as a lemma? *)
+  Lemma map_disjoint_difference m1 m2 :
+    m1 ##ₘ m2 →
+    m1 = m1 ∖ m2.
+  Proof.
+    intros Hdisj. apply (partial_order_anti_symm (R := (⊆))).
+    - apply map_subseteq_spec.
+      intros i x Hlook. apply lookup_difference_Some. split; [done | ].
+      by eapply map_disjoint_Some_l.
+    - by apply map_subseteq_difference_l.
+  Qed.
+
+End map.
+
+Infix "##ₘ" := map_disjoint (at level 70) : stdpp_scope.
+Global Hint Extern 0 (_ ##ₘ _) => symmetry; eassumption : core.

theories/lib/sets.v

@@ -0,0 +1,137 @@
+From stdpp Require Import gmap.
+From stdpp Require Export relations orders.
+
+(** * Finite sets *)
+(** This file provides lemmas on finite sets [gset].
+  The stdpp library provides a definitions and lemmas on finite sets [gset], but states lemmas axiomatically in terms of the [FinSet] typeclass, which may make them hard to read for novice users of stdpp.
+  We therefore instantiate the most important lemmas specifically for [gset] to make the statements easier to comprehend.
+
+  The most important operations are:
+   - the empty set ∅ defines a set with no elements
+   - the singleton set {[ x ]} defines a singleton set
+   - the union operation X ∪ Y represents the union of two sets
+   - the intersection operation X ∩ Y represents the union of two sets
+   - the difference operation X ∖ Y represents the difference (Note: this is NOT a backslash. Pay attention to use the right unicode symbol.)
+   - the subset predicate X ⊆ Y states that X is a subset of Y
+   - the element predicate x ∈ X states that x is an element of X
+   - the elements operation elements X gives a duplicate-free list of elements of X
+
+  stdpp's sets satisfy extensional Leibniz equality -- that is, two sets X and Y are equal (X = Y) iff they contain the same elements.
+ *)
+
+Section sets.
+  Context {K} {A : Type} `{Countable K}.
+
+  Definition gset := gset.
+  #[global]
+  Arguments gset _ {_ _}.
+
+  Implicit Types (X Y : gset K).
+
+  Lemma elem_of_singleton x y : x ∈ ({[ y ]} : gset K) ↔ x = y.
+  Proof. apply elem_of_singleton. Qed.
+  Lemma elem_of_union X Y x : x ∈ X ∪ Y ↔ x ∈ X ∨ x ∈ Y.
+  Proof. apply elem_of_union. Qed.
+  Lemma elem_of_intersection X Y x : x ∈ X ∩ Y ↔ x ∈ X ∧ x ∈ Y.
+  Proof. apply elem_of_intersection. Qed.
+  Lemma elem_of_difference X Y x : x ∈ X ∖ Y ↔ x ∈ X ∧ x ∉ Y.
+  Proof. apply elem_of_difference. Qed.
+
+  Lemma elem_of_elements X x : x ∈ elements X ↔ x ∈ X.
+  Proof. apply elem_of_elements. Qed.
+  Lemma elements_empty : elements (∅ : gset K) = [].
+  Proof. apply elements_empty. Qed.
+  Lemma elements_empty_iff X : elements X = [] ↔ X = ∅.
+  Proof. rewrite elements_empty_iff. by rewrite leibniz_equiv_iff. Qed.
+
+  Lemma set_equiv X Y : X = Y ↔ ∀ x, x ∈ X ↔ x ∈ Y.
+  Proof. set_solver. Qed.
+  Lemma set_equiv_subseteq X Y : X = Y ↔ X ⊆ Y ∧ Y ⊆ X.
+  Proof. set_solver. Qed.
+
+  (** Subset relation *)
+  Lemma subseteq_union X Y : X ⊆ Y ↔ X ∪ Y = Y.
+  Proof. set_solver. Qed.
+  Lemma subseteq_union_1 X Y : X ⊆ Y → X ∪ Y = Y.
+  Proof. by rewrite subseteq_union. Qed.
+  Lemma subseteq_union_2 X Y : X ∪ Y = Y → X ⊆ Y.
+  Proof. by rewrite subseteq_union. Qed.
+
+  Lemma union_subseteq_l X Y : X ⊆ X ∪ Y.
+  Proof. set_solver. Qed.
+  Lemma union_subseteq_l' X X' Y : X ⊆ X' → X ⊆ X' ∪ Y.
+  Proof. set_solver. Qed.
+  Lemma union_subseteq_r X Y : Y ⊆ X ∪ Y.
+  Proof. set_solver. Qed.
+  Lemma union_subseteq_r' X Y Y' : Y ⊆ Y' → Y ⊆ X ∪ Y'.
+  Proof. set_solver. Qed.
+  Lemma union_least X Y Z : X ⊆ Z → Y ⊆ Z → X ∪ Y ⊆ Z.
+  Proof. set_solver. Qed.
+
+  Lemma elem_of_subseteq X Y : X ⊆ Y ↔ ∀ x, x ∈ X → x ∈ Y.
+  Proof. done. Qed.
+  Lemma elem_of_subset X Y : X ⊂ Y ↔ (∀ x, x ∈ X → x ∈ Y) ∧ ¬(∀ x, x ∈ Y → x ∈ X).
+  Proof. set_solver. Qed.
+  Lemma elem_of_weaken x X Y : x ∈ X → X ⊆ Y → x ∈ Y.
+  Proof. set_solver. Qed.
+
+  Lemma not_elem_of_weaken x X Y : x ∉ Y → X ⊆ Y → x ∉ X.
+  Proof. set_solver. Qed.
+
+  (** Union *)
+  Lemma union_subseteq X Y Z : X ∪ Y ⊆ Z ↔ X ⊆ Z ∧ Y ⊆ Z.
+  Proof. set_solver. Qed.
+  Lemma not_elem_of_union x X Y : x ∉ X ∪ Y ↔ x ∉ X ∧ x ∉ Y.
+  Proof. set_solver. Qed.
+  Lemma elem_of_union_l x X Y : x ∈ X → x ∈ X ∪ Y.
+  Proof. set_solver. Qed.
+  Lemma elem_of_union_r x X Y : x ∈ Y → x ∈ X ∪ Y.
+  Proof. set_solver. Qed.
+  Lemma union_mono_l X Y1 Y2 : Y1 ⊆ Y2 → X ∪ Y1 ⊆ X ∪ Y2.
+  Proof. set_solver. Qed.
+  Lemma union_mono_r X1 X2 Y : X1 ⊆ X2 → X1 ∪ Y ⊆ X2 ∪ Y.
+  Proof. set_solver. Qed.
+  Lemma union_mono X1 X2 Y1 Y2 : X1 ⊆ X2 → Y1 ⊆ Y2 → X1 ∪ Y1 ⊆ X2 ∪ Y2.
+  Proof. set_solver. Qed.
+
+  Lemma empty_union X Y : X ∪ Y = ∅ ↔ X = ∅ ∧ Y = ∅.
+  Proof. set_solver. Qed.
+
+  (** Empty *)
+  Lemma empty_subseteq X : ∅ ⊆ X.
+  Proof. set_solver. Qed.
+  Lemma elem_of_equiv_empty X : X = ∅ ↔ ∀ x, x ∉ X.
+  Proof. set_solver. Qed.
+  Lemma elem_of_empty x : x ∈ (∅ : gset K) ↔ False.
+  Proof. set_solver. Qed.
+  Lemma equiv_empty X : X ⊆ ∅ → X = ∅.
+  Proof. set_solver. Qed.
+  Lemma union_positive_l X Y : X ∪ Y ≡ ∅ → X ≡ ∅.
+  Proof. set_solver. Qed.
+  Lemma union_positive_l_alt X Y : X ≢ ∅ → X ∪ Y ≢ ∅.
+  Proof. set_solver. Qed.
+  Lemma non_empty_inhabited x X : x ∈ X → X ≢ ∅.
+  Proof. set_solver. Qed.
+
+  (** Singleton *)
+  Lemma elem_of_singleton_1 x y : x ∈ ({[y]} : gset K) → x = y.
+  Proof. by rewrite elem_of_singleton. Qed.
+  Lemma elem_of_singleton_2 x y : x = y → x ∈ ({[y]} : gset K).
+  Proof. by rewrite elem_of_singleton. Qed.
+  Lemma elem_of_subseteq_singleton x X : x ∈ X ↔ {[ x ]} ⊆ X.
+  Proof. set_solver. Qed.
+  Lemma non_empty_singleton x : ({[ x ]} : gset K) ≠ ∅.
+  Proof. set_solver. Qed.
+  Lemma not_elem_of_singleton x y : x ∉ ({[ y ]} : gset K) ↔ x ≠ y.
+  Proof. by rewrite elem_of_singleton. Qed.
+  Lemma not_elem_of_singleton_1 x y : x ∉ ({[ y ]} : gset K) → x ≠ y.
+  Proof. apply not_elem_of_singleton. Qed.
+  Lemma not_elem_of_singleton_2 x y : x ≠ y → x ∉ ({[ y ]} : gset K).
+  Proof. apply not_elem_of_singleton. Qed.
+
+  Lemma singleton_subseteq_l x X : {[ x ]} ⊆ X ↔ x ∈ X.
+  Proof. set_solver. Qed.
+  Lemma singleton_subseteq x y : ({[ x ]} : gset K) ⊆ {[ y ]} ↔ x = y.
+  Proof. set_solver. Qed.
+
+End sets.

theories/type_systems/warmup/warmup.v

@@ -0,0 +1,154 @@
+(* 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 :=
+  (* TODO: write the function *)
+  0.
+
+(** 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.
+
+ (* We can use our nice notation to write expressions!
+    (note the [%E] to tell Coq to parse this as an arithmetical expression with the
+    notations we just defined).
+  *)
+ Check (Const 5 + Const 5)%E.
+ (* The notation also still works for [Z] and [nat]: *)
+ Check (5 + 5)%Z.
+ Check (5 + 5).
+
+ (* As an exercise, rephrase the following lemmas using the newly defined notation *)
+
+Lemma expr_eval_test: expr_eval (Plus (Const (-4)) (Const 5)) = 1%Z.
+Proof.
+  (* should be solved by:  simpl. lia. *)
+  (* TODO: exercise *)
+Admitted.
+
+
+Lemma plus_eval_comm e1 e2 :
+  expr_eval (Plus e1 e2) = expr_eval (Plus e2 e1).
+Proof.
+  (* TODO: exercise *)
+Admitted.
+
+Lemma plus_syntax_not_comm :
+  Plus (Const 0) (Const 1) ≠ Plus (Const 1) (Const 0).
+Proof.
+  (* TODO: exercise *)
+Admitted.
+
+
+(** 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. *)
+    admit.
+  - done.
+  - (* Locate the notation for && by typing: Locate "&&". Then search for the right lemmas.*)
+    admit.
+  - admit.
+Admitted.
+
+(* 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.
+  (* TODO: exercise *)
+Admitted.
+
+
+(* 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.
+  (* TODO: exercise *)
+Admitted.
+