Update wrt Iris. Add dependency on TLC.

README.md

@@ -2,7 +2,8 @@
 
 The project is known to compile with:
  *  Coq 8.7.2
- *  coq-iris dev.2018-04-10.0 (development version of Iris)
+ *  coq-iris dev.2018-10-13.0.7041c043 (development version of Iris)
+ *  coq-tlc 20180316 (for the proof of union-find)
 
 ### Step 1: Install opam
 
@@ -35,13 +36,22 @@ support it.
 
     opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git
     opam update
-    opam pin add coq-iris -k version dev.2018-04-10.0
+    opam pin add coq-iris -k version dev.2018-10-13.0.7041c043
 
 (This will also install `coq-stdpp`, another Coq library made available through
 the same repo.)
 
 More info on the Coq development of Iris: [there][coq-iris].
 
+### Step 4: Install TLC
+
+The TLC library is required by the proof of the union-find algorithm. It is
+available through an opam package in the Coq repository (added earlier).
+
+    opam install coq-tlc
+
+TODO: version?
+
 ## Compiling
 
 To compile the Coq scripts:

theories/TimeCredits.v

@@ -201,17 +201,6 @@ Section Tick_lemmas.
     prim_exec  (tick v) (<[ℓ := #(S n)]> σ)  v (<[ℓ := #n]> σ)  [].
   Proof. by apply exec_tick_success. Qed.
 
-(* MERGE: to be merged into Iris: *)
-  Definition head_stuck e σ :=
-  to_val e = None ∧ head_irreducible e σ.
-  Lemma head_stuck_stuck e σ :
-    head_stuck e σ → sub_redexes_are_values e → stuck e σ.
-  Proof.
-    intros [] ?. split; first done.
-    by apply prim_head_irreducible.
-  Qed.
-(* /MERGE *)
-
   (* Semantics in the “failing” case. *)
 
   Lemma not_safe_tick v σ :

theories/Translation.v

@@ -619,7 +619,7 @@ Section ClosureFree.
 
   Fixpoint closure_free (v : val) : bool :=
     match v with
-    | RecV _ _ _ _ => false
+    | RecV _ _ _ => false
     | LitV _ => true
     | PairV v1 v2 => closure_free v1 && closure_free v2
     | InjLV v1 => closure_free v1