Skip to content

Commit 98ab206

Browse files
leodemouraleodemoura
committed
feat: helper theorems for grind order
This PR adds helper theorems for justifying proofs constructed by `grind order`
1 parent 18832eb commit 98ab206

File tree

4 files changed

+284
-0
lines changed

4 files changed

+284
-0
lines changed

‎src/Init/Grind.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,3 +24,4 @@ public import Init.Grind.Attr
2424
public import Init.Data.Int.OfNat -- This may not have otherwise been imported, breaking `grind` proofs.
2525
public import Init.Grind.AC
2626
public import Init.Grind.Injective
27+
public import Init.Grind.Order

‎src/Init/Grind/Order.lean‎

Lines changed: 215 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,215 @@
1+
/-
2+
Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Leonardo de Moura
5+
-/
6+
module
7+
prelude
8+
public import Init.Grind.Ordered.Ring
9+
import Init.Grind.Ring
10+
public section
11+
namespace Lean.Grind.Order
12+
13+
/-!
14+
Helper theorems to assert constraints
15+
-/
16+
17+
theorem le_of_eq {α} [LE α] [Std.IsPreorder α]
18+
(a b : α) : a = b → a ≤ b := by
19+
intro h; subst a; apply Std.IsPreorder.le_refl
20+
21+
theorem le_of_not_le {α} [LE α] [Std.IsLinearPreorder α]
22+
(a b : α) : ¬ a ≤ b → b ≤ a := by
23+
intro h
24+
have := Std.IsLinearPreorder.le_total a b
25+
cases this; contradiction; assumption
26+
27+
theorem lt_of_not_le {α} [LE α] [LT α] [Std.IsLinearPreorder α] [Std.LawfulOrderLT α]
28+
(a b : α) : ¬ a ≤ b → b < a := by
29+
intro h
30+
rw [Std.LawfulOrderLT.lt_iff]
31+
have := Std.IsLinearPreorder.le_total a b
32+
cases this; contradiction; simp [*]
33+
34+
theorem le_of_not_lt {α} [LE α] [LT α] [Std.IsLinearPreorder α] [Std.LawfulOrderLT α]
35+
(a b : α) : ¬ a < b → b ≤ a := by
36+
rw [Std.LawfulOrderLT.lt_iff]
37+
open Classical in
38+
rw [Classical.not_and_iff_not_or_not, Classical.not_not]
39+
intro h; cases h
40+
next =>
41+
have := Std.IsLinearPreorder.le_total a b
42+
cases this; contradiction; assumption
43+
next => assumption
44+
45+
theorem int_lt (x y k : Int) : x < y + k → x ≤ y + (k-1) := by
46+
omega
47+
48+
/-!
49+
Helper theorem for equality propagation
50+
-/
51+
52+
theorem eq_of_le_of_le {α} [LE α] [Std.IsPartialOrder α] {a b : α} : a ≤ b → b ≤ a → a = b :=
53+
Std.IsPartialOrder.le_antisymm _ _
54+
55+
/-!
56+
Transitivity
57+
-/
58+
59+
theorem le_trans {α} [LE α] [Std.IsPreorder α] {a b c : α} (h₁ : a ≤ b) (h₂ : b ≤ c) : a ≤ c :=
60+
Std.IsPreorder.le_trans _ _ _ h₁ h₂
61+
62+
theorem lt_trans {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] {a b c : α} (h₁ : a < b) (h₂ : b < c) : a < c :=
63+
Preorder.lt_trans h₁ h₂
64+
65+
theorem le_lt_trans {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] {a b c : α} (h₁ : a ≤ b) (h₂ : b < c) : a < c :=
66+
Preorder.lt_of_le_of_lt h₁ h₂
67+
68+
theorem lt_le_trans {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] {a b c : α} (h₁ : a < b) (h₂ : b ≤ c) : a < c :=
69+
Preorder.lt_of_lt_of_le h₁ h₂
70+
71+
theorem lt_unsat {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] (a : α) : a < a → False :=
72+
Preorder.lt_irrefl a
73+
74+
/-!
75+
Transitivity with offsets
76+
-/
77+
78+
attribute [local instance] Ring.intCast
79+
80+
theorem le_trans_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α]
81+
(a b c : α) (k₁ k₂ k : Int) (h₁ : a ≤ b + k₁) (h₂ : b ≤ c + k₂) : k == k₂ + k₁ → a ≤ c + k := by
82+
intro h; simp at h; subst k
83+
replace h₂ := OrderedAdd.add_le_left_iff (M := α) k₁ |>.mp h₂
84+
have := le_trans h₁ h₂
85+
simp [Ring.intCast_add, ← Semiring.add_assoc, this]
86+
87+
theorem lt_trans_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α]
88+
(a b c : α) (k₁ k₂ k : Int) (h₁ : a < b + k₁) (h₂ : b < c + k₂) : k == k₂ + k₁ → a < c + k := by
89+
intro h; simp at h; subst k
90+
replace h₂ := OrderedAdd.add_lt_left_iff (M := α) k₁ |>.mp h₂
91+
have := lt_trans h₁ h₂
92+
simp [Ring.intCast_add, ← Semiring.add_assoc, this]
93+
94+
theorem le_lt_trans_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α]
95+
(a b c : α) (k₁ k₂ k : Int) (h₁ : a ≤ b + k₁) (h₂ : b < c + k₂) : k == k₂ + k₁ → a < c + k := by
96+
intro h; simp at h; subst k
97+
replace h₂ := OrderedAdd.add_lt_left_iff (M := α) k₁ |>.mp h₂
98+
have := le_lt_trans h₁ h₂
99+
simp [Ring.intCast_add, ← Semiring.add_assoc, this]
100+
101+
theorem lt_le_trans_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α]
102+
(a b c : α) (k₁ k₂ k : Int) (h₁ : a < b + k₁) (h₂ : b ≤ c + k₂) : k == k₂ + k₁ → a < c + k := by
103+
intro h; simp at h; subst k
104+
replace h₂ := OrderedAdd.add_le_left_iff (M := α) k₁ |>.mp h₂
105+
have := lt_le_trans h₁ h₂
106+
simp [Ring.intCast_add, ← Semiring.add_assoc, this]
107+
108+
/-!
109+
Unsat detection
110+
-/
111+
112+
theorem le_unsat_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α]
113+
(a : α) (k : Int) : k.blt' 0 → a ≤ a + k → False := by
114+
simp; intro h₁ h₂
115+
replace h₂ := OrderedAdd.add_le_left_iff (-a) |>.mp h₂
116+
rw [AddCommGroup.add_neg_cancel, Semiring.add_assoc, Semiring.add_comm _ (-a)] at h₂
117+
rw [← Semiring.add_assoc, AddCommGroup.add_neg_cancel, Semiring.add_comm, Semiring.add_zero] at h₂
118+
rw [← Ring.intCast_zero] at h₂
119+
replace h₂ := OrderedRing.le_of_intCast_le_intCast _ _ h₂
120+
omega
121+
122+
theorem lt_unsat_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α]
123+
(a : α) (k : Int) : k.ble' 0 → a < a + k → False := by
124+
simp; intro h₁ h₂
125+
replace h₂ := OrderedAdd.add_lt_left_iff (-a) |>.mp h₂
126+
rw [AddCommGroup.add_neg_cancel, Semiring.add_assoc, Semiring.add_comm _ (-a)] at h₂
127+
rw [← Semiring.add_assoc, AddCommGroup.add_neg_cancel, Semiring.add_comm, Semiring.add_zero] at h₂
128+
rw [← Ring.intCast_zero] at h₂
129+
replace h₂ := OrderedRing.lt_of_intCast_lt_intCast _ _ h₂
130+
omega
131+
132+
/-!
133+
Helper theorems
134+
-/
135+
136+
private theorem add_lt_add_of_le_of_lt {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α]
137+
{a b c d : α} (hab : a ≤ b) (hcd : c < d) : a + c < b + d :=
138+
lt_le_trans (OrderedAdd.add_lt_right a hcd) (OrderedAdd.add_le_left hab d)
139+
140+
private theorem add_lt_add_of_lt_of_le {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α]
141+
{a b c d : α} (hab : a < b) (hcd : c ≤ d) : a + c < b + d :=
142+
le_lt_trans (OrderedAdd.add_le_right a hcd) (OrderedAdd.add_lt_left hab d)
143+
144+
/-! Theorems for propagating constraints to `True` -/
145+
146+
theorem le_eq_true_of_le_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α]
147+
(a b : α) (k₁ k₂ : Int) : k₁.ble' k₂ → a ≤ b + k₁ → (a ≤ b + k₂) = True := by
148+
simp; intro h₁ h₂
149+
replace h₁ : 0 ≤ k₂ - k₁ := by omega
150+
replace h₁ := OrderedRing.nonneg_intCast_of_nonneg (R := α) _ h₁
151+
replace h₁ := OrderedAdd.add_le_add h₂ h₁
152+
rw [Semiring.add_zero, Semiring.add_assoc, Int.sub_eq_add_neg, Int.add_comm] at h₁
153+
rw [Ring.intCast_add, Ring.intCast_neg, ← Semiring.add_assoc (k₁ : α)] at h₁
154+
rw [AddCommGroup.add_neg_cancel, Semiring.add_comm 0, Semiring.add_zero] at h₁
155+
assumption
156+
157+
theorem le_eq_true_of_lt_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α]
158+
(a b : α) (k₁ k₂ : Int) : k₁.ble' k₂ → a < b + k₁ → (a ≤ b + k₂) = True := by
159+
intro h₁ h₂
160+
replace h₂ := Std.le_of_lt h₂
161+
apply le_eq_true_of_le_k <;> assumption
162+
163+
theorem lt_eq_true_of_lt_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α]
164+
(a b : α) (k₁ k₂ : Int) : k₁.ble' k₂ → a < b + k₁ → (a < b + k₂) = True := by
165+
simp; intro h₁ h₂
166+
replace h₁ : 0 ≤ k₂ - k₁ := by omega
167+
replace h₁ := OrderedRing.nonneg_intCast_of_nonneg (R := α) _ h₁
168+
replace h₁ := add_lt_add_of_le_of_lt h₁ h₂
169+
rw [Semiring.add_comm, Semiring.add_zero, Semiring.add_comm, Semiring.add_assoc, Int.sub_eq_add_neg, Int.add_comm] at h₁
170+
rw [Ring.intCast_add, Ring.intCast_neg, ← Semiring.add_assoc (k₁ : α)] at h₁
171+
rw [AddCommGroup.add_neg_cancel, Semiring.add_comm 0, Semiring.add_zero] at h₁
172+
assumption
173+
174+
theorem lt_eq_true_of_le_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α]
175+
(a b : α) (k₁ k₂ : Int) : k₁.blt' k₂ → a ≤ b + k₁ → (a < b + k₂) = True := by
176+
simp; intro h₁ h₂
177+
replace h₁ : 0 < k₂ - k₁ := by omega
178+
replace h₁ := OrderedRing.pos_intCast_of_pos (R := α) _ h₁
179+
replace h₁ := add_lt_add_of_le_of_lt h₂ h₁
180+
rw [Semiring.add_zero, Semiring.add_assoc, Int.sub_eq_add_neg, Int.add_comm] at h₁
181+
rw [Ring.intCast_add, Ring.intCast_neg, ← Semiring.add_assoc (k₁ : α)] at h₁
182+
rw [AddCommGroup.add_neg_cancel, Semiring.add_comm 0, Semiring.add_zero] at h₁
183+
assumption
184+
185+
/-! Theorems for propagating constraints to `False` -/
186+
187+
theorem le_eq_false_of_le_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α]
188+
(a b : α) (k₁ k₂ : Int) : (k₂ + k₁).blt' 0 → a ≤ b + k₁ → (b ≤ a + k₂) = False := by
189+
intro h₁; simp; intro h₂ h₃
190+
have h := le_trans_k _ _ _ _ _ (k₂ + k₁) h₂ h₃
191+
simp at h
192+
apply le_unsat_k _ _ h₁ h
193+
194+
theorem lt_eq_false_of_le_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α]
195+
(a b : α) (k₁ k₂ : Int) : (k₂ + k₁).ble' 0 → a ≤ b + k₁ → (b < a + k₂) = False := by
196+
intro h₁; simp; intro h₂ h₃
197+
have h := le_lt_trans_k _ _ _ _ _ (k₂ + k₁) h₂ h₃
198+
simp at h
199+
apply lt_unsat_k _ _ h₁ h
200+
201+
theorem lt_eq_false_of_lt_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α]
202+
(a b : α) (k₁ k₂ : Int) : (k₂ + k₁).ble' 0 → a < b + k₁ → (b < a + k₂) = False := by
203+
intro h₁; simp; intro h₂ h₃
204+
have h := lt_trans_k _ _ _ _ _ (k₂ + k₁) h₂ h₃
205+
simp at h
206+
apply lt_unsat_k _ _ h₁ h
207+
208+
theorem le_eq_false_of_lt_k {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [Ring α] [OrderedRing α]
209+
(a b : α) (k₁ k₂ : Int) : (k₂ + k₁).ble' 0 → a < b + k₁ → (b ≤ a + k₂) = False := by
210+
intro h₁; simp; intro h₂ h₃
211+
have h := lt_le_trans_k _ _ _ _ _ (k₂ + k₁) h₂ h₃
212+
simp at h
213+
apply lt_unsat_k _ _ h₁ h
214+
215+
end Lean.Grind.Order

‎src/Init/Grind/Ordered/Module.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -73,6 +73,9 @@ theorem add_lt_left_iff {a b : M} (c : M) : a < b ↔ a + c < b + c := by
7373
theorem add_lt_right_iff {a b : M} (c : M) : a < b ↔ c + a < c + b := by
7474
rw [add_comm c a, add_comm c b, add_lt_left_iff]
7575

76+
theorem add_lt_add {a b c d : M} (hab : a < b) (hcd : c < d) : a + c < b + d :=
77+
Preorder.lt_trans (add_lt_right a hcd) (add_lt_left hab d)
78+
7679
end
7780

7881
section

‎src/Init/Grind/Ordered/Ring.lean‎

Lines changed: 65 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -133,6 +133,71 @@ theorem lt_of_intCast_lt_intCast (a b : Int) : (a : R) < (b : R) → a < b := by
133133
replace h := lt_of_natCast_lt_natCast _ _ h
134134
omega
135135

136+
theorem natCast_le_natCast_of_le (a b : Nat) : a ≤ b → (a : R) ≤ (b : R) := by
137+
induction a generalizing b <;> cases b <;> simp
138+
next => simp [Semiring.natCast_zero, Std.IsPreorder.le_refl]
139+
next n =>
140+
have := ofNat_nonneg (R := R) n
141+
simp [Semiring.ofNat_eq_natCast] at this
142+
rw [Semiring.natCast_zero] at this
143+
simp [Semiring.natCast_zero, Semiring.natCast_add, Semiring.natCast_one]
144+
replace this := OrderedAdd.add_le_left_iff 1 |>.mp this
145+
rw [Semiring.add_comm, Semiring.add_zero] at this
146+
replace this := Std.lt_of_lt_of_le zero_lt_one this
147+
exact Std.le_of_lt this
148+
next n ih m =>
149+
intro h
150+
replace ih := ih _ h
151+
simp [Semiring.natCast_add, Semiring.natCast_one]
152+
exact OrderedAdd.add_le_left_iff _ |>.mp ih
153+
154+
theorem natCast_lt_natCast_of_lt (a b : Nat) : a < b → (a : R) < (b : R) := by
155+
induction a generalizing b <;> cases b <;> simp
156+
next n =>
157+
have := ofNat_nonneg (R := R) n
158+
simp [Semiring.ofNat_eq_natCast] at this
159+
rw [Semiring.natCast_zero] at this
160+
simp [Semiring.natCast_zero, Semiring.natCast_add, Semiring.natCast_one]
161+
replace this := OrderedAdd.add_le_left_iff 1 |>.mp this
162+
rw [Semiring.add_comm, Semiring.add_zero] at this
163+
exact Std.lt_of_lt_of_le zero_lt_one this
164+
next n ih m =>
165+
intro h
166+
replace ih := ih _ h
167+
simp [Semiring.natCast_add, Semiring.natCast_one]
168+
exact OrderedAdd.add_lt_left_iff _ |>.mp ih
169+
170+
theorem pos_natCast_of_pos (a : Nat) : 0 < a → 0 < (a : R) := by
171+
induction a
172+
next => simp
173+
next n ih =>
174+
simp; cases n
175+
next => simp +arith; rw [Semiring.natCast_one]; apply zero_lt_one
176+
next =>
177+
simp at ih
178+
replace ih := OrderedAdd.add_lt_add ih zero_lt_one
179+
rw [Semiring.add_zero, ← Semiring.natCast_one, ← Semiring.natCast_add] at ih
180+
assumption
181+
182+
theorem pos_intCast_of_pos (a : Int) : 0 < a → 0 < (a : R) := by
183+
cases a
184+
next n =>
185+
intro h
186+
replace h : 0 < n := by cases n; simp at h; simp
187+
replace h := pos_natCast_of_pos (R := R) _ h
188+
rw [Int.ofNat_eq_natCast, Ring.intCast_natCast]
189+
assumption
190+
next => omega
191+
192+
theorem nonneg_intCast_of_nonneg (a : Int) : 0 ≤ a → 0 ≤ (a : R) := by
193+
cases a
194+
next n =>
195+
intro; rw [Int.ofNat_eq_natCast, Ring.intCast_natCast]
196+
have := ofNat_nonneg (R := R) n
197+
rw [Semiring.ofNat_eq_natCast] at this
198+
assumption
199+
next => omega
200+
136201
instance [Ring R] [LE R] [LT R] [LawfulOrderLT R] [IsPreorder R] [OrderedRing R] :
137202
IsCharP R 0 := IsCharP.mk' _ _ <| by
138203
intro x

0 commit comments

Comments
 (0)