3

I'm just starting out with lean.

Say I want to prove something about functions between two finite types. For example

example (f : Bool -> Bool) : (∀ x : Bool, f (f (f x)) = f x) := sorry

since there are just a few possibilities for f ideally I'd want something like cases x <;> cases f <;> rfl, but I can't do cases f.

Currently, I don't know how to prove this at all, I'd think cases/match on (f false) and (f true) but lean doesn't seem to remember this information about the function once it goes into the case.

acupoftea
  • 181
  • 2
  • 11
  • 1
    there's some versions of this proof (for lean 3) [here](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Kaminski's.20Equation); I think when the theory of finite types is passed along to lean 4 this should be very simole indeed – It'sNotALie. Sep 06 '22 at 13:53
  • 1
    (it may already be there! I don't know much about lean4...) – It'sNotALie. Sep 06 '22 at 13:53
  • 1
    From that thread, it seems like the cleanest lean 3 proof is `by revert f; dec_trivial`. Maybe you can do something similar in lean 4? – user2395649 Sep 06 '22 at 13:58

1 Answers1

3

Here's a proof along your original lines (not dec_trivial), note we use the h : syntax to name the case hypothesis:

example (f : Bool -> Bool) : (∀ x : Bool, f (f (f x)) = f x) := 
by
  intro x
  cases x <;>
  cases h : f true <;>
  cases h2 : f false <;>
  simp [h, h2]
Marcus Rossel
  • 3,196
  • 1
  • 26
  • 41
Alex J Best
  • 306
  • 1
  • 6
  • thanks, is there a general way to split a function? – acupoftea Sep 06 '22 at 14:12
  • 2
    What do you mean exactly? To always do cases on the finitely many outputs for a finite type? In Lean 3 there is a `fin_cases` tactic which was quite useful for this, but it hasn't finished being ported yet. – Alex J Best Sep 06 '22 at 14:16