Lean4
/-- The main combinator which combines multiple `positivity` results.
It assumes `t₁` has already been run for a result, and runs `t₂` and takes the best result.
It will skip `t₂` if `t₁` is already a proof of `.positive`, and can also combine
`.nonnegative` and `.nonzero` to produce a `.positive` result. -/
def orElse {e : Q($α)} (t₁ : Strictness zα pα e) (t₂ : MetaM (Strictness zα pα e)) : MetaM (Strictness zα pα e) := do
match t₁ with
| .none =>
catchNone t₂
| p@(.positive _) =>
pure p
| .nonnegative p₁ =>
match ← catchNone t₂ with
| p@(.positive _) =>
pure p
| .nonzero p₂ =>
pure (.positive q(lt_of_le_of_ne' $p₁ $p₂))
| _ =>
pure (.nonnegative p₁)
| .nonzero p₁ =>
match ← catchNone t₂ with
| p@(.positive _) =>
pure p
| .nonnegative p₂ =>
pure (.positive q(lt_of_le_of_ne' $p₂ $p₁))
| _ =>
pure (.nonzero p₁)
