From c5600db874e8732280df631687fc5b5c1494f711 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@csail.mit.edu>
Date: Tue, 21 Mar 2017 19:27:36 -0400
Subject: [PATCH] SubsetTypes

---
 Frap.v                  | 374 +-----------------------
 FrapWithoutSets.v       | 373 +++++++++++++++++++++++
 Map.v                   |  12 +-
 MessagesAndRefinement.v |  10 +-
 ModelCheck.v            |   4 +-
 README.md               |   4 +
 Sets.v                  |  16 +-
 SubsetTypes.v           | 633 ++++++++++++++++++++++++++++++++++++++++
 _CoqProject             |   2 +
 9 files changed, 1038 insertions(+), 390 deletions(-)
 create mode 100644 FrapWithoutSets.v
 create mode 100644 SubsetTypes.v

diff --git a/Frap.v b/Frap.v
index 85687a2..0a6ea17 100644
--- a/Frap.v
+++ b/Frap.v
@@ -1,373 +1,3 @@
-Require Import Eqdep String Arith Omega Program Sets Relations Map Var Invariant Bool ModelCheck.
-Export String Arith Sets Relations Map Var Invariant Bool ModelCheck.
-Require Import List.
-Export List ListNotations.
-Open Scope string_scope.
-Open Scope list_scope.
+Require Export FrapWithoutSets.
 
-Ltac inductN n :=
-  match goal with
-    | [ |- forall x : ?E, _ ] =>
-      match type of E with
-        | Prop =>
-          let H := fresh in intro H;
-            match n with
-              | 1 => dependent induction H
-              | S ?n' => inductN n'
-            end
-        | _ => intro; inductN n
-      end
-  end.
-
-Ltac same_structure x y :=
-  match x with
-  | ?f ?a1 ?b1 ?c1 ?d1 =>
-    match y with
-    | f ?a2 ?b2 ?c2 ?d2 => same_structure a1 a2; same_structure b1 b2; same_structure c1 c2; same_structure d1 d2
-    | _ => fail 2
-    end
-  | ?f ?a1 ?b1 ?c1 =>
-    match y with
-    | f ?a2 ?b2 ?c2 => same_structure a1 a2; same_structure b1 b2; same_structure c1 c2
-    | _ => fail 2
-    end
-  | ?f ?a1 ?b1 =>
-    match y with
-    | f ?a2 ?b2 => same_structure a1 a2; same_structure b1 b2
-    | _ => fail 2
-    end
-  | ?f ?a1 =>
-    match y with
-    | f ?a2 => same_structure a1 a2
-    | _ => fail 2
-    end
-  | _ =>
-    match y with
-    | ?f ?a1 ?b1 ?c1 ?d1 =>
-      match x with
-      | f ?a2 ?b2 ?c2 ?d2 => same_structure a1 a2; same_structure b1 b2; same_structure c1 c2; same_structure d1 d2
-      | _ => fail 2
-      end
-    | ?f ?a1 ?b1 ?c1 =>
-      match x with
-      | f ?a2 ?b2 ?c2 => same_structure a1 a2; same_structure b1 b2; same_structure c1 c2
-      | _ => fail 2
-      end
-    | ?f ?a1 ?b1 =>
-      match x with
-      | f ?a2 ?b2 => same_structure a1 a2; same_structure b1 b2
-      | _ => fail 2
-      end
-    | ?f ?a1 =>
-      match x with
-      | f ?a2 => same_structure a1 a2
-      | _ => fail 2
-      end
-    | _ => idtac
-    end
-  end.
-
-Ltac instantiate_obvious1 H :=
-  match type of H with
-  | _ ++ _ = _ ++ _ -> _ => fail 1
-  | ?x = ?y -> _ =>
-    (same_structure x y; specialize (H eq_refl))
-    || (has_evar (x, y); fail 3)
-  | JMeq.JMeq ?x ?y -> _ =>
-    (same_structure x y; specialize (H JMeq.JMeq_refl))
-    || (has_evar (x, y); fail 3)
-  | forall x : ?T, _ =>
-    match type of T with
-    | Prop => fail 1
-    | _ =>
-      let x' := fresh x in
-      evar (x' : T);
-      let x'' := eval unfold x' in x' in specialize (H x''); clear x';
-        instantiate_obvious1 H
-    end
-  end.
-
-Ltac instantiate_obvious H :=
-  match type of H with
-    | context[@eq string _  _] => idtac
-    | _ => repeat instantiate_obvious1 H
-  end.
-
-Ltac instantiate_obviouses :=
-  repeat match goal with
-         | [ H : _ |- _ ] => instantiate_obvious H
-         end.
-
-Ltac induct e := (inductN e || dependent induction e); instantiate_obviouses.
-
-Ltac invert' H := inversion H; clear H; subst.
-
-Ltac invertN n :=
-  match goal with
-    | [ |- forall x : ?E, _ ] =>
-      match type of E with
-        | Prop =>
-          let H := fresh in intro H;
-            match n with
-              | 1 => invert' H
-              | S ?n' => invertN n'
-            end
-        | _ => intro; invertN n
-      end
-  end.
-
-Ltac invert e := invertN e || invert' e.
-
-Ltac invert0 e := invert e; fail.
-Ltac invert1 e := invert0 e || (invert e; []).
-Ltac invert2 e := invert1 e || (invert e; [|]).
-
-Ltac maps_neq :=
-  match goal with
-  | [ H : ?m1 = ?m2 |- _ ] =>
-    let rec recur E :=
-        match E with
-        | ?E' $+ (?k, _) => 
-          (apply (f_equal (fun m => m $? k)) in H; simpl in *; autorewrite with core in *; simpl in *; congruence)
-          || recur E'
-        end in
-    recur m1 || recur m2
-end.
-
-Ltac fancy_neq :=
-  repeat match goal with
-         | _ => maps_neq
-         | [ H : @eq (nat -> _) _ _ |- _ ] => apply (f_equal (fun f => f 0)) in H
-         | [ H : @eq ?T _ _ |- _ ] =>
-           match eval compute in T with
-           | fmap _ _ => fail 1
-           | _ => invert H
-           end
-         end.
-
-Ltac maps_equal' := progress Frap.Map.M.maps_equal; autorewrite with core; simpl.
-
-Ltac removeDups :=
-  match goal with
-  | [ |- context[constant ?ls] ] =>
-    someMatch ls;
-    erewrite (@removeDups_ok _ ls)
-      by repeat (apply RdNil
-                 || (apply RdNew; [ simpl; intuition (congruence || solve [ fancy_neq ]) | ])
-                 || (apply RdDup; [ simpl; intuition (congruence || (repeat (maps_equal' || f_equal))) | ]))
-  end.
-
-Ltac doSubtract :=
-  match goal with
-  | [ |- context[constant ?ls \setminus constant ?ls0] ] =>
-    erewrite (@doSubtract_ok _ ls ls0)
-      by repeat (apply DsNil
-                 || (apply DsKeep; [ simpl; intuition (congruence || solve [ fancy_neq ]) | ])
-                 || (apply DsDrop; [ simpl; intuition (congruence || (repeat (maps_equal' || f_equal))) | ]))
-  end.
-
-Ltac simpl_maps :=
-  repeat match goal with
-         | [ |- context[add ?m ?k1 ?v $? ?k2] ] =>
-           (rewrite (@lookup_add_ne _ _ m k1 k2 v) by (congruence || omega))
-           || (rewrite (@lookup_add_eq _ _ m k1 k2 v) by (congruence || omega))
-         end.
-
-Ltac simplify := repeat (unifyTails; pose proof I);
-                repeat match goal with
-                       | [ H : True |- _ ] => clear H
-                       end;
-                repeat progress (simpl in *; intros; try autorewrite with core in *; simpl_maps);
-                                 repeat (normalize_set || doSubtract).
-Ltac propositional := intuition idtac.
-
-Ltac linear_arithmetic := intros;
-    repeat match goal with
-           | [ |- context[max ?a ?b] ] =>
-             let Heq := fresh "Heq" in destruct (Max.max_spec a b) as [[? Heq] | [? Heq]];
-               rewrite Heq in *; clear Heq
-           | [ _ : context[max ?a ?b] |- _ ] =>
-             let Heq := fresh "Heq" in destruct (Max.max_spec a b) as [[? Heq] | [? Heq]];
-               rewrite Heq in *; clear Heq
-           | [ |- context[min ?a ?b] ] =>
-             let Heq := fresh "Heq" in destruct (Min.min_spec a b) as [[? Heq] | [? Heq]];
-               rewrite Heq in *; clear Heq
-           | [ _ : context[min ?a ?b] |- _ ] =>
-             let Heq := fresh "Heq" in destruct (Min.min_spec a b) as [[? Heq] | [? Heq]];
-               rewrite Heq in *; clear Heq
-           end; omega.
-
-Ltac equality := intuition congruence.
-
-Ltac cases E :=
-  ((is_var E; destruct E)
-   || match type of E with
-      | {_} + {_} => destruct E
-      | _ => let Heq := fresh "Heq" in destruct E eqn:Heq
-      end);
-  repeat match goal with
-         | [ H : _ = left _ |- _ ] => clear H
-         | [ H : _ = right _ |- _ ] => clear H
-         end.
-
-Global Opaque max min.
-
-Infix "==n" := eq_nat_dec (no associativity, at level 50).
-Infix "<=?" := le_lt_dec.
-
-Export Frap.Map.
-
-Ltac maps_equal := Frap.Map.M.maps_equal; simplify.
-
-Ltac first_order := firstorder idtac.
-
-
-(** * Model checking *)
-
-Lemma eq_iff : forall P Q,
-    P = Q
-    -> (P <-> Q).
-Proof.
-  equality.
-Qed.
-
-Ltac sets0 := Sets.sets ltac:(simpl in *; intuition (subst; auto; try equality; try linear_arithmetic)).
-
-Ltac sets := propositional;
-  try match goal with
-      | [ |- @eq (set _) _ _ ] =>
-        let x := fresh "x" in
-        apply sets_equal; intro x;
-        repeat match goal with
-               | [ H : @eq (set _) _ _ |- _ ] => apply (f_equal (fun f => f x)) in H;
-                                                apply eq_iff in H
-               end
-      end; sets0;
-  try match goal with
-      | [ H : @eq (set ?T) _ _, x : ?T |- _ ] =>
-        repeat match goal with
-               | [ H : @eq (set T) _ _ |- _ ] => apply (f_equal (fun f => f x)) in H;
-                                                 apply eq_iff in H
-               end;
-          solve [ sets0 ]
-      end.
-
-Ltac model_check_invert1 :=
-  match goal with
-  | [ H : ?P |- _ ] =>
-    match type of P with
-    | Prop => invert H;
-              repeat match goal with
-                     | [ H : existT _ ?x _ = existT _ ?x _ |- _ ] =>
-                       apply inj_pair2 in H; subst
-                     end; simplify
-    end
-  end.
-
-Ltac model_check_invert := simplify; subst; repeat model_check_invert1.
-
-Lemma oneStepClosure_solve : forall A (sys : trsys A) I I',
-  oneStepClosure sys I I'
-  -> I = I'
-  -> oneStepClosure sys I I.
-Proof.
-  equality.
-Qed.
-
-Ltac singletoner := try (exfalso; solve [ sets ]);
-  repeat match goal with
-         (* | _ => apply singleton_in *)
-         | [ |- _ ?S ] => idtac S; apply singleton_in
-         | [ |- (_ \cup _) _ ] => apply singleton_in_other
-         end.
-
-Ltac closure :=
-  repeat (apply oneStepClosure_empty
-          || (apply oneStepClosure_split; [ model_check_invert; try equality; solve [ singletoner ] | ])).
-
-Ltac model_check_done :=
-  apply MscDone; eapply oneStepClosure_solve; [ closure | simplify; solve [ sets ] ].
-
-Ltac model_check_step0 :=
-  eapply MscStep; [ closure | simplify ].
-
-Ltac model_check_step :=
-  match goal with
-  | [ |- multiStepClosure _ ?inv1 _ _ ] =>
-    model_check_step0;
-    match goal with
-    | [ |- multiStepClosure _ ?inv2 _ _ ] =>
-      (assert (inv1 = inv2) by compare_sets; fail 3)
-      || idtac
-    end
-  end.
-
-Ltac model_check_steps1 := model_check_step || model_check_done.
-Ltac model_check_steps := repeat model_check_steps1.
-
-Ltac model_check_finish := simplify; propositional; subst; simplify; try equality; try linear_arithmetic.
-
-Ltac model_check_infer :=
-  apply multiStepClosure_ok; simplify; model_check_steps.
-
-Ltac model_check_find_invariant :=
-  simplify; eapply invariant_weaken; [ model_check_infer | ]; cbv beta in *.
-
-Ltac model_check := model_check_find_invariant; model_check_finish.
-
-Inductive ordering (n m : nat) :=
-| Lt (_ : n < m)
-| Eq (_ : n = m)
-| Gt (_ : n > m).
-
-Local Hint Constructors ordering.
-Local Hint Extern 1 (_ < _) => omega.
-Local Hint Extern 1 (_ > _) => omega.
-
-Theorem totally_ordered : forall n m, ordering n m.
-Proof.
-  induction n; destruct m; simpl; eauto.
-  destruct (IHn m); eauto.
-Qed.
-
-Ltac total_ordering N M := destruct (totally_ordered N M).
-
-Ltac inList x xs :=
-  match xs with
-  | (x, _) => true
-  | (_, ?xs') => inList x xs'
-  | _ => false
-  end.
-
-Ltac maybe_simplify_map m found kont :=
-  match m with
-  | @empty ?A ?B => kont (@empty A B)
-  | ?m' $+ (?k, ?v) =>
-    let iL := inList k found in
-    match iL with
-    | true => maybe_simplify_map m' found kont
-    | false =>
-      maybe_simplify_map m' (k, found) ltac:(fun m' => kont (m' $+ (k, v)))
-    end
-  end.
-
-Ltac simplify_map' m found kont :=
-  match m with
-  | ?m' $+ (?k, ?v) =>
-    let iL := inList k found in
-      match iL with
-      | true => maybe_simplify_map m' found kont
-      | false =>
-        simplify_map' m' (k, found) ltac:(fun m' => kont (m' $+ (k, v)))
-      end
-  end.
-
-Ltac simplify_map :=
-  match goal with
-  | [ |- context[@add ?A ?B ?m ?k ?v] ] =>
-    simplify_map' (m $+ (k, v)) tt ltac:(fun m' =>
-                                           replace (@add A B m k v) with m' by maps_equal)
-  end.
-
-Require Import Classical.
-Ltac excluded_middle P := destruct (classic P).
+Module Export SN := SetNotations(FrapWithoutSets).
diff --git a/FrapWithoutSets.v b/FrapWithoutSets.v
new file mode 100644
index 0000000..85687a2
--- /dev/null
+++ b/FrapWithoutSets.v
@@ -0,0 +1,373 @@
+Require Import Eqdep String Arith Omega Program Sets Relations Map Var Invariant Bool ModelCheck.
+Export String Arith Sets Relations Map Var Invariant Bool ModelCheck.
+Require Import List.
+Export List ListNotations.
+Open Scope string_scope.
+Open Scope list_scope.
+
+Ltac inductN n :=
+  match goal with
+    | [ |- forall x : ?E, _ ] =>
+      match type of E with
+        | Prop =>
+          let H := fresh in intro H;
+            match n with
+              | 1 => dependent induction H
+              | S ?n' => inductN n'
+            end
+        | _ => intro; inductN n
+      end
+  end.
+
+Ltac same_structure x y :=
+  match x with
+  | ?f ?a1 ?b1 ?c1 ?d1 =>
+    match y with
+    | f ?a2 ?b2 ?c2 ?d2 => same_structure a1 a2; same_structure b1 b2; same_structure c1 c2; same_structure d1 d2
+    | _ => fail 2
+    end
+  | ?f ?a1 ?b1 ?c1 =>
+    match y with
+    | f ?a2 ?b2 ?c2 => same_structure a1 a2; same_structure b1 b2; same_structure c1 c2
+    | _ => fail 2
+    end
+  | ?f ?a1 ?b1 =>
+    match y with
+    | f ?a2 ?b2 => same_structure a1 a2; same_structure b1 b2
+    | _ => fail 2
+    end
+  | ?f ?a1 =>
+    match y with
+    | f ?a2 => same_structure a1 a2
+    | _ => fail 2
+    end
+  | _ =>
+    match y with
+    | ?f ?a1 ?b1 ?c1 ?d1 =>
+      match x with
+      | f ?a2 ?b2 ?c2 ?d2 => same_structure a1 a2; same_structure b1 b2; same_structure c1 c2; same_structure d1 d2
+      | _ => fail 2
+      end
+    | ?f ?a1 ?b1 ?c1 =>
+      match x with
+      | f ?a2 ?b2 ?c2 => same_structure a1 a2; same_structure b1 b2; same_structure c1 c2
+      | _ => fail 2
+      end
+    | ?f ?a1 ?b1 =>
+      match x with
+      | f ?a2 ?b2 => same_structure a1 a2; same_structure b1 b2
+      | _ => fail 2
+      end
+    | ?f ?a1 =>
+      match x with
+      | f ?a2 => same_structure a1 a2
+      | _ => fail 2
+      end
+    | _ => idtac
+    end
+  end.
+
+Ltac instantiate_obvious1 H :=
+  match type of H with
+  | _ ++ _ = _ ++ _ -> _ => fail 1
+  | ?x = ?y -> _ =>
+    (same_structure x y; specialize (H eq_refl))
+    || (has_evar (x, y); fail 3)
+  | JMeq.JMeq ?x ?y -> _ =>
+    (same_structure x y; specialize (H JMeq.JMeq_refl))
+    || (has_evar (x, y); fail 3)
+  | forall x : ?T, _ =>
+    match type of T with
+    | Prop => fail 1
+    | _ =>
+      let x' := fresh x in
+      evar (x' : T);
+      let x'' := eval unfold x' in x' in specialize (H x''); clear x';
+        instantiate_obvious1 H
+    end
+  end.
+
+Ltac instantiate_obvious H :=
+  match type of H with
+    | context[@eq string _  _] => idtac
+    | _ => repeat instantiate_obvious1 H
+  end.
+
+Ltac instantiate_obviouses :=
+  repeat match goal with
+         | [ H : _ |- _ ] => instantiate_obvious H
+         end.
+
+Ltac induct e := (inductN e || dependent induction e); instantiate_obviouses.
+
+Ltac invert' H := inversion H; clear H; subst.
+
+Ltac invertN n :=
+  match goal with
+    | [ |- forall x : ?E, _ ] =>
+      match type of E with
+        | Prop =>
+          let H := fresh in intro H;
+            match n with
+              | 1 => invert' H
+              | S ?n' => invertN n'
+            end
+        | _ => intro; invertN n
+      end
+  end.
+
+Ltac invert e := invertN e || invert' e.
+
+Ltac invert0 e := invert e; fail.
+Ltac invert1 e := invert0 e || (invert e; []).
+Ltac invert2 e := invert1 e || (invert e; [|]).
+
+Ltac maps_neq :=
+  match goal with
+  | [ H : ?m1 = ?m2 |- _ ] =>
+    let rec recur E :=
+        match E with
+        | ?E' $+ (?k, _) => 
+          (apply (f_equal (fun m => m $? k)) in H; simpl in *; autorewrite with core in *; simpl in *; congruence)
+          || recur E'
+        end in
+    recur m1 || recur m2
+end.
+
+Ltac fancy_neq :=
+  repeat match goal with
+         | _ => maps_neq
+         | [ H : @eq (nat -> _) _ _ |- _ ] => apply (f_equal (fun f => f 0)) in H
+         | [ H : @eq ?T _ _ |- _ ] =>
+           match eval compute in T with
+           | fmap _ _ => fail 1
+           | _ => invert H
+           end
+         end.
+
+Ltac maps_equal' := progress Frap.Map.M.maps_equal; autorewrite with core; simpl.
+
+Ltac removeDups :=
+  match goal with
+  | [ |- context[constant ?ls] ] =>
+    someMatch ls;
+    erewrite (@removeDups_ok _ ls)
+      by repeat (apply RdNil
+                 || (apply RdNew; [ simpl; intuition (congruence || solve [ fancy_neq ]) | ])
+                 || (apply RdDup; [ simpl; intuition (congruence || (repeat (maps_equal' || f_equal))) | ]))
+  end.
+
+Ltac doSubtract :=
+  match goal with
+  | [ |- context[constant ?ls \setminus constant ?ls0] ] =>
+    erewrite (@doSubtract_ok _ ls ls0)
+      by repeat (apply DsNil
+                 || (apply DsKeep; [ simpl; intuition (congruence || solve [ fancy_neq ]) | ])
+                 || (apply DsDrop; [ simpl; intuition (congruence || (repeat (maps_equal' || f_equal))) | ]))
+  end.
+
+Ltac simpl_maps :=
+  repeat match goal with
+         | [ |- context[add ?m ?k1 ?v $? ?k2] ] =>
+           (rewrite (@lookup_add_ne _ _ m k1 k2 v) by (congruence || omega))
+           || (rewrite (@lookup_add_eq _ _ m k1 k2 v) by (congruence || omega))
+         end.
+
+Ltac simplify := repeat (unifyTails; pose proof I);
+                repeat match goal with
+                       | [ H : True |- _ ] => clear H
+                       end;
+                repeat progress (simpl in *; intros; try autorewrite with core in *; simpl_maps);
+                                 repeat (normalize_set || doSubtract).
+Ltac propositional := intuition idtac.
+
+Ltac linear_arithmetic := intros;
+    repeat match goal with
+           | [ |- context[max ?a ?b] ] =>
+             let Heq := fresh "Heq" in destruct (Max.max_spec a b) as [[? Heq] | [? Heq]];
+               rewrite Heq in *; clear Heq
+           | [ _ : context[max ?a ?b] |- _ ] =>
+             let Heq := fresh "Heq" in destruct (Max.max_spec a b) as [[? Heq] | [? Heq]];
+               rewrite Heq in *; clear Heq
+           | [ |- context[min ?a ?b] ] =>
+             let Heq := fresh "Heq" in destruct (Min.min_spec a b) as [[? Heq] | [? Heq]];
+               rewrite Heq in *; clear Heq
+           | [ _ : context[min ?a ?b] |- _ ] =>
+             let Heq := fresh "Heq" in destruct (Min.min_spec a b) as [[? Heq] | [? Heq]];
+               rewrite Heq in *; clear Heq
+           end; omega.
+
+Ltac equality := intuition congruence.
+
+Ltac cases E :=
+  ((is_var E; destruct E)
+   || match type of E with
+      | {_} + {_} => destruct E
+      | _ => let Heq := fresh "Heq" in destruct E eqn:Heq
+      end);
+  repeat match goal with
+         | [ H : _ = left _ |- _ ] => clear H
+         | [ H : _ = right _ |- _ ] => clear H
+         end.
+
+Global Opaque max min.
+
+Infix "==n" := eq_nat_dec (no associativity, at level 50).
+Infix "<=?" := le_lt_dec.
+
+Export Frap.Map.
+
+Ltac maps_equal := Frap.Map.M.maps_equal; simplify.
+
+Ltac first_order := firstorder idtac.
+
+
+(** * Model checking *)
+
+Lemma eq_iff : forall P Q,
+    P = Q
+    -> (P <-> Q).
+Proof.
+  equality.
+Qed.
+
+Ltac sets0 := Sets.sets ltac:(simpl in *; intuition (subst; auto; try equality; try linear_arithmetic)).
+
+Ltac sets := propositional;
+  try match goal with
+      | [ |- @eq (set _) _ _ ] =>
+        let x := fresh "x" in
+        apply sets_equal; intro x;
+        repeat match goal with
+               | [ H : @eq (set _) _ _ |- _ ] => apply (f_equal (fun f => f x)) in H;
+                                                apply eq_iff in H
+               end
+      end; sets0;
+  try match goal with
+      | [ H : @eq (set ?T) _ _, x : ?T |- _ ] =>
+        repeat match goal with
+               | [ H : @eq (set T) _ _ |- _ ] => apply (f_equal (fun f => f x)) in H;
+                                                 apply eq_iff in H
+               end;
+          solve [ sets0 ]
+      end.
+
+Ltac model_check_invert1 :=
+  match goal with
+  | [ H : ?P |- _ ] =>
+    match type of P with
+    | Prop => invert H;
+              repeat match goal with
+                     | [ H : existT _ ?x _ = existT _ ?x _ |- _ ] =>
+                       apply inj_pair2 in H; subst
+                     end; simplify
+    end
+  end.
+
+Ltac model_check_invert := simplify; subst; repeat model_check_invert1.
+
+Lemma oneStepClosure_solve : forall A (sys : trsys A) I I',
+  oneStepClosure sys I I'
+  -> I = I'
+  -> oneStepClosure sys I I.
+Proof.
+  equality.
+Qed.
+
+Ltac singletoner := try (exfalso; solve [ sets ]);
+  repeat match goal with
+         (* | _ => apply singleton_in *)
+         | [ |- _ ?S ] => idtac S; apply singleton_in
+         | [ |- (_ \cup _) _ ] => apply singleton_in_other
+         end.
+
+Ltac closure :=
+  repeat (apply oneStepClosure_empty
+          || (apply oneStepClosure_split; [ model_check_invert; try equality; solve [ singletoner ] | ])).
+
+Ltac model_check_done :=
+  apply MscDone; eapply oneStepClosure_solve; [ closure | simplify; solve [ sets ] ].
+
+Ltac model_check_step0 :=
+  eapply MscStep; [ closure | simplify ].
+
+Ltac model_check_step :=
+  match goal with
+  | [ |- multiStepClosure _ ?inv1 _ _ ] =>
+    model_check_step0;
+    match goal with
+    | [ |- multiStepClosure _ ?inv2 _ _ ] =>
+      (assert (inv1 = inv2) by compare_sets; fail 3)
+      || idtac
+    end
+  end.
+
+Ltac model_check_steps1 := model_check_step || model_check_done.
+Ltac model_check_steps := repeat model_check_steps1.
+
+Ltac model_check_finish := simplify; propositional; subst; simplify; try equality; try linear_arithmetic.
+
+Ltac model_check_infer :=
+  apply multiStepClosure_ok; simplify; model_check_steps.
+
+Ltac model_check_find_invariant :=
+  simplify; eapply invariant_weaken; [ model_check_infer | ]; cbv beta in *.
+
+Ltac model_check := model_check_find_invariant; model_check_finish.
+
+Inductive ordering (n m : nat) :=
+| Lt (_ : n < m)
+| Eq (_ : n = m)
+| Gt (_ : n > m).
+
+Local Hint Constructors ordering.
+Local Hint Extern 1 (_ < _) => omega.
+Local Hint Extern 1 (_ > _) => omega.
+
+Theorem totally_ordered : forall n m, ordering n m.
+Proof.
+  induction n; destruct m; simpl; eauto.
+  destruct (IHn m); eauto.
+Qed.
+
+Ltac total_ordering N M := destruct (totally_ordered N M).
+
+Ltac inList x xs :=
+  match xs with
+  | (x, _) => true
+  | (_, ?xs') => inList x xs'
+  | _ => false
+  end.
+
+Ltac maybe_simplify_map m found kont :=
+  match m with
+  | @empty ?A ?B => kont (@empty A B)
+  | ?m' $+ (?k, ?v) =>
+    let iL := inList k found in
+    match iL with
+    | true => maybe_simplify_map m' found kont
+    | false =>
+      maybe_simplify_map m' (k, found) ltac:(fun m' => kont (m' $+ (k, v)))
+    end
+  end.
+
+Ltac simplify_map' m found kont :=
+  match m with
+  | ?m' $+ (?k, ?v) =>
+    let iL := inList k found in
+      match iL with
+      | true => maybe_simplify_map m' found kont
+      | false =>
+        simplify_map' m' (k, found) ltac:(fun m' => kont (m' $+ (k, v)))
+      end
+  end.
+
+Ltac simplify_map :=
+  match goal with
+  | [ |- context[@add ?A ?B ?m ?k ?v] ] =>
+    simplify_map' (m $+ (k, v)) tt ltac:(fun m' =>
+                                           replace (@add A B m k v) with m' by maps_equal)
+  end.
+
+Require Import Classical.
+Ltac excluded_middle P := destruct (classic P).
diff --git a/Map.v b/Map.v
index 743200e..b097f56 100644
--- a/Map.v
+++ b/Map.v
@@ -64,7 +64,7 @@ Module Type S.
     -> (m1 $++ m2) $? k = m2 $? k.
 
   Axiom join_comm : forall A B (m1 m2 : fmap A B),
-    dom m1 \cap dom m2 = {}
+    dom m1 \cap dom m2 = constant nil
     -> m1 $++ m2 = m2 $++ m1.
 
   Axiom join_assoc : forall A B (m1 m2 m3 : fmap A B),
@@ -116,10 +116,10 @@ Module Type S.
 
   Axiom empty_includes : forall A B (m : fmap A B), empty A B $<= m.
 
-  Axiom dom_empty : forall A B, dom (empty A B) = {}.
+  Axiom dom_empty : forall A B, dom (empty A B) = constant nil.
 
   Axiom dom_add : forall A B (m : fmap A B) (k : A) (v : B),
-    dom (add m k v) = {k} \cup dom m.
+    dom (add m k v) = constant (k :: nil) \cup dom m.
 
   Axiom lookup_restrict_true : forall A B (P : A -> Prop) (m : fmap A B) k,
     P k
@@ -390,7 +390,7 @@ Module M : S.
   Qed.
 
   Theorem join_comm : forall A B (m1 m2 : fmap A B),
-    dom m1 \cap dom m2 = {}
+    dom m1 \cap dom m2 = constant nil
     -> join m1 m2 = join m2 m1.
   Proof.
     intros; apply fmap_ext; unfold join, lookup; intros.
@@ -508,13 +508,13 @@ Module M : S.
     unfold includes, empty; intuition congruence.
   Qed.
 
-  Theorem dom_empty : forall A B, dom (empty (A := A) B) = {}.
+  Theorem dom_empty : forall A B, dom (empty (A := A) B) = constant nil.
   Proof.
     unfold dom, empty; intros; sets idtac.
   Qed.
 
   Theorem dom_add : forall A B (m : fmap A B) (k : A) (v : B),
-    dom (add m k v) = {k} \cup dom m.
+    dom (add m k v) = constant (k :: nil) \cup dom m.
   Proof.
     unfold dom, add; simpl; intros.
     sets ltac:(simpl in *; try match goal with
diff --git a/MessagesAndRefinement.v b/MessagesAndRefinement.v
index 6a6f9d7..a1183ae 100644
--- a/MessagesAndRefinement.v
+++ b/MessagesAndRefinement.v
@@ -10,11 +10,11 @@ Set Asymmetric Patterns.
 
 (** * First, an unexplained tactic that will come in handy.... *)
 
-Ltac invert H := (Frap.invert H || (inversion H; clear H));
-                repeat match goal with
-                       | [ x : _ |- _ ] => subst x
-                       | [ H : existT _ _ _ = existT _ _ _ |- _ ] => apply inj_pair2 in H; try subst
-                       end.
+Ltac invert H := (FrapWithoutSets.invert H || (inversion H; clear H));
+                 repeat match goal with
+                        | [ x : _ |- _ ] => subst x
+                        | [ H : existT _ _ _ = existT _ _ _ |- _ ] => apply inj_pair2 in H; try subst
+                        end.
 
 
 (** * A process algebra: syntax and semantics *)
diff --git a/ModelCheck.v b/ModelCheck.v
index 0ac91ef..ef04754 100644
--- a/ModelCheck.v
+++ b/ModelCheck.v
@@ -75,7 +75,7 @@ Qed.
 Theorem oneStepClosure_split : forall state (sys : trsys state) st sts (inv1 inv2 : state -> Prop),
   (forall st', sys.(Step) st st' -> inv1 st')
   -> oneStepClosure sys (constant sts) inv2
-  -> oneStepClosure sys (constant (st :: sts)) ({st} \cup inv1 \cup inv2).
+  -> oneStepClosure sys (constant (st :: sts)) (constant (st :: nil) \cup inv1 \cup inv2).
 Proof.
   unfold oneStepClosure, oneStepClosure_current, oneStepClosure_new; intuition.
 
@@ -89,7 +89,7 @@ Proof.
 Qed.
 
 Theorem singleton_in : forall {A} (x : A) rest,
-  ({x} \cup rest) x.
+  (constant (x :: nil) \cup rest) x.
 Proof.
   unfold union; simpl; auto.
 Qed.
diff --git a/README.md b/README.md
index 0801854..a617797 100644
--- a/README.md
+++ b/README.md
@@ -28,3 +28,7 @@ The main narrative, also present in the book PDF, presents standard program-proo
 * Chapter 15: `SharedMemory.v`
 * Chapter 16: `ConcurrentSeparationLogic.v`
 * Chapter 17: `MessagesAndRefinement.v`
+
+There are also two supplementary files that are independent of the main narrative, for introducing programming with dependent types, a distinctive Coq feature that we neither use nor recommend for the problem sets, but which many students find interesting (and useful in other contexts).
+* `SubsetTypes.v`: a first introduction to dependent types by attaching predicates to normal types (used after `CompilerCorrectness.v` in the last course offering)
+* One more coming soon
diff --git a/Sets.v b/Sets.v
index 315e787..447751f 100644
--- a/Sets.v
+++ b/Sets.v
@@ -35,8 +35,6 @@ Section set.
 End set.
 
 Infix "\in" := In (at level 70).
-Notation "{ }" := (constant nil).
-Notation "{ x1 , .. , xN }" := (constant (cons x1 (.. (cons xN nil) ..))).
 Notation "[ P ]" := (check P).
 Infix "\cup" := union (at level 40).
 Infix "\cap" := intersection (at level 40).
@@ -45,6 +43,14 @@ Infix "\subseteq" := subseteq (at level 70).
 Infix "\subset" := subset (at level 70).
 Notation "[ x | P ]" := (scomp (fun x => P)).
 
+Module Type EMPTY.
+End EMPTY.
+Module SetNotations(M : EMPTY).
+  Notation "{ }" := (constant nil).
+  Notation "{ x1 , .. , xN }" := (constant (cons x1 (.. (cons xN nil) ..))).
+End SetNotations.
+
+
 Ltac sets' tac :=
   unfold In, constant, universe, check, union, intersection, minus, complement, subseteq, subset, scomp in *;
     tauto || intuition tac.
@@ -288,7 +294,7 @@ Section setexpr.
     match e with
     | Literal vs =>
       match env with
-      | [] => {}
+      | [] => constant []
       | x :: _ => constant (map (nth_default x env) vs)
       end
     | Constant s => s
@@ -339,7 +345,7 @@ Section setexpr.
 
   Definition interp_normal_form (env : list A) (nf : normal_form) : set A :=
     let cs := match env with
-              | [] => {}
+              | [] => constant []
               | x :: _ => constant (map (nth_default x env) nf.(Elements))
               end in
     match nf.(Other) with
@@ -557,7 +563,7 @@ Ltac quote E env k :=
             quote' E2 env' ltac:(fun e2 env'' =>
               k (Union e1 e2) env''))
         | _ =>
-          (let pf := constr:(eq_refl : E = {}) in
+          (let pf := constr:(eq_refl : E = constant []) in
            k (Literal A []) env)
           || k (Constant E) env
         end in
diff --git a/SubsetTypes.v b/SubsetTypes.v
new file mode 100644
index 0000000..7c3fe32
--- /dev/null
+++ b/SubsetTypes.v
@@ -0,0 +1,633 @@
+(** Formal Reasoning About Programs <http://adam.chlipala.net/frap/>
+  * Supplementary Coq material: subset types
+  * Author: Adam Chlipala
+  * License: https://creativecommons.org/licenses/by-nc-nd/4.0/
+  * Much of the material comes from CPDT <http://adam.chlipala.net/cpdt/> by the same author. *)
+
+Require Import FrapWithoutSets.
+(* We import a pared-down version of the book library, to avoid notations that
+ * clash with some we want to use here. *)
+
+Set Implicit Arguments.
+Set Asymmetric Patterns.
+(* Compatibility flag that affects pattern matching for fancy types *)
+
+
+(* So far, we have seen many examples of what we might call "classical program
+ * verification."  We write programs, write their specifications, and then prove
+ * that the programs satisfy their specifications.  The programs that we have
+ * written in Coq have been normal functional programs that we could just as
+ * well have written in Haskell or ML.  In this lecture, we start investigating
+ * uses of _dependent types_ to integrate programming, specification, and
+ * proving into a single phase.  The techniques we will learn make it possible
+ * to reduce the cost of program verification dramatically. *)
+
+
+(** * Introducing Subset Types *)
+
+(** Let us consider several ways of implementing the natural-number-predecessor
+ * function.  We start by displaying the definition from the standard library: *)
+
+Compute pred.
+
+(* We can use a new command, [Extraction], to produce an OCaml version of this
+ * function. *)
+
+Extraction pred.
+
+(* Returning 0 as the predecessor of 0 can come across as somewhat of a hack.
+ * In some situations, we might like to be sure that we never try to take the
+ * predecessor of 0.  We can enforce this by giving [pred] a stronger, dependent
+ * type. *)
+
+Lemma zgtz : 0 > 0 -> False.
+Proof.
+  linear_arithmetic.
+Qed.
+
+Definition pred_strong1 (n : nat) : n > 0 -> nat :=
+  match n with
+    | O => fun pf : 0 > 0 => match zgtz pf with end
+    | S n' => fun _ => n'
+  end.
+
+(* We expand the type of [pred] to include a _proof_ that its argument [n] is
+ * greater than 0.  When [n] is 0, we use the proof to derive a contradiction,
+ * which we can use to build a value of any type via a vacuous pattern match.
+ * When [n] is a successor, we have no need for the proof and just return the
+ * answer.  The proof argument can be said to have a _dependent_ type, because
+ * its type depends on the _value_ of the argument [n].
+ *
+ * Coq's [Compute] command can execute particular invocations of [pred_strong1]
+ * just as easily as it can execute more traditional functional programs. *)
+
+Theorem two_gt0 : 2 > 0.
+Proof.
+  linear_arithmetic.
+Qed.
+
+Compute pred_strong1 two_gt0.
+
+(* One aspect in particular of the definition of [pred_strong1] may be
+ * surprising.  We took advantage of [Definition]'s syntactic sugar for defining
+ * function arguments in the case of [n], but we bound the proofs later with
+ * explicit [fun] expressions.  Let us see what happens if we write this
+ * function in the way that at first seems most natural. *)
+
+Fail Definition pred_strong1' (n : nat) (pf : n > 0) : nat :=
+  match n with
+    | O => match zgtz pf with end
+    | S n' => n'
+  end.
+
+(* The term [zgtz pf] fails to type-check.  Somehow the type checker has failed
+ * to take into account information that follows from which [match] branch that
+ * term appears in.  The problem is that, by default, [match] does not let us
+ * use such implied information.  To get refined typing, we must always rely on
+ * [match] annotations, either written explicitly or inferred.
+ *
+ * In this case, we must use a [return] annotation to declare the relationship
+ * between the _value_ of the [match] discriminee and the _type_ of the result.
+ * There is no annotation that lets us declare a relationship between the
+ * discriminee and the type of a variable that is already in scope; hence, we
+ * delay the binding of [pf], so that we can use the [return] annotation to
+ * express the needed relationship.
+ *
+ * We are lucky that Coq's heuristics infer the [return] clause (specifically,
+ * [return n > 0 -> nat]) for us in the definition of [pred_strong1], leading to
+ * the following elaborated code: *)
+
+Definition pred_strong1' (n : nat) : n > 0 -> nat :=
+  match n return n > 0 -> nat with
+    | O => fun pf : 0 > 0 => match zgtz pf with end
+    | S n' => fun _ => n'
+  end.
+
+(* By making explicit the functional relationship between value [n] and the
+ * result type of the [match], we guide Coq toward proper type checking.  The
+ * clause for this example follows by simple copying of the original annotation
+ * on the definition.  In general, however, the [match] annotation inference
+ * problem is undecidable.  The known undecidable problem of
+ * _higher-order unification_ reduces to the [match] type inference problem.
+ * Over time, Coq is enhanced with more and more heuristics to get around this
+ * problem, but there must always exist [match]es whose types Coq cannot infer
+ * without annotations.
+ *
+ * Let us now take a look at the OCaml code Coq generates for [pred_strong1]. *)
+
+Extraction pred_strong1.
+
+(* The proof argument has disappeared!  We get exactly the OCaml code we would
+ * have written manually.  This is our first demonstration of the main
+ * technically interesting feature of Coq program extraction: proofs are erased
+ * systematically.
+ *
+ * We can reimplement our dependently typed [pred] based on _subset types_,
+ * defined in the standard library with the type family %[sig]. *)
+
+Print sig.
+
+(* We rewrite [pred_strong1], using some syntactic sugar for subset types, after
+ * we deactivate some clashing notations for set literals. *)
+
+Locate "{ _ : _ | _ }".
+
+Definition pred_strong2 (s : {n : nat | n > 0} ) : nat :=
+  match s with
+    | exist O pf => match zgtz pf with end
+    | exist (S n') _ => n'
+  end.
+
+(* To build a value of a subset type, we use the [exist] constructor, and the
+ * details of how to do that follow from the output of our earlier [Print sig]
+ * command, where we elided the extra information that parameter [A] is
+ * implicit.  We need an extra [_] here and not in the definition of
+ * [pred_strong2] because _parameters_ of inductive types (like the predicate
+ * [P] for [sig]) are not mentioned in pattern matching, but _are_ mentioned in
+ * construction of terms (if they are not marked as implicit arguments).
+ * (Actually, this behavior changed between Coq versions 8.4 and 8.5, hence the
+ * near at the top of the file to revert to the old behavior.) *)
+
+Compute pred_strong2 (exist _ 2 two_gt0).
+
+Extraction pred_strong2.
+
+(* We arrive at the same OCaml code as was extracted from [pred_strong1], which
+ * may seem surprising at first.  The reason is that a value of [sig] is a pair
+ * of two pieces, a value and a proof about it.  Extraction erases the proof,
+ * which reduces the constructor [exist] of [sig] to taking just a single
+ * argument.  An optimization eliminates uses of datatypes with single
+ * constructors taking single arguments, and we arrive back where we started.
+ *
+ * We can continue on in the process of refining [pred]'s type.  Let us change
+ * its result type to capture that the output is really the predecessor of the
+ * input. *)
+
+Definition pred_strong3 (s : {n : nat | n > 0}) : {m : nat | proj1_sig s = S m} :=
+  match s return {m : nat | proj1_sig s = S m} with
+    | exist 0 pf => match zgtz pf with end
+    | exist (S n') pf => exist _ n' (eq_refl _)
+  end.
+
+Compute pred_strong3 (exist _ 2 two_gt0).
+
+(* A value in a subset type can be thought of as a _dependent pair_ (or
+ * _sigma type_ of a base value and a proof about it.  The function [proj1_sig]
+ * extracts the first component of the pair.  It turns out that we need to
+ * include an explicit [return] clause here, since Coq's heuristics are not
+ * smart enough to propagate the result type that we wrote earlier.
+ *
+ * By now, the reader is probably ready to believe that the new [pred_strong]
+ * leads to the same OCaml code as we have seen several times so far, and Coq
+ * does not disappoint. *)
+
+Extraction pred_strong3.
+
+(* We have managed to reach a type that is, in a formal sense, the most
+ * expressive possible for [pred].  Any other implementation of the same type
+ * must have the same input-output behavior.  However, there is still room for
+ * improvement in making this kind of code easier to write.  Here is a version
+ * that takes advantage of tactic-based theorem proving.  We switch back to
+ * passing a separate proof argument instead of using a subset type for the
+ * function's input, because this leads to cleaner code.  ([False_rec] is a
+ * library function that can be used to produce a value in any type given a
+ * proof of [False].  It's defined in terms of the vacuous pattern match we saw
+ * earlier.) *)
+
+Definition pred_strong4 : forall (n : nat), n > 0 -> {m : nat | n = S m}.
+  refine (fun n =>
+    match n with
+      | O => fun _ => False_rec _ _
+      | S n' => fun _ => exist _ n' _
+    end).
+
+  (* We build [pred_strong4] using tactic-based proving, beginning with a
+   * [Definition] command that ends in a period before a definition is given.
+   * Such a command enters the interactive proving mode, with the type given for
+   * the new identifier as our proof goal.
+   *
+   * We do most of the work with the [refine] tactic, to which we pass a partial
+   * "proof" of the type we are trying to prove.  There may be some pieces left
+   * to fill in, indicated by underscores.  Any underscore that Coq cannot
+   * reconstruct with type inference is added as a proof subgoal.  In this case,
+   * we have two subgoals.
+   *
+   * We can see that the first subgoal comes from the second underscore passed
+   * to [False_rec], and the second subgoal comes from the second underscore
+   * passed to [exist].  In the first case, we see that, though we bound the
+   * proof variable with an underscore, it is still available in our proof
+   * context.  It is hard to refer to underscore-named variables in manual
+   * proofs, but automation makes short work of them.  Both subgoals are easy to
+   * discharge that way, so let us back up and ask to prove all subgoals
+   * automatically. *)
+
+  Undo.
+  refine (fun n =>
+    match n with
+      | O => fun _ => False_rec _ _
+      | S n' => fun _ => exist _ n' _
+    end); equality || linear_arithmetic.
+Defined.
+
+(* We end the "proof" with [Defined] instead of [Qed], so that the definition we
+ * constructed remains visible.  This contrasts to the case of ending a proof
+ * with [Qed], where the details of the proof are hidden afterward.  (More
+ * formally, [Defined] marks an identifier as _transparent_, allowing it to be
+ * unfolded; while [Qed] marks an identifier as _opaque_, preventing unfolding.)
+ * Let us see what our proof script constructed. *)
+
+Print pred_strong4.
+
+(* We see the code we entered, with some (pretty long!) proofs filled in. *)
+
+Compute pred_strong4 two_gt0.
+
+(* We are almost done with the ideal implementation of dependent predecessor.
+ * We can use Coq's syntax extension facility to arrive at code with almost no
+ * complexity beyond a Haskell or ML program with a complete specification in a
+ * comment.  In this book, we will not dwell on the details of syntax
+ * extensions; the Coq manual gives a straightforward introduction to them. *)
+
+Notation "!" := (False_rec _ _).
+Notation "[ e ]" := (exist _ e _).
+
+Definition pred_strong5 : forall (n : nat), n > 0 -> {m : nat | n = S m}.
+  refine (fun n =>
+    match n with
+      | O => fun _ => !
+      | S n' => fun _ => [n']
+    end); equality || linear_arithmetic.
+Defined.
+
+(* By default, notations are also used in pretty-printing terms, including
+ * results of evaluation. *)
+
+Compute pred_strong5 two_gt0.
+
+
+(** * Decidable Proposition Types *)
+
+(* There is another type in the standard library that captures the idea of
+ * program values that indicate which of two propositions is true. *)
+
+Print sumbool.
+
+(* Here, the constructors of [sumbool] have types written in terms of a
+ * registered notation for [sumbool], such that the result type of each
+ * constructor desugars to [sumbool A B].  We can define some notations of our
+ * own to make working with [sumbool] more convenient. *)
+
+Notation "'Yes'" := (left _ _).
+Notation "'No'" := (right _ _).
+Notation "'Reduce' x" := (if x then Yes else No) (at level 50).
+
+(* The [Reduce] notation is notable because it demonstrates how [if] is
+ * overloaded in Coq.  The [if] form actually works when the test expression has
+ * any two-constructor inductive type.  Moreover, in the [then] and [else]
+ * branches, the appropriate constructor arguments are bound.  This is important
+ * when working with [sumbool]s, when we want to have the proof stored in the
+ * test expression available when proving the proof obligations generated in the
+ * appropriate branch.
+ *
+ * Now we can write [eq_nat_dec], which compares two natural numbers, returning
+ * either a proof of their equality or a proof of their inequality. *)
+
+Definition eq_nat_dec : forall n m : nat, {n = m} + {n <> m}.
+  refine (fix f (n m : nat) : {n = m} + {n <> m} :=
+    match n, m with
+      | O, O => Yes
+      | S n', S m' => Reduce (f n' m')
+      | _, _ => No
+    end); equality.
+Defined.
+
+Compute eq_nat_dec 2 2.
+Compute eq_nat_dec 2 3.
+
+(* Note that the [Yes] and [No] notations are hiding proofs establishing the
+ * correctness of the outputs.
+ *
+ * Our definition extracts to reasonable OCaml code. *)
+
+Extraction eq_nat_dec.
+
+(* Proving this kind of decidable equality result is so common that Coq comes
+ * with a tactic for automating it. *)
+
+Definition eq_nat_dec' (n m : nat) : {n = m} + {n <> m}.
+  decide equality.
+Defined.
+
+(* Curious readers can verify that the [decide equality] version extracts to the
+ * same OCaml code as our more manual version does.  That OCaml code had one
+ * undesirable property, which is that it uses [Left] and [Right] constructors
+ * instead of the Boolean values built into OCaml.  We can fix this, by using
+ * Coq's facility for mapping Coq inductive types to OCaml variant types. *)
+
+Extract Inductive sumbool => "bool" ["true" "false"].
+Extraction eq_nat_dec'.
+
+(* We can build "smart" versions of the usual Boolean operators and put them to
+ * good use in certified programming.  For instance, here is a [sumbool] version
+ * of Boolean "or." *)
+
+Notation "x || y" := (if x then Yes else Reduce y).
+
+(* Let us use it for building a function that decides list membership.  We need
+ * to assume the existence of an equality decision procedure for the type of
+ * list elements. *)
+
+Section In_dec.
+  Variable A : Set.
+  Variable A_eq_dec : forall x y : A, {x = y} + {x <> y}.
+
+  (* The final function is easy to write using the techniques we have developed
+   * so far. *)
+
+  Definition In_dec : forall (x : A) (ls : list A), {In x ls} + {~ In x ls}.
+    refine (fix f (x : A) (ls : list A) : {In x ls} + {~ In x ls} :=
+      match ls with
+	| nil => No
+	| x' :: ls' => A_eq_dec x x' || f x ls'
+      end); simplify; equality.
+  Defined.
+End In_dec.
+
+Compute In_dec eq_nat_dec 2 (1 :: 2 :: nil).
+Compute In_dec eq_nat_dec 3 (1 :: 2 :: nil).
+
+(* The [In_dec] function has a reasonable extraction to OCaml. *)
+
+Extraction In_dec.
+
+(* This is more or the less code for the corresponding function from the OCaml
+ * standard library. *)
+
+
+(** * Partial Subset Types *)
+
+(* Our final implementation of dependent predecessor used a very specific
+ * argument type to ensure that execution could always complete normally.
+ * Sometimes we want to allow execution to fail, and we want a more principled
+ * way of signaling failure than returning a default value, as [pred] does for
+ * [0].  One approach is to define this type family [maybe], which is a version
+ * of [sig] that allows obligation-free failure. *)
+
+Inductive maybe (A : Set) (P : A -> Prop) : Set :=
+| Unknown : maybe P
+| Found : forall x : A, P x -> maybe P.
+
+(* We can define some new notations, analogous to those we defined for subset
+ * types. *)
+
+Notation "{{ x | P }}" := (maybe (fun x => P)).
+Notation "??" := (Unknown _).
+Notation "[| x |]" := (Found _ x _).
+
+(* Now our next version of [pred] is trivial to write. *)
+
+Definition pred_strong7 : forall n : nat, {{m | n = S m}}.
+  refine (fun n =>
+    match n return {{m | n = S m}} with
+      | O => ??
+      | S n' => [|n'|]
+    end); trivial.
+Defined.
+
+Compute pred_strong7 2.
+Compute pred_strong7 0.
+
+(* Because we used [maybe], one valid implementation of the type we gave
+ * [pred_strong7] would return [??] in every case.  We can strengthen the type
+ * to rule out such vacuous implementations, and the type family [sumor] from
+ * the standard library provides the easiest starting point.  For type [A] and
+ * proposition [B], [A + {B}] desugars to [sumor A B], whose values are either
+ * values of [A] or proofs of [B]. *)
+
+Print sumor.
+
+(* We add notations for easy use of the [sumor] constructors.  The second
+ * notation is specialized to [sumor]s whose [A] parameters are instantiated
+ * with regular subset types, since this is how we will use [sumor] below. *)
+
+Notation "!!" := (inright _ _).
+Notation "[|| x ||]" := (inleft _ [x]).
+
+(* Now we are ready to give the final version of possibly failing predecessor.
+ * The [sumor]-based type that we use is maximally expressive; any
+ * implementation of the type has the same input-output behavior. *)
+
+Definition pred_strong8 : forall n : nat, {m : nat | n = S m} + {n = 0}.
+  refine (fun n =>
+    match n with
+      | O => !!
+      | S n' => [||n'||]
+    end); trivial.
+Defined.
+
+Compute pred_strong8 2.
+Compute pred_strong8 0.
+
+(* As with our other maximally expressive [pred] function, we arrive at quite
+ * simple output values, thanks to notations. *)
+
+
+(** * Monadic Notations *)
+
+(* We can treat [maybe] like a monad, in the same way that the Haskell [Maybe]
+ * type is interpreted as a failure monad.  Our [maybe] has the wrong type to be
+ * a literal monad, but a "bind"-like notation will still be helpful. *)
+
+Notation "x <- e1 ; e2" := (match e1 with
+                             | Unknown => ??
+                             | Found x _ => e2
+                           end)
+(right associativity, at level 60).
+
+(* The meaning of [x <- e1; e2] is: First run [e1].  If it fails to find an
+ * answer, then announce failure for our derived computation, too.  If [e1]
+ * _does_ find an answer, pass that answer on to [e2] to find the final result.
+ * The variable [x] can be considered bound in [e2].
+ *
+ * This notation is very helpful for composing richly typed procedures.  For
+ * instance, here is a very simple implementation of a function to take the
+ * predecessors of two naturals at once. *)
+
+Definition doublePred : forall n1 n2 : nat, {{p | n1 = S (fst p) /\ n2 = S (snd p)}}.
+  refine (fun n1 n2 =>
+    m1 <- pred_strong7 n1;
+    m2 <- pred_strong7 n2;
+    [|(m1, m2)|]); propositional.
+Defined.
+
+(* We can build a [sumor] version of the "bind" notation and use it to write a
+ * similarly straightforward version of this function. *)
+
+Notation "x <-- e1 ; e2" := (match e1 with
+                               | inright _ => !!
+                               | inleft (exist x _) => e2
+                             end)
+(right associativity, at level 60).
+
+Definition doublePred' : forall n1 n2 : nat,
+  {p : nat * nat | n1 = S (fst p) /\ n2 = S (snd p)}
+  + {n1 = 0 \/ n2 = 0}.
+  refine (fun n1 n2 =>
+    m1 <-- pred_strong8 n1;
+    m2 <-- pred_strong8 n2;
+    [||(m1, m2)||]); propositional.
+Defined.
+
+(* This example demonstrates how judicious selection of notations can hide
+ * complexities in the rich types of programs. *)
+
+
+(** * A Type-Checking Example *)
+
+(* We can apply these specification types to build a certified type checker for
+ * a simple expression language. *)
+
+Inductive exp :=
+| Nat (n : nat)
+| Plus (e1 e2 : exp)
+| Bool (b : bool)
+| And (e1 e2 : exp).
+
+(* We define a simple language of types and its typing rules. *)
+
+Inductive type := TNat | TBool.
+
+Inductive hasType : exp -> type -> Prop :=
+| HtNat : forall n,
+  hasType (Nat n) TNat
+| HtPlus : forall e1 e2,
+  hasType e1 TNat
+  -> hasType e2 TNat
+  -> hasType (Plus e1 e2) TNat
+| HtBool : forall b,
+  hasType (Bool b) TBool
+| HtAnd : forall e1 e2,
+  hasType e1 TBool
+  -> hasType e2 TBool
+  -> hasType (And e1 e2) TBool.
+
+(* It will be helpful to have a function for comparing two types.  We build one
+ * using [decide equality]. *)
+
+Definition eq_type_dec : forall t1 t2 : type, {t1 = t2} + {t1 <> t2}.
+  decide equality.
+Defined.
+
+(* Another notation complements the monadic notation for [maybe] that we defined
+ * earlier.  Sometimes we want to include "assertions" in our procedures.  That
+ * is, we want to run a decision procedure and fail if it fails; otherwise, we
+ * want to continue, with the proof that it produced made available to us.  This
+ * infix notation captures that idea, for a procedure that returns an arbitrary
+ * two-constructor type. *)
+
+Notation "e1 ;; e2" := (if e1 then e2 else ??)
+  (right associativity, at level 60).
+
+(* With that notation defined, we can implement a [typeCheck] function, whose
+ * code is only more complex than what we would write in ML because it needs to
+ * include some extra type annotations.  Every [[|e|]] expression adds a
+ * [hasType] proof obligation, and [eauto] makes short work of them when we add
+ * [hasType]'s constructors as hints. *)
+
+Hint Constructors hasType.
+
+Definition typeCheck : forall e : exp, {{t | hasType e t}}.
+  refine (fix F (e : exp) : {{t | hasType e t}} :=
+    match e return {{t | hasType e t}} with
+      | Nat _ => [|TNat|]
+      | Plus e1 e2 =>
+        t1 <- F e1;
+        t2 <- F e2;
+        eq_type_dec t1 TNat;;
+        eq_type_dec t2 TNat;;
+        [|TNat|]
+      | Bool _ => [|TBool|]
+      | And e1 e2 =>
+        t1 <- F e1;
+        t2 <- F e2;
+        eq_type_dec t1 TBool;;
+        eq_type_dec t2 TBool;;
+        [|TBool|]
+    end); subst; eauto.
+Defined.
+
+(* Despite manipulating proofs, our type checker is easy to run. *)
+
+Compute typeCheck (Nat 0).
+Compute typeCheck (Plus (Nat 1) (Nat 2)).
+Compute typeCheck (Plus (Nat 1) (Bool false)).
+
+(* The type checker also extracts to some reasonable OCaml code. *)
+
+Extraction typeCheck.
+
+(* We can adapt this implementation to use [sumor], so that we know our type-checker
+ * only fails on ill-typed inputs.  First, we define an analogue to the
+ * "assertion" notation. *)
+
+Notation "e1 ;;; e2" := (if e1 then e2 else !!)
+  (right associativity, at level 60).
+
+(* Next, we prove a helpful lemma, which states that a given expression can have
+ * at most one type. *)
+
+Lemma hasType_det : forall e t1,
+  hasType e t1
+  -> forall t2, hasType e t2
+    -> t1 = t2.
+Proof.
+  induct 1; invert 1; equality.
+Qed.
+
+(* Now we can define the type-checker.  Its type expresses that it only fails on
+ * untypable expressions. *)
+
+Hint Resolve hasType_det.
+(* The lemma [hasType_det] will also be useful for proving proof obligations
+ * with contradictory contexts. *)
+
+Definition typeCheck' : forall e : exp, {t : type | hasType e t} + {forall t, ~ hasType e t}.
+  (* Finally, the implementation of [typeCheck] can be transcribed literally,
+   * simply switching notations as needed. *)
+
+  refine (fix F (e : exp) : {t : type | hasType e t} + {forall t, ~ hasType e t} :=
+    match e return {t : type | hasType e t} + {forall t, ~ hasType e t} with
+      | Nat _ => [||TNat||]
+      | Plus e1 e2 =>
+        t1 <-- F e1;
+        t2 <-- F e2;
+        eq_type_dec t1 TNat;;;
+        eq_type_dec t2 TNat;;;
+        [||TNat||]
+      | Bool _ => [||TBool||]
+      | And e1 e2 =>
+        t1 <-- F e1;
+        t2 <-- F e2;
+        eq_type_dec t1 TBool;;;
+        eq_type_dec t2 TBool;;;
+        [||TBool||]
+    end); simplify; propositional; subst; eauto;
+    match goal with
+    | [ H : hasType _ _ |- _ ] => invert2 H
+    end; eauto.
+Defined.
+
+(* The short implementation here hides just how time-saving automation is.
+ * Every use of one of the notations adds a proof obligation, giving us 12 in
+ * total.  Most of these obligations require inversions and either uses of
+ * [hasType_det] or applications of [hasType] rules.
+ *
+ * Our new function remains easy to test: *)
+
+Compute typeCheck' (Nat 0).
+Compute typeCheck' (Plus (Nat 1) (Nat 2)).
+Compute typeCheck' (Plus (Nat 1) (Bool false)).
+
+(* The results of simplifying calls to [typeCheck'] look deceptively similar to
+ * the results for [typeCheck], but now the types of the results provide more
+ * information. *)
diff --git a/_CoqProject b/_CoqProject
index 4ebe200..10bdc6d 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -7,6 +7,7 @@ Invariant.v
 ModelCheck.v
 Imp.v
 AbstractInterpret.v
+FrapWithoutSets.v
 Frap.v
 BasicSyntax_template.v
 BasicSyntax.v
@@ -31,6 +32,7 @@ LogicProgramming_template.v
 AbstractInterpretation.v
 CompilerCorrectness.v
 CompilerCorrectness_template.v
+SubsetTypes.v
 LambdaCalculusAndTypeSoundness_template.v
 LambdaCalculusAndTypeSoundness.v
 TypesAndMutation.v