Skip to content

cleanup: remove dead lemmas and simplify verbose proofs #11

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
zachary-kent wants to merge 2 commits into
base: main
Choose a base branch
from
Draft

cleanup: remove dead lemmas and simplify verbose proofs #11

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
f97128e
fix: compatibility fixes for nightly-2026-04-29
May 21, 2026
8ffabf7
cleanup: remove dead lemmas and simplify verbose proofs
May 21, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 1 addition & 15 deletions autoclrs/ch16-greedy/CLRS.Ch16.Huffman.PQForest.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -866,21 +866,7 @@ let merge_bundle_step_aux
cost_invariant_from_merge_bundle freq_seq nd_old pq0 pq1 active0 n
freq1 freq2 idx1 idx2 j1 j2;
cost_invariant_merge_step active0 j1 j2 freq1 freq2 sum_freq idx1 merged
t1 t2 (seq_to_pos_list freq_seq 0);
// Assert postcondition conjuncts explicitly to help Z3 assemble them
assert (valid_pq_entries pq3 n);
assert (pq_freqs_positive pq3);
assert (pq_idx_unique pq3);
assert (pq_indices_in_forest pq3 new_active);
assert (pq_tree_freq_match pq3 new_active);
assert (forest_has_pq_entry pq3 new_active);
assert (forest_distinct_indices new_active);
assert (forall (k: nat). k < L.length new_active ==>
SZ.v (entry_idx (L.index new_active k)) < n /\
Seq.index nd_new (SZ.v (entry_idx (L.index new_active k))) == entry_ptr (L.index new_active k));
assert (forall (x: pos). L.count x (all_leaf_freqs new_active) == L.count x (seq_to_pos_list freq_seq 0));
assert (forest_total_cost new_active + HOpt.greedy_cost (forest_root_freqs new_active) ==
HOpt.greedy_cost (seq_to_pos_list freq_seq 0))
t1 t2 (seq_to_pos_list freq_seq 0)
#pop-options

let merge_bundle_step
Expand Down
105 changes: 0 additions & 105 deletions autoclrs/ch22-elementary-graph/CLRS.Ch22.BFS.Impl.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -278,15 +278,6 @@ let blacken_preserves_pred_dist_ok
PREDICATE LEMMAS — Key reasoning steps for BFS proof
================================================================ *)

(* Discovering (WHITE->GRAY) preserves source_ok *)
let discover_preserves_source_ok
(scolor sdist: Seq.seq int) (source n j: nat) (dval: int)
: Lemma
(requires source_ok scolor sdist source n /\ j < n /\ n <= Seq.length scolor /\
n <= Seq.length sdist /\ Seq.index scolor j == 0 /\ dval >= 0)
(ensures source_ok (Seq.upd scolor j 1) (Seq.upd sdist j dval) source n)
= () // source != j (source is non-WHITE, j is WHITE)

(* Blackening preserves source_ok *)
let blacken_preserves_source_ok
(scolor sdist: Seq.seq int) (source n u: nat)
Expand All @@ -295,15 +286,6 @@ let blacken_preserves_source_ok
(ensures source_ok (Seq.upd scolor u 2) sdist source n)
= () // Either u == source (2 <> 0) or u != source (unchanged)

(* Discovering preserves dist_ok *)
let discover_preserves_dist_ok
(scolor sdist: Seq.seq int) (n j: nat) (dval: int)
: Lemma
(requires dist_ok scolor sdist n /\ j < n /\ n <= Seq.length scolor /\
n <= Seq.length sdist /\ Seq.index scolor j == 0 /\ dval >= 0)
(ensures dist_ok (Seq.upd scolor j 1) (Seq.upd sdist j dval) n)
= () // old non-WHITE: unchanged; j: new color 1, dist dval >= 0

(* Discovering vertex j from u preserves dist_reachable.
Precondition: u is discovered (color[u] <> 0) with dist[u] = du,
edge (u, j) exists, j is WHITE, and we set dist[j] = du + 1.
Expand Down Expand Up @@ -347,15 +329,6 @@ let blacken_preserves_dist_ok
(ensures dist_ok (Seq.upd scolor u 2) sdist n)
= () // For w != u: unchanged. For w == u: was non-WHITE so dist >= 0, still >= 0.

(* Discovering preserves queue_ok for existing entries *)
let discover_preserves_queue_ok
(scolor: Seq.seq int) (squeue: Seq.seq SZ.t) (n head tail j: nat)
: Lemma
(requires queue_ok scolor squeue n head tail /\ j < n /\ n <= Seq.length scolor /\
Seq.index scolor j == 0)
(ensures queue_ok (Seq.upd scolor j 1) squeue n head tail)
= () // Queue entries are non-WHITE, j is WHITE, so j != any queue entry. Colors unchanged.

(* Blackening preserves queue_ok when u is not in queue range *)
let blacken_preserves_queue_ok
(scolor: Seq.seq int) (squeue: Seq.seq SZ.t) (n head tail u: nat)
Expand All @@ -379,22 +352,6 @@ let frame_preserves_source_ok
(ensures source_ok scolor' sdist' source n)
= ()

(* Frame preserves dist_ok when only WHITE->non-WHITE changes with non-negative dist *)
let frame_preserves_dist_ok
(scolor scolor' sdist sdist': Seq.seq int) (n: nat)
: Lemma
(requires
dist_ok scolor sdist n /\
Seq.length scolor' >= n /\ Seq.length sdist' >= n /\
// Frame: old non-WHITE unchanged
(forall (w:nat). w < n /\ Seq.index scolor w <> 0 ==>
Seq.index scolor' w == Seq.index scolor w /\ Seq.index sdist' w == Seq.index sdist w) /\
// New non-WHITE vertices have non-negative dist
(forall (w:nat). w < n /\ Seq.index scolor w == 0 /\ Seq.index scolor' w <> 0 ==>
Seq.index sdist' w >= 0))
(ensures dist_ok scolor' sdist' n)
= ()

(* Proving queue_ok after discovering a WHITE vertex.
Uses exact Seq.upd terms so Z3 can chain:
- Seq.upd axiom fires on conclusion → introduces Seq.index squeue i
Expand Down Expand Up @@ -458,16 +415,6 @@ let blacken_preserves_scanned_all (sadj scolor: Seq.seq int) (n u: nat)
(ensures scanned_all sadj n (Seq.upd scolor u 2))
= ()

let init_scanned_partial (sadj scolor: Seq.seq int) (n u: nat)
: Lemma (requires n <= Seq.length scolor /\ n * n <= Seq.length sadj /\ u < n)
(ensures scanned_partial sadj n scolor u 0)
= ()

let discover_preserves_scanned_partial (sadj scolor: Seq.seq int) (n u k j: nat)
: Lemma (requires scanned_partial sadj n scolor u k /\ j < n /\ Seq.index scolor j == 0)
(ensures scanned_partial sadj n (Seq.upd scolor j 1) u k)
= ()

let extend_scanned_partial_discover (sadj scolor: Seq.seq int) (n u vv: nat)
: Lemma
(requires scanned_partial sadj n scolor u vv /\ vv < n /\ u < n /\
Expand All @@ -483,12 +430,6 @@ let extend_scanned_partial_skip (sadj scolor: Seq.seq int) (n u vv: nat)
(ensures scanned_partial sadj n scolor u (vv + 1))
= ()

let blacken_preserves_scanned_partial (sadj scolor: Seq.seq int) (n u k: nat)
: Lemma (requires scanned_partial sadj n scolor u k /\ u < n /\ n <= Seq.length scolor /\
Seq.index scolor u <> 0)
(ensures scanned_partial sadj n (Seq.upd scolor u 2) u k)
= ()

(* ================================================================
COMPLETENESS LEMMA — induction on reachability steps
================================================================ *)
Expand Down Expand Up @@ -675,24 +616,6 @@ let init_dist_optimal (adj: Seq.seq int) (n: nat) (scolor_zeros sdist_zeros: Seq
dist_optimal adj n (Seq.upd scolor_zeros source 1) (Seq.upd sdist_zeros source 0) source)
= () // Only source is non-WHITE (color 1) with dist 0. 0 <= k for any nat k.

let init_layer_complete (adj: Seq.seq int) (n: nat) (scolor: Seq.seq int) (source: nat)
: Lemma
(requires source < n /\ n <= Seq.length scolor /\ Seq.length adj >= n * n)
(ensures layer_complete adj n scolor source 0)
= () // Vacuously true: no k < 0.

let init_queue_dist_min (sdist: Seq.seq int) (squeue: Seq.seq SZ.t) (n head tail: nat) (d: int)
: Lemma
(requires
n >= 1 /\ Seq.length sdist >= n /\ Seq.length squeue >= n /\
head <= tail /\ tail <= n /\ d <= 0 /\
(forall (i: nat). {:pattern (Seq.index squeue i)}
i >= head /\ i < tail ==>
SZ.v (Seq.index squeue i) < n /\
Seq.index sdist (SZ.v (Seq.index squeue i)) >= 0))
(ensures queue_dist_min sdist squeue n head tail d)
= ()

let init_queue_nondecreasing (sdist: Seq.seq int) (squeue: Seq.seq SZ.t) (n: nat) (source: SZ.t)
: Lemma
(requires
Expand Down Expand Up @@ -819,27 +742,6 @@ let blacken_preserves_dist_optimal
dist_optimal adj n (Seq.upd scolor u 2) sdist source)
= () // Blackening only changes color (not dist). Non-WHITE stays non-WHITE.

let blacken_preserves_layer_complete
(adj: Seq.seq int) (n: nat) (scolor: Seq.seq int) (source d u: nat)
: Lemma
(requires
layer_complete adj n scolor source d /\
u < n /\ Seq.index scolor u <> 0 /\
Seq.length scolor >= n)
(ensures
layer_complete adj n (Seq.upd scolor u 2) source d)
= () // Blackening u: was non-WHITE → now color 2 (≠0, ≠1). Only strengthens layer_complete.

let blacken_preserves_queue_dist_min
(sdist: Seq.seq int) (squeue: Seq.seq SZ.t) (n head tail u: nat) (d: int)
: Lemma
(requires
queue_dist_min sdist squeue n head tail d /\
u < n)
(ensures
queue_dist_min sdist squeue n head tail d)
= () // Blackening doesn't change dist or queue.

(* --- Queue ordering preservation lemmas --- *)

let discover_preserves_queue_nondecreasing
Expand Down Expand Up @@ -882,13 +784,6 @@ let blacken_preserves_queue_nondecreasing
(ensures queue_nondecreasing sdist squeue n head tail)
= ()

let blacken_preserves_queue_dist_ub
(sdist: Seq.seq int) (squeue: Seq.seq SZ.t) (n head tail u: nat) (d_ub: int)
: Lemma
(requires queue_dist_ub sdist squeue n head tail d_ub /\ u < n)
(ensures queue_dist_ub sdist squeue n head tail d_ub)
= ()

(* Derive queue_dist_min from queue_nondecreasing: if queue is non-decreasing and
front has dist d, then all entries have dist >= d.
This is a transitivity argument: dist[queue[head]] <= dist[queue[i]] for all i >= head. *)
Expand Down
6 changes: 1 addition & 5 deletions autoclrs/ch22-elementary-graph/CLRS.Ch22.DFS.Impl.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -622,11 +622,7 @@ let final_pred_finish_lemma
let lemma_dfs_bound_correct (outer_count inner_count n: nat)
: Lemma (requires n >= 1 /\ outer_count <= n /\ inner_count <= n * n)
(ensures outer_count + inner_count <= 2 * (n * n))
= assert (outer_count <= n);
assert (n <= n * n);
assert (outer_count + inner_count <= n + n * n);
assert (n + n * n <= n * n + n * n);
assert (n * n + n * n == 2 * (n * n))
= ()

(* ================================================================
SUM_SCAN_IDX — sum of scan_idx values for complexity accounting
Expand Down
121 changes: 11 additions & 110 deletions autoclrs/ch23-mst/CLRS.Ch23.Kruskal.Spec.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -392,16 +392,7 @@ let rec lemma_kruskal_process_maximal_forest
assert (same_component forest e'.u e'.v);
same_component_mono forest e e'.u e'.v
end
end;

eliminate exists (prefix: list edge). all_sorted == prefix @ (e :: rest)
returns (exists (prefix': list edge). all_sorted == prefix' @ rest)
with _. begin
List.Tot.Properties.append_assoc prefix [e] rest;
assert (all_sorted == (prefix @ [e]) @ rest)
end;

lemma_kruskal_process_maximal_forest rest all_sorted forest' n
end
end else begin
assert (forest' == forest);
introduce forall (e': edge). mem_edge e' all_sorted /\ ~(mem_edge e' rest) /\
Expand All @@ -425,17 +416,17 @@ let rec lemma_kruskal_process_maximal_forest
assert (~(mem_edge e' sorted_edges));
()
end
end
end;

eliminate exists (prefix: list edge). all_sorted == prefix @ (e :: rest)
returns (exists (prefix': list edge). all_sorted == prefix' @ rest)
with _. begin
List.Tot.Properties.append_assoc prefix [e] rest;
assert (all_sorted == (prefix @ [e]) @ rest)
end;

eliminate exists (prefix: list edge). all_sorted == prefix @ (e :: rest)
returns (exists (prefix': list edge). all_sorted == prefix' @ rest)
with _. begin
List.Tot.Properties.append_assoc prefix [e] rest;
assert (all_sorted == (prefix @ [e]) @ rest)
end;

lemma_kruskal_process_maximal_forest rest all_sorted forest' n
end

lemma_kruskal_process_maximal_forest rest all_sorted forest' n

// MST invariant: kruskal_process maintains "forest is subset of some MST"
// This needs the "minimum weight among unused cross-component edges" property
Expand Down Expand Up @@ -1202,10 +1193,6 @@ let rec count_pred (f: nat -> bool) (n: nat) : nat =
let count_reachable (es: list edge) (root: nat) (n m: nat) : nat =
count_pred (fun v -> v < n && same_component_dec es root v) m

let rec count_pred_le (f: nat -> bool) (n: nat)
: Lemma (ensures count_pred f n <= n) (decreases n)
= if n = 0 then () else count_pred_le f (n - 1)

// If f1 implies f2, count f1 ≤ count f2
let rec count_pred_mono (f1 f2: (nat -> bool)) (n: nat)
: Lemma (requires forall (i: nat). i < n ==> f1 i ==> f2 i)
Expand Down Expand Up @@ -1337,14 +1324,6 @@ let reachable_uses_component_edges (es: list edge) (root v: nat)
path_in_filtered path
end

// The component filter respects edge_eq
let component_filter_respects_eq (es: list edge) (root: nat) (e1 e2: edge)
: Lemma (requires edge_eq e1 e2)
(ensures (let g = fun (e: edge) -> same_component_dec es root e.u &&
same_component_dec es root e.v in
g e1 = g e2))
= edge_eq_endpoints e1 e2

// Bridge edge decomposition: symmetric version (e.v reachable, e.u not)
let bridge_edge_reachability_sym (tl: list edge) (e: edge) (root v: nat)
: Lemma (requires same_component tl root e.v /\ ~(same_component tl root e.u) /\
Expand Down Expand Up @@ -1918,12 +1897,6 @@ let component_of_empty (v: nat) (n: nat)
(ensures component_of [] v n == [v])
= vertices_in_component_empty v n 0

/// Helper: vertex j is not in component_of [] i n when i <> j and both < n
let not_in_different_component_empty (i j: nat) (n: nat)
: Lemma (requires i < n /\ j < n /\ i <> j)
(ensures ~(mem j (component_of [] i n)))
= component_of_empty i n

/// Helper: build_components with empty edges produces n singletons
#push-options "--fuel 2 --ifuel 1 --z3rlimit 5"
let rec build_components_empty_length (n: nat) (i: nat{i <= n})
Expand Down Expand Up @@ -1979,76 +1952,4 @@ let rec build_components_empty_length (n: nat) (i: nat{i <= n})
end
#pop-options

// Initially n components (each vertex is its own component)
let lemma_initial_components (n: nat)
: Lemma (requires n > 0)
(ensures length (components [] n) = n)
= build_components_empty_length n 0 []

// Final spanning tree has 1 component
let lemma_spanning_tree_one_component (g: graph) (t: list edge)
: Lemma (requires is_spanning_tree g t)
(ensures length (components t g.n) = 1)
= // all_connected g.n t: forall v < g.n. reachable t 0 v
// So same_component t 0 v for all v < g.n
// By BFS completeness: same_component_dec t 0 v = true for all v < g.n
let n = g.n in
assert (n > 0);
assert (all_connected n t);

// Step 1: same_component_dec t 0 v = true for all v < n
let aux_dec (v: nat)
: Lemma (requires v < n) (ensures same_component_dec t 0 v = true)
= assert (reachable t 0 v);
same_component_dec_complete t 0 v
in

// Step 2: vertices_in_component t 0 n i includes all vertices from i to n-1
let rec all_in_component (i: nat{i <= n})
: Lemma (ensures forall (v: nat). i <= v /\ v < n ==>
mem v (vertices_in_component t 0 n i))
(decreases (n - i))
= if i >= n then ()
else begin
aux_dec i;
assert (same_component_dec t 0 i = true);
all_in_component (i + 1);
// vertices_in_component t 0 n i = i :: vertices_in_component t 0 n (i+1)
// All v with i+1 <= v < n are in the tail (by IH)
// And i itself is the head
()
end
in
all_in_component 0;
// component_of t 0 n contains all vertices 0..n-1
assert (forall (v: nat). v < n ==> mem v (component_of t 0 n));

// Step 3: in_some_component returns true for all v < n when acc = [component_of t 0 n]
let in_comp_of_0 (v: nat)
: Lemma (requires v < n)
(ensures in_some_component v [component_of t 0 n] = true)
= assert (mem v (component_of t 0 n))
in

// Step 4: build_components with i=0 creates exactly [component_of t 0 n]
// At i=0: 0 is not in acc=[]. Creates component_of t 0 n. acc = [component_of t 0 n].
// For i=1..n-1: i is in component_of t 0 n, so in_some_component i acc = true. Skip.
let rec build_one_comp (i: nat{i <= n})
: Lemma (requires i > 0)
(ensures build_components t n i [component_of t 0 n] == [component_of t 0 n])
(decreases (n - i))
= if i >= n then ()
else begin
in_comp_of_0 i;
assert (in_some_component i [component_of t 0 n] = true);
build_one_comp (i + 1)
end
in

// At i=0: 0 is not in [], creates component_of t 0 n
in_some_component_false 0 ([] #(list nat));
assert (in_some_component 0 ([] #(list nat)) = false);
// build_components t n 0 [] = build_components t n 1 [component_of t 0 n]
if n > 1 then build_one_comp 1
else ()
// Result: [component_of t 0 n], length = 1
Loading