max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

test: rationals in grind linarith (#10958)

Browse source
This commit is contained in:
Leonardo de Moura 2025-10-25 14:48:43 -07:00 • committed by GitHub
parent 962e7d5a30
commit 48f0eb206c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 21 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
tests/lean/run/grind_linarith_rational.lean Normal file
View file

@ -0,0 +1,21 @@
open Lean Grind Std
variable [Field α] [LT α] [LE α] [LawfulOrderLT α] [IsLinearOrder α] [OrderedRing α]
example (x : α) : x ≥ 1/3 → x ≥ 0 := by grind
example (x : α) : x ≥ 1/3 → x ≥ 1/4 := by grind
example : (1/3 : α) ≥ 0 := by grind
example : (2/3 : α) ≥ 1/3 := by grind
example (x : α) : x + 1/3 ≤ x + 1/2 := by grind
example (x : α) (h : x ≤ 7/5) : 5*x ≤ 7 := by grind
example (x : α) (h : 3*x ≤ 7) : x ≤ 7/3 := by grind
example (x y : α) (h : x ≤ y - 1/3) : x + 1/6 ≤ y - 1/6 := by grind
example (x y : α) (h : x < y) : x + 1/3 < y + 1/3 := by grind
example (x : α) : x ≤ x + 1/7 := by grind
example (x : α) (h : x ≤ 1/4) : x - 1/3 ≤ -1/12 := by grind
example (x : α) (h : x ≤ x - 1/3) : False := by grind
example : (1/3 : α) ≤ 2/3 := by grind
example : (1/3 : α) ≤ (2/5 : α) := by grind
example (x y : α) (h : x ≤ y - (1/3 : α)) : x + (1/6 : α) ≤ y - (1/6 : α) := by grind
example (x : α) (h : x ≤ (1/4 : α)) : x - (1/3 : α) ≤ (-1/12 : α) := by grind
example (x : α) (h : x ≤ x - (1/5 : α)) : False := by grind