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

test: grind cutsat (#10106)

Browse source
This commit is contained in:
Leonardo de Moura 2025-08-24 20:04:32 -07:00 • committed by GitHub
parent 5651192fa2
commit cc5ff2afb1
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 32 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

32
tests/lean/run/grind_cutsat_pow.lean Normal file
View file

@ -0,0 +1,32 @@
example (n : Nat) : n = 3 → 2 ^ n > 8 → False := by
grind
example (n : Nat) : n = 2 → n ^ 3 > 8 → False := by
grind
example (n : Int) : n = 2 → n ^ 3 > 8 → False := by
grind
example (n : Nat) : 2 ^ n > 8 → 3 ≤ n → n ≤ 3 → False := by
grind
example (n : Nat) : n ^ 3 > 8 → 2 ≤ n → n ≤ 2 → False := by
grind
example (n : Nat) : n = 2 → 2 ^ (n+1) > 8 → False := by
grind
example (n : Nat) : n = 2 → 2 ^ (n+1) = 8 := by
grind
example (n : Nat) : n = 2 → 2 ^ (2*n) = 16 := by
grind
example (n m : Nat) : n ≤ 2 → m ≤ n → m = 2 → 2 ^ (2*n) = 16 := by
grind
example (a n : Nat) : a ^ n ≠ 8 → 3 ≤ n → n ≤ 3 → a = 2 → False := by
grind
example (a b : Int) (n : Nat) : a ^ n ≠ 8 → 3 ≤ n → n ≤ 3 → a = b + 1 → 1 ≤ b → b ≤ 1 → False := by
grind