08eb78a5b2
This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting. For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.
310 lines
8.1 KiB
Text
310 lines
8.1 KiB
Text
|
||
namespace Ex1
|
||
opaque f : Nat → Nat
|
||
axiom fax : f x ≥ f (f x)
|
||
|
||
grind_pattern fax => f x where
|
||
depth x < 2
|
||
|
||
/--
|
||
trace: [grind.ematch.instance] fax: f a ≥ f (f a)
|
||
[grind.ematch.instance] fax: f (f a) ≥ f (f (f a))
|
||
-/
|
||
#guard_msgs (drop error, trace) in
|
||
set_option trace.grind.ematch.instance true in
|
||
example (h : f a = 0) : False := by
|
||
grind
|
||
end Ex1
|
||
|
||
namespace Ex2
|
||
opaque f : Nat → Nat
|
||
axiom fax : f x ≥ f (f x)
|
||
|
||
grind_pattern fax => f x where
|
||
is_ground x
|
||
depth x < 3
|
||
|
||
opaque b : Nat
|
||
|
||
-- Theorems containing `a` should not be instantiate since it is a local variable
|
||
/--
|
||
trace: [grind.ematch.instance] fax: f b ≥ f (f b)
|
||
[grind.ematch.instance] fax: f (f b) ≥ f (f (f b))
|
||
[grind.ematch.instance] fax: f (f (f b)) ≥ f (f (f (f b)))
|
||
-/
|
||
#guard_msgs (drop error, trace) in
|
||
set_option trace.grind.ematch.instance true in
|
||
example : f a = 0 → f b = 0 → False := by
|
||
grind
|
||
end Ex2
|
||
|
||
namespace Ex3
|
||
def f {α : Type} : α → α → α := fun x _ => x
|
||
axiom fax [LE α] (x : α) : f x x ≥ f (f x x) (f x x)
|
||
|
||
grind_pattern fax => f x x where
|
||
size x < 5
|
||
|
||
/--
|
||
trace: [grind.ematch.instance] fax: f a a ≥ f (f a a) (f a a)
|
||
[grind.ematch.instance] fax: f (f a a) (f a a) ≥ f (f (f a a) (f a a)) (f (f a a) (f a a))
|
||
-/
|
||
#guard_msgs (drop error, trace) in
|
||
set_option trace.grind.ematch.instance true in
|
||
example (a b : List (List Nat)) : f a a = b → False := by
|
||
grind
|
||
end Ex3
|
||
|
||
namespace Ex4
|
||
def f {α : Type} : α → α → α := fun x _ => x
|
||
axiom fax [LE α] (x : α) : f x x ≥ f (f x x) (f x x)
|
||
|
||
grind_pattern fax => f x x where
|
||
gen < 2
|
||
|
||
/--
|
||
trace: [grind.ematch.instance] fax: f a a ≥ f (f a a) (f a a)
|
||
[grind.ematch.instance] fax: f (f a a) (f a a) ≥ f (f (f a a) (f a a)) (f (f a a) (f a a))
|
||
-/
|
||
#guard_msgs (drop error, trace) in
|
||
set_option trace.grind.ematch.instance true in
|
||
example (a b : List (List Nat)) : f a a = b → False := by
|
||
grind
|
||
end Ex4
|
||
|
||
|
||
namespace Ex5
|
||
opaque f : Nat → Nat
|
||
axiom fax : f x ≥ f (f x)
|
||
|
||
grind_pattern fax => f x where
|
||
max_insts < 4
|
||
|
||
/--
|
||
trace: [grind.ematch.instance] fax: f c ≥ f (f c)
|
||
[grind.ematch.instance] fax: f b ≥ f (f b)
|
||
[grind.ematch.instance] fax: f a ≥ f (f a)
|
||
-/
|
||
#guard_msgs (drop error, trace) in
|
||
set_option trace.grind.ematch.instance true in
|
||
example : f a = 0 → f b = 0 → f c = 0 → False := by
|
||
grind
|
||
|
||
end Ex5
|
||
|
||
namespace Ex6
|
||
|
||
opaque g : List Nat → Nat
|
||
opaque f : List Nat → List Nat
|
||
axiom gax (as : List Nat) : g as > g (f as)
|
||
|
||
grind_pattern gax => g as where
|
||
as =?= _ :: _
|
||
|
||
/-- trace: [grind.ematch.instance] gax: g [1, 2, 3] > g (f [1, 2, 3]) -/
|
||
#guard_msgs (drop error, trace) in
|
||
set_option trace.grind.ematch.instance true in
|
||
example (h : g [1, 2, 3] > 0) : False := by
|
||
grind
|
||
|
||
end Ex6
|
||
|
||
namespace Ex7
|
||
|
||
opaque f {α : Type u} : List α × α → Nat
|
||
axiom fax : f x > 0
|
||
|
||
grind_pattern fax => f x where
|
||
is_value x
|
||
|
||
/--
|
||
trace: [grind.ematch.instance] fax: f ([true], false) > 0
|
||
[grind.ematch.instance] fax: f ([1, 2], 4) > 0
|
||
[grind.ematch.instance] fax: f ([fun x => x], fun x => x) > 0
|
||
-/
|
||
#guard_msgs (drop error, trace) in
|
||
set_option trace.grind.ematch.instance true in
|
||
example
|
||
: f (as, bs) = f ([1], c) →
|
||
f ([fun x : Nat => x], fun y => y) = d →
|
||
f ([1, 2], 4) = f ([true], false) →
|
||
False := by
|
||
grind
|
||
|
||
end Ex7
|
||
|
||
namespace Ex8
|
||
|
||
opaque f {α : Type u} : List α × α → Nat
|
||
axiom fax : f x > 0
|
||
|
||
grind_pattern fax => f x where
|
||
is_strict_value x
|
||
|
||
/--
|
||
trace: [grind.ematch.instance] fax: f ([true], false) > 0
|
||
[grind.ematch.instance] fax: f ([1, 2], 4) > 0
|
||
-/
|
||
#guard_msgs (drop error, trace) in
|
||
set_option trace.grind.ematch.instance true in
|
||
example
|
||
: f (as, bs) = f ([1], c) →
|
||
f ([fun x : Nat => x], fun y => y) = d →
|
||
f ([1, 2], 4) = f ([true], false) →
|
||
False := by
|
||
grind
|
||
|
||
end Ex8
|
||
|
||
namespace Ex9
|
||
|
||
opaque f : Nat → Nat → Nat
|
||
axiom fax : x ≠ y → f x y > 0
|
||
|
||
grind_pattern fax => f x y where
|
||
guard x ≠ y
|
||
|
||
/--
|
||
trace: [grind.ematch.instance.delayed] `fax` waiting
|
||
¬x = y
|
||
-/
|
||
#guard_msgs (trace, drop error) in
|
||
example : f x y = 5 → False := by
|
||
set_option trace.grind.ematch.instance true in
|
||
set_option trace.grind.ematch.instance.delayed true in
|
||
grind
|
||
|
||
|
||
/--
|
||
trace: [grind.ematch.instance.delayed] `fax` waiting
|
||
¬x = y
|
||
[grind.ematch.instance] fax: x ≠ y → f x y > 0
|
||
-/
|
||
#guard_msgs in
|
||
example : x ≠ y → f x y = 0 → False := by
|
||
set_option trace.grind.ematch.instance true in
|
||
set_option trace.grind.ematch.instance.delayed true in
|
||
grind
|
||
|
||
end Ex9
|
||
|
||
namespace Ex10
|
||
|
||
opaque f : Nat → Nat → Nat
|
||
axiom fax : x = y → f x y > 0
|
||
|
||
grind_pattern fax => f x y where
|
||
check x = y
|
||
|
||
/--
|
||
trace: [grind.ematch.instance.delayed] `fax` waiting
|
||
x = y
|
||
[grind.split] x = y, generation: 1
|
||
[grind.ematch.instance] fax: x = y → f x y > 0
|
||
-/
|
||
#guard_msgs (drop error, trace) in
|
||
example : f x y = 0 → False := by
|
||
set_option trace.grind.ematch.instance true in
|
||
set_option trace.grind.ematch.instance.delayed true in
|
||
set_option trace.grind.split true in
|
||
grind
|
||
|
||
end Ex10
|
||
|
||
namespace Ex11
|
||
|
||
opaque f : Nat → Nat → Nat
|
||
axiom fax : x = y → f x y > 0
|
||
|
||
grind_pattern fax => f x y where
|
||
guard x = y
|
||
|
||
-- `grind` will not case-split on `x = y` since `guard` was used instead of `check`
|
||
/--
|
||
trace: [grind.ematch.instance.delayed] `fax` waiting
|
||
x = y
|
||
-/
|
||
#guard_msgs (drop error, trace) in
|
||
example : f x y = 0 → False := by
|
||
set_option trace.grind.ematch.instance true in
|
||
set_option trace.grind.ematch.instance.delayed true in
|
||
set_option trace.grind.split true in
|
||
grind
|
||
|
||
end Ex11
|
||
|
||
namespace Ex12
|
||
|
||
opaque f : Nat → Nat
|
||
axiom fMono : x ≤ y → f x ≤ f y
|
||
grind_pattern fMono => f x, f y
|
||
|
||
-- Many unnecessary instances were generated.
|
||
/--
|
||
trace: [grind.ematch.instance] fMono: f a ≤ b → f (f a) ≤ f b
|
||
[grind.ematch.instance] fMono: f a ≤ c → f (f a) ≤ f c
|
||
[grind.ematch.instance] fMono: f a ≤ a → f (f a) ≤ f a
|
||
[grind.ematch.instance] fMono: f a ≤ f (f a) → f (f a) ≤ f (f (f a))
|
||
[grind.ematch.instance] fMono: f a ≤ f a → f (f a) ≤ f (f a)
|
||
[grind.ematch.instance] fMono: f (f a) ≤ b → f (f (f a)) ≤ f b
|
||
[grind.ematch.instance] fMono: f (f a) ≤ c → f (f (f a)) ≤ f c
|
||
[grind.ematch.instance] fMono: f (f a) ≤ a → f (f (f a)) ≤ f a
|
||
[grind.ematch.instance] fMono: f (f a) ≤ f (f a) → f (f (f a)) ≤ f (f (f a))
|
||
[grind.ematch.instance] fMono: f (f a) ≤ f a → f (f (f a)) ≤ f (f a)
|
||
[grind.ematch.instance] fMono: a ≤ b → f a ≤ f b
|
||
[grind.ematch.instance] fMono: a ≤ c → f a ≤ f c
|
||
[grind.ematch.instance] fMono: a ≤ a → f a ≤ f a
|
||
[grind.ematch.instance] fMono: a ≤ f (f a) → f a ≤ f (f (f a))
|
||
[grind.ematch.instance] fMono: a ≤ f a → f a ≤ f (f a)
|
||
[grind.ematch.instance] fMono: c ≤ b → f c ≤ f b
|
||
[grind.ematch.instance] fMono: c ≤ c → f c ≤ f c
|
||
[grind.ematch.instance] fMono: c ≤ a → f c ≤ f a
|
||
[grind.ematch.instance] fMono: c ≤ f (f a) → f c ≤ f (f (f a))
|
||
[grind.ematch.instance] fMono: c ≤ f a → f c ≤ f (f a)
|
||
[grind.ematch.instance] fMono: b ≤ b → f b ≤ f b
|
||
[grind.ematch.instance] fMono: b ≤ c → f b ≤ f c
|
||
[grind.ematch.instance] fMono: b ≤ a → f b ≤ f a
|
||
[grind.ematch.instance] fMono: b ≤ f (f a) → f b ≤ f (f (f a))
|
||
[grind.ematch.instance] fMono: b ≤ f a → f b ≤ f (f a)
|
||
-/
|
||
#guard_msgs in
|
||
example : f b = f c → a ≤ f a → f (f a) ≤ f (f (f a)) := by
|
||
set_option trace.grind.ematch.instance true in
|
||
grind
|
||
|
||
end Ex12
|
||
|
||
namespace Ex13
|
||
-- Same example but using constraints to control theorem/axiom instantiation
|
||
opaque f : Nat → Nat
|
||
axiom fMono : x ≤ y → f x ≤ f y
|
||
grind_pattern fMono => f x, f y where
|
||
guard x ≤ y
|
||
x =/= y
|
||
|
||
/--
|
||
trace: [grind.ematch.instance] fMono: a ≤ f a → f a ≤ f (f a)
|
||
[grind.ematch.instance] fMono: f a ≤ f (f a) → f (f a) ≤ f (f (f a))
|
||
[grind.ematch.instance] fMono: a ≤ f (f a) → f a ≤ f (f (f a))
|
||
-/
|
||
#guard_msgs in
|
||
example : f b = f c → a ≤ f a → f (f a) ≤ f (f (f a)) := by
|
||
set_option trace.grind.ematch.instance true in
|
||
grind
|
||
|
||
end Ex13
|
||
|
||
namespace Ex14
|
||
|
||
opaque f : Nat → Nat
|
||
axiom fax : f x ≤ x
|
||
grind_pattern fax => f x where
|
||
not_value x
|
||
|
||
/-- trace: [grind.ematch.instance] fax: f x ≤ x -/
|
||
#guard_msgs in
|
||
example : f 1 = a → f 2 = b → x ≤ y → f x ≤ y := by
|
||
set_option trace.grind.ematch.instance true in
|
||
grind
|
||
|
||
end Ex14
|