How to use proof with disjunctions?

Stream: new members

[Evgeny Kurnevsky]

Hi. I'm trying to write a function like:

def f (x: Nat) (p: x = 1 ∨ x = 2 ∨ x = 3): Nat :=
  match x with
  | 1 => 7
  | 2 => 8
  | 3 => 9
  | _ => sorry

What is the easiest way to use the proof to make this pattern matching exhaustive? I can't pattern match on the proof itself because this way I'd need to eliminate Prop into Type.

[Henrik Böving]

def f (x: Nat) (p: x = 1 ∨ x = 2 ∨ x = 3): Nat :=
  match x with
  | 1 => 7
  | 2 => 8
  | 3 => 9
  | x + 4 => False.elim <| by simp at p

works for example

[Evgeny Kurnevsky]

Thanks! I'm not really confident with tactics as the only dependently typed language I know is Agda :)

What I'm actually trying to do is a bit more complex. Is it possible to do the similar with variables? Like:

def f (x: Nat) (y: Nat) (z: Nat) (p: x = y ∨ x = z): Nat :=
  if x = y then
    0
  else if x = z then
    1
  else
    sorry

Comparing to the first example I can't use pattern matching on x anymore and don't get any information in the else block.

[Damiano Testa]

You can name the hypothesis, to access it later on:

if h : x = y then

[Henrik Böving]

def f (x: Nat) (y: Nat) (z: Nat) (p: x = y ∨ x = z): Nat :=
  if h1 : x = y then
    0
  else if h2 : x = z then
    1
  else
    False.elim <| by omega

@Evgeny Kurnevsky