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

test: cutsat (#7582)

Browse source 
Additional tests for cutsat
This commit is contained in:
Leonardo de Moura 2025-03-19 17:46:07 -07:00 • committed by GitHub
parent 497ac70c38
commit 22b327f077
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 28 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
tests/lean/run/grind_omega_examples.lean Normal file
View file

@ -0,0 +1,28 @@
set_option grind.warning false
example {x y : Nat} (_ : x + y > 10) (_ : x < 5) (_ : y < 5) : False := by grind
example {x y : Nat} (_ : x + y > 10) (_ : 2 * x < 11) (_ : y < 5) : False := by grind
example {x y : Nat} (_ : 2 * x + 4 * y = 5) : False := by grind
example {x y : Nat} (_ : 6 * x + 7 * y = 5) : False := by grind
example {x y z : Nat} (_ : x - y - z = 0) (_ : x > y + z) : False := by grind
example {x y : Nat} (_ : x / 2 - y / 3 < 1) (_ : 3 * x ≥ 2 * y + 4) : False := by grind
example {x : Nat} : 1 < (1 + ((x + 1 : Nat) : Int) + 2) / 2 := by grind
example {x : Nat} (_ : 10000 ∣ x) (_ : ¬ 100 ∣ x) : False := by grind
example (x : Nat) : x % 1024 - x % 2048 = 0 := by grind
example (a b c d e : Int)
(ha : 2 * a + b + c + d + e = 4)
(hb : a + 2 * b + c + d + e = 5)
(hc : a + b + 2 * c + d + e = 6)
(hd : a + b + c + 2 * d + e = 7)
(he : a + b + c + d + 2 * e = 8) : e = 3 := by grind
example (a b c d e : Int)
(ha : 2 * a + b + c + d + e = 4)
(hb : a + 2 * b + c + d + e = 5)
(hc : a + b + 2 * c + d + e = 6)
(hd : a + b + c + 2 * d + e = 7)
(he : a + b + c + d + 2 * e = 8 ∨ e = 3) : e = 3 := by grind
example (ε : Int) (_ : ε > 0) : (ε - 2 ≤ ε / 3 + ε / 2 + ε / 2) ∧ (ε / 3 + ε / 4 + ε / 5 ≤ ε) := by
grind
example {x : Int} (h₁ : 0 ≤ 2 * x + 1) (h₂ : 2 * x + 1 ≤ 0) : False := by
iterate 64 have := h₁
iterate 64 have := h₂
grind