From 4344ec36d160fa9b5bf04bc72ce27c9d2159b3eb Mon Sep 17 00:00:00 2001 From: Jesse Alama Date: Tue, 27 Oct 2026 06:26:00 +0000 Subject: [PATCH 1/4] chore(Circuit): prove a synthesis step directly instead of with grind --- Cslib/Computability/Circuit/Full.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Cslib/Computability/Circuit/Full.lean b/Cslib/Computability/Circuit/Full.lean index 20377cf48..b163ec43c 100644 --- a/Cslib/Computability/Circuit/Full.lean +++ b/Cslib/Computability/Circuit/Full.lean @@ -124,8 +124,7 @@ private theorem exists_full_synthesis_finset [DecidableEq U] obtain ⟨a, ha⟩ := exists_full_synthesis_point (f point) default point obtain ⟨b, hb⟩ := ih have hstep := ha.full_binary hb (fun v acc => if v = default then acc else v) - use a + b + 1 - grind only [= Finset.mem_insert] + exact ⟨_, by convert hstep using 2; funext x; by_cases hx : x = point <;> simp [hx, hp]⟩ private theorem fullInterpretation_isComplete_two [Finite U] : (fullInterpretation (k := 2) (Carrier := U)).IsComplete where From 2a98f503d8778e1342970aeafab8c17337b9e66e Mon Sep 17 00:00:00 2001 From: Jesse Alama Date: Tue, 27 Oct 2026 06:40:00 +0000 Subject: [PATCH 2/4] chore(CCS/VendingMachine): merge tactics into grind --- Cslib/Algorithms/CCS/VendingMachine.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Cslib/Algorithms/CCS/VendingMachine.lean b/Cslib/Algorithms/CCS/VendingMachine.lean index dc964d4ad..601d173b8 100644 --- a/Cslib/Algorithms/CCS/VendingMachine.lean +++ b/Cslib/Algorithms/CCS/VendingMachine.lean @@ -84,8 +84,7 @@ theorem vm_ltsD_ltsND_not_bisim : ¬(vm ~[ltsD, ltsND] vm) := by let p₁ := `(CCS| (Tea. const Constant.vm) + (Coffee. const Constant.vm)) let q₁ := `(CCS| Tea. const Constant.vm) have ltsD_vm_deterministic : ltsD.DeterministicStateLabel vm Coin := by - intro _ _ htr₁ htr₂ - grind [const_tr htr₁, const_tr htr₂] + grind have h : r p₁ q₁ := match_deterministic hbisim hr From 9915512df0b4f0383999f31f2d90674f5e76f22d Mon Sep 17 00:00:00 2001 From: Jesse Alama Date: Tue, 27 Oct 2026 06:54:00 +0000 Subject: [PATCH 3/4] doc(Query): close an inline code span in a docstring --- Cslib/Algorithms/Lean/Query/Sort/LowerBound.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Cslib/Algorithms/Lean/Query/Sort/LowerBound.lean b/Cslib/Algorithms/Lean/Query/Sort/LowerBound.lean index d514b7203..cf8dec5c6 100644 --- a/Cslib/Algorithms/Lean/Query/Sort/LowerBound.lean +++ b/Cslib/Algorithms/Lean/Query/Sort/LowerBound.lean @@ -53,8 +53,8 @@ private theorem finPrefix_injective (h : ↑n ≤ #α) : (finEmbedding h).injective.extend_of_disjoint Sum.inl_injective Sum.inr_injective Set.isCompl_range_inl_range_inr.disjoint -/-- A total order on an type `α` with at least `n` elements, that orders `n` embedded elements - (via `finEmbedding) according to `σ⁻¹`, with embedded elements +/-- A total order on a type `α` with at least `n` elements, that orders `n` embedded elements + (via `finEmbedding`) according to `σ⁻¹`, with embedded elements preceding all others, and a well-ordering among non-embedded elements. -/ private noncomputable def PrefixPermOrder (h : ↑n ≤ #α) (σ : Equiv.Perm (Fin n)) : α → α → Prop := From 20eda18454499a50039a50294580be332192c8f3 Mon Sep 17 00:00:00 2001 From: Jesse Alama Date: Wed, 28 Oct 2026 08:09:03 +0100 Subject: [PATCH 4/4] chore(Circuit): merge tactics into grind --- Cslib/Computability/Circuit/Full.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cslib/Computability/Circuit/Full.lean b/Cslib/Computability/Circuit/Full.lean index b163ec43c..9450d2041 100644 --- a/Cslib/Computability/Circuit/Full.lean +++ b/Cslib/Computability/Circuit/Full.lean @@ -124,7 +124,7 @@ private theorem exists_full_synthesis_finset [DecidableEq U] obtain ⟨a, ha⟩ := exists_full_synthesis_point (f point) default point obtain ⟨b, hb⟩ := ih have hstep := ha.full_binary hb (fun v acc => if v = default then acc else v) - exact ⟨_, by convert hstep using 2; funext x; by_cases hx : x = point <;> simp [hx, hp]⟩ + grind private theorem fullInterpretation_isComplete_two [Finite U] : (fullInterpretation (k := 2) (Carrier := U)).IsComplete where