Prove things about match

Stream: lean4

[Andrew Yang]

Maybe this belongs in #new members instead but how do I prove things about match? Is there a way to do the following without writing all 9 (or 7) possibilities?

inductive Foo | A | B | C

def foo : Foo → Foo → Nat
  | .A, _ => 0
  | _, .C => 0
  | _, _ => 0

example : ∀ n m, foo n m = 0
  | .A, _ => by simp [foo]
  | _, .C => by simp [foo]; sorry -- doesn't work as lean doesn't know the first thing is not `.A`
  | _, _ => by simp [foo]; sorry

[Aaron Liu]

You can split

[Aaron Liu]

inductive Foo | A | B | C

def foo : Foo → Foo → Nat
  | .A, _ => 0
  | _, .C => 0
  | _, _ => 0

example (n m : Foo) : foo n m = 0 := by
  unfold foo
  split
  · simp
  · simp
  · simp

[Andrew Yang]

Great! Can I achieve this without tactic mode if I e.g. want to construct data?

[Aaron Liu]

Can you give more details?

[Andrew Yang]

I have nothing more specific but for example if I want

inductive Foo | A | B | C

def foo : Foo → Foo → Nat
  | .A, _ => 0
  | _, .C => 1
  | _, _ => 2

def foo2 : ∀ (n m : Foo), Σ' x : Nat, foo n m = x
| .A, _ => ⟨0, by simp [foo]⟩
| _, .C => ⟨1, sorry⟩
| _, _ => ⟨2, sorry⟩

And split gives bad defeqs.

[Aaron Liu]

Sorry, I don't have a solution for you in that case.

[Aaron Liu]

You could try an if-then-else statement, instead of match

[Edward van de Meent]

here's a fun proof:

example : ∀ n m, foo n m = 0 := by
  intro n m
  fun_cases foo n m <;> simp [foo]

[Robin Arnez]

soon to be fun_cases foo n m <;> rfl! (lean#8104)