Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus.
On Mac, use
Cmd instead of
Ctrl .
/-
Copyright (c) 2022 Mario Carneiro, Heather Macbeth. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro, Heather Macbeth, Yaël Dillies
-/
import Std.Lean.Parser
import Mathlib.Data.Int.Order.Basic
import Mathlib.Data.Nat.Factorial.Basic
import Mathlib.Tactic.Positivity.Core
import Mathlib.Algebra.GroupPower.Order
import Mathlib.Algebra.Order.Field.Basic
import Qq
/-!
## `positivity` core extensions
This file sets up the basic `positivity` extensions tagged with the `@[positivity]` attribute.
-/
namespace Mathlib.Meta.Positivity
open Lean Meta Qq Function
section LinearOrder
variable [ LinearOrder R ] { a b c : R }
private lemma le_min_of_lt_of_le : a < b a ≤ c a ≤ min b c le_min_of_lt_of_le ( ha : a < b ) ( hb : a ≤ c ) : a ≤ min : {α : Type ?u.657} → [self : Min α α → α → α b c := le_min ha . le hb
private lemma le_min_of_le_of_lt ( ha : a ≤ b ) ( hb : a < c ) : a ≤ min : {α : Type ?u.1798} → [self : Min α α → α → α b c := le_min ha hb . le
private lemma min_ne ( ha : a ≠ c ) ( hb : b ≠ c ) : min : {α : Type ?u.2322} → [self : Min α α → α → α a b ≠ c :=
by rw [ min_def (if a ≤ b a else b ) ≠ c ] (if a ≤ b a else b ) ≠ c ; (if a ≤ b a else b ) ≠ c split_ifs (if a ≤ b a else b ) ≠ c <;> (if a ≤ b a else b ) ≠ c assumption
private lemma min_ne_of_ne_of_lt : a ≠ c c < b min a b ≠ c min_ne_of_ne_of_lt ( ha : a ≠ c ) ( hb : c < b ) : min : {α : Type ?u.3242} → [self : Min α α → α → α a b ≠ c := min_ne ha hb . ne' : ∀ {α : Type ?u.3380} [inst : Preorder α x y : α }, x < y y ≠ x
private lemma min_ne_of_lt_of_ne ( ha : c < a ) ( hb : b ≠ c ) : min : {α : Type ?u.4119} → [self : Min α α → α → α a b ≠ c := min_ne ha . ne' : ∀ {α : Type ?u.4256} [inst : Preorder α x y : α }, x < y y ≠ x hb
private lemma max_ne ( ha : a ≠ c ) ( hb : b ≠ c ) : max : {α : Type ?u.4647} → [self : Max α α → α → α a b ≠ c :=
by rw [ max_def (if a ≤ b b else a ) ≠ c ] (if a ≤ b b else a ) ≠ c ; (if a ≤ b b else a ) ≠ c split_ifs (if a ≤ b b else a ) ≠ c <;> (if a ≤ b b else a ) ≠ c assumption
end LinearOrder
/-- The `positivity` extension which identifies expressions of the form `min a b`,
such that `positivity` successfully recognises both `a` and `b`. -/
@[ positivity min : {α : Type ?u.15863} → [self : Min α α → α → α _ _ ] def evalMin : PositivityExt where eval { u α } zα pα e := do
let .app ( .app ( f : Q( $α → $α → $α) ) ( a : Q( $α) )) ( b : Q( $α) ) ← withReducible ( whnf e )
| throwError "not min" : ?m.8674 ?m.8675
throwError throwError "not min" : ?m.8674 ?m.8675
let _e_eq : «$e» =Q «$f» «$a» «$b»
_e_eq : $ e =Q $ f $ a $ b := ⟨⟩ : «$e» =Q «$f» «$a» «$b»
let _a ← synthInstanceQ ( q( LinearOrder : Type ?u.5448 → Type ?u.5448LinearOrder $ α ) : Q( Type u ))
assumeInstancesCommute
let ⟨ _f_eq ⟩ ← withDefault <| withNewMCtxDepth <| assertDefEqQ : {u : Level } →
{α :
let u := u ;
Q(Sort u) } →
(a b : Q(«$α» ) ) → MetaM (PLift («$a» =Q «$b» (u := u . succ ) f q( min )
match ← core zα pα a , ← core zα pα b with
| .positive pa , .positive pb => pure : {f : Type ?u.7440 → Type ?u.7439[self : Pure f {α : Type ?u.7440} → α → f α ( .positive q( lt_min $ pa $ pb ))
| .positive pa , .nonnegative pb => pure : {f : Type ?u.7579 → Type ?u.7578[self : Pure f {α : Type ?u.7579} → α → f α ( .nonnegative q( le_min_of_lt_of_le le_min_of_lt_of_le $pa $pb : ?m.5135
$ pa le_min_of_lt_of_le $pa $pb : ?m.5135
$ pb ))
| .nonnegative pa , .positive pb => pure : {f : Type ?u.7686 → Type ?u.7685[self : Pure f {α : Type ?u.7686} → α → f α ( .nonnegative q( le_min_of_le_of_lt le_min_of_le_of_lt $pa $pb : ?m.5135
$ pa le_min_of_le_of_lt $pa $pb : ?m.5135
$ pb ))
| .nonnegative pa , .nonnegative pb => pure : {f : Type ?u.7783 → Type ?u.7782[self : Pure f {α : Type ?u.7783} → α → f α ( .nonnegative q( le_min $ pa $ pb ))
| .positive pa , .nonzero pb => pure : {f : Type ?u.7882 → Type ?u.7881[self : Pure f {α : Type ?u.7882} → α → f α ( .nonzero q( min_ne_of_lt_of_ne min_ne_of_lt_of_ne $pa $pb : ?m.5135
$ pa min_ne_of_lt_of_ne $pa $pb : ?m.5135
$ pb ))
| .nonzero pa , .positive pb => pure : {f : Type ?u.7979 → Type ?u.7978[self : Pure f {α : Type ?u.7979} → α → f α ( .nonzero q( min_ne_of_ne_of_lt min_ne_of_ne_of_lt $pa $pb : ?m.5135
$ pa min_ne_of_ne_of_lt $pa $pb : ?m.5135
$ pb ))
| .nonzero pa , .nonzero pb => pure : {f : Type ?u.8073 → Type ?u.8072[self : Pure f {α : Type ?u.8073} → α → f α ( .nonzero q( min_ne $ pa $ pb ))
| _, _ => pure : {f : Type ?u.8154 → Type ?u.8153[self : Pure f {α : Type ?u.8154} → α → f α .none
/-- Extension for the `max` operator. The `max` of two numbers is nonnegative if at least one
is nonnegative, strictly positive if at least one is positive, and nonzero if both are nonzero. -/
@[ positivity max : {α : Type ?u.25669} → [self : Max α α → α → α _ _ ] def evalMax : PositivityExt where eval { u α } zα pα e := do
let .app ( .app ( f : Q( $α → $α → $α) ) ( a : Q( $α) )) ( b : Q( $α) ) ← withReducible ( whnf e )
| throwError "not max" : ?m.19545 ?m.19546
throwError throwError "not max" : ?m.19545 ?m.19546
let _e_eq : «$e» =Q «$f» «$a» «$b»
_e_eq : $ e =Q $ f $ a $ b := ⟨⟩ : «$e» =Q «$f» «$a» «$b»
let _a ← synthInstanceQ ( q( LinearOrder : Type ?u.16200 → Type ?u.16200LinearOrder $ α ) : Q( Type u ))
assumeInstancesCommute
let ⟨ _f_eq ⟩ ← withDefault <| withNewMCtxDepth <| assertDefEqQ : {u : Level } →
{α :
let u := u ;
Q(Sort u) } →
(a b : Q(«$α» ) ) → MetaM (PLift («$a» =Q «$b» (u := u . succ ) f q( max )
let result : Strictness zα pα e ← catchNone do
let ra ← core zα pα a
match ra with
| .positive pa => pure : {f : Type ?u.18184 → Type ?u.18183[self : Pure f {α : Type ?u.18184} → α → f α ( .positive q( lt_max_of_lt_left lt_max_of_lt_left $pa : ?m.15887
$ pa ))
| .nonnegative pa => pure : {f : Type ?u.18309 → Type ?u.18308[self : Pure f {α : Type ?u.18309} → α → f α ( .nonnegative q( le_max_of_le_left le_max_of_le_left $pa : ?m.15887
$ pa ))
-- If `a ≠ 0`, we might prove `max a b ≠ 0` if `b ≠ 0` but we don't want to evaluate
-- `b` before having ruled out `0 < a`, for performance. So we do that in the second branch
-- of the `orElse'`.
| _ => pure : {f : Type ?u.18393 → Type ?u.18392[self : Pure f {α : Type ?u.18393} → α → f α .none
orElse result do
let rb ← core zα pα b
match rb with
| .positive pb => pure : {f : Type ?u.18666 → Type ?u.18665[self : Pure f {α : Type ?u.18666} → α → f α ( .positive q( lt_max_of_lt_right lt_max_of_lt_right $pb : ?m.15887
$ pb ))
| .nonnegative pb => pure : {f : Type ?u.18810 → Type ?u.18809[self : Pure f {α : Type ?u.18810} → α → f α ( .nonnegative q( le_max_of_le_right le_max_of_le_right $pb : ?m.15887
$ pb ))
| .nonzero pb => do
match ← core zα pα a with
| .nonzero pa => pure : {f : Type ?u.18967 → Type ?u.18966[self : Pure f {α : Type ?u.18967} → α → f α ( .nonzero q( max_ne $ pa $ pb ))
| _ => pure : {f : Type ?u.19044 → Type ?u.19043[self : Pure f {α : Type ?u.19044} → α → f α .none
| _ => pure : {f : Type ?u.19210 → Type ?u.19209[self : Pure f {α : Type ?u.19210} → α → f α .none
/-- The `positivity` extension which identifies expressions of the form `a + b`,
such that `positivity` successfully recognises both `a` and `b`. -/
@[ positivity _ + _ , Add.add : {α : Type ?u.37295} → [self : Add α α → α → α _ _ ] def evalAdd : PositivityExt where eval { u α } zα pα e := do
let .app ( .app ( f : Q( $α → $α → $α) ) ( a : Q( $α) )) ( b : Q( $α) ) ← withReducible ( whnf e )
| throwError "not +" : ?m.30239 ?m.30240
throwError throwError "not +" : ?m.30239 ?m.30240
let _e_eq : «$e» =Q «$f» «$a» «$b»
_e_eq : $ e =Q $ f $ a $ b := ⟨⟩ : «$e» =Q «$f» «$a» «$b»
let _a ← synthInstanceQ ( q( AddZeroClass : Type ?u.26006 → Type ?u.26006AddZeroClass AddZeroClass $α : ?m.25693
$ α ) : Q( Type u ))
assumeInstancesCommute
let ⟨ _f_eq ⟩ ← withDefault <| withNewMCtxDepth <| assertDefEqQ : {u : Level } →
{α :
let u := u ;
Q(Sort u) } →
(a b : Q(«$α» ) ) → MetaM (PLift («$a» =Q «$b» (u := u . succ ) f q( HAdd.hAdd )
let ra ← core zα pα a ; let rb ← core zα pα b
match ra , rb with
| .positive pa , .positive pb =>
let _a ← synthInstanceQ ( q( CovariantClass : (M : Type ?u.27962) → (N : Type ?u.27961) → (M → N → N (N → N → Prop Prop CovariantClass CovariantClass $α $α (·+·) (·<·) : ?m.25693
$ α CovariantClass $α $α (·+·) (·<·) : ?m.25693
$ α CovariantClass $α $α (·+·) (·<·) : ?m.25693
(·+·) : «$α» → «$α» → «$α»
(·+·) CovariantClass $α $α (·+·) (·<·) : ?m.25693
(·<·) : «$α» → «$α» → Prop (·<·) ) : Q( Prop ))
pure : {f : Type ?u.28240 → Type ?u.28239[self : Pure f {α : Type ?u.28240} → α → f α ( .positive q( add_pos add_pos $pa $pb : ?m.25693
$ pa add_pos $pa $pb : ?m.25693
$ pb ))
| .positive pa , .nonnegative pb =>
let _a ← synthInstanceQ ( q( CovariantClass : (M : Type ?u.28483) → (N : Type ?u.28482) → (M → N → N (N → N → Prop Prop CovariantClass CovariantClass $α $α (swap (·+·)) (·<·) : ?m.25693
$ α CovariantClass $α $α (swap (·+·)) (·<·) : ?m.25693
$ α CovariantClass $α $α (swap (·+·)) (·<·) : ?m.25693
( swap : {α : Sort ?u.28486} →
{β : Sort ?u.28485} → {φ : α → β → Sort ?u.28484((x : α ) → (y : β ) → φ x y ) → (y : β ) → (x : α ) → φ x y swap CovariantClass $α $α (swap (·+·)) (·<·) : ?m.25693
(·+·) : «$α» → «$α» → «$α»
(·+·) CovariantClass $α $α (swap (·+·)) (·<·) : ?m.25693
) (·<·) : «$α» → «$α» → Prop (·<·) ) : Q( Prop ))
pure : {f : Type ?u.28758 → Type ?u.28757[self : Pure f {α : Type ?u.28758} → α → f α ( .positive q( lt_add_of_pos_of_le lt_add_of_pos_of_le $pa $pb : ?m.25693
$ pa lt_add_of_pos_of_le $pa $pb : ?m.25693
$ pb ))
| .nonnegative pa , .positive pb =>
let _a ← synthInstanceQ ( q( CovariantClass : (M : Type ?u.28962) → (N : Type ?u.28961) → (M → N → N (N → N → Prop Prop CovariantClass CovariantClass $α $α (·+·) (·<·) : ?m.25693
$ α CovariantClass $α $α (·+·) (·<·) : ?m.25693
$ α CovariantClass $α $α (·+·) (·<·) : ?m.25693
(·+·) : «$α» → «$α» → «$α»
(·+·) CovariantClass $α $α (·+·) (·<·) : ?m.25693
(·<·) : «$α» → «$α» → Prop (·<·) ) : Q( Prop ))
pure : {f : Type ?u.29215 → Type ?u.29214[self : Pure f {α : Type ?u.29215} → α → f α ( .positive q( lt_add_of_le_of_pos lt_add_of_le_of_pos $pa $pb : ?m.25693
$ pa lt_add_of_le_of_pos $pa $pb : ?m.25693
$ pb ))
| .nonnegative pa , .nonnegative pb =>
let _a ← synthInstanceQ ( q( CovariantClass : (M : Type ?u.29410) → (N : Type ?u.29409) → (M → N → N (N → N → Prop Prop CovariantClass CovariantClass $α $α (·+·) (·≤·) : ?m.25693
$ α CovariantClass $α $α (·+·) (·≤·) : ?m.25693
$ α CovariantClass $α $α (·+·) (·≤·) : ?m.25693
(·+·) : «$α» → «$α» → «$α»
(·+·) CovariantClass $α $α (·+·) (·≤·) : ?m.25693
(·≤·) : «$α» → «$α» → Prop (·≤·) ) : Q( Prop ))
pure : {f : Type ?u.29685 → Type ?u.29684[self : Pure f {α : Type ?u.29685} → α → f α ( .nonnegative q( add_nonneg add_nonneg $pa $pb : ?m.25693
$ pa add_nonneg $pa $pb : ?m.25693
$ pb ))
| _, _ => failure
private theorem mul_nonneg_of_pos_of_nonneg [ OrderedSemiring : Type ?u.37331 → Type ?u.37331 α ] { a b : α }
( ha : 0 < a ) ( hb : 0 ≤ b ) : 0 ≤ a * b :=
mul_nonneg ha . le : ∀ {α : Type ?u.38534} [inst : Preorder α a b : α }, a < b a ≤ b hb
private theorem mul_nonneg_of_nonneg_of_pos [ OrderedSemiring : Type ?u.38662 → Type ?u.38662 α ] { a b : α }
( ha : 0 ≤ a ) ( hb : 0 < b ) : 0 ≤ a * b :=
mul_nonneg ha hb . le : ∀ {α : Type ?u.39867} [inst : Preorder α a b : α }, a < b a ≤ b
private theorem mul_ne_zero_of_ne_zero_of_pos [ OrderedSemiring : Type ?u.39992 → Type ?u.39992 α ] [ NoZeroDivisors : (M₀ : Type ?u.39995) → [inst : Mul M₀ [inst : Zero M₀ Prop α ]
{ a b : α } ( ha : a ≠ 0 ) ( hb : 0 < b ) : a * b ≠ 0 :=
mul_ne_zero ha ( ne_of_gt : ∀ {α : Type ?u.41139} [inst : Preorder α a b : α }, b < a a ≠ b hb )
private theorem mul_ne_zero_of_pos_of_ne_zero [ OrderedSemiring : Type ?u.41662 → Type ?u.41662 α ] [ NoZeroDivisors : (M₀ : Type ?u.41665) → [inst : Mul M₀ [inst : Zero M₀ Prop α ]
{ a b : α } ( ha : 0 < a ) ( hb : b ≠ 0 ) : a * b ≠ 0 :=
mul_ne_zero ( ne_of_gt : ∀ {α : Type ?u.42808} [inst : Preorder α a b : α }, b < a a ≠ b ha ) hb
/-- The `positivity` extension which identifies expressions of the form `a * b`,
such that `positivity` successfully recognises both `a` and `b`. -/
@[ positivity _ * _ , Mul.mul : {α : Type ?u.53651} → [self : Mul α α → α → α _ _ ] def evalMul : PositivityExt where eval { u α } zα pα e := do
let .app ( .app ( f : Q( $α → $α → $α) ) ( a : Q( $α) )) ( b : Q( $α) ) ← withReducible ( whnf e )
| throwError "not *" : ?m.46614 ?m.46615
throwError throwError "not *" : ?m.46614 ?m.46615
let _e_eq : «$e» =Q «$f» «$a» «$b»
_e_eq : $ e =Q $ f $ a $ b := ⟨⟩ : «$e» =Q «$f» «$a» «$b»
let _a ← synthInstanceQ ( q( StrictOrderedSemiring : Type ?u.43642 → Type ?u.43642StrictOrderedSemiring StrictOrderedSemiring $α : ?m.43329
$ α ) : Q( Type u ))
assumeInstancesCommute
let ⟨ _f_eq ⟩ ← withDefault <| withNewMCtxDepth <| assertDefEqQ : {u : Level } →
{α :
let u := u ;
Q(Sort u) } →
(a b : Q(«$α» ) ) → MetaM (PLift («$a» =Q «$b» (u := u . succ ) f q( HMul.hMul )
let ra ← core zα pα a ; let rb ← core zα pα b
match ra , rb with
| .positive pa , .positive pb => pure : {f : Type ?u.44436 → Type ?u.44435[self : Pure f {α : Type ?u.44436} → α → f α ( .positive q( mul_pos mul_pos $pa $pb : ?m.43329
$ pa mul_pos $pa $pb : ?m.43329
$ pb ))
| .positive pa , .nonnegative pb => pure : {f : Type ?u.44841 → Type ?u.44840[self : Pure f {α : Type ?u.44841} → α → f α ( .nonnegative q( mul_nonneg_of_pos_of_nonneg mul_nonneg_of_pos_of_nonneg $pa $pb : ?m.43329
$ pa mul_nonneg_of_pos_of_nonneg $pa $pb : ?m.43329
$ pb ))
| .nonnegative pa , .positive pb => pure : {f : Type ?u.44983 → Type ?u.44982[self : Pure f {α : Type ?u.44983} → α → f α ( .nonnegative q( mul_nonneg_of_nonneg_of_pos mul_nonneg_of_nonneg_of_pos $pa $pb : ?m.43329
$ pa mul_nonneg_of_nonneg_of_pos $pa $pb : ?m.43329
$ pb ))
| .nonnegative pa , .nonnegative pb => pure : {f : Type ?u.45064 → Type ?u.45063[self : Pure f {α : Type ?u.45064} → α → f α ( .nonnegative q( mul_nonneg mul_nonneg $pa $pb : ?m.43329
$ pa mul_nonneg $pa $pb : ?m.43329
$ pb ))
| .positive pa , .nonzero pb =>
let _a ← synthInstanceQ ( q( NoZeroDivisors : (M₀ : Type ?u.45292) → [inst : Mul M₀ [inst : Zero M₀ Prop NoZeroDivisors NoZeroDivisors $α : ?m.43329
$ α ) : Q( Prop ))
pure : {f : Type ?u.45440 → Type ?u.45439[self : Pure f {α : Type ?u.45440} → α → f α ( .nonzero q( mul_ne_zero_of_pos_of_ne_zero mul_ne_zero_of_pos_of_ne_zero $pa $pb : ?m.43329
$ pa mul_ne_zero_of_pos_of_ne_zero $pa $pb : ?m.43329
$ pb ))
| .nonzero pa , .positive pb =>
let _a ← synthInstanceQ ( q( NoZeroDivisors : (M₀ : Type ?u.45659) → [inst : Mul M₀ [inst : Zero M₀ Prop NoZeroDivisors NoZeroDivisors $α : ?m.43329
$ α ) : Q( Prop ))
pure : {f : Type ?u.45671 → Type ?u.45670[self : Pure f {α : Type ?u.45671} → α → f α ( .nonzero q( mul_ne_zero_of_ne_zero_of_pos mul_ne_zero_of_ne_zero_of_pos $pa $pb : ?m.43329
$ pa mul_ne_zero_of_ne_zero_of_pos $pa $pb : ?m.43329
$ pb ))
| .nonzero pa , .nonzero pb =>
let _a ← synthInstanceQ ( q( NoZeroDivisors : (M₀ : Type ?u.45869) → [inst : Mul M₀ [inst : Zero M₀ Prop NoZeroDivisors NoZeroDivisors $α : ?m.43329
$ α ) : Q( Prop ))
pure : {f : Type ?u.45881 → Type ?u.45880[self : Pure f {α : Type ?u.45881} → α → f α ( .nonzero ( q( mul_ne_zero mul_ne_zero $pa $pb : ?m.43329
$ pa mul_ne_zero $pa $pb : ?m.43329
$ pb )))
| _, _ => pure : {f : Type ?u.46160 → Type ?u.46159[self : Pure f {α : Type ?u.46160} → α → f α .none
private lemma int_div_self_pos : ∀ {a : ℤ }, 0 < a 0 < a / a int_div_self_pos { a : ℤ } ( ha : 0 < a ) : 0 < a / a :=
by { rw [ Int.ediv_self : ∀ {a : ℤ }, a ≠ 0 a / a = 1 ha . ne' : ∀ {α : Type ?u.53809} [inst : Preorder α x y : α }, x < y y ≠ x ] ; exact zero_lt_one }
private lemma int_div_nonneg_of_pos_of_nonneg : ∀ {a b : ℤ }, 0 < a 0 ≤ b 0 ≤ a / b int_div_nonneg_of_pos_of_nonneg { a b : ℤ } ( ha : 0 < a ) ( hb : 0 ≤ b ) : 0 ≤ a / b :=
Int.ediv_nonneg : ∀ {a b : ℤ }, 0 ≤ a 0 ≤ b 0 ≤ a / b ha . le : ∀ {α : Type ?u.54732} [inst : Preorder α a b : α }, a < b a ≤ b hb
private lemma int_div_nonneg_of_nonneg_of_pos : ∀ {a b : ℤ }, 0 ≤ a 0 < b 0 ≤ a / b int_div_nonneg_of_nonneg_of_pos { a b : ℤ } ( ha : 0 ≤ a ) ( hb : 0 < b ) : 0 ≤ a / b :=
Int.ediv_nonneg : ∀ {a b : ℤ }, 0 ≤ a 0 ≤ b 0 ≤ a / b ha hb . le : ∀ {α : Type ?u.54962} [inst : Preorder α a b : α }, a < b a ≤ b
private lemma int_div_nonneg_of_pos_of_pos : ∀ {a b : ℤ }, 0 < a 0 < b 0 ≤ a / b int_div_nonneg_of_pos_of_pos { a b : ℤ } ( ha : 0 < a ) ( hb : 0 < b ) : 0 ≤ a / b :=
Int.ediv_nonneg : ∀ {a b : ℤ }, 0 ≤ a 0 ≤ b 0 ≤ a / b ha . le : ∀ {α : Type ?u.55192} [inst : Preorder α a b : α }, a < b a ≤ b hb . le : ∀ {α : Type ?u.55248} [inst : Preorder α a b : α }, a < b a ≤ b
/-- The `positivity` extension which identifies expressions of the form `a / b`,
where `a` and `b` are integers. -/
@[ positivity ( _ : ℤ) / ( _ : ℤ)] def evalIntDiv : PositivityExt where eval { _u _α } zα pα e := do
let .app ( .app f ( a : Q( ℤ))) ( b : Q( ℤ)) ← withReducible ( whnf e ) | throwError "not /" : ?m.57039 ?m.57040
throwError throwError "not /" : ?m.57039 ?m.57040
let ra ← core zα pα a ; let rb ← core zα pα b
guard <|← withDefault <| withNewMCtxDepth <| isDefEq f q( HDiv.hDiv (α := ℤ ) (β := ℤ ))
match ra , rb with
| .positive pa , .positive pb =>
have pa' : Q( 0 < $ a ) := pa
have pb' : Q( 0 < $ b ) := pb
if pa == pb then -- Only attempts to prove `0 < a / a`, otherwise falls back to `0 ≤ a / b`
pure : {f : Type ?u.56149 → Type ?u.56148[self : Pure f {α : Type ?u.56149} → α → f α ( .positive ( q( int_div_self_pos : ∀ {a : ℤ }, 0 < a 0 < a / a $ pa' ) : Expr ))
else
pure : {f : Type ?u.56218 → Type ?u.56217[self : Pure f {α : Type ?u.56218} → α → f α ( .nonnegative ( q( int_div_nonneg_of_pos_of_pos : ∀ {a b : ℤ }, 0 < a 0 < b 0 ≤ a / b $ pa' $ pb' ) : Expr ))
| .positive pa , .nonnegative pb =>
have pa' : Q( 0 < $ a ) := pa
have pb' : Q( 0 ≤ $ b ) := pb
pure : {f : Type ?u.56359 → Type ?u.56358[self : Pure f {α : Type ?u.56359} → α → f α ( .nonnegative ( q( int_div_nonneg_of_pos_of_nonneg : ∀ {a b : ℤ }, 0 < a 0 ≤ b 0 ≤ a / b $ pa' $ pb' ) : Expr ))
| .nonnegative pa , .positive pb =>
have pa' : Q( 0 ≤ $ a ) := pa
have pb' : Q( 0 < $ b ) := pb
pure : {f : Type ?u.56496 → Type ?u.56495[self : Pure f {α : Type ?u.56496} → α → f α ( .nonnegative ( q( int_div_nonneg_of_nonneg_of_pos : ∀ {a b : ℤ }, 0 ≤ a 0 < b 0 ≤ a / b $ pa' $ pb' ) : Expr ))
| .nonnegative pa , .nonnegative pb =>
have pa' : Q( 0 ≤ $ a ) := pa
have pb' : Q( 0 ≤ $ b ) := pb
pure : {f : Type ?u.56629 → Type ?u.56628[self : Pure f {α : Type ?u.56629} → α → f α ( .nonnegative ( q( Int.ediv_nonneg : ∀ {a b : ℤ }, 0 ≤ a 0 ≤ b 0 ≤ a / b $ pa' $ pb' ) : Expr ))
| _, _ => pure : {f : Type ?u.56690 → Type ?u.56689[self : Pure f {α : Type ?u.56690} → α → f α .none
section LinearOrderedSemifield
variable [ LinearOrderedSemifield : Type ?u.63074 → Type ?u.63074 R ] { a b : R }
private lemma div_nonneg_of_pos_of_nonneg ( ha : 0 < a ) ( hb : 0 ≤ b ) : 0 ≤ a / b :=
div_nonneg ha . le : ∀ {α : Type ?u.63467} [inst : Preorder α a b : α }, a < b a ≤ b hb
private lemma div_nonneg_of_nonneg_of_pos ( ha : 0 ≤ a ) ( hb : 0 < b ) : 0 ≤ a / b :=
div_nonneg ha hb . le : ∀ {α : Type ?u.63945} [inst : Preorder α a b : α }, a < b a ≤ b
private lemma div_ne_zero_of_pos_of_ne_zero : 0 < a b ≠ 0 a / b ≠ 0 div_ne_zero_of_pos_of_ne_zero ( ha : 0 < a ) ( hb : b ≠ 0 ) : a / b ≠ 0 :=
div_ne_zero ha . ne' : ∀ {α : Type ?u.64336} [inst : Preorder α x y : α }, x < y y ≠ x hb
private lemma div_ne_zero_of_ne_zero_of_pos : a ≠ 0 0 < b a / b ≠ 0 div_ne_zero_of_ne_zero_of_pos ( ha : a ≠ 0 ) ( hb : 0 < b ) : a / b ≠ 0 :=
div_ne_zero ha hb . ne' : ∀ {α : Type ?u.64734} [inst : Preorder α x y : α }, x < y y ≠ x
end LinearOrderedSemifield
/-- The `positivity` extension which identifies expressions of the form `a / b`,
such that `positivity` successfully recognises both `a` and `b`. -/
@[ positivity _ / _ ] def evalDiv : PositivityExt where eval { u α } zα pα e := do
let .app ( .app ( f : Q( $α → $α → $α) ) ( a : Q( $α) )) ( b : Q( $α) ) ← withReducible ( whnf e )
| throwError "not /" : ?m.66751 ?m.66752
throwError throwError "not /" : ?m.66751 ?m.66752
let _e_eq : «$e» =Q «$f» «$a» «$b»
_e_eq : $ e =Q $ f $ a $ b := ⟨⟩ : «$e» =Q «$f» «$a» «$b»
let _a ← synthInstanceQ ( q( LinearOrderedSemifield : Type ?u.65146 → Type ?u.65146LinearOrderedSemifield LinearOrderedSemifield $α : ?m.64833
$ α ) : Q( Type u ))
assumeInstancesCommute
let ⟨ _f_eq ⟩ ← withDefault <| withNewMCtxDepth <| assertDefEqQ : {u : Level } →
{α :
let u := u ;
Q(Sort u) } →
(a b : Q(«$α» ) ) → MetaM (PLift («$a» =Q «$b» (u := u . succ ) f q( HDiv.hDiv )
let ra ← core zα pα a ; let rb ← core zα pα b
match ra , rb with
| .positive pa , .positive pb => pure : {f : Type ?u.65659 → Type ?u.65658[self : Pure f {α : Type ?u.65659} → α → f α ( .positive q( div_pos div_pos $pa $pb : ?m.64833
$ pa div_pos $pa $pb : ?m.64833
$ pb ))
| .positive pa , .nonnegative pb => pure : {f : Type ?u.65795 → Type ?u.65794[self : Pure f {α : Type ?u.65795} → α → f α ( .nonnegative q( div_nonneg_of_pos_of_nonneg div_nonneg_of_pos_of_nonneg $pa $pb : ?m.64833
$ pa div_nonneg_of_pos_of_nonneg $pa $pb : ?m.64833
$ pb ))
| .nonnegative pa , .positive pb => pure : {f : Type ?u.65884 → Type ?u.65883[self : Pure f {α : Type ?u.65884} → α → f α ( .nonnegative q( div_nonneg_of_nonneg_of_pos div_nonneg_of_nonneg_of_pos $pa $pb : ?m.64833
$ pa div_nonneg_of_nonneg_of_pos $pa $pb : ?m.64833
$ pb ))
| .nonnegative pa , .nonnegative pb => pure : {f : Type ?u.65965 → Type ?u.65964[self : Pure f {α : Type ?u.65965} → α → f α ( .nonnegative q( div_nonneg div_nonneg $pa $pb : ?m.64833
$ pa div_nonneg $pa $pb : ?m.64833
$ pb ))
| .positive pa , .nonzero pb => pure : {f : Type ?u.66046 → Type ?u.66045[self : Pure f {α : Type ?u.66046} → α → f α ( .nonzero q( div_ne_zero_of_pos_of_ne_zero div_ne_zero_of_pos_of_ne_zero $pa $pb : ?m.64833
$ pa div_ne_zero_of_pos_of_ne_zero $pa $pb : ?m.64833
$ pb ))
| .nonzero pa , .positive pb => pure : {f : Type ?u.66127 → Type ?u.66126[self : Pure f {α : Type ?u.66127} → α → f α ( .nonzero q( div_ne_zero_of_ne_zero_of_pos div_ne_zero_of_ne_zero_of_pos $pa $pb : ?m.64833
$ pa div_ne_zero_of_ne_zero_of_pos $pa $pb : ?m.64833
$ pb ))
| .nonzero pa , .nonzero pb => pure : {f : Type ?u.66203 → Type ?u.66202[self : Pure f {α : Type ?u.66203} → α → f α ( .nonzero q( div_ne_zero div_ne_zero $pa $pb : ?m.64833
$ pa div_ne_zero $pa $pb : ?m.64833
$ pb ))
| _, _ => pure : {f : Type ?u.66295 → Type ?u.66294[self : Pure f {α : Type ?u.66295} → α → f α .none
/-- The `positivity` extension which identifies expressions of the form `a⁻¹`,
such that `positivity` successfully recognises `a`. -/
@[ positivity ( _ : α )⁻¹]
def evalInv : PositivityExt where eval { u α } zα pα e := do
let .app ( f : Q( $α → $α) ) ( a : Q( $α) ) ← withReducible ( whnf e ) | throwError "not ⁻¹" : ?m.74031 ?m.74032
throwError throwError "not ⁻¹" : ?m.74031 ?m.74032
let _e_eq : $ e =Q $ f $ a := ⟨⟩
let _a ← synthInstanceQ ( q( LinearOrderedSemifield : Type ?u.73021 → Type ?u.73021LinearOrderedSemifield LinearOrderedSemifield $α : ?m.72720
$ α ) : Q( Type u ))
assumeInstancesCommute
let ⟨ _f_eq ⟩ ← withDefault <| withNewMCtxDepth <| assertDefEqQ : {u : Level } →
{α :
let u := u ;
Q(Sort u) } →
(a b : Q(«$α» ) ) → MetaM (PLift («$a» =Q «$b» (u := u . succ ) f q( Inv.inv )
let ra ← core zα pα a
match ra with
| .positive pa => pure : {f : Type ?u.73476 → Type ?u.73475[self : Pure f {α : Type ?u.73476} → α → f α ( .positive q( inv_pos_of_pos inv_pos_of_pos $pa : ?m.72720
$ pa ))
| .nonnegative pa => pure : {f : Type ?u.73594 → Type ?u.73593[self : Pure f {α : Type ?u.73594} → α → f α ( .nonnegative q( inv_nonneg_of_nonneg inv_nonneg_of_nonneg $pa : ?m.72720
$ pa ))
| .nonzero pa => pure : {f : Type ?u.73668 → Type ?u.73667[self : Pure f {α : Type ?u.73668} → α → f α ( .nonzero q( inv_ne_zero inv_ne_zero $pa : ?m.72720
$ pa ))
| .none => pure : {f : Type ?u.73754 → Type ?u.73753[self : Pure f {α : Type ?u.73754} → α → f α .none
private theorem pow_zero_pos [ OrderedSemiring : Type ?u.77668 → Type ?u.77668 α ] [ Nontrivial α ] ( a : α ) : 0 < a ^ 0 :=
zero_lt_one . trans_le : ∀ {α : Type ?u.78590} [inst : Preorder α a b c : α }, a < b b ≤ c a < c ( pow_zero : ∀ {M : Type ?u.78794} [inst : Monoid M a : M ), a ^ 0 = 1 a ). ge : ∀ {α : Type ?u.78903} [inst : Preorder α x y : α }, x = y y ≤ x ge
private lemma zpow_zero_pos [ LinearOrderedSemifield : Type ?u.79471 → Type ?u.79471 R ] ( a : R ) : 0 < a ^ ( 0 : ℤ ) :=
zero_lt_one . trans_le : ∀ {α : Type ?u.82695} [inst : Preorder α a b c : α }, a < b b ≤ c a < c ( zpow_zero a ). ge : ∀ {α : Type ?u.82903} [inst : Preorder α x y : α }, x = y y ≤ x ge
/-- The `positivity` extension which identifies expressions of the form `a ^ (0:ℕ)`.
This extension is run in addition to the general `a ^ b` extension (they are overlapping). -/
@[ positivity ( _ : α ) ^ ( 0 :ℕ) , Pow.pow : {α : Type ?u.89497} → {β : Type ?u.89496} → [self : Pow α β α → β → α _ ( 0 :ℕ)]
def evalPowZeroNat : PositivityExt where eval { u α } _zα _pα e := do
let .app ( .app _ ( a : Q( $α) )) _ ← withReducible ( whnf e ) | throwError "not ^" : ?m.83834 ?m.83835
throwError throwError "not ^" : ?m.83834 ?m.83835
_ ← synthInstanceQ ( q( OrderedSemiring : Type ?u.83632 → Type ?u.83632OrderedSemiring OrderedSemiring $α : ?m.83360
$ α ) : Q( Type u ))
_ ← synthInstanceQ ( q( Nontrivial $ α ) : Q( Prop ))
pure : {f : Type ?u.83714 → Type ?u.83713[self : Pure f {α : Type ?u.83714} → α → f α ( .positive ( q( pow_zero_pos pow_zero_pos $a : ?m.83360
$ a ) : Expr ))
/-- The `positivity` extension which identifies expressions of the form `a ^ (0:ℤ)`. -/
@[ positivity ( _ : α ) ^ ( 0 :ℤ) , Pow.pow : {α : Type ?u.95222} → {β : Type ?u.95221} → [self : Pow α β α → β → α _ ( 0 :ℤ)]
def evalPowZeroInt : PositivityExt where eval { u α } _zα _pα e := do
let .app ( .app _ ( a : Q( $α) )) _ ← withReducible ( whnf e ) | throwError "not ^" : ?m.89915 ?m.89916
throwError throwError "not ^" : ?m.89915 ?m.89916
_ ← synthInstanceQ ( q( LinearOrderedSemifield : Type ?u.89803 → Type ?u.89803LinearOrderedSemifield LinearOrderedSemifield $α : ?m.89531
$ α ) : Q( Type u ))
pure : {f : Type ?u.89821 → Type ?u.89820[self : Pure f {α : Type ?u.89821} → α → f α ( .positive ( q( zpow_zero_pos zpow_zero_pos $a : ?m.89531
$ a ) : Expr ))
/-- The `positivity` extension which identifies expressions of the form `a ^ (b : ℕ)`,
such that `positivity` successfully recognises both `a` and `b`. -/
@[ positivity ( _ : α ) ^ ( _ : ℕ) , Pow.pow : {α : Type ?u.110938} → {β : Type ?u.110937} → [self : Pow α β α → β → α _ ( _ : ℕ)]
def evalPow : PositivityExt where eval { u α } zα pα e := do
let .app ( .app _ ( a : Q( $α) )) ( b : Q( ℕ)) ← withReducible ( whnf e ) | throwError "not ^" : ?m.100035 ?m.100036
throwError throwError "not ^" : ?m.100035 ?m.100036
let result ← catchNone do
let .true := b . isAppOfArity `` OfNat.ofNat : {α : Type u} → (x : ℕ ) → [self : OfNat α x α 3 | throwError "not a ^ n where n is a literal" : ?m.96299 ?m.96300
throwError throwError "not a ^ n where n is a literal" : ?m.96299 ?m.96300
let some n := ( b . getRevArg! 1 ). natLit? | throwError "not a ^ n where n is a literal" : ?m.95999 ?m.96000
throwError throwError "not a ^ n where n is a literal" : ?m.95999 ?m.96000
guard ( n % 2 = 0 )
let m : Q( ℕ ) := mkRawNatLit ( n / 2 )
let _a ← synthInstanceQ ( q( LinearOrderedRing : Type ?u.95876 → Type ?u.95876LinearOrderedRing LinearOrderedRing $α : ?m.95256
$ α ) : Q( Type u ))
pure : {f : Type ?u.95888 → Type ?u.95887[self : Pure f {α : Type ?u.95888} → α → f α ( .nonnegative ( q( pow_bit0_nonneg pow_bit0_nonneg $a $m : ?m.95256
$ a pow_bit0_nonneg $a $m : ?m.95256
$ m ) : Expr ))
orElse result do
let ra ← core zα pα a
let ofNonneg pa ( oα : Q( OrderedSemiring : Type ?u.96710 → Type ?u.96710OrderedSemiring OrderedSemiring $α : ?m.95256
$ α )) : MetaM ( Strictness zα pα e ) := do
have pa' : Q( by clear! «$zα» «$pα» ; exact 0 ≤ $ a ) := pa
pure : {f : Type ?u.97071 → Type ?u.97070[self : Pure f {α : Type ?u.97071} → α → f α ( .nonnegative ( q( pow_nonneg pow_nonneg $pa' $b : ?m.95256
$ pa' pow_nonneg $pa' $b : ?m.95256
$ b ) : Expr ))
let ofNonzero pa ( oα : Q( OrderedSemiring : Type ?u.97194 → Type ?u.97194OrderedSemiring OrderedSemiring $α : ?m.95256
$ α )) : MetaM ( Strictness zα pα e ) := do
have pa' : Q( by clear! «$zα» «$pα» ; exact $ a ≠ 0 ) := pa
let _a ← synthInstanceQ ( q( by clear! «$zα» «$pα» ; exact NoZeroDivisors : (M₀ : Type ?u.97440) → [inst : Mul M₀ [inst : Zero M₀ Prop NoZeroDivisors $ α ) : Q( Prop ))
pure : {f : Type ?u.97787 → Type ?u.97786[self : Pure f {α : Type ?u.97787} → α → f α ( .nonzero ( q( pow_ne_zero pow_ne_zero $b $pa' : ?m.95256
$ b pow_ne_zero $b $pa' : ?m.95256
$ pa' ) : Expr ))
match ra with
| .positive pa =>
try
let _a ← synthInstanceQ ( q( StrictOrderedSemiring : Type ?u.98116 → Type ?u.98116StrictOrderedSemiring StrictOrderedSemiring $α : ?m.95256
$ α ) : Q( Type u ))
have pa' : Q( by