Zulip Chat Archive

Stream: general

Topic: Proving things about `option.get`


Sabrina Jewson (Jan 03 2023 at 18:57):

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 (Jan 03 2023 at 19:16):

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

Martin Dvořák (Jan 03 2023 at 19:22):

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 (Jan 03 2023 at 19:47):

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 (Jan 03 2023 at 19:53):

Oh the curse of MWEs!


Last updated: Dec 20 2023 at 11:08 UTC