Compute through option

Stream: general

[Scott Viteri]

Suppose I have the following definition:

def option_and (o₁ o₂ : option bool) : option bool :=
 do x₁ ← o₁, x₂ ← o₂, band x₁ x₂

Running #eval (option_and none none) gives me none as expected.

But I am not sure what tactic or rewrite I need to use to close the following result of the monadic computation.

lemma th : option_and none none = none := ...

[Yakov Pechersky]

import data.option.basic

def option_and (o₁ o₂ : option bool) : option bool :=
 do x₁ ← o₁, x₂ ← o₂, band x₁ x₂

lemma th : option_and none none = none := by simp [option_and]

[Yakov Pechersky]

Alternatively,

import data.option.basic

@[simp] def option_and (o₁ o₂ : option bool) : option bool :=
 do x₁ ← o₁, x₂ ← o₂, band x₁ x₂

lemma th : option_and none none = none := by simp

[Scott Viteri]

Haha woops thanks

[Yakov Pechersky]

And I don't know if you have a preference for monads or applicatives, because:

import data.option.basic

@[simp] lemma option.seq_none {α β : Type*} (a : option α) :
  (none : option (α → β)) <*> a = none := rfl

@[simp] lemma option.seq_some {α β : Type*} (f : α → β) (a : option α) :
  (some f) <*> a = a.map f := rfl

@[simp] def option_and (o₁ o₂ : option bool) : option bool :=
  band <$> o₁ <*> o₂

lemma th : option_and none none = none := by simp

[Scott Viteri]

I see, this is useful

[Mario Carneiro]

surely rfl also works as a proof here

[Scott Viteri]

yes it does