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.
217 lines
5.2 KiB
Lean4
217 lines
5.2 KiB
Lean4
|
||
namespace Test
|
||
/--
|
||
error: incomplete set of termination hints:
|
||
This function is mutually recursive with Test.f, Test.h, and Test.i, which do not have a termination hint.
|
||
The present clause is ignored.
|
||
-/
|
||
#guard_msgs in
|
||
mutual
|
||
def f : Nat → α → α → α
|
||
| 0, a, b => a
|
||
| n+1, a, b => g n a b |>.1
|
||
|
||
def g : Nat → α → α → (α × α)
|
||
| 0, a, b => (a, b)
|
||
| n+1, a, b => (h n a b, a)
|
||
termination_by n _ _ => n -- Error
|
||
|
||
def h : Nat → α → α → α
|
||
| 0, a, b => b
|
||
| n+1, a, b => i n a b
|
||
|
||
def i : Nat → α → α → α
|
||
| 0, a, b => b
|
||
| n+1, a, b => f n a b
|
||
end
|
||
end Test
|
||
|
||
namespace Test2
|
||
/--
|
||
error: Incompatible termination hint; this function is mutually recursive with Test2.f, which is marked as `termination_by structural` so this one also needs to be marked `structural`.
|
||
-/
|
||
#guard_msgs in
|
||
mutual
|
||
def f : Nat → α → α → α
|
||
| 0, a, b => a
|
||
| n+1, a, b => g n a b |>.1
|
||
termination_by structural n _ _ => n
|
||
|
||
def g : Nat → α → α → (α × α)
|
||
| 0, a, b => (a, b)
|
||
| n+1, a, b => (h n a b, a)
|
||
termination_by n _ _ => n -- Error
|
||
|
||
def h : Nat → α → α → α
|
||
| 0, a, b => b
|
||
| n+1, a, b => f n a b
|
||
termination_by n _ _ => n
|
||
end
|
||
end Test2
|
||
|
||
namespace Test3
|
||
/--
|
||
error: Incompatible termination hint; this function is mutually recursive with Test3.f, which is not marked as `structural` so this one cannot be `structural` either.
|
||
-/
|
||
#guard_msgs in
|
||
mutual
|
||
def f : Nat → α → α → α
|
||
| 0, a, b => a
|
||
| n+1, a, b => g n a b |>.1
|
||
termination_by n _ _ => n
|
||
|
||
def g : Nat → α → α → (α × α)
|
||
| 0, a, b => (a, b)
|
||
| n+1, a, b => (h n a b, a)
|
||
termination_by structural n _ _ => n -- Error
|
||
|
||
def h : Nat → α → α → α
|
||
| 0, a, b => b
|
||
| n+1, a, b => f n a b
|
||
termination_by structural n _ _ => n
|
||
end
|
||
end Test3
|
||
|
||
namespace Test4
|
||
|
||
/--
|
||
error: Incompatible termination hint; this function is mutually recursive with Test4.f, which is not marked as `structural` so this one cannot be `structural` either.
|
||
-/
|
||
#guard_msgs in
|
||
mutual
|
||
def f : Nat → α → α → α
|
||
| 0, a, b => a
|
||
| n+1, a, b => g n a b |>.1
|
||
termination_by n _ _ => n
|
||
|
||
def g : Nat → α → α → (α × α)
|
||
| 0, a, b => (a, b)
|
||
| n+1, a, b => (h n a b, a)
|
||
termination_by n _ _ => n
|
||
|
||
def h : Nat → α → α → α
|
||
| 0, a, b => b
|
||
| n+1, a, b => f n a b
|
||
termination_by structural n _ _ => n -- Error
|
||
end
|
||
end Test4
|
||
|
||
namespace Test5
|
||
/--
|
||
error: Incompatible termination hint; this function is marked as structurally recursive, so no explicit termination proof is needed.
|
||
-/
|
||
#guard_msgs in
|
||
mutual
|
||
def f : Nat → α → α → α
|
||
| 0, a, b => a
|
||
| n+1, a, b => g n a b |>.1
|
||
termination_by structural n _ _ => n
|
||
|
||
def g : Nat → α → α → (α × α)
|
||
| 0, a, b => (a, b)
|
||
| n+1, a, b => (h n a b, a)
|
||
termination_by structural n _ _ => n
|
||
decreasing_by sorry -- Error
|
||
|
||
def h : Nat → α → α → α
|
||
| 0, a, b => b
|
||
| n+1, a, b => f n a b
|
||
termination_by structural n _ _ => n
|
||
end
|
||
end Test5
|
||
|
||
namespace Test6
|
||
/--
|
||
error: Incompatible termination hint; this function is mutually recursive with Test6.f, which is marked as `partial_fixpoint` so this one also needs to be marked `partial_fixpoint`.
|
||
-/
|
||
#guard_msgs in
|
||
mutual
|
||
def f (x : Nat) : Prop :=
|
||
g (x + 1)
|
||
partial_fixpoint
|
||
|
||
def g (x : Nat) : Prop := f (x + 1)
|
||
inductive_fixpoint
|
||
end
|
||
end Test6
|
||
|
||
|
||
namespace Test7
|
||
/--
|
||
error: Incompatible termination hint; this function is mutually recursive with Test7.f, which is marked as `coinductive_fixpoint` so this one also needs to be marked `inductive_fixpoint` or `coinductive_fixpoint`.
|
||
-/
|
||
#guard_msgs in
|
||
mutual
|
||
def f (x : Nat) : Prop :=
|
||
g (x + 1)
|
||
coinductive_fixpoint
|
||
|
||
def g (x : Nat) : Prop :=
|
||
f (x + 1)
|
||
partial_fixpoint
|
||
end
|
||
end Test7
|
||
|
||
namespace Test8
|
||
/--
|
||
error: Incompatible termination hint; this function is mutually recursive with Test8.f, which is not also marked as `partial_fixpoint`, so this one cannot be either.
|
||
-/
|
||
#guard_msgs in
|
||
mutual
|
||
def f (x : Nat) : Prop :=
|
||
g (x + 1)
|
||
termination_by?
|
||
|
||
def g (x : Nat) : Prop :=
|
||
f (x + 1)
|
||
partial_fixpoint
|
||
end
|
||
end Test8
|
||
|
||
namespace Test9
|
||
/--
|
||
error: Incompatible termination hint; this function is mutually recursive with Test9.f, which is not also marked as `inductive_fixpoint` or `coinductive_fixpoint`, so this one cannot be either.
|
||
-/
|
||
#guard_msgs in
|
||
mutual
|
||
def f (x : Nat) : Prop :=
|
||
g (x + 1)
|
||
termination_by?
|
||
|
||
def g (x : Nat) : Prop :=
|
||
f (x + 1)
|
||
inductive_fixpoint
|
||
end
|
||
end Test9
|
||
|
||
namespace Test10
|
||
/--
|
||
error: Incompatible termination hint; this function is mutually recursive with Test10.f, which is marked as `coinductive_fixpoint` so this one also needs to be marked `inductive_fixpoint` or `coinductive_fixpoint`.
|
||
-/
|
||
#guard_msgs in
|
||
mutual
|
||
def f (x : Nat) : Prop :=
|
||
g (x + 1)
|
||
coinductive_fixpoint
|
||
|
||
def g (x : Nat) : Prop :=
|
||
f (x + 1)
|
||
termination_by?
|
||
end
|
||
end Test10
|
||
|
||
namespace Test11
|
||
/--
|
||
error: Incompatible termination hint; this function is mutually recursive with Test11.f, which is marked as `partial_fixpoint` so this one also needs to be marked `partial_fixpoint`.
|
||
-/
|
||
#guard_msgs in
|
||
mutual
|
||
def f (x : Nat) : Prop :=
|
||
g (x +1)
|
||
partial_fixpoint
|
||
|
||
def g (x : Nat) : Prop :=
|
||
f (x + 1)
|
||
end
|
||
end Test11
|