.

tests/lean/run/grind_regression.lean

@@ -0,0 +1,743 @@
+/-
+Copyright (c) 2024 Marcus Rossel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Marcus Rossel, Kim Morrison
+-/
+import Lean.Elab.Term
+
+/-!
+These tests are originally from the `lean-egg` repository at
+https://github.com/marcusrossel/lean-egg and were written by Marcus Rossel.
+
+They are re-used here with permission, and adapted as regression tests for the `grind` tactic.
+-/
+
+section
+
+example (p q : Nat → Prop) : ((∀ x, p x) ∧ (∀ x, q x)) ↔ ∀ x, p x ∧ q x := by
+  grind
+
+example (p q : Nat → Nat → Prop) : ((∀ x, p 1 x) ∧ (∀ x, q 1 x)) ↔ ∀ x, p 1 x ∧ q 1 x := by
+  grind
+
+example (p q : Nat → Nat → Prop) : ((∀ x, p x 1) ∧ (∀ x, q x 1)) ↔ ∀ x, p x 1 ∧ q x 1 := by
+  grind
+
+example (p q : Nat → Nat → Prop) : ((∀ x, p x 1) ∧ (∀ x, q x 1)) ↔ ∀ x, p x 1 ∧ q x 1 := by
+  grind
+
+end
+
+section
+
+example : (fun x => x) 0 = 0 := by
+  grind
+
+example : (fun _ => 1) 0 = 1 := by
+  grind
+
+example : (fun x => (fun y => y) x) 0 = 0 := by
+  grind
+
+example : (fun x => (fun _ => x) x) 0 = 0 := by
+  grind
+
+example : (fun x => (fun _ => x) 0) 1 = 1 := by
+  grind
+
+example : id ((fun x => x + 1) 2) = id (2 + 1) := by
+  grind
+
+example (h : y + 1 = z) : (fun _ => y + 1) 0 = z := by
+  grind
+
+example (h : y + 1 = z) : (fun x => x + 1) y = z := by
+  grind
+
+end
+
+section
+
+example :
+    (∀ (α : Type) (l : List α), l.length = l.length) ↔
+    (∀ (α : Type) (l : List α), l.length = l.length) := by
+  grind
+
+end
+
+section
+
+example (h₁ : x ∧ y) (h₂ : x ∧ y → 1 = 2) : 1 = 2 := by
+  grind
+
+example (h₁ : x ∧ y) (h₂ : x ∧ y → 1 = 2) : 1 = 2 := by
+  grind
+
+example (h₁ : x ∧ y) (h₂ : y ∧ x → 1 = 2) : 1 = 2 := by
+  grind
+
+example (h₁ : x ∧ y) (h₂ : y ∧ x → 1 = 2) : 1 = 2 := by
+  grind
+
+example (h₁ : x ∧ y) (h₂ : y ∧ x → 1 = 2) : 1 = 2 := by
+  grind
+
+example {a : Nat} (h : a < b) : a % b = a := by
+  grind only [Nat.mod_eq_of_lt]
+
+example {x : Nat} (h₁ : x = y) (h₂ : x = y → 1 = 2) : 1 = 2 := by
+  grind
+
+example {x : Nat} (h₁ : x = y) (h₂ : x = y → 1 = 2) : 1 = 2 := by
+  grind
+
+example {x : Nat} (h₁ : x = y) (h₂ : x = y → 1 = 2) : 1 = 2 := by
+  grind
+
+example (h : ∀ p : Prop, p → 1 = id 1) : 1 = id 1 := by
+  grind only [id]
+
+example {p q r : Prop} (h₁ : p) (h₂ : p ↔ q) (h₃ : q → (p ↔ r)) : p ↔ r := by
+  grind
+
+example {p q r : Prop} (h₁ : p) (h₂ : p ↔ q) (h₃ : q ↔ r) (h₄ : r → (p ↔ s)) : p ↔ s := by
+  grind
+
+end
+
+section
+
+example (h : 0 = 0 → 1 = 2) : 1 = 2 := by
+  grind
+
+example (h : (0 = (fun x => x) 0) → 1 = 2) : 1 = 2 := by
+  grind
+
+variable {x : Nat} {f : Nat → Nat}
+
+example (h₁ : x = y) (h₂ : x = y → 1 = 2) : 1 = 2 := by
+  grind
+
+example (h₁ : x = y) (h₂ : x = y → 1 = 2) : 1 = 2 := by
+  grind
+
+example (h₁ : x = y) (h₂ : y = z) (h₃ : x = z → 1 = 2) : 1 = 2 := by
+  grind
+
+example (h₁ : ∀ a : Nat, f a = a) (h₂ : f x = x → 1 = 2) : 1 = 2 := by
+  grind
+
+example (h₁ : ∀ a : Nat, f a = a) (h₂ : p ∧ q) (h₃ : (f x = x) → (p ∧ q) → 1 = 2) : 1 = 2 := by
+  grind
+
+example (h₁ : ∀ a : Nat, f a = a) (h₂ : p ∧ q) (h₃ : p ∧ q ↔ r) (h₄ : (f x = x) → r → 1 = 2) :
+    1 = 2 := by
+  grind
+
+end
+
+section
+
+example : (fun _ => 1) 0 = 1 := by
+  grind
+
+end
+
+section
+
+example : (fun (z : α → α → α) x => (fun _y => z) x x) = (fun x => x) := by
+  grind
+
+end
+
+section
+
+example : (fun x => Nat.succ x) = Nat.succ := by
+  grind
+
+example : id (fun x => Nat.succ x) = id Nat.succ := by
+  grind
+
+example : (fun x => Nat.succ x) x = Nat.succ x := by
+  grind
+
+example (f : Nat → Nat) (h : f = g) : (fun x : Nat => f x) y = g y := by
+  grind
+
+example (f : Nat → Nat) (h : f y = g) : (fun x : Nat => f x) y = g := by
+  grind
+
+elab "eta" n:num fn:ident ty:term : term => open Lean.Elab.Term in do
+  let rec go (n : Nat) :=
+    if n = 0
+    then elabTerm fn none
+    else return .lam `x (← elabTerm ty none) (.app (← go <| n - 1) (.bvar 0)) .default
+  go n.getNat
+
+example : (eta 2 Nat.succ Nat) = Nat.succ := by
+  grind
+
+example : (eta 2 Nat.succ Nat) x = Nat.succ x := by
+  grind
+
+example : id (eta 2 Nat.succ Nat) = id Nat.succ := by
+  grind
+
+example : (eta 50 Nat.succ Nat) = Nat.succ := by
+  grind
+
+example (f : α → α → α → α) : (fun a b => (fun x => (f a b) x)) = (fun a b => f a b) := by
+  grind
+
+end
+
+section
+
+example : true = true := by
+  grind
+
+example (h : true = false) : true = false := by
+  grind
+
+variable (f : Nat → Nat → Nat)
+
+example (h : ∀ x y : Nat, f x y = f y x) : f 1 2 = f 2 1 := by
+  grind
+
+example (a b : Nat) (h : ∀ x y : Nat, f x y = f y x) : f a b = f b a := by
+  grind
+
+example (a b : Nat) (h : ∀ x y : Nat, f x x = f y x) : f a a = f b a := by
+  grind
+
+end
+
+section
+
+namespace Functional
+
+inductive List α
+  | nil : List α
+  | cons : α → List α → List α
+
+def append : List α → List α → List α
+  | .nil,       bs => bs
+  | .cons a as, bs => .cons a (append as bs)
+
+theorem append_nil (as : List α) : append as .nil = as := by
+  induction as with
+  | nil         => grind only [append]
+  | cons _ _ ih => grind only [append]
+
+theorem append_assoc (as bs cs : List α) : append (append as bs) cs = append as (append bs cs) := by
+  induction as with
+  | nil         => grind only [append]
+  | cons _ _ ih => grind only [append]
+
+def reverseAux : List α → List α → List α
+  | .nil,      r => r
+  | .cons a l, r => reverseAux l (.cons a r)
+
+def reverse (as : List α) : List α :=
+  reverseAux as .nil
+
+theorem reverseAux_eq_append (as bs : List α) :
+    reverseAux as bs = append (reverseAux as .nil) bs := by
+  induction as generalizing bs with
+  | nil         => grind only [reverseAux, append]
+  | cons _ _ ih => grind only [reverseAux, append_assoc, append]
+
+theorem reverse_nil : reverse (.nil : List α) = .nil := by
+  grind only [reverse, reverseAux]
+
+theorem reverse_cons (a : α) (as : List α) :
+    reverse (.cons a as) = append (reverse as) (.cons a .nil) := by
+  grind only [reverse, reverseAux, reverseAux_eq_append]
+
+theorem reverse_append (as bs : List α) :
+    reverse (append as bs) = append (reverse bs) (reverse as) := by
+  induction as generalizing bs with
+  | nil          => grind only [reverse_nil, append_nil, append]
+  | cons a as ih => grind only [append_assoc, reverse_cons, append]
+
+def map (f : α → β) : List α → List β
+  | .nil       => .nil
+  | .cons a as => .cons (f a) (map f as)
+
+def foldr (f : α → β → β) (init : β) : List α → β
+  | .nil      => init
+  | .cons a l => f a (foldr f init l)
+
+def all (p : α → Bool) (xs : List α) : Bool :=
+  foldr and true (map p xs)
+
+def all' (p : α → Bool) : List α → Bool
+  | .nil       => true
+  | .cons x xs => (p x) && (all' p xs)
+
+theorem all_deforestation (p : α → Bool) (xs : List α) : all p xs = all' p xs := by
+  induction xs with
+  | nil         => grind only [all, all', foldr, map]
+  | cons _ _ ih => grind only [all, all', foldr, map]
+
+end Functional
+
+end
+
+section
+
+example (h₁ : ∀ p, p ∧ p) (h₂ : (∀ p, p ∧ p) → q = True) : q = True := by
+  grind
+
+end
+
+section
+
+example (a b : Nat) : a + b = b + a := by
+  have h := Nat.add_comm
+  grind
+
+example (a : Nat) : (∀ x, x + 1 = 1 + x) → a + 1 = 1 + a :=
+  fun h => by grind
+
+example (a : Nat) : (∀ x, x + 1 = 1 + x) → a + 1 = 1 + a := by
+  grind
+
+example (a : Nat) : a + 1 = 1 + a := by
+  grind
+
+example (a : Nat) : (∀ x, x + 1 = 1 + x) → a + 1 = 1 + a :=
+  fun _ => by grind
+
+variable (h : ∀ x, x + 1 = 1 + x) in
+example (a : Nat) : a + 1 = 1 + a := by
+  grind
+
+variable {h : ∀ x, x + 1 = 1 + x} in
+example (a : Nat) : a + 1 = 1 + a := by
+  grind
+
+end
+
+section
+
+example {a : Int} : ((a * b) - (2 * c)) * d - (a * b) = (d - 1) * (a * b) - (2 * c * d) := by
+  grind only [Int.sub_mul, Int.sub_sub, Int.add_comm, Int.mul_comm, Int.one_mul]
+
+end
+
+section
+
+example : Nat → (x : Nat) → x = x := by
+  intro x
+  grind
+
+example : Nat → (x : Nat) → (x_1 : Nat) → x = x := by
+  intro x_1
+  grind
+
+end
+
+section
+
+example (f : α → γ) (g : β → δ) : List.map (Prod.map f g) [] = [] := by
+  grind only [List.map]
+
+example (f : α → γ) (g : β → δ) : List.map (Prod.map f g) [] = [] := by
+  grind only [List.map]
+
+variable {α : Type _} {β : Type _} {γ : Type _} {δ : Type _}
+
+example (f : α → γ) (g : β → δ) : List.map (Prod.map f g) [] = [] := by
+  grind only [List.map]
+
+example (f : α → γ) (g : β → δ) : List.map (Prod.map f g) [] = [] := by
+  grind only [List.map]
+
+-- This example requires `Level.succ (Level.max _ _) = Level.max (Level.succ _) (Level.succ _)`.
+example (h : ∀ γ : Type (max u v), γ = id γ) (α : Type u) (β : Type v) : (α × β) = id (α × β) := by
+  grind
+
+end
+
+section
+
+example : 0 = Nat.zero := by
+  grind
+
+example : 1 = Nat.succ 0 := by
+  grind
+
+example : Nat.succ 1 = Nat.succ (Nat.succ Nat.zero) := by
+  grind
+
+example : Int.ofNat (Nat.succ 1) = Int.ofNat (Nat.succ (Nat.succ Nat.zero)) := by
+  grind
+
+example (h : ∀ n, Nat.succ n = n + 1) : 1 = Nat.zero + 1 := by
+  grind
+
+example : 1 = Nat.zero + 1 := by
+  grind
+
+elab "app" n:num fn:ident arg:term : term => open Lean.Elab.Term in do
+  let fn ← elabTerm fn none
+  let rec go (n : Nat) := if n = 0 then elabTerm arg none else return .app fn <| ← go (n - 1)
+  go n.getNat
+
+example : (app 80 Nat.succ (nat_lit 0)) = (nat_lit 80) := by grind
+
+example : 12345 + 67890 = 80235 := by
+  grind
+
+example : 12345 - 67890 = 0 := by
+  grind
+
+example : 67890 - 12345 = 55545 := by
+  grind
+
+example : 12345 * 67890 = 838102050 := by
+  grind
+
+example : 1234 ^ 5 = 2861381721051424 := by
+  grind
+
+example : 12345 / 67890 = 0 := by
+  grind
+
+example : 67890 / 12345 = 5 := by
+  grind
+
+example : 12345 / 0 = 0 := by
+  grind
+
+example : 67890 % 12345 = 6165 := by
+  grind
+
+example : 12345 % 67890 = 12345 := by
+  grind
+
+example : 12345 % 0 = 12345 := by
+  grind
+
+end
+
+section
+
+example (h : (a = b) ↔ (c = d)) : 0 = 0 := by
+  grind
+
+example (h₁ : (a = b) ↔ (c = d)) (h₂ : a = b) : c = d := by
+  grind
+
+example (h₁ : (a = b) ↔ (c = d)) (h₂ : a = b) : c = d := by
+  grind
+
+example (h₁ : (a = b) ↔ (c = d)) (h₂ : c = d) : a = b := by
+  grind
+
+example (h₁ : (a = b) ↔ (c = d)) (h₂ : a = b) (h₃ : d = e) : c = e := by
+  grind
+
+end
+
+section
+
+variable {I : Type u} {f : I → Type v₁} (x y : (i : I) → f i) (i : I)
+
+instance instMul [∀ i, Mul <| f i] : Mul (∀ i : I, f i) :=
+  ⟨fun f g i => f i * g i⟩
+
+theorem mul_apply [∀ i, Mul <| f i] : (x * y) i = x i * y i :=
+  rfl
+
+example : True = True := by
+  grind only [mul_apply]
+
+end
+
+section
+
+variable (h : ∀ (p : Nat → Nat) (x : Nat), p x = p (x + 0))
+
+example (f : Nat → Nat → Nat) : (f 1) x = (f 1) (x + 0) := by
+  grind
+
+example (f : Nat → Nat → Nat) : (f (nat_lit 1)) x = (f 1) (x + 0) := by
+  grind
+
+example (f : Nat → Nat → Nat) : (f 1) x = (f (nat_lit 1)) (x + 0) := by
+  grind
+
+example (f : Nat → Nat → Nat) : (f 1) x = (f 1) (x + (nat_lit 0)) := by
+  grind
+
+example (f : Nat → Nat → Nat) : (f 1) x = (f 1) (x + 0) := by
+  grind
+
+example (f : Nat → Nat → Nat) : (f 1) x = (f 1) (x + 0) := by
+  grind
+
+end
+
+section
+
+example : ([] : List α) = [] := by
+  grind
+
+example {l₁ l₂ : List α} : l₁ ++ l₂ = (l₂.reverse ++ l₁.reverse).reverse := by
+  grind only [List.reverse_append, List.reverse_reverse]
+
+end
+
+section
+
+example : True := by
+  grind
+
+example : True ↔ True := by
+  grind
+
+example (p q : Prop) (h : p ↔ q) : p ↔ q := by
+  grind
+
+example (x : Nat) : (x.add (.succ .zero) = x) ↔ ((Nat.succ .zero).add x = x) := by
+  have h (x y : Nat) : x.add y = y.add x := Nat.add_comm ..
+  grind
+
+example (h : False) : False := by
+  grind
+
+example {p q r : Prop} (h₁ : p ∧ q) (h₂ : p ∧ q → r) : r := by
+  grind
+
+example (h : True) : True := by
+  grind
+
+example (h : 0 = 0) : 0 = 0 := by
+  grind
+
+example (a b : Nat) (h : a = b) : a = b := by
+  grind
+
+example (a b c : Nat) (h₁ : a = b) (h₂ : b = c) : a = c := by
+  grind
+
+example (h : p ∧ q ∧ r) : r ∧ r ∧ q ∧ p ∧ q ∧ r ∧ p := by
+  grind
+
+example (P : Nat → Prop) (hp : P Nat.zero.succ) (h : ∀ n, P n ↔ P n.succ) :
+    P Nat.zero.succ.succ.succ.succ := by
+  grind
+
+end
+
+section
+
+example : 0 = 0 := by
+  grind
+
+example (a b c : Nat) (h₁ : a = b) (h₂ : b = c) : a = c := by
+  grind
+
+open List in
+example (as bs : List α) : reverse (as ++ bs) = (reverse bs) ++ (reverse as) := by
+  induction as generalizing bs with
+  | nil  => grind only [reverse_nil, append_nil, List.nil_append]
+  | cons => grind only [append_assoc, reverse_cons, List.cons_append]
+
+variable (a b c d : Int)
+
+example : ((a * b) - (2 * c)) * d - (a * b) = (d - 1) * (a * b) - (2 * c * d) := by
+  grind only [Int.sub_mul, Int.sub_sub, Int.add_comm, Int.mul_comm, Int.one_mul]
+
+example {p q r : Prop} (h₁ : p) (h₂ : p ↔ q) (h₃ : q → (p ↔ r)) : p ↔ r := by
+  grind
+
+end
+
+section
+
+example (arr : Array α) (i : Nat) (h₁ h₂ : i < arr.size) : arr[i]'h₁ = arr[i]'h₂ := by
+  grind
+
+end
+
+section
+
+example : true = true := by
+  grind
+
+example : True → true = true := by
+  grind
+
+example : True → False → true = true := by
+  grind
+
+abbrev P := ∀ x y : Nat, x + y = x + y
+
+example : P := by
+  grind
+
+abbrev R := true = false
+
+example (h : R) : true = false := by
+  grind
+
+abbrev S := ∀ _ : 0 = 0, R
+
+example (h : S) : R := by
+  grind
+
+end
+
+section
+
+example : (fun x => (fun t _y => t) (fun z => x z)) = (fun (x : α → α) (_y : α) => x) := by
+  grind
+
+end
+
+section
+
+example : 0 = Nat.zero := by
+  grind
+
+example : 1 = Nat.succ 0 := by
+  grind
+
+example : Nat.succ 1 = Nat.succ (Nat.succ Nat.zero) := by
+  grind
+
+example : Int.ofNat (Nat.succ 1) = Int.ofNat (Nat.succ (Nat.succ Nat.zero)) := by
+  grind
+
+example (h : ∀ n, Nat.succ n = n + 1) : 1 = Nat.zero + 1 := by
+  grind
+
+end
+
+section
+
+example : "a" = "a" := by
+  grind
+
+example : "a\nb" = "a\nb" := by
+  grind
+
+example : "" = "" := by
+  grind
+
+example : " " = " " := by
+  grind
+
+example : "a b" = "a b" := by
+  grind
+
+example : "(" = "(" := by
+  grind
+
+example : ")" = ")" := by
+  grind
+
+example (h : "Le " ++ " an" = "Le  an") : "Le " ++ " an" = "Le  an" := by
+  grind
+
+end
+
+section
+
+class One (α) where one : α
+instance [One α] : OfNat α 1 where ofNat := One.one
+
+class Inv (α) where inv : α → α
+postfix:max "⁻¹" => Inv.inv
+
+class Group (α) extends Mul α, One α, Inv α where
+  mul_assoc    (a b c : α) : (a * b) * c = a * (b * c)
+  one_mul      (a : α)     : 1 * a = a
+  mul_one      (a : α)     : a * 1 = a
+  inv_mul_self (a : α)     : a⁻¹ * a = 1
+  mul_inv_self (a : α)     : a * a⁻¹ = 1
+
+variable [Group α] (a b x y : α)
+
+attribute [grind _=_] Group.mul_assoc
+attribute [grind] Group.one_mul
+attribute [grind] Group.mul_one
+attribute [grind] Group.inv_mul_self
+attribute [grind] Group.mul_inv_self
+
+example : a⁻¹ * (a * b) = b := by grind
+
+@[grind]
+theorem inv_mul_cancel_left : a⁻¹ * (a * b) = b := by grind
+
+@[grind]
+theorem mul_inv_cancel_left : a * (a⁻¹ * b) = b := by grind
+
+end
+
+section
+
+example (h : ∀ [inst : Neg Int] (x : Int), @Neg.neg Int inst x = x) : (0 : Int) = (0 : Int) := by
+  grind
+
+example (h : ∀ [inst : Neg Int] (x : Int), @Neg.neg Int inst x = x) : (0 : Int) = (0 : Int) := by
+  grind
+
+example (h : ∀ (α) [inst : Neg α] (x : α), @Neg.neg α inst x = x) : (0 : Int) = (0 : Int) := by
+  grind
+
+end
+
+section -- from `TC Proj Binders.lean`
+
+example (h : (fun (α) [Mul α] (x y : α) => x * y) = a) : true = true := by
+  grind
+
+example (x : Nat) (h : ∀ (_ : x * y = z), z = z) : x = x := by
+  grind
+
+end
+
+section -- from `TC Stuck.lean`
+
+def f [Inhabited α] : α := Inhabited.default
+
+example : 0 = 0 := by
+  grind only [f]
+
+end
+
+section -- (failing tests) from `Thomas.lean`
+
+example :
+    ((fun x => (fun t (_y : α) => t) (fun z => x z)) (fun (z : α → α → α) x => ((fun _y => z) x) x))
+    = fun _y => (fun z => z) := by
+  grind
+
+example :
+    ((fun x => (fun t (_y : α) => t) (fun z => x z)) (fun (z : α → α → α) x => ((fun _y => z) x) x))
+    = fun _y => (fun z => z) := by
+  grind
+
+end
+
+section
+
+variable (h : True ↔ ∀ (a : Nat) (_ : a > 0), True)
+
+example : True ↔ ∀ (a : Nat) (_ : a > 0), True := by
+  grind
+
+end
+
+section -- (failing test) from `WIP AC.lean`
+
+example {a b c d e f g h i j k l m n o p q r s t u v w x y z : Nat} :
+    a + b + c + d + e + f + g + h + i + j + k + l + m + n + o + p + q + r + s + t + u + v + w + x + y + z =
+    z + y + x + w + v + u + t + s + r + q + p + o + n + m + l + k + j + i + h + g + f + e + d + c + b + a := by
+  grind
+
+end