From 39beb25f16ea8aa27220d9a69a93c457e6d72477 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 26 Sep 2025 21:04:44 -0700 Subject: [PATCH] feat: helper theorems for `grind order` (#10589) This PR adds helper theorems for implementing `grind order` --- src/Init/Grind.lean | 1 + src/Init/Grind/Order.lean | 215 +++++++++++++++++++++++++++++ src/Init/Grind/Ordered/Module.lean | 3 + src/Init/Grind/Ordered/Ring.lean | 65 +++++++++ 4 files changed, 284 insertions(+) create mode 100644 src/Init/Grind/Order.lean diff --git a/src/Init/Grind.lean b/src/Init/Grind.lean index d86da4bac7..5d6bc6d744 100644 --- a/src/Init/Grind.lean +++ b/src/Init/Grind.lean @@ -24,3 +24,4 @@ public import Init.Grind.Attr public import Init.Data.Int.OfNat -- This may not have otherwise been imported, breaking `grind` proofs. public import Init.Grind.AC public import Init.Grind.Injective +public import Init.Grind.Order diff --git a/src/Init/Grind/Order.lean b/src/Init/Grind/Order.lean new file mode 100644 index 0000000000..c9dffe6135 --- /dev/null +++ b/src/Init/Grind/Order.lean @@ -0,0 +1,215 @@ +/- +Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +module +prelude +public import Init.Grind.Ordered.Ring +import Init.Grind.Ring +public section +namespace Lean.Grind.Order + +/-! +Helper theorems to assert constraints +-/ + +theorem le_of_eq {α} [LE α] [Std.IsPreorder α] + (a b : α) : a = b → a ≤ b := by + intro h; subst a; apply Std.IsPreorder.le_refl + +theorem le_of_not_le {α} [LE α] [Std.IsLinearPreorder α] + (a b : α) : ¬ a ≤ b → b ≤ a := by + intro h + have := Std.IsLinearPreorder.le_total a b + cases this; contradiction; assumption + +theorem lt_of_not_le {α} [LE α] [LT α] [Std.IsLinearPreorder α] [Std.LawfulOrderLT α] + (a b : α) : ¬ a ≤ b → b < a := by + intro h + rw [Std.LawfulOrderLT.lt_iff] + have := Std.IsLinearPreorder.le_total a b + cases this; contradiction; simp [*] + +theorem le_of_not_lt {α} [LE α] [LT α] [Std.IsLinearPreorder α] [Std.LawfulOrderLT α] + (a b : α) : ¬ a < b → b ≤ a := by + rw [Std.LawfulOrderLT.lt_iff] + open Classical in + rw [Classical.not_and_iff_not_or_not, Classical.not_not] + intro h; cases h + next => + have := Std.IsLinearPreorder.le_total a b + cases this; contradiction; assumption + next => assumption + +theorem int_lt (x y k : Int) : x < y + k → x ≤ y + (k-1) := by + omega + +/-! +Helper theorem for equality propagation +-/ + +theorem eq_of_le_of_le {α} [LE α] [Std.IsPartialOrder α] {a b : α} : a ≤ b → b ≤ a → a = b := + Std.IsPartialOrder.le_antisymm _ _ + +/-! +Transitivity +-/ + +theorem le_trans {α} [LE α] [Std.IsPreorder α] {a b c : α} (h₁ : a ≤ b) (h₂ : b ≤ c) : a ≤ c := + Std.IsPreorder.le_trans _ _ _ h₁ h₂ + +theorem lt_trans {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] {a b c : α} (h₁ : a < b) (h₂ : b < c) : a < c := + Preorder.lt_trans h₁ h₂ + +theorem le_lt_trans {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] {a b c : α} (h₁ : a ≤ b) (h₂ : b < c) : a < c := + Preorder.lt_of_le_of_lt h₁ h₂ + +theorem lt_le_trans {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] {a b c : α} (h₁ : a < b) (h₂ : b ≤ c) : a < c := + Preorder.lt_of_lt_of_le h₁ h₂ + +theorem lt_unsat {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] (a : α) : a < a → False := + Preorder.lt_irrefl a + +/-! +Transitivity with offsets +-/ + +attribute [local instance] Ring.intCast + +theorem le_trans_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α] + (a b c : α) (k₁ k₂ k : Int) (h₁ : a ≤ b + k₁) (h₂ : b ≤ c + k₂) : k == k₂ + k₁ → a ≤ c + k := by + intro h; simp at h; subst k + replace h₂ := OrderedAdd.add_le_left_iff (M := α) k₁ |>.mp h₂ + have := le_trans h₁ h₂ + simp [Ring.intCast_add, ← Semiring.add_assoc, this] + +theorem lt_trans_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α] + (a b c : α) (k₁ k₂ k : Int) (h₁ : a < b + k₁) (h₂ : b < c + k₂) : k == k₂ + k₁ → a < c + k := by + intro h; simp at h; subst k + replace h₂ := OrderedAdd.add_lt_left_iff (M := α) k₁ |>.mp h₂ + have := lt_trans h₁ h₂ + simp [Ring.intCast_add, ← Semiring.add_assoc, this] + +theorem le_lt_trans_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α] + (a b c : α) (k₁ k₂ k : Int) (h₁ : a ≤ b + k₁) (h₂ : b < c + k₂) : k == k₂ + k₁ → a < c + k := by + intro h; simp at h; subst k + replace h₂ := OrderedAdd.add_lt_left_iff (M := α) k₁ |>.mp h₂ + have := le_lt_trans h₁ h₂ + simp [Ring.intCast_add, ← Semiring.add_assoc, this] + +theorem lt_le_trans_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α] + (a b c : α) (k₁ k₂ k : Int) (h₁ : a < b + k₁) (h₂ : b ≤ c + k₂) : k == k₂ + k₁ → a < c + k := by + intro h; simp at h; subst k + replace h₂ := OrderedAdd.add_le_left_iff (M := α) k₁ |>.mp h₂ + have := lt_le_trans h₁ h₂ + simp [Ring.intCast_add, ← Semiring.add_assoc, this] + +/-! +Unsat detection +-/ + +theorem le_unsat_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α] + (a : α) (k : Int) : k.blt' 0 → a ≤ a + k → False := by + simp; intro h₁ h₂ + replace h₂ := OrderedAdd.add_le_left_iff (-a) |>.mp h₂ + rw [AddCommGroup.add_neg_cancel, Semiring.add_assoc, Semiring.add_comm _ (-a)] at h₂ + rw [← Semiring.add_assoc, AddCommGroup.add_neg_cancel, Semiring.add_comm, Semiring.add_zero] at h₂ + rw [← Ring.intCast_zero] at h₂ + replace h₂ := OrderedRing.le_of_intCast_le_intCast _ _ h₂ + omega + +theorem lt_unsat_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α] + (a : α) (k : Int) : k.ble' 0 → a < a + k → False := by + simp; intro h₁ h₂ + replace h₂ := OrderedAdd.add_lt_left_iff (-a) |>.mp h₂ + rw [AddCommGroup.add_neg_cancel, Semiring.add_assoc, Semiring.add_comm _ (-a)] at h₂ + rw [← Semiring.add_assoc, AddCommGroup.add_neg_cancel, Semiring.add_comm, Semiring.add_zero] at h₂ + rw [← Ring.intCast_zero] at h₂ + replace h₂ := OrderedRing.lt_of_intCast_lt_intCast _ _ h₂ + omega + +/-! +Helper theorems +-/ + +private theorem add_lt_add_of_le_of_lt {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α] + {a b c d : α} (hab : a ≤ b) (hcd : c < d) : a + c < b + d := + lt_le_trans (OrderedAdd.add_lt_right a hcd) (OrderedAdd.add_le_left hab d) + +private theorem add_lt_add_of_lt_of_le {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α] + {a b c d : α} (hab : a < b) (hcd : c ≤ d) : a + c < b + d := + le_lt_trans (OrderedAdd.add_le_right a hcd) (OrderedAdd.add_lt_left hab d) + +/-! Theorems for propagating constraints to `True` -/ + +theorem le_eq_true_of_le_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α] + (a b : α) (k₁ k₂ : Int) : k₁.ble' k₂ → a ≤ b + k₁ → (a ≤ b + k₂) = True := by + simp; intro h₁ h₂ + replace h₁ : 0 ≤ k₂ - k₁ := by omega + replace h₁ := OrderedRing.nonneg_intCast_of_nonneg (R := α) _ h₁ + replace h₁ := OrderedAdd.add_le_add h₂ h₁ + rw [Semiring.add_zero, Semiring.add_assoc, Int.sub_eq_add_neg, Int.add_comm] at h₁ + rw [Ring.intCast_add, Ring.intCast_neg, ← Semiring.add_assoc (k₁ : α)] at h₁ + rw [AddCommGroup.add_neg_cancel, Semiring.add_comm 0, Semiring.add_zero] at h₁ + assumption + +theorem le_eq_true_of_lt_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α] + (a b : α) (k₁ k₂ : Int) : k₁.ble' k₂ → a < b + k₁ → (a ≤ b + k₂) = True := by + intro h₁ h₂ + replace h₂ := Std.le_of_lt h₂ + apply le_eq_true_of_le_k <;> assumption + +theorem lt_eq_true_of_lt_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α] + (a b : α) (k₁ k₂ : Int) : k₁.ble' k₂ → a < b + k₁ → (a < b + k₂) = True := by + simp; intro h₁ h₂ + replace h₁ : 0 ≤ k₂ - k₁ := by omega + replace h₁ := OrderedRing.nonneg_intCast_of_nonneg (R := α) _ h₁ + replace h₁ := add_lt_add_of_le_of_lt h₁ h₂ + rw [Semiring.add_comm, Semiring.add_zero, Semiring.add_comm, Semiring.add_assoc, Int.sub_eq_add_neg, Int.add_comm] at h₁ + rw [Ring.intCast_add, Ring.intCast_neg, ← Semiring.add_assoc (k₁ : α)] at h₁ + rw [AddCommGroup.add_neg_cancel, Semiring.add_comm 0, Semiring.add_zero] at h₁ + assumption + +theorem lt_eq_true_of_le_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α] + (a b : α) (k₁ k₂ : Int) : k₁.blt' k₂ → a ≤ b + k₁ → (a < b + k₂) = True := by + simp; intro h₁ h₂ + replace h₁ : 0 < k₂ - k₁ := by omega + replace h₁ := OrderedRing.pos_intCast_of_pos (R := α) _ h₁ + replace h₁ := add_lt_add_of_le_of_lt h₂ h₁ + rw [Semiring.add_zero, Semiring.add_assoc, Int.sub_eq_add_neg, Int.add_comm] at h₁ + rw [Ring.intCast_add, Ring.intCast_neg, ← Semiring.add_assoc (k₁ : α)] at h₁ + rw [AddCommGroup.add_neg_cancel, Semiring.add_comm 0, Semiring.add_zero] at h₁ + assumption + +/-! Theorems for propagating constraints to `False` -/ + +theorem le_eq_false_of_le_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α] + (a b : α) (k₁ k₂ : Int) : (k₂ + k₁).blt' 0 → a ≤ b + k₁ → (b ≤ a + k₂) = False := by + intro h₁; simp; intro h₂ h₃ + have h := le_trans_k _ _ _ _ _ (k₂ + k₁) h₂ h₃ + simp at h + apply le_unsat_k _ _ h₁ h + +theorem lt_eq_false_of_le_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α] + (a b : α) (k₁ k₂ : Int) : (k₂ + k₁).ble' 0 → a ≤ b + k₁ → (b < a + k₂) = False := by + intro h₁; simp; intro h₂ h₃ + have h := le_lt_trans_k _ _ _ _ _ (k₂ + k₁) h₂ h₃ + simp at h + apply lt_unsat_k _ _ h₁ h + +theorem lt_eq_false_of_lt_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α] + (a b : α) (k₁ k₂ : Int) : (k₂ + k₁).ble' 0 → a < b + k₁ → (b < a + k₂) = False := by + intro h₁; simp; intro h₂ h₃ + have h := lt_trans_k _ _ _ _ _ (k₂ + k₁) h₂ h₃ + simp at h + apply lt_unsat_k _ _ h₁ h + +theorem le_eq_false_of_lt_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α] + (a b : α) (k₁ k₂ : Int) : (k₂ + k₁).ble' 0 → a < b + k₁ → (b ≤ a + k₂) = False := by + intro h₁; simp; intro h₂ h₃ + have h := lt_le_trans_k _ _ _ _ _ (k₂ + k₁) h₂ h₃ + simp at h + apply lt_unsat_k _ _ h₁ h + +end Lean.Grind.Order diff --git a/src/Init/Grind/Ordered/Module.lean b/src/Init/Grind/Ordered/Module.lean index 003b7ccde6..903c2fc044 100644 --- a/src/Init/Grind/Ordered/Module.lean +++ b/src/Init/Grind/Ordered/Module.lean @@ -73,6 +73,9 @@ theorem add_lt_left_iff {a b : M} (c : M) : a < b ↔ a + c < b + c := by theorem add_lt_right_iff {a b : M} (c : M) : a < b ↔ c + a < c + b := by rw [add_comm c a, add_comm c b, add_lt_left_iff] +theorem add_lt_add {a b c d : M} (hab : a < b) (hcd : c < d) : a + c < b + d := + Preorder.lt_trans (add_lt_right a hcd) (add_lt_left hab d) + end section diff --git a/src/Init/Grind/Ordered/Ring.lean b/src/Init/Grind/Ordered/Ring.lean index ad634de03f..34114e2257 100644 --- a/src/Init/Grind/Ordered/Ring.lean +++ b/src/Init/Grind/Ordered/Ring.lean @@ -133,6 +133,71 @@ theorem lt_of_intCast_lt_intCast (a b : Int) : (a : R) < (b : R) → a < b := by replace h := lt_of_natCast_lt_natCast _ _ h omega +theorem natCast_le_natCast_of_le (a b : Nat) : a ≤ b → (a : R) ≤ (b : R) := by + induction a generalizing b <;> cases b <;> simp + next => simp [Semiring.natCast_zero, Std.IsPreorder.le_refl] + next n => + have := ofNat_nonneg (R := R) n + simp [Semiring.ofNat_eq_natCast] at this + rw [Semiring.natCast_zero] at this + simp [Semiring.natCast_zero, Semiring.natCast_add, Semiring.natCast_one] + replace this := OrderedAdd.add_le_left_iff 1 |>.mp this + rw [Semiring.add_comm, Semiring.add_zero] at this + replace this := Std.lt_of_lt_of_le zero_lt_one this + exact Std.le_of_lt this + next n ih m => + intro h + replace ih := ih _ h + simp [Semiring.natCast_add, Semiring.natCast_one] + exact OrderedAdd.add_le_left_iff _ |>.mp ih + +theorem natCast_lt_natCast_of_lt (a b : Nat) : a < b → (a : R) < (b : R) := by + induction a generalizing b <;> cases b <;> simp + next n => + have := ofNat_nonneg (R := R) n + simp [Semiring.ofNat_eq_natCast] at this + rw [Semiring.natCast_zero] at this + simp [Semiring.natCast_zero, Semiring.natCast_add, Semiring.natCast_one] + replace this := OrderedAdd.add_le_left_iff 1 |>.mp this + rw [Semiring.add_comm, Semiring.add_zero] at this + exact Std.lt_of_lt_of_le zero_lt_one this + next n ih m => + intro h + replace ih := ih _ h + simp [Semiring.natCast_add, Semiring.natCast_one] + exact OrderedAdd.add_lt_left_iff _ |>.mp ih + +theorem pos_natCast_of_pos (a : Nat) : 0 < a → 0 < (a : R) := by + induction a + next => simp + next n ih => + simp; cases n + next => simp +arith; rw [Semiring.natCast_one]; apply zero_lt_one + next => + simp at ih + replace ih := OrderedAdd.add_lt_add ih zero_lt_one + rw [Semiring.add_zero, ← Semiring.natCast_one, ← Semiring.natCast_add] at ih + assumption + +theorem pos_intCast_of_pos (a : Int) : 0 < a → 0 < (a : R) := by + cases a + next n => + intro h + replace h : 0 < n := by cases n; simp at h; simp + replace h := pos_natCast_of_pos (R := R) _ h + rw [Int.ofNat_eq_natCast, Ring.intCast_natCast] + assumption + next => omega + +theorem nonneg_intCast_of_nonneg (a : Int) : 0 ≤ a → 0 ≤ (a : R) := by + cases a + next n => + intro; rw [Int.ofNat_eq_natCast, Ring.intCast_natCast] + have := ofNat_nonneg (R := R) n + rw [Semiring.ofNat_eq_natCast] at this + assumption + next => omega + instance [Ring R] [LE R] [LT R] [LawfulOrderLT R] [IsPreorder R] [OrderedRing R] : IsCharP R 0 := IsCharP.mk' _ _ <| by intro x