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.
26 lines
1.1 KiB
Lean4
26 lines
1.1 KiB
Lean4
/--
|
||
Tests that `partial_fixpoint` is not picking up the partial order structure on Prop, that is exclusively used for defining (co)inductive predicates. Since `Prop` is inhabitted, `partial_fixpoint` will synthetise a `FlatOrder` instance, but in the provided example, it will not be able to prove that the recursive calls are monotone in their arguments.
|
||
-/
|
||
|
||
-- This works as `∨` is monotone in its arguments with respect to the (`ImplicationOrder`/`ReverseImplicationOrder` on `Prop`.
|
||
def f (x : Nat) : Prop :=
|
||
f (x + 1) ∨ f ( x + 2)
|
||
coinductive_fixpoint
|
||
|
||
def f' (x : Nat) : Prop :=
|
||
f' (x + 1) ∨ f' ( x + 2)
|
||
inductive_fixpoint
|
||
|
||
/--
|
||
error: Could not prove 'f''' to be monotone in its recursive calls:
|
||
Cannot eliminate recursive call `f'' (x + 1)` enclosed in
|
||
f'' (x + 1) ∨ f'' (x + 2)
|
||
Tried to apply 'Lean.Order.implication_order_monotone_or' and 'Lean.Order.coind_monotone_or', but failed.
|
||
Possible cause: A missing `Lean.Order.MonoBind` instance.
|
||
Use `set_option trace.Elab.Tactic.monotonicity true` to debug.
|
||
-/
|
||
#guard_msgs in
|
||
def f'' (x : Nat) : Prop :=
|
||
f'' (x + 1) ∨ f'' ( x + 2)
|
||
partial_fixpoint
|