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?