From 8161110f20b970471575c2d589bf501b2587b7bc Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Thu, 5 Mar 2026 23:21:18 +0000
Subject: [PATCH 1/7] WIP: feat: mechanization of "Interval Tree Clocks"

This PR introduces a simplified version of "Interval Tree Clocks",
described by Almeida et al. in their similarly named paper.

Note: we just introduce the tree-based definitions, and prove they have
the desired properties directly, without defining the denotation of such
trees into actual intervals/sets.

We also simplify the model a lot, by removing arbitrary events, and
instead saying that a merge also counts as an event. By doing so, we can
replace the event-tree by a single natural number, making it much
simpler to reason about. We do use the id-tree exactly as defined in the
paper, but since we eliminated the tree structure from the event
component, we had to come up with a novel definition of the
happens-before relation.

This gives us a clock with a fork and join operations. This PR also
proves that the arguments to these operations always happen before
their results. Desired properties around independence are stated, but
not yet proven.

WIP because I had to last-minute tweak the happens-before relation,
and should still check that the new definition (a) actually is the
correct one, and (b) is consistent with the documentation.
---
 EffectSSA/ITC.lean                 |   6 +
 EffectSSA/ITC/CanonicalIdTree.lean | 167 +++++++++++
 EffectSSA/ITC/Clock.lean           | 463 +++++++++++++++++++++++++++++
 EffectSSA/ITC/IdTree.lean          |  78 +++++
 EffectSSA/ITC/Lemmas.lean          |   0
 EffectSSA/ITC/Ops.lean             |   0
 EffectSSA/ITC/Scratch.lean         |  31 ++
 7 files changed, 745 insertions(+)
 create mode 100644 EffectSSA/ITC.lean
 create mode 100644 EffectSSA/ITC/CanonicalIdTree.lean
 create mode 100644 EffectSSA/ITC/Clock.lean
 create mode 100644 EffectSSA/ITC/IdTree.lean
 create mode 100644 EffectSSA/ITC/Lemmas.lean
 create mode 100644 EffectSSA/ITC/Ops.lean
 create mode 100644 EffectSSA/ITC/Scratch.lean

diff --git a/EffectSSA/ITC.lean b/EffectSSA/ITC.lean
new file mode 100644
index 0000000..e109523
--- /dev/null
+++ b/EffectSSA/ITC.lean
@@ -0,0 +1,6 @@
+import EffectSSA.ITC.IdTree
+import EffectSSA.ITC.CanonicalIdTree
+import EffectSSA.ITC.Clock
+
+namespace EffectSSA
+export ITC (Clock)
diff --git a/EffectSSA/ITC/CanonicalIdTree.lean b/EffectSSA/ITC/CanonicalIdTree.lean
new file mode 100644
index 0000000..a88b180
--- /dev/null
+++ b/EffectSSA/ITC/CanonicalIdTree.lean
@@ -0,0 +1,167 @@
+import EffectSSA.ITC.IdTree
+
+/-!
+# Canonical Id Trees
+
+-/
+namespace EffectSSA.ITC
+
+/--
+A `CanonicalIdTree` is an `IdTree` which is guaranteed to be in normal form.
+-/
+structure CanonicalIdTree where
+  raw : IdTree
+  eq_normalize : raw.normalize = raw := by solve | rfl | simp; try grind
+  deriving DecidableEq
+
+namespace CanonicalIdTree
+
+/-! ## Basic Lemmas -/
+section Lemmas
+variable {i j : CanonicalIdTree}
+
+attribute [grind =] CanonicalIdTree.eq_normalize
+
+@[ext, grind ext]
+theorem ext : i.raw = j.raw → i = j := by
+  grind [cases CanonicalIdTree]
+
+@[simp] theorem eq_iff_raw_eq : i = j ↔ i.raw = j.raw := by grind
+
+@[simp, grind .] theorem mk_eq_iff {raw : IdTree} {h : raw.normalize = raw} {j : CanonicalIdTree} :
+    ⟨raw, h⟩ = j ↔ raw = j.raw := by grind
+
+@[simp, grind .] theorem eq_mk_iff {i : CanonicalIdTree} {raw : IdTree} {h : raw.normalize = raw} :
+    i = ⟨raw, h⟩ ↔ i.raw = raw := by grind
+
+end Lemmas
+
+/-! ## Constructors -/
+section Ctors
+
+/-- The canonical representation of the empty set (i.e., `zero`). -/
+@[match_pattern]
+def zero : CanonicalIdTree where
+  raw := .zero
+
+/-- The canonical representation of the full interval (i.e., `one`). -/
+@[match_pattern]
+def one : CanonicalIdTree where
+  raw := .one
+
+/--
+A node with left child `l` and right child `r`.
+Requires that the node is canonical, i.e., it's not allowed for both children to
+be `zero` or both to be `one`.
+-/
+@[match_pattern]
+def node (l r : CanonicalIdTree)
+    (hz : ¬(l = zero ∧ r = zero) := by simp; try grind)
+    (ho : l ≠ one ∨ r ≠ one := by simp; try grind) :
+    CanonicalIdTree where
+  raw := .node l.raw r.raw
+  eq_normalize := by
+    rcases l with ⟨l, hl⟩
+    rcases r with ⟨r, hr⟩
+    replace hz : ¬(l = .zero ∧ r = .zero) := by simpa using hz
+    replace ho : l ≠ .one ∨ r ≠ .one := by simpa using ho
+    grind [IdTree.normalize]
+
+/--
+`node'` returns an id tree equivalent to the node with children `l` and `r`.
+
+NOTE: the normalization means that the result of `node'` is not necessarily an
+actual node in the tree! E.g., if `l = r = zero`, then the result is just a
+single `zero` leaf.
+-/
+def node' (l r : CanonicalIdTree) : CanonicalIdTree where
+  raw := (IdTree.node l.raw r.raw).normalize
+
+/-! ### Constructor Lemmas -/
+section CtorLemmas
+variable {i l r : CanonicalIdTree} {hz ho}
+
+@[simp, grind =] theorem raw_zero : zero.raw = .zero := rfl
+@[simp, grind =] theorem raw_one  : one.raw = .one := rfl
+@[simp, grind =] theorem raw_node : (node l r hz ho).raw = .node l.raw r.raw := rfl
+@[simp, grind =] theorem raw_node' : (node' l r).raw = .normalize (.node l.raw r.raw) := rfl
+
+@[simp, grind .] theorem eq_zero_iff :           i = zero ↔ i.raw = .zero             := by grind
+@[simp, grind .] theorem eq_one_iff  :            i = one ↔ i.raw = .one              := by grind
+@[simp, grind .] theorem eq_node_iff : i = node l r hz ho ↔ i.raw = .node l.raw r.raw := by grind
+
+@[simp] theorem zero_ne_one : (zero : CanonicalIdTree) ≠ one := by simp
+@[simp] theorem one_ne_zero : (one : CanonicalIdTree) ≠ zero := by simp
+@[simp] theorem node_ne_zero : node l r hz ho ≠ zero := by simp
+@[simp] theorem node_ne_one : node l r hz ho ≠ one := by simp
+@[simp] theorem zero_ne_node : zero ≠ node l r hz ho := by simp
+
+@[simp] theorem one_ne_node : one ≠ node l r hz ho := by
+  intro heq; cases heq
+
+theorem node_injective :
+    node l₁ r₁ hz₁ ho₁ = node l₂ r₂ hz₂ ho₂ → l₁ = l₂ ∧ r₁ = r₂ := by
+  grind
+
+@[simp, grind =] theorem mk_zero_eq_zero {h} : (⟨.zero, h⟩ : CanonicalIdTree) = zero := by rfl
+@[simp, grind =] theorem mk_one_eq_one {h} : (⟨.one, h⟩ : CanonicalIdTree) = one := by rfl
+
+@[simp, grind =] theorem mk_node_eq_node {l r : IdTree} (h : (IdTree.node l r).normalize = .node l r) :
+    (⟨.node l r, h⟩ : CanonicalIdTree) = node ⟨l, by grind⟩ ⟨r, by grind⟩ := by rfl
+
+@[simp] theorem mk_normalize_node {l r : IdTree} :
+    ⟨(IdTree.node l r).normalize, by grind⟩ = node' ⟨l.normalize, by grind⟩ ⟨r.normalize, by grind⟩ := by
+  simp [node', IdTree.normalize]
+
+/-! #### node' -/
+
+@[simp, grind =] theorem one_node'_one : node' one one = one := by grind [node', IdTree.normalize]
+@[simp, grind =] theorem zero_node'_zero : node' zero zero = zero := by grind [node', IdTree.normalize]
+
+@[simp, grind =] theorem node'_eq_node_of (hz : ¬(l = zero ∧ r = zero)) (ho : l ≠ one ∨ r ≠ one) :
+    node' l r = node l r hz ho := by grind [node']
+
+end CtorLemmas
+end Ctors
+
+/-! ## Recursion Principle -/
+section Recursion
+
+/--
+Recursion principle for `CanonicalIdTree` using the high-level constructors.
+-/
+@[elab_as_elim, induction_eliminator]
+def rec' {motive : CanonicalIdTree → Sort u}
+    (zero : motive CanonicalIdTree.zero)
+    (one : motive CanonicalIdTree.one)
+    (node : ∀ (l r : CanonicalIdTree) (hz : ¬(l = .zero ∧ r = .zero)) (ho : l ≠ .one ∨ r ≠ .one),
+      motive l → motive r → motive (CanonicalIdTree.node l r hz ho))
+    (t : CanonicalIdTree) : motive t :=
+  go t.raw t.eq_normalize
+  where
+    go : (raw : IdTree) → (h_canon : raw.normalize = raw) → motive ⟨raw, h_canon⟩
+    | .zero, _ => zero
+    | .one, _ => one
+    | .node l r, hcanon =>
+      let l : CanonicalIdTree := ⟨l, by grind⟩
+      let r : CanonicalIdTree := ⟨r, by grind⟩
+      have ho := by simp; grind
+      have hz := by simp; grind
+      node l r ho hz (go l.1 l.2) (go r.1 r.2)
+
+/--
+Cases principle for `CanonicalIdTree` using the high-level constructors.
+-/
+@[cases_eliminator]
+def cases' {motive : CanonicalIdTree → Sort u}
+    (t : CanonicalIdTree)
+    (zero : motive CanonicalIdTree.zero)
+    (one : motive CanonicalIdTree.one)
+    (node : ∀ (l r : CanonicalIdTree) (hz : ¬(l = .zero ∧ r = .zero)) (ho : l ≠ .one ∨ r ≠ .one),
+      motive (CanonicalIdTree.node l r hz ho)) : motive t :=
+  rec' zero one (fun l r hz ho _ _ => node l r hz ho) t
+
+end Recursion
+
+end CanonicalIdTree
+end EffectSSA.ITC
diff --git a/EffectSSA/ITC/Clock.lean b/EffectSSA/ITC/Clock.lean
new file mode 100644
index 0000000..5457f20
--- /dev/null
+++ b/EffectSSA/ITC/Clock.lean
@@ -0,0 +1,463 @@
+import EffectSSA.ITC.CanonicalIdTree
+
+/-!
+# Simplified Interval Tree Clock
+
+We combine a (canonical) id tree with an event counter to obtain our simplification
+of the interval tree clock. [1]
+
+Referenes:
+[1]: Almeida et al. "Interval Tree Clocks: A Logical Clock for Dynamic Systems"
+-/
+namespace EffectSSA.ITC
+
+/--
+A clock combines a (canonical) id tree with an event counter.
+-/
+structure Clock where
+  /--
+  `i` is the id component.
+
+  The id determines whether two threads are concurrent.
+  -/
+  i : CanonicalIdTree
+  /--
+  `e` tracks the maximal number of splits (or merges, TBD) which have occured
+  in any one path in the history of the current thread.
+
+  This is used to disambiguate between two non-concurrent threads,
+  which thread precedes the other.
+  -/
+  e : Nat
+  deriving DecidableEq
+
+
+/-!
+## Comparison
+Section 5.3.1 in [1]
+-/
+section Compare
+
+/--
+We say that `i ≤ j`, for two (canonical) id trees `i` and `j`, when the set
+represented by `i` is a *subset* of the set represented by `j`.
+-/
+def CanonicalIdTree.le (i : CanonicalIdTree) (j : CanonicalIdTree) : Bool :=
+  go i.raw j.raw
+  where
+    go : IdTree → IdTree → Bool
+    | .zero, _ => true
+    | _, .one  => true
+    | .node l₁ r₁, .node l₂ r₂ => go l₁ l₂ ∧ go r₁ r₂
+    | _, _ => false
+instance : LE CanonicalIdTree where le i j := i.le j
+
+/--
+We say that `(i₁, e₁) ≤ (i₂, e₂)`, when either
+`i₁` is a subset of `i₂` and `e₁` is less than or equal to `e₂`, or
+`i₁` is a superset of `i₂` and `e₁` is strictly less than `e₂`.
+
+That is, whether two clocks are *concurrent* (i.e. unrelated in the
+happens-before relation) is determined by the id component of the clock.
+Whenever two ids *are* related (in either direction), the event counter
+disambiguates in which direction the clocks ought to be related.
+
+Recall that a split will give disjoint subsets of its argument and keep the event
+counter constant, which is why the first branch allows for the event counter to
+be equal on both sides. A merge, on the other hand, gives a superset of its
+arguments, but increments the event counter. Thus, when we see that `i₁` is a
+superset of `i₂` we only relate the clocks if `e₂` has seen at least one more
+merge than `e₁`.
+
+TODO: I tweaked the definition below after writing the docstring, so
+I should doublecheck the docs are still accurate
+-/
+instance : LE Clock where le c₁ c₂ :=
+  -- Firstly, if `c₁` is a subset of (i.e, could have been split off from) `c₂`,
+  -- then for `c₁` to have happened *before* `c₂`, it must have seen *stricty* more merges
+  (c₁.i ≤ c₂.i ∧ c₁.e < c₂.e)
+  -- Secondly, if `c₁` is a superset of `c₂`, then `c₁` cannot have been directly
+  -- split of from `c₂` without having seen a merge in between, thus we say that
+  -- `c₁` has happened before `c₂` if it has seen at least as many merges.
+  ∨ (c₂.i ≤ c₁.i ∧ c₁.e ≤ c₂.e)
+
+section CompareLemmas
+variable {i j : CanonicalIdTree} {c₁ c₂ : Clock}
+
+/-! ### CanonicalIdTree LE lemmas -/
+namespace CanonicalIdTree
+
+attribute [local grind] le le.go
+@[local simp, local grind =] theorem le_iff' : (i ≤ j) ↔ i.le j = true := by
+  simp [LE.le]
+
+instance : DecidableLE CanonicalIdTree := by
+  intro i j
+  apply decidable_of_bool (i.le j)
+  rfl
+
+@[simp, grind .] theorem zero_le : zero ≤ i := by rfl
+@[simp, grind .] theorem le_one : i ≤ one := by cases i <;> rfl
+
+
+@[simp, grind .] theorem one_le_iff : one ≤ i ↔ i = one := by grind
+@[simp, grind .] theorem le_zero_iff : i ≤ zero ↔ i = zero := by grind
+
+@[simp, grind .] theorem node_le_node_iff {l₁ r₁ l₂ r₂ : CanonicalIdTree} {hz₁ ho₁ hz₂ ho₂} :
+    (node l₁ r₁ hz₁ ho₁) ≤ (node l₂ r₂ hz₂ ho₂) ↔ l₁ ≤ l₂ ∧ r₁ ≤ r₂ := by
+  grind
+
+@[simp, grind .] theorem node_le_node'_iff {l₁ r₁ l₂ r₂ : CanonicalIdTree} {hz ho} :
+    node l₁ r₁ hz ho ≤ node' l₂ r₂ ↔ l₁ ≤ l₂ ∧ r₁ ≤ r₂ := by
+  by_cases ho : l₂ = zero ∧ r₂ = zero
+  · grind
+  by_cases hz : l₂ = one ∧ r₂ = one
+  <;> grind
+
+@[simp, grind .] theorem le_refl : i ≤ i := by induction i <;> grind
+
+-- NOTE: we deliberatelyy put `le_iff` just before closing the namespace, as it
+--       would otherwise cause divergence with the local `le_iff'` simp-lemma.
+@[simp, grind =] theorem le_iff : (i.le j = true) ↔ (i ≤ j) := by
+  simp [LE.le]
+
+end CanonicalIdTree
+
+/-! ### Clock LE lemmas -/
+namespace Clock
+variable {e : Nat}
+
+@[grind =] theorem le_iff :
+    c₁ ≤ c₂ ↔ ((c₁.i ≤ c₂.i ∧ c₁.e < c₂.e) ∨ (c₂.i ≤ c₁.i ∧ c₁.e ≤ c₂.e)) := by rfl
+
+instance : DecidableLE Clock := fun _ _ => decidable_of_iff' _ le_iff
+
+@[simp, grind .] theorem le_refl : c₁ ≤ c₁ := by grind
+
+-- TODO: reinstate the below lemmas, if needed?
+-- @[simp, grind .] theorem zero_le_iff : ⟨.zero, e⟩ ≤ c₁ ↔ c₁.e < e := by grind
+-- @[simp, grind .] theorem le_one_iff : c₁ ≤ ⟨.one, e⟩ ↔ c₁.e ≤ e := by grind
+
+end Clock
+end CompareLemmas
+end Compare
+
+/-!
+## Unrelated
+We're especially interested in whether two clocks are unrelated (in either
+direction), for which we introduce a short-hand `x # y` (not present in [1]).
+-/
+section Unrel
+
+/--
+`x # y` is short for `¬(x ≤ y) ∧ ¬(y ≤ x)`
+
+The preferred spelling in theorems is `unrel`
+-/
+def Unrelated {α} [LE α] (x y : α) : Prop := ¬(x ≤ y) ∧ ¬(y ≤ x)
+@[inherit_doc] infix:67 " # " => Unrelated
+
+section UnrelLemmas
+
+/-! ### Generic Unrelated lemmas -/
+section GenericUnrelLemmas
+variable {α : Type _} [LE α] {x y : α}
+
+@[grind =] theorem unrel_iff : x # y ↔ ¬(x ≤ y) ∧ ¬(y ≤ x) := by rfl
+
+instance [DecidableLE α] : Decidable (x # y) := by unfold Unrelated; infer_instance
+
+theorem unrel_symm : x # y ↔ y # x := by grind
+theorem unrel_refl_iff : x # x ↔ ¬(x ≤ x) := by grind
+
+end GenericUnrelLemmas
+
+variable {i j : CanonicalIdTree} {c₁ c₂ : Clock}
+
+/-! ### CanonicalIdTree Unrelated lemmas -/
+namespace CanonicalIdTree
+
+@[simp, grind .] theorem unrefl_irrefl : ¬(i # i) := by grind
+
+@[simp, grind .] theorem not_unrel_zero : ¬(i # zero) := by grind
+@[simp, grind .] theorem not_zero_unrel : ¬(zero # j) := by grind
+
+@[simp, grind .] theorem not_unrel_one : ¬(i # one) := by grind
+@[simp, grind .] theorem not_one_unrel : ¬(one # j) := by grind
+
+@[simp, grind .] theorem node_unrel_node_iff {l₁ r₁ l₂ r₂ : CanonicalIdTree} {hz₁ ho₁ hz₂ ho₂} :
+    (node l₁ r₁ hz₁ ho₁) # (node l₂ r₂ hz₂ ho₂) ↔
+      l₁ # l₂ ∨ r₁ # r₂ ∨ (¬l₁ ≤ l₂ ∧ ¬r₂ ≤ r₁) ∨ (¬r₁ ≤ r₂ ∧ ¬l₂ ≤ l₁) := by grind
+
+end CanonicalIdTree
+
+/-! ### Clock Unrelated lemmas -/
+namespace Clock
+
+/-- Two clocks are unrelated iff their id components are unrelated -/
+@[simp, grind =] theorem unrel_iff : c₁ # c₂ ↔ c₁.i # c₂.i := by grind
+
+end Clock
+end UnrelLemmas
+end Unrel
+
+/-!
+## Fork
+Section 5.3.2 of [1]
+-/
+section Fork
+
+namespace IdTree
+def split : IdTree → IdTree × IdTree
+  | zero => (zero, zero)
+  | one => (.node one zero, .node zero one)
+  | node zero i =>
+      let i := split i
+      (node zero i.1, node zero i.2)
+  | node i zero =>
+      let i := split i
+      (node i.1 zero, node i.2 zero)
+  | node i₁ i₂ => (node i₁ zero, node zero i₂)
+
+section SplitLemmas
+variable {i : IdTree}
+
+@[simp, grind =] theorem split_zero : split zero = (zero, zero) := rfl
+@[simp, grind =] theorem split_one : split one = (.node one zero, .node zero one) := rfl
+@[simp, grind =] theorem split_node_zero  : split (node zero i) = (node zero (split i).1, node zero (split i).2) := rfl
+@[simp, grind =] theorem split_zero_node : split (node i zero) = (node (split i).1 zero, node (split i).2 zero) := by
+  cases i <;> rfl
+
+@[simp, grind =] theorem split_node_node {i₁ i₂ : IdTree} (h₁ : i₁ ≠ zero) (h₂ : i₂ ≠ zero) :
+    split (node i₁ i₂) = (node i₁ zero, node zero i₂) := by
+  simp only [split]
+
+@[simp, grind =] theorem split_fst_eq_zero_iff : (split i).1 = zero ↔ i = zero := by
+  cases i with
+  | node l r => cases l <;> cases r <;> grind
+  | _ => simp
+@[simp, grind =] theorem split_snd_eq_zero_iff : (split i).2 = zero ↔ i = zero := by
+  cases i with
+  | node l r => cases l <;> cases r <;> grind
+  | _ => simp
+
+@[simp, grind =] theorem normalize_split_fst (hi : i.normalize = i) :
+    (split i).1.normalize = (split i).1 := by
+  fun_induction IdTree.split i <;> grind
+
+@[simp, grind =] theorem normalize_split_snd (hi : i.normalize = i) :
+    (split i).2.normalize = (split i).2 := by
+  fun_induction IdTree.split i <;> grind
+
+end SplitLemmas
+end IdTree
+
+namespace CanonicalIdTree
+def split (i : CanonicalIdTree) : CanonicalIdTree × CanonicalIdTree :=
+  let is := i.raw.split
+  (⟨is.1, by grind⟩, ⟨is.2, by grind⟩)
+
+section SplitLemmas
+variable {i : CanonicalIdTree}
+
+@[simp] theorem split_mk {t : IdTree} {h : t.normalize = t} :
+    split ⟨t, h⟩ = (⟨t.split.1, by grind⟩, ⟨t.split.2, by grind⟩) := by
+  grind [split]
+
+@[simp, grind =] theorem raw_split_fst : (split i).1.raw = i.raw.split.1 := by simp [split]
+@[simp, grind =] theorem raw_split_snd : (split i).2.raw = i.raw.split.2 := by simp [split]
+
+/-- Custom functional induction principle for `CanonicalIdTree.split`. -/
+theorem split.induct_unfolding (motive : CanonicalIdTree → CanonicalIdTree × CanonicalIdTree → Prop)
+    (case1 : motive zero (zero, zero))
+    (case2 : ∀ ho hz, motive one (node one zero hz ho, node zero one (by simp) (by simp)))
+    (case3 : ∀ (i : CanonicalIdTree) (hi : i ≠ .zero),
+      motive i (split i) → ∀ hz ho, motive (node zero i hz ho)
+        (node zero (split i).1, node zero (split i).2))
+    (case4 : ∀ (i : CanonicalIdTree) (hi : i.raw ≠ .zero),
+      motive i (split i) →
+      ∀ hz ho, motive (node i zero hz ho)
+        (node (split i).1 zero, node (split i).2 zero))
+    (case5 : ∀ (i₁ i₂ : CanonicalIdTree) (h₁ : i₁ ≠ .zero) (h₂ : i₂ ≠ .zero),
+      ∀ hz ho, motive (node i₁ i₂ hz ho)
+        (node i₁ zero, node zero i₂))
+    (i : CanonicalIdTree) : motive i (split i) := by
+  rcases i with ⟨i, hi⟩
+  simp only [split_mk]
+  fun_induction IdTree.split i <;> grind
+
+theorem split_le : (split i).1 ≤ i ∧ (split i).2 ≤ i := by
+  induction i using split.induct_unfolding <;> grind
+
+@[simp, grind .] theorem split_fst_le : (split i).1 ≤ i := split_le.1
+@[simp, grind .] theorem split_snd_le : (split i).2 ≤ i := split_le.2
+
+theorem not_le_split (h : i ≠ zero) : ¬(i ≤ i.split.1) ∧ ¬(i ≤ i.split.2) := by
+  induction i using split.induct_unfolding <;> grind
+
+@[simp, grind .] theorem not_le_split_fst (h : i ≠ zero) : ¬(i ≤ i.split.1) := (not_le_split h).1
+@[simp, grind .] theorem not_le_split_snd (h : i ≠ zero) : ¬(i ≤ i.split.2) := (not_le_split h).2
+
+end SplitLemmas
+end CanonicalIdTree
+
+namespace Clock
+def fork (id : Clock) : Clock × Clock :=
+  let (i₁, i₂) := id.i.split
+  (⟨i₁, id.e⟩, ⟨i₂, id.e⟩)
+
+section ForkLemmas
+variable (c c' : Clock)
+
+@[simp, grind =] theorem i_fork_fst : c.fork.1.i = (c.i.split).1 := by rfl
+@[simp, grind =] theorem i_fork_snd : c.fork.2.i = (c.i.split).2 := by rfl
+@[simp, grind =] theorem e_fork_fst : c.fork.1.e = c.e := by rfl
+@[simp, grind =] theorem e_fork_snd : c.fork.2.e = c.e := by rfl
+
+/--
+`c` happens-before both results of `c.fork`
+-/
+theorem le_fork : c ≤ c.fork.fst ∧ c ≤ c.fork.snd := by grind
+
+variable {c c'} in
+/--
+If `c` is independent from `c'`, then the same holds for either result of `c.fork`.
+-/
+theorem indep_fork (h : c # c') : c.fork.fst # c' ∧ c.fork.snd # c' := by
+  sorry
+
+end ForkLemmas
+end Clock
+end Fork
+/-!
+## Join
+Section 5.3.3 of [1]
+-/
+section Join
+
+namespace IdTree
+def sum : IdTree → IdTree → IdTree
+  | zero, i | i, zero => i
+  | one, _i | _i, one => one
+  | node l₁ r₁, node l₂ r₂ =>
+    let l := sum l₁ l₂
+    let r := sum r₁ r₂
+    normalize (node l r)
+
+section SumLemmas
+variable {i₁ i₂ : IdTree}
+
+@[simp, grind =] theorem zero_sum : sum zero i₂ = i₂ := by rfl
+@[simp, grind =] theorem sum_zero : sum i₁ zero = i₁ := by cases i₁ <;> rfl
+@[simp, grind =] theorem one_sum : sum one i₂ = one := by cases i₂ <;> rfl
+@[simp, grind =] theorem sum_one : sum i₁ one = one := by cases i₁ <;> rfl
+
+@[simp, grind =] theorem node_sum_node {l₁ r₁ l₂ r₂ : IdTree} :
+    sum (node l₁ r₁) (node l₂ r₂) = normalize (node (sum l₁ l₂) (sum r₁ r₂)) := by rfl
+
+@[simp, grind =] theorem normalize_sum (h₁ : i₁.normalize = i₁) (h₂ : i₂.normalize = i₂) :
+    (sum i₁ i₂).normalize = sum i₁ i₂ := by
+  fun_induction sum i₁ i₂ <;> grind
+
+end SumLemmas
+end IdTree
+
+namespace CanonicalIdTree
+def sum (i₁ : CanonicalIdTree) (i₂ : CanonicalIdTree) : CanonicalIdTree :=
+  ⟨.sum i₁.raw i₂.raw, by grind⟩
+
+section SumLemmas
+variable {i₁ i₂ : CanonicalIdTree}
+
+@[simp] theorem sum_mk {t₁ t₂ : IdTree} {h₁ : t₁.normalize = t₁} {h₂ : t₂.normalize = t₂} :
+    sum ⟨t₁, h₁⟩ ⟨t₂, h₂⟩ = ⟨t₁.sum t₂, by grind⟩ := rfl
+
+/-- Custom functional induction principle for `CanonicalIdTree.sum`. -/
+theorem sum.induct_unfolding (motive : CanonicalIdTree → CanonicalIdTree → CanonicalIdTree → Prop)
+    (case1 : ∀ i, motive zero i i)
+    (case2 : ∀ i, motive i zero i)
+    (case3 : ∀ i, motive one i one)
+    (case4 : ∀ i, motive i one one)
+    (case5 : ∀ (l₁ r₁ l₂ r₂ : CanonicalIdTree) hz₁ ho₁ hz₂ ho₂,
+      motive l₁ l₂ (sum l₁ l₂) →
+      motive r₁ r₂ (sum r₁ r₂) →
+      motive (node l₁ r₁ hz₁ ho₁) (node l₂ r₂ hz₂ ho₂)
+        (node' (sum l₁ l₂) (sum r₁ r₂)))
+    (i₁ i₂ : CanonicalIdTree) : motive i₁ i₂ (sum i₁ i₂) := by
+  rcases i₁ with ⟨i₁, h₁⟩
+  rcases i₂ with ⟨i₂, h₂⟩
+  simp only [sum_mk]
+  fun_induction IdTree.sum i₁ i₂ with
+  | case5 l₁ r₁ l₂ r₂ l r ihl ihr =>
+      -- TODO: the following should be reducable to just `grind`, with appropriate grind-lemmas
+      have : l₁.normalize = l₁ := by grind
+      have : l₂.normalize = l₂ := by grind
+      have : r₁.normalize = r₁ := by grind
+      have : r₂.normalize = r₂ := by grind
+      simp [*]
+      apply case5 <;> (simp; grind)
+  | _ => grind
+
+theorem sum_le : i₁ ≤ sum i₁ i₂ ∧ i₂ ≤ sum i₁ i₂ := by
+  induction i₁, i₂ using sum.induct_unfolding <;> grind
+
+@[simp, grind .] theorem le_sum_left : i₁ ≤ sum i₁ i₂ := sum_le.1
+@[simp, grind .] theorem le_sum_right : i₂ ≤ sum i₁ i₂ := sum_le.2
+
+@[simp, grind =] theorem sum_eq_zero_iff : sum i₁ i₂ = zero ↔ i₁ = zero ∧ i₂ = zero := by
+  induction i₁, i₂ using sum.induct_unfolding <;> simp; grind
+
+
+/-
+TODO: Check if not_sum_lt actually holds, and finish proof
+-/
+theorem not_sum_lt (h : i₁ # i₂) : ¬(sum i₁ i₂ ≤ i₁) ∧ ¬(sum i₁ i₂ ≤ i₂) := by
+  have : i₁ ≠ zero := by grind
+  have : i₂ ≠ zero := by grind
+  induction i₁, i₂ using sum.induct_unfolding with
+  | case5 l₁ r₁ l₂ r₂ hz₁ ho₁ hz₂ ho₂ ihl ihr =>
+    sorry
+  | _ => grind
+
+-- @[simp, grind .] theorem not_sum_le_left (h₁ : i₁ ≠ zero) (h₂ : i₂ ≠ zero) : ¬(sum i₁ i₂ ≤ i₁) :=
+--   (not_sum_le h₁ h₂).1
+-- @[simp, grind .] theorem not_sum_le_right (h₁ : i₁ ≠ zero) (h₂ : i₂ ≠ zero) : ¬(sum i₁ i₂ ≤ i₂) :=
+--   (not_sum_le h₁ h₂).2
+
+end SumLemmas
+end CanonicalIdTree
+
+
+namespace Clock
+def join : Clock → Clock → Clock
+  | ⟨i₁, e₁⟩, ⟨i₂, e₂⟩ => ⟨i₁.sum i₂, max e₁ e₂ + 1⟩
+  -- -----------------------------------------  ^^^
+  -- For now, we're incrementing both here and in the fork/split semantics,
+  -- just to be sure. One of these ought to be redundant, but we'll figure out
+  -- which one later
+
+section JoinLemmas
+variable {c₁ c₂ c' : Clock}
+
+@[simp, grind =] theorem i_join : (c₁.join c₂).i = c₁.i.sum c₂.i := by rfl
+@[simp, grind =] theorem e_join : (c₁.join c₂).e = max c₁.e c₂.e + 1 := by rfl
+
+/--
+`c₁` and `c₂` both happen-before `c₁.join c₂`
+-/
+theorem le_join (c₁ c₂ : Clock) : c₁ ≤ c₁.join c₂ ∧ c₂ ≤ c₁.join c₂ := by grind
+
+@[simp, grind .] theorem le_join_fst : c₁ ≤ c₁.join c₂ := (le_join c₁ c₂).1
+@[simp, grind .] theorem le_join_snd : c₂ ≤ c₁.join c₂ := (le_join c₁ c₂).2
+
+/--
+If `c₁` and `c₂` are both independent from `c'`,
+then the same holds for `c₁.join c₂`.
+-/
+theorem indep_join (h₁ : c₁ # c') (h₂ : c₂ # c') : c₁.join c₂ # c' := by
+  -- TODO: finish proof
+  sorry
+
+end JoinLemmas
+end Clock
+end Join
diff --git a/EffectSSA/ITC/IdTree.lean b/EffectSSA/ITC/IdTree.lean
new file mode 100644
index 0000000..91920cb
--- /dev/null
+++ b/EffectSSA/ITC/IdTree.lean
@@ -0,0 +1,78 @@
+
+
+/-!
+# Id Trees
+These formalize the id component of an Interval Tree Clock.
+
+[1]: Almeida et al. "Interval Tree Clocks: A Logical Clock for Dynamic Systems"
+-/
+namespace EffectSSA.ITC
+
+/--
+An `IdTree` represents a subset of the interval `[0, 1]` as a binary tree with
+Booleans at the leaves.
+-/
+inductive IdTree
+  | zero
+  | one
+  | node (left : IdTree) (right : IdTree)
+  deriving DecidableEq
+
+/-!
+## Normal Forms
+Section 5.2 of [1]
+-/
+namespace IdTree
+
+def normalize : IdTree → IdTree
+  | zero => zero
+  | one => one
+  | node left right =>
+    match left.normalize, right.normalize with
+    | zero, zero => zero
+    | one, one => one
+    | left, right => node left right
+
+/-!
+## Lemmas
+-/
+section Lemmas
+variable {l r : IdTree}
+
+@[simp, grind =] theorem normalize_zero : normalize zero = zero := by rfl
+@[simp, grind =] theorem normalize_one : normalize one = one := by rfl
+
+@[simp, grind =] theorem normalize_normalize (i : IdTree) : (normalize i).normalize = normalize i := by
+  induction i <;> grind [normalize]
+
+@[simp, grind =] theorem normalize_node_eq_zero_iff :
+    normalize (node l r) = zero ↔ l.normalize = zero ∧ r.normalize = zero := by
+  grind [normalize]
+
+@[simp, grind =] theorem normalize_node_eq_one_iff :
+    normalize (node l r) = one ↔ l.normalize = one ∧ r.normalize = one := by
+  grind [normalize]
+
+/-!
+We'll often use an assumption of the form `i.normalize = i` to express that `i`
+is canonical. Although we don't introduce an explicit Lean definition, we do
+use the name *canonical* to refer to such assumption in theorems.
+-/
+
+
+@[simp, grind =] theorem node_canonical_iff :
+    normalize (node l r) = node l' r'
+    ↔ l.normalize = l' ∧ r.normalize = r'
+      ∧ ¬(l' = zero ∧ r' = zero) ∧ ¬(l' = one ∧ r' = one) := by
+  grind [normalize]
+
+@[simp, grind =] theorem zero_node_canonical_iff :
+    normalize (node zero r) = node zero r' ↔ r.normalize = r' ∧ r' ≠ zero := by grind
+
+@[simp, grind =] theorem node_zero_canonical_iff :
+    normalize (node l zero) = node l' zero ↔ l.normalize = l' ∧ l' ≠ zero := by grind
+
+
+-- theorem canonical_node_iff : (node l r).normalize = (node l r)
+
+end Lemmas
diff --git a/EffectSSA/ITC/Lemmas.lean b/EffectSSA/ITC/Lemmas.lean
new file mode 100644
index 0000000..e69de29
diff --git a/EffectSSA/ITC/Ops.lean b/EffectSSA/ITC/Ops.lean
new file mode 100644
index 0000000..e69de29
diff --git a/EffectSSA/ITC/Scratch.lean b/EffectSSA/ITC/Scratch.lean
new file mode 100644
index 0000000..7ad3bd6
--- /dev/null
+++ b/EffectSSA/ITC/Scratch.lean
@@ -0,0 +1,31 @@
+
+structure NonZeroNat where
+  raw : Nat
+  h : raw ≠ 0 := by grind
+
+namespace NonZeroNat
+
+instance : OfNat NonZeroNat (n + 1) where
+  ofNat := { raw := n + 1 }
+
+@[simp, grind =] theorem raw_ofNat (m : Nat) : raw (OfNat.ofNat (m + 1)) = m + 1 := by rfl
+
+@[ext, grind ext] theorem ext {n m : NonZeroNat} (h : n.raw = m.raw) : n = m := by
+  cases n; cases m; grind
+
+/-- info: NonZeroNat.ext_iff {n m : NonZeroNat} : n = m ↔ n.raw = m.raw -/
+#guard_msgs in #check NonZeroNat.ext_iff
+
+attribute [simp, grind =_] NonZeroNat.ext_iff
+-- -------------------^^^
+-- I would like this to be just `grind =`, to make the rewrite work the same in
+-- `grind` as in `simp`, but that gives the following error:
+-- ```
+--   invalid pattern, (non-forbidden) application expected
+--     #1
+-- ```
+
+@[simp]
+theorem eq_one_iff : (1 : NonZeroNat) ≠ 2 := by
+  simp; grind
+  -- ^^ This proof does not go through with just `grind`

From df1e9be32c21daf48028a93df9b73bc0d8a9754e Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Fri, 6 Mar 2026 17:58:52 +0000
Subject: [PATCH 2/7] cleanup, remove stale comment

---
 EffectSSA/ITC/Clock.lean | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/EffectSSA/ITC/Clock.lean b/EffectSSA/ITC/Clock.lean
index 5457f20..e885a4e 100644
--- a/EffectSSA/ITC/Clock.lean
+++ b/EffectSSA/ITC/Clock.lean
@@ -429,12 +429,9 @@ end CanonicalIdTree
 
 
 namespace Clock
-def join : Clock → Clock → Clock
-  | ⟨i₁, e₁⟩, ⟨i₂, e₂⟩ => ⟨i₁.sum i₂, max e₁ e₂ + 1⟩
-  -- -----------------------------------------  ^^^
-  -- For now, we're incrementing both here and in the fork/split semantics,
-  -- just to be sure. One of these ought to be redundant, but we'll figure out
-  -- which one later
+def join (c₁ : Clock) (c₂ : Clock) : Clock where
+  i := .sum c₁.i c₂.i
+  e := (max c₁.e c₂.e) + 1
 
 section JoinLemmas
 variable {c₁ c₂ c' : Clock}

From f456e88cf86311cbf7e95f400aba6d93adffaa6a Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Fri, 6 Mar 2026 18:01:23 +0000
Subject: [PATCH 3/7] add both flavours of indep_fork statement

---
 EffectSSA/ITC/Clock.lean | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/EffectSSA/ITC/Clock.lean b/EffectSSA/ITC/Clock.lean
index e885a4e..962619e 100644
--- a/EffectSSA/ITC/Clock.lean
+++ b/EffectSSA/ITC/Clock.lean
@@ -319,11 +319,17 @@ variable (c c' : Clock)
 -/
 theorem le_fork : c ≤ c.fork.fst ∧ c ≤ c.fork.snd := by grind
 
+/--
+`c.fork.fst` is independent from `c.fork.snd`.
+-/
+theorem indep_fork: c.fork.fst # c.fork.snd := by
+  sorry
+
 variable {c c'} in
 /--
 If `c` is independent from `c'`, then the same holds for either result of `c.fork`.
 -/
-theorem indep_fork (h : c # c') : c.fork.fst # c' ∧ c.fork.snd # c' := by
+theorem indep_fork' (h : c # c') : c.fork.fst # c' ∧ c.fork.snd # c' := by
   sorry
 
 end ForkLemmas

From 771bacd49b693202806f029f7ae5ea42efe221ef Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Fri, 6 Mar 2026 18:01:35 +0000
Subject: [PATCH 4/7] format

---
 EffectSSA/ITC/Clock.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/EffectSSA/ITC/Clock.lean b/EffectSSA/ITC/Clock.lean
index 962619e..524a9ad 100644
--- a/EffectSSA/ITC/Clock.lean
+++ b/EffectSSA/ITC/Clock.lean
@@ -322,7 +322,7 @@ theorem le_fork : c ≤ c.fork.fst ∧ c ≤ c.fork.snd := by grind
 /--
 `c.fork.fst` is independent from `c.fork.snd`.
 -/
-theorem indep_fork: c.fork.fst # c.fork.snd := by
+theorem indep_fork : c.fork.fst # c.fork.snd := by
   sorry
 
 variable {c c'} in

From 452238d53283aa3a26ee0ef31311ccb6ec730238 Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Fri, 6 Mar 2026 18:18:51 +0000
Subject: [PATCH 5/7] rename indep_fork'

---
 EffectSSA/ITC/Clock.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/EffectSSA/ITC/Clock.lean b/EffectSSA/ITC/Clock.lean
index 524a9ad..f2c0362 100644
--- a/EffectSSA/ITC/Clock.lean
+++ b/EffectSSA/ITC/Clock.lean
@@ -320,7 +320,7 @@ variable (c c' : Clock)
 theorem le_fork : c ≤ c.fork.fst ∧ c ≤ c.fork.snd := by grind
 
 /--
-`c.fork.fst` is independent from `c.fork.snd`.
+The results of a `fork` are independent.
 -/
 theorem indep_fork : c.fork.fst # c.fork.snd := by
   sorry
@@ -329,7 +329,7 @@ variable {c c'} in
 /--
 If `c` is independent from `c'`, then the same holds for either result of `c.fork`.
 -/
-theorem indep_fork' (h : c # c') : c.fork.fst # c' ∧ c.fork.snd # c' := by
+theorem indep_fork_congr (h : c # c') : c.fork.fst # c' ∧ c.fork.snd # c' := by
   sorry
 
 end ForkLemmas
@@ -457,7 +457,7 @@ theorem le_join (c₁ c₂ : Clock) : c₁ ≤ c₁.join c₂ ∧ c₂ ≤ c₁.
 If `c₁` and `c₂` are both independent from `c'`,
 then the same holds for `c₁.join c₂`.
 -/
-theorem indep_join (h₁ : c₁ # c') (h₂ : c₂ # c') : c₁.join c₂ # c' := by
+theorem indep_join_congr (h₁ : c₁ # c') (h₂ : c₂ # c') : c₁.join c₂ # c' := by
   -- TODO: finish proof
   sorry
 

From 74abad9e785342b04851bb48901c9ea9353ce812 Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Fri, 6 Mar 2026 18:22:14 +0000
Subject: [PATCH 6/7] prove indep_fork

---
 EffectSSA/ITC/Clock.lean | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/EffectSSA/ITC/Clock.lean b/EffectSSA/ITC/Clock.lean
index f2c0362..c6be2ed 100644
--- a/EffectSSA/ITC/Clock.lean
+++ b/EffectSSA/ITC/Clock.lean
@@ -298,6 +298,9 @@ theorem not_le_split (h : i ≠ zero) : ¬(i ≤ i.split.1) ∧ ¬(i ≤ i.split
 @[simp, grind .] theorem not_le_split_fst (h : i ≠ zero) : ¬(i ≤ i.split.1) := (not_le_split h).1
 @[simp, grind .] theorem not_le_split_snd (h : i ≠ zero) : ¬(i ≤ i.split.2) := (not_le_split h).2
 
+@[simp, grind .] theorem indep_split (h : i ≠ zero) : i.split.fst # i.split.snd := by
+  induction i using split.induct_unfolding <;> grind
+
 end SplitLemmas
 end CanonicalIdTree
 
@@ -322,8 +325,7 @@ theorem le_fork : c ≤ c.fork.fst ∧ c ≤ c.fork.snd := by grind
 /--
 The results of a `fork` are independent.
 -/
-theorem indep_fork : c.fork.fst # c.fork.snd := by
-  sorry
+theorem indep_fork (h : c.i ≠ .zero) : c.fork.fst # c.fork.snd := by grind
 
 variable {c c'} in
 /--

From 04a48b00e9ab4faeb70769120ce20d0eb53c4d2d Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Fri, 6 Mar 2026 22:52:46 +0000
Subject: [PATCH 7/7] not_fork_le, show that id-order is a pre-order

---
 EffectSSA/ITC/Clock.lean | 33 +++++++++++++++++++++++++++++----
 1 file changed, 29 insertions(+), 4 deletions(-)

diff --git a/EffectSSA/ITC/Clock.lean b/EffectSSA/ITC/Clock.lean
index c6be2ed..4828185 100644
--- a/EffectSSA/ITC/Clock.lean
+++ b/EffectSSA/ITC/Clock.lean
@@ -115,6 +115,14 @@ instance : DecidableLE CanonicalIdTree := by
   <;> grind
 
 @[simp, grind .] theorem le_refl : i ≤ i := by induction i <;> grind
+@[simp, grind .] theorem le_trans {i₁ i₂ i₃ : CanonicalIdTree} : i₁ ≤ i₂ → i₂ ≤ i₃ → i₁ ≤ i₃ := by
+  induction i₁ generalizing i₂ i₃ <;> try grind
+  cases i₂ <;> try grind
+  cases i₃ <;> grind
+
+instance : Std.IsPreorder CanonicalIdTree where
+  le_refl _ := le_refl
+  le_trans _ _ _ := le_trans
 
 -- NOTE: we deliberatelyy put `le_iff` just before closing the namespace, as it
 --       would otherwise cause divergence with the local `le_iff'` simp-lemma.
@@ -164,12 +172,25 @@ section GenericUnrelLemmas
 variable {α : Type _} [LE α] {x y : α}
 
 @[grind =] theorem unrel_iff : x # y ↔ ¬(x ≤ y) ∧ ¬(y ≤ x) := by rfl
+@[grind =] theorem not_unrel_iff : ¬(x # y) ↔ x ≤ y ∨ y ≤ x := by grind
 
 instance [DecidableLE α] : Decidable (x # y) := by unfold Unrelated; infer_instance
 
+/-- `#` is symmetric -/
 theorem unrel_symm : x # y ↔ y # x := by grind
+instance : Std.Symm (@Unrelated α _) where
+  symm _ _ := @unrel_symm.mp
+
+/-!
+`#` is irreflexive (when `≤` is reflexive)
+-/
+
 theorem unrel_refl_iff : x # x ↔ ¬(x ≤ x) := by grind
 
+@[simp, grind .] theorem unrel_irrefl [Std.Refl (@LE.le α _)] (x : α) : ¬(x # x) := by
+  simp [unrel_refl_iff, Std.Refl.refl]
+instance [Std.Refl (@LE.le α _)] : Std.Irrefl (@Unrelated α _) where irrefl := unrel_irrefl
+
 end GenericUnrelLemmas
 
 variable {i j : CanonicalIdTree} {c₁ c₂ : Clock}
@@ -177,7 +198,7 @@ variable {i j : CanonicalIdTree} {c₁ c₂ : Clock}
 /-! ### CanonicalIdTree Unrelated lemmas -/
 namespace CanonicalIdTree
 
-@[simp, grind .] theorem unrefl_irrefl : ¬(i # i) := by grind
+@[simp, grind .] theorem unrel_irrefl : ¬(i # i) := by grind
 
 @[simp, grind .] theorem not_unrel_zero : ¬(i # zero) := by grind
 @[simp, grind .] theorem not_zero_unrel : ¬(zero # j) := by grind
@@ -317,10 +338,14 @@ variable (c c' : Clock)
 @[simp, grind =] theorem e_fork_fst : c.fork.1.e = c.e := by rfl
 @[simp, grind =] theorem e_fork_snd : c.fork.2.e = c.e := by rfl
 
-/--
-`c` happens-before both results of `c.fork`
+/-!
+`c` (strictly) happens-before both results of `c.fork`
 -/
-theorem le_fork : c ≤ c.fork.fst ∧ c ≤ c.fork.snd := by grind
+@[simp, grind .] theorem le_fork_snd : c ≤ c.fork.snd := by grind
+@[simp, grind .] theorem le_fork_fst : c ≤ c.fork.fst := by grind
+
+@[simp, grind .] theorem not_fork_fst_le (h : c.i ≠ .zero) : ¬(c.fork.fst ≤ c) := by grind
+@[simp, grind .] theorem not_fork_snd_le (h : c.i ≠ .zero) : ¬(c.fork.snd ≤ c) := by grind
 
 /--
 The results of a `fork` are independent.