From 6afa7df44462cc15b3ae46a14d6284c578563181 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Tue, 23 Jun 2026 12:42:53 -0500 Subject: [PATCH] Remove unused plus/minus mono_left/mono_right projections MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit These eight one-line projections of plus_mono₂/minus_mono₂ were never referenced; eval_mono uses the bundled Monotone₂ facts directly. Co-Authored-By: Claude Opus 4.8 --- lean/Spa/Analysis/Constant.lean | 8 -------- lean/Spa/Analysis/Sign.lean | 8 -------- 2 files changed, 16 deletions(-) diff --git a/lean/Spa/Analysis/Constant.lean b/lean/Spa/Analysis/Constant.lean index 7aa6542..ad03af2 100644 --- a/lean/Spa/Analysis/Constant.lean +++ b/lean/Spa/Analysis/Constant.lean @@ -31,20 +31,12 @@ theorem plus_mono₂ : Monotone₂ plus := (fun y hy => by cases y <;> first | exact absurd rfl hy | rfl) (fun x hx => by cases x <;> first | exact absurd rfl hx | rfl) -theorem plus_mono_left (s₂ : ConstLattice) : Monotone (plus · s₂) := plus_mono₂.1 s₂ - -theorem plus_mono_right (s₁ : ConstLattice) : Monotone (plus s₁) := plus_mono₂.2 s₁ - theorem minus_mono₂ : Monotone₂ minus := AboveBelow.monotone₂_of_strict minus (fun y => by cases y <;> rfl) (fun x => by cases x <;> rfl) (fun y hy => by cases y <;> first | exact absurd rfl hy | rfl) (fun x hx => by cases x <;> first | exact absurd rfl hx | rfl) -theorem minus_mono_left (s₂ : ConstLattice) : Monotone (minus · s₂) := minus_mono₂.1 s₂ - -theorem minus_mono_right (s₁ : ConstLattice) : Monotone (minus s₁) := minus_mono₂.2 s₁ - def interpConst : ConstLattice → Value → Prop | .bot, _ => False | .top, _ => True diff --git a/lean/Spa/Analysis/Sign.lean b/lean/Spa/Analysis/Sign.lean index 842ba23..51c2fed 100644 --- a/lean/Spa/Analysis/Sign.lean +++ b/lean/Spa/Analysis/Sign.lean @@ -62,10 +62,6 @@ theorem plus_mono₂ : Monotone₂ plus := rcases x with _ | _ | s <;> first | exact absurd rfl hx | rfl | (cases s <;> rfl)) -theorem plus_mono_left (s₂ : SignLattice) : Monotone (plus · s₂) := plus_mono₂.1 s₂ - -theorem plus_mono_right (s₁ : SignLattice) : Monotone (plus s₁) := plus_mono₂.2 s₁ - theorem minus_mono₂ : Monotone₂ minus := AboveBelow.monotone₂_of_strict minus (fun y => by cases y <;> rfl) @@ -75,10 +71,6 @@ theorem minus_mono₂ : Monotone₂ minus := rcases x with _ | _ | s <;> first | exact absurd rfl hx | rfl | (cases s <;> rfl)) -theorem minus_mono_left (s₂ : SignLattice) : Monotone (minus · s₂) := minus_mono₂.1 s₂ - -theorem minus_mono_right (s₁ : SignLattice) : Monotone (minus s₁) := minus_mono₂.2 s₁ - def interpSign : SignLattice → Value → Prop | .bot, _ => False | .top, _ => True