mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
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.
80 lines
2.3 KiB
Lean4
80 lines
2.3 KiB
Lean4
/-!
|
||
This test contains functions with fixed parameter that have dependencies on varying parameter,
|
||
which can happen when those dependencies reduce away.
|
||
-/
|
||
|
||
def const (x : α) (_ : β) : α := x
|
||
|
||
private axiom test_sorry : ∀ {α}, α
|
||
|
||
namespace Ex1
|
||
|
||
mutual
|
||
def foo (varying : Nat) (fixed : const Nat varying) : Nat := bar fixed (Nat.add varying fixed)
|
||
decreasing_by exact test_sorry
|
||
def bar (fixed : Nat) (varying : Nat) : Nat := foo (varying + fixed) fixed
|
||
decreasing_by exact test_sorry
|
||
end
|
||
|
||
/--
|
||
info: equations:
|
||
theorem Ex1.foo.eq_1 : ∀ (varying : Nat) (fixed : const Nat varying), foo varying fixed = bar fixed (varying.add fixed)
|
||
-/
|
||
#guard_msgs in
|
||
#print equations foo
|
||
|
||
/--
|
||
info: equations:
|
||
theorem Ex1.bar.eq_1 : ∀ (fixed varying : Nat), bar fixed varying = foo (varying + fixed) fixed
|
||
-/
|
||
#guard_msgs in
|
||
#print equations bar
|
||
|
||
|
||
/--
|
||
info: Ex1.foo.induct (motive1 : (varying : Nat) → const Nat varying → Prop) (motive2 : Nat → Nat → Prop)
|
||
(case1 : ∀ (varying : Nat) (fixed : const Nat varying), motive2 fixed (varying.add fixed) → motive1 varying fixed)
|
||
(case2 : ∀ (fixed varying : Nat), motive1 (varying + fixed) fixed → motive2 fixed varying) (varying : Nat)
|
||
(fixed : const Nat varying) : motive1 varying fixed
|
||
-/
|
||
#guard_msgs in
|
||
#check foo.induct
|
||
|
||
|
||
end Ex1
|
||
|
||
namespace Ex2
|
||
|
||
mutual
|
||
def bar (fixed : Nat) (varying : Nat) : Nat := foo (varying + fixed) fixed
|
||
decreasing_by exact test_sorry
|
||
def foo (varying : Nat) (fixed : const Nat varying) : Nat := bar fixed (Nat.add varying fixed)
|
||
decreasing_by exact test_sorry
|
||
end
|
||
|
||
/--
|
||
info: equations:
|
||
theorem Ex2.foo.eq_1 : ∀ (varying : Nat) (fixed : const Nat varying), foo varying fixed = bar fixed (varying.add fixed)
|
||
-/
|
||
#guard_msgs in
|
||
#print equations foo
|
||
|
||
/--
|
||
info: equations:
|
||
theorem Ex2.bar.eq_1 : ∀ (fixed varying : Nat), bar fixed varying = foo (varying + fixed) fixed
|
||
-/
|
||
#guard_msgs in
|
||
#print equations bar
|
||
|
||
/--
|
||
info: Ex2.foo.induct (motive1 : Nat → Nat → Prop) (motive2 : (varying : Nat) → const Nat varying → Prop)
|
||
(case1 : ∀ (fixed varying : Nat), motive2 (varying + fixed) fixed → motive1 fixed varying)
|
||
(case2 : ∀ (varying : Nat) (fixed : const Nat varying), motive1 fixed (varying.add fixed) → motive2 varying fixed)
|
||
(varying : Nat) (fixed : const Nat varying) : motive2 varying fixed
|
||
-/
|
||
#guard_msgs in
|
||
#check foo.induct
|
||
|
||
|
||
end Ex2
|