feat: regression tests for grind adapted from lean-egg (#6688)
Adapts, with permission, unit tests from `lean-egg` written by Marcus Rossel as regression tests for `grind`.
This commit is contained in:
Kim Morrison
GitHub
parent
8a8417f6e1
commit
5998ba545b
1 changed files with 743 additions and 0 deletions
743
tests/lean/run/grind_regression.lean
Normal file
743
tests/lean/run/grind_regression.lean
Normal file
|
|
@ -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
|
||||
Loading…
Add table
Reference in a new issue