forked from leanprover/lean4
-
Notifications
You must be signed in to change notification settings - Fork 1
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
fix: don't try to generate
below
for nested predicates. (leanprover…
…#2390) * fix: don't try to generate `below` for nested predicates. * doc : document test leanprover#2389 * doc : document `mkBelow` * test: extend `2389.lean` * style: fix comments in `IndPredBelow.lean` and `2389.lean`
- Loading branch information
1 parent
e79370a
commit 325fab1
Showing
3 changed files
with
41 additions
and
2 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,35 @@ | ||
/-! | ||
# Verify that nested predicates don't trigger the generation of `below` lemmas | ||
Since the case of nested predicates is not currently handled by `mkBelow` (in `src/Lean/Meta/IndPredBelow.lean`), | ||
trying to generate `OnlyZeros.below` triggers an error upon defining the inductive type. | ||
-/ | ||
|
||
inductive Forall (P : α → Prop) : List α → Prop | ||
| nil : Forall P [] | ||
| cons : {x : α} → P x → Forall P l → Forall P (x::l) | ||
|
||
inductive Tree : Type := | ||
| leaf : Nat → Tree | ||
| node : List Tree → Tree | ||
|
||
set_option trace.Meta.IndPredBelow true in | ||
|
||
/-- Despite not having `.below` and `.brecOn`, | ||
the type is still usable thanks to well-founded recursion. -/ | ||
inductive OnlyZeros : Tree → Prop := | ||
| leaf : OnlyZeros (.leaf 0) | ||
| node (l : List Tree): Forall OnlyZeros l → OnlyZeros (.node l) | ||
|
||
/-- Equivalent definition of `OnlyZeros`, defined by a function instead of an inductive type. -/ | ||
def onlyZeros : Tree → Prop | ||
| .leaf n => n = 0 | ||
| .node [] => True | ||
| .node (x::s) => onlyZeros x ∧ onlyZeros (.node s) | ||
|
||
/-- Pattern-matching on `OnlyZeros` works despite `below` and `brecOn` not being generated. -/ | ||
def toFixPoint : OnlyZeros t → onlyZeros t | ||
| .leaf => rfl | ||
| .node [] _ => True.intro | ||
| .node (x::s) (.cons h p) => by | ||
rw [onlyZeros] -- necessary because `onlyZeros` isn't structurally recursive | ||
exact And.intro (toFixPoint h) (toFixPoint (.node s p)) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
[Meta.IndPredBelow] Nested or not recursive |