Preserve equality with match expression

Question

How can I prove that the matched pattern is equal to the original argument?

For example, in the following function, what can I write instead of sorry to prove the equality?

def e1 (x: Option Nat): Nat :=
  match x with
  | none => 1
  | some y =>
    have : some y = x := sorry
    y+1

The only option I could come up with was using a pair with an equality proof, but that seems a bit too complex:

def e2 (x: Option Nat): Nat :=
  let x' := x
  have x'_eq: x' = x := rfl
  match x', x'_eq with
  | none, _ => 1
  | some y, y_eq =>
    have : some y = x := y_eq
    y+1

Is there an easier way to do this?

Answer 1

The syntax for this is match h : x with, no whitespace after h or :, which will leave you with hypotheses of h : x = none and h : x = some y in each branch. There's an open PR to add this to the docs, it will probably be pulled in the next day or two.

Answer 2

In Lean 3, you can solve this using the following syntax:

def e1 (x : option ℕ) : ℕ :=
match _, rfl : ∀ y, y = x → _ with
| none, h := 1
| some y, h :=
  have some y = x := h,
  y+1
end

The match x, y : T with syntax means "generate a function of type T called e1._match or similar, and then replace this match expression with e1._match x y". T is usually therefore of the form X → Y → _, where _ is the type of the values within the match expression.

Note that this is essentially the same as your solution, but the match expression lets us combine it all into one line.

Answer 3

Your question is for Lean, but users of other languages might stumble over it as it is a quite common problem, so it might be useful to collect design patterns in all languages.

In Agda, the inspect idiom is usually defined to create a singleton which also contains a witness that the matched expression is equal to the original expression. For built-in Equality, it can be defined like this:

data Singleton {a} {A : Set a} (x : A) : Set a where
  _with≡_ : (y : A) → x ≡ y → Singleton x

inspect : ∀ {a} {A : Set a} (x : A) → Singleton x
inspect x = x with≡ refl

Your example then can be implemented like this (using built-in Nat and Maybe):

e1 : Maybe Nat → Nat
e1 x with inspect x
... | nothing with≡ p = 1
... | just y  with≡ p = {! p : x ≡ just y !}