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

fix: add grind normalization theorem for Int.negSucc (#8775)

Browse source 
This PR adds a `grind` normalization theorem for `Int.negSucc`. Example:

```lean
example (p : Int) (n : Nat) (hmp : Int.negSucc (n + 1) + 1 = p)
    (hnm : Int.negSucc (n + 1 + 1) + 1 = Int.negSucc (n + 1)) : p = Int.negSucc n := by
  grind
```
This commit is contained in:
Leonardo de Moura 2025-06-13 12:53:42 -04:00 • committed by GitHub
parent 32eedc2c22
commit 4b7ea26d91
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 12 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Grind/Norm.lean
View file

@ -182,7 +182,7 @@ init_grind_norm
Int.emod_neg Int.ediv_neg
Int.ediv_zero Int.emod_zero
Int.ediv_one Int.emod_one
Int.negSucc_eq
natCast_eq natCast_div natCast_mod
natCast_add natCast_mul

6
tests/lean/grind/omega_regressions.lean
View file

@ -1,9 +1,3 @@
-- These are test cases extracted from Mathlib, where `omega` works but `grind` does not (yet!)
example (n : Int) (n0 : ¬0 ≤ n) (a : Nat) : n ≠ (a : Int) := by grind
-- TODO: add to the library?
attribute [grind] Int.negSucc_eq
example (p : Int) (n : Nat) (hmp : Int.negSucc (n + 1) + 1 = p)
(hnm : Int.negSucc (n + 1 + 1) + 1 = Int.negSucc (n + 1)) : p = Int.negSucc n := by grind

28
tests/lean/run/grind_cutsat_eq_1.lean
View file

@ -12,28 +12,28 @@ example (a b : Int) (f : Int → Int) (h₁ : f a + b + 3 = 2) : False := by
fail_if_success grind
sorry
theorem ex₁ (a b : Int) (_ : 2*a + 3*b = 0) (_ : 2 ∣ 3*b + 1) : False := by
example (a b : Int) (_ : 2*a + 3*b = 0) (_ : 2 ∣ 3*b + 1) : False := by
grind
theorem ex₂ (a b : Int) (_ : 2 ∣ 3*a + 1) (_ : 2*b + 3*a = 0) : False := by
example (a b : Int) (_ : 2 ∣ 3*a + 1) (_ : 2*b + 3*a = 0) : False := by
grind
theorem ex₃ (a b c : Int) (_ : c + 3*a = 0) (_ : 2 ∣ 3*a + 1) (_ : 2*b + c = 0) : False := by
example (a b c : Int) (_ : c + 3*a = 0) (_ : 2 ∣ 3*a + 1) (_ : 2*b + c = 0) : False := by
grind
theorem ex₄ (a b c : Int) (_ : 2*c + 3*a = 0) (_ : 2*b + c = 0) (_ : 2 ∣ 3*a + 1) : False := by
example (a b c : Int) (_ : 2*c + 3*a = 0) (_ : 2*b + c = 0) (_ : 2 ∣ 3*a + 1) : False := by
grind
theorem ex₅ (a c : Int) (_ : 2*c + 3*a = 0) (_ : c + 1 = 0) : False := by
example (a c : Int) (_ : 2*c + 3*a = 0) (_ : c + 1 = 0) : False := by
grind
theorem ex₆ (a c : Int) (_ : c + 3*a = 0) (_ : c + 3*a = 1) : False := by
example (a c : Int) (_ : c + 3*a = 0) (_ : c + 3*a = 1) : False := by
grind
theorem ex₇ (a c : Int) (_ : c + 3*a = 0) (_ : c - 3*a = 6) (_ : 2*c + a = 0) : False := by
example (a c : Int) (_ : c + 3*a = 0) (_ : c - 3*a = 6) (_ : 2*c + a = 0) : False := by
grind
theorem ex₈ (a b : Int) (_ : 2 ∣ a + 1) (_ : a = 2*b) : False := by
example (a b : Int) (_ : 2 ∣ a + 1) (_ : a = 2*b) : False := by
grind
example (a b : Int) (_ : a = 2*b) (_ : 2 ∣ a + 1) : False := by
@ -70,12 +70,6 @@ example (a b : Int) : a = 0 → b = 1 → a + b > 2 → False := by
example (a b c : Int) : a = 0 → a + b > 2 → b = c → 1 = c → False := by
grind
#print ex₁
#print ex₂
#print ex₃
#print ex₄
#print ex₅
#print ex₆
#print ex₇
#print ex₈
#print ex₉
example (p : Int) (n : Nat) (hmp : Int.negSucc (n + 1) + 1 = p)
(hnm : Int.negSucc (n + 1 + 1) + 1 = Int.negSucc (n + 1)) : p = Int.negSucc n := by
grind