7
$\begingroup$

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?

$\endgroup$

3 Answers 3

8
$\begingroup$

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.

$\endgroup$
1
  • 3
    $\begingroup$ Note: The syntax isn't whitespace sensitive anymore. $\endgroup$ Apr 23 at 9:32
8
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ 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. $\endgroup$
    – user32157
    Jul 14 at 10:28
5
$\begingroup$

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 !}
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.