Proving things about `option.get`

Stream: general

[Sabrina Jewson]

I have code roughly analagous to this:

def p : ℕ → option ℕ
| 0 := none
| (n + 1) := some n

def p_nonzero_some {n : ℕ} (n_nonzero : n ≠ 0) : (p n).is_some
:= begin induction n, contradiction, simp [p, option.is_some] end

def p_nonzero {n : ℕ} (n_nonzero : n ≠ 0) : ℕ := option.get (p_nonzero_some n_nonzero)

def succ_p {n : ℕ} (n_nonzero : n ≠ 0) : (p_nonzero n_nonzero) + 1 = n := begin
  simp [p_nonzero, p_nonzero_some],
end

But I really don’t know how to prove the goal. The context looks like:

n : ℕ
n_nonzero : n ≠ 0
⊢ option.get _ + 1 = n

My actual use-case is using option.get for docs#finmap.lookup, since I don’t think there’s a non-option variant.

[Logan Murphy]

Not sure if this maps to your use case, but could you do cases n, contradiction, refl?

[Martin Dvořák]

def succ_p {n : ℕ} (n_nonzero : n ≠ 0) : (p_nonzero n_nonzero) + 1 = n := begin
  cases n;
  finish,
end

works as well as

def succ_p {n : ℕ} (n_nonzero : n ≠ 0) : (p_nonzero n_nonzero) + 1 = n := begin
  cases n,
  {
    exfalso,
    exact n_nonzero rfl,
  },
  {
    refl,
  },
end

[Sabrina Jewson]

Aah, shame on me for posting an oversimplified example :sweat_smile:. I think I it gave me some inspiration now though, so thanks for the input!

[Martin Dvořák]

Oh the curse of MWEs!