feat: add Fin.any and Fin.all
#1435
Conversation
github-actions
bot
added
the
awaiting-review
fgdorais
force-pushed
the
fin_all_any
branch
from
587c487 to
133191e
Compare
|
Mathlib CI status (docs):
|
| theorem all_eq_true_iff {p : Fin n → Bool} : Fin.all p = true ↔ ∀ i, p i = true := by simp | ||
|
|
||
| theorem all_eq_false_iff {p : Fin n → Bool} : Fin.all p = false ↔ ∃ i, p i = false := by simp | ||
|
|
There was a problem hiding this comment.
So arguably we are missing some lemmas but you could argue they are covered by the fact this is just an abbrev.
I would expect any_zero, all_zero, any_succ and all_succ, though.
I also think you want something like not_any_eq_all_not and not_all_eq_any_not which are not hard proofs but I think are probably worth having. You could also have all_eq_not_any_not in the same way. In general I would consider what lemmas from here: https://leanprover-community.github.io/mathlib4_docs/Init/Data/List/Lemmas.html#List.not_any_eq_all_not are wanted by analogy.
There was a problem hiding this comment.
How about going a step further and have classes to standardize the basic API for all and any?
| Short-circuits upon encountering the first false. | ||
| -/ | ||
| protected abbrev all (p : Fin n → Bool) := find? (! p ·) |>.isNone |
There was a problem hiding this comment.
Could also consider simply ! any (! p ·).
There was a problem hiding this comment.
Potatoes/Tomatoes? I don't have a preference either way.
|
Some good work here! I think we have slightly different tastes for number of lemmas etc. in some ways - but I absolutely agree we should have this. (We're also missing, say, |
fgdorais
force-pushed
the
fin_all_any
branch
from
1e034ff to
48005a6
Compare
leanprover-community-mathlib4-bot
added
the
merge-conflict
leanprover-community-mathlib4-bot
removed
the
merge-conflict
leanprover-community-mathlib4-bot
added
the
merge-conflict
leanprover-community-mathlib4-bot
removed
the
merge-conflict
No description provided.