# Preserve equality with match expression

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?

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.

• Note: The syntax isn't whitespace sensitive anymore. Apr 23, 2022 at 9:32

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.

• Is there a way to do this that still easily allows recursion? I was using the alternative match notation (without the explicit match keyword or :=) since my function is recursively defined. I don't see how to do that with that alternative match syntax. Jul 14, 2022 at 10:28

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 !}

• Note that the inspect idiom is built into Agda now, you don't need to define your own Singleton type and inspect function, you can just use the in keyword: agda.readthedocs.io/en/latest/language/… Nov 6 at 18:56