Skip to content

Optimize Redhill subsum sign arguments #658

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

Merged
Vilin97 merged 1 commit into from
Oct 16, 2026
Merged

Optimize Redhill subsum sign arguments #658

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
7 changes: 7 additions & 0 deletions LeanPool/Redhill/Common/SubsumCondition.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,13 @@ def StrongSSC : Prop :=

variable {a}

lemma SignType.natAbs_intCast_le_one (b : SignType) : (b : ℤ).natAbs ≤ 1 := by
cases b <;> decide

lemma SignType.one_le_natAbs_intCast_sub {b₁ b₂ : SignType} (h : b₁ ≠ b₂) :
1 ≤ (b₁ - b₂ : ℤ).natAbs := by
cases b₁ <;> cases b₂ <;> simp_all

lemma StrongSSC.SSC (h : StrongSSC a) : SSC a := by
unfold _root_.SSC StrongSSC IsSubsumBlock at *
contrapose! h
Expand Down
20 changes: 11 additions & 9 deletions LeanPool/Redhill/General/Subsum.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -124,9 +124,10 @@ lemma X4_le_natAbs_b4 {b₁ b₂ b₃ b₄ : SignType} (hl : b₄ < b₃) :
refine Nat.sub_le_sub_right ?_ _
obtain rfl | rfl | rfl := b₃.trichotomy
· simp at hl
· obtain rfl : b₄ = -1 := by decide +revert
· obtain rfl : b₄ = -1 := SignType.neg_iff.mp hl
simpa using b₄_lower_bound hh
· obtain rfl | rfl : b₄ = 0 ∨ b₄ = -1 := by decide +revert
· obtain rfl | rfl : b₄ = 0 ∨ b₄ = -1 :=
(SignType.nonpos_iff.mp (SignType.lt_one_iff.mp hl)).symm
· simpa using b₃_lower_bound hh
· simp_rw [SignType.coe_neg, SignType.coe_one, neg_one_mul, neg_neg, one_mul]
have n₁ : 0 ≤ (X F h - Y F : ℤ) ^ 5 := by
Expand All @@ -143,7 +144,7 @@ lemma X4_le_natAbs_b4 {b₁ b₂ b₃ b₄ : SignType} (hl : b₄ < b₃) :
rw [add_mul]
refine (Int.natAbs_add_le _ _).trans (Nat.add_le_add ?_ ?_)
· rw [Int.natAbs_mul, ← one_mul (4 * _)]
exact mul_le_mul' (by decide +revert) (b₁_upper_bound hh)
exact mul_le_mul' (SignType.natAbs_intCast_le_one b₁) (b₁_upper_bound hh)
· rw [show (10 * Y F - 1 : ℤ) = (10 * Y F - 1 : ℕ) by grind [Y_pos], ← mul_assoc]
simp_rw [Int.natAbs_mul, Int.natAbs_pow, Int.natAbs_natCast]
apply Nat.mul_le_mul_right
Expand All @@ -169,18 +170,19 @@ lemma X4_le_natAbs_b3 {b₁ b₂ b₃ : SignType} (hl : b₃ < b₂) :
_ ≤ 5 * X F h ^ 4 - (b₁ * (X F h ^ 2 + 10 * Y F ^ 3 : ℤ) ^ 2).natAbs := by
refine Nat.sub_le_sub_left ?_ _
rw [Int.natAbs_mul, ← one_mul (4 * _)]
exact mul_le_mul' (by decide +revert) (b₁_upper_bound hh)
exact mul_le_mul' (SignType.natAbs_intCast_le_one b₁) (b₁_upper_bound hh)
_ ≤ (b₂ * ((10 * Y F - 1 : ℤ) * X F h ^ 4) +
b₃ * (-2 * Y F * (5 * X F h ^ 4 + 10 * X F h ^ 2 * Y F ^ 2 + Y F ^ 4))).natAbs -
(b₁ * (X F h ^ 2 + 10 * Y F ^ 3 : ℤ) ^ 2).natAbs := by
refine Nat.sub_le_sub_right ?_ _
obtain rfl | rfl | rfl := b₂.trichotomy
· simp at hl
· obtain rfl : b₃ = -1 := by decide +revert
· obtain rfl : b₃ = -1 := SignType.neg_iff.mp hl
simpa using b₃_lower_bound_2
· have cY : (10 * Y F - 1 : ℤ) = (10 * Y F - 1 : ℕ) := by grind [Y_pos]
rw [SignType.coe_one, one_mul, cY]
obtain rfl | rfl : b₃ = 0 ∨ b₃ = -1 := by decide +revert
obtain rfl | rfl : b₃ = 0 ∨ b₃ = -1 :=
(SignType.nonpos_iff.mp (SignType.lt_one_iff.mp hl)).symm
· rw [SignType.coe_zero, zero_mul, add_zero, Int.natAbs_mul]
simp_rw [Int.natAbs_pow, Int.natAbs_natCast]
exact Nat.mul_le_mul_right _ (by lia)
Expand Down Expand Up @@ -243,7 +245,7 @@ lemma X_le_natAbs_redEmb1 {b₁ b₂ b₃ b₄ : SignType} (hb : b₁ ≠ b₂
rw [Int.natAbs_mul, ← one_mul (X F h ^ 4 + _)]
norm_cast
apply Nat.mul_le_mul_right
decide +revert
exact SignType.one_le_natAbs_intCast_sub hb
_ ≤ ((b₁ - b₂ : ℤ) * (X F h ^ 4 + 20 * X F h ^ 2 * Y F ^ 3)).natAbs -
(100 * Y F ^ 6 * b₁ - 2 * Y F ^ 5 * b₂ : ℤ).natAbs := by
refine Nat.sub_le_sub_left ((Y6_le_X hh).trans' ?_) _
Expand All @@ -252,10 +254,10 @@ lemma X_le_natAbs_redEmb1 {b₁ b₂ b₃ b₄ : SignType} (hb : b₁ ≠ b₂
calc
_ ≤ 100 * Y F ^ 6 * 1 + 2 * Y F ^ 6 * 1 := by
gcongr
· decide +revert
· exact SignType.natAbs_intCast_le_one b₁
· exact Y_pos
· decide
· decide +revert
· exact SignType.natAbs_intCast_le_one b₂
_ ≤ _ := by lia
_ ≤ _ := Int.sub_le_add_natAbs

Expand Down
8 changes: 6 additions & 2 deletions LeanPool/Redhill/Odd/Subsum.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -152,7 +152,7 @@ lemma natAbs_le_redEmb1_reduced {b₁ b₂ : SignType} (h : b₁ ≠ b₂) (hx :
refine (tsub_le_tsub ?_ ?_).trans Int.sub_le_add_natAbs
· simp only [Int.natAbs_mul, Int.natAbs_pow, Int.reduceAbs,
Int.natAbs_add_of_nonneg (sq_nonneg _) zero_le_one]
have : 1 ≤ (b₂ - b₁ : ℤ).natAbs := by cases b₁ <;> cases b₂ <;> simp_all
have : 1 ≤ (b₂ - b₁ : ℤ).natAbs := SignType.one_le_natAbs_intCast_sub h.symm
rw [← mul_assoc]
apply mul_le_mul' (by lia)
calc
Expand Down Expand Up @@ -196,7 +196,11 @@ lemma isSubsumBlock_redEmb1 (hx : Y n F ≤ x.natAbs) :
Y n F ≤ (b₁ * (x - 1) ^ 5 + b₂ * (10 * (x ^ 2 + 1) ^ 2) + b₃ * -(x + 1) ^ 5).natAbs by
apply this
contrapose! ncb
exact ⟨b 0, fun i ↦ by fin_cases i <;> tauto⟩
refine ⟨b 0, fun i ↦ ?_⟩
fin_cases i
· rfl
· exact ncb.1.symm
· exact ncb.2.symm
exact fun h ↦ Y_le_natAbs_redEmb1 h hx

lemma tupReduce_tup {c₁ : n + 2 = n + 5 - #(univ.map redEmb1)} :
Expand Down
Loading