[Merged by Bors] - feat(data/bool/basic): Kaminski's equation #14159
Conversation
bool.apply_apply_apply : ∀ (f : bool → bool) (x : bool), f (f (f x)) = f x
slerpyyy
added
the
easy
|
✌️ slerpyyy can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-bot-assistant
added
the
delegated
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
| theorem apply_apply_apply (f : bool → bool) (x : bool) : f (f (f x)) = f x := | ||
| by cases x; cases h₁ : f tt; cases h₂ : f ff; simp only [h₁, h₂] |
There was a problem hiding this comment.
Does this shorter proof work in this file?
| theorem apply_apply_apply (f : bool → bool) (x : bool) : f (f (f x)) = f x := | |
| by cases x; cases h₁ : f tt; cases h₂ : f ff; simp only [h₁, h₂] | |
| theorem apply_apply_apply : ∀ (f : bool → bool) (x : bool), f (f (f x)) = f x := | |
| dec_trivial |
There was a problem hiding this comment.
I checked locally and it seems like it doesn't
There was a problem hiding this comment.
Neither does Patrick Johnson's fin_cases proof
There was a problem hiding this comment.
@eric-wieser What imports did that need? This module is a mathlib root (no imports!)
There was a problem hiding this comment.
It needs data.fintype.basic:
import data.fintype.basic
lemma foo : ∀ (f : bool → bool) {x : bool}, f (f (f x)) = f x :=
dec_trivial
as it uses pi.fintype.
There was a problem hiding this comment.
Surely this would make for a nice (if niche) simp theorem?
There was a problem hiding this comment.
It's not valid for simp because the head symbol is not a constant, so lean can infer f = fun x, x and get stuck in a loop
|
We should probably wait for the ongoing Zulip discussion about whether "Kaminski's equation" is a reasonable name to resolve before merging this. |
|
It seems there is no more discussion about this so I will go ahead and merge it |
|
bors r+ |
YaelDillies
changed the title
`bool.apply_apply_apply : ∀ (f : bool → bool) (x : bool), f (f (f x)) = f x`
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
bool.apply_apply_apply : ∀ (f : bool → bool) (x : bool), f (f (f x)) = f x