DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Remove unused plus/minus mono_left/mono_right projections

Browse Source 
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 <noreply@anthropic.com>
This commit is contained in:
Danila Fedorin
2026-06-23 12:42:53 -05:00
parent 7f753a4f38
commit 6afa7df444
2 changed files with 0 additions and 16 deletions
Download Patch File Download Diff File Expand all files Collapse all files

8
lean/Spa/Analysis/Constant.lean
View File

@@ -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

8
lean/Spa/Analysis/Sign.lean
View File

@@ -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