positivity on nat and fin

Stream: general

[Yakov Pechersky]

Which of these are in the feature scope of positivity? And are PRs welcome to make these work?

import tactic.positivity

variables {n : ℕ} (a b : fin (n + 2))

example : 0 ≤ 2 := by positivity -- works
example : 0 ≤ n := by positivity
example : 0 ≤ (n + 2) := by positivity
example : 0 < (n + 2) := by positivity

example : 0 ≤ a := by positivity
example : 0 ≤ (n : fin (n + 2)) := by positivity
example : 0 ≤ (n + 2) - a := by positivity

example : 0 ≤ (2 : ℤ) := by positivity -- works
example : 0 ≤ (n : ℤ) := by positivity
example : 0 ≤ (a : ℤ) := by positivity
example : 0 ≤ (n + 2 : ℤ) := by positivity
example : 0 ≤ ((n + 2 : ℕ) : ℤ) := by positivity
example : 0 ≤ ((n + 2 : ℕ) : ℤ) - a := by positivity
example : 0 < ((n + 2 : ℕ) : ℤ) - a := by positivity
example : 0 ≤ -(a : ℤ) + (n + 2) := by positivity
example : 0 ≤ -(a : ℤ) + ((n + 2) : ℕ) := by positivity
example : 0 ≤ (a : ℤ) - b + ((n + 2) : ℕ) := by positivity -- my actual goal

example {α : Type*} [subsingleton α] [has_le α] [has_zero α] (u : α) : 0 ≤ u := by positivity

[Mario Carneiro]

the 0 <= n is in scope, and so the others in the same block would also work. Same for 0 <= a, but I think 0 ≤ (n + 2) - a is out of scope (you should provide it as a hypothesis)

[Mario Carneiro]

the ones involving cast to Z should also work

[Mario Carneiro]

So I would say that these are the only ones that you should not expect to work:

example : 0 ≤ (n + 2) - a := by positivity
example : 0 ≤ ((n + 2 : ℕ) : ℤ) - a := by positivity
example : 0 < ((n + 2 : ℕ) : ℤ) - a := by positivity
example : 0 ≤ -(a : ℤ) + (n + 2) := by positivity
example : 0 ≤ -(a : ℤ) + ((n + 2) : ℕ) := by positivity
example : 0 ≤ (a : ℤ) - b + ((n + 2) : ℕ) := by positivity -- my actual goal

The last one is really weird

[Mario Carneiro]

Specifically, @Heather Macbeth described this tactic to me as proving things positive/nonnegative because it is "structurally obvious" from the term. That means that terms involving subtraction are generally out; you should use linarith for that

[Mario Carneiro]

example : 0 ≤ (a : ℤ) - b + ((n + 2) : ℕ) :=
by have := b.2; simp at *; linarith [@nat.cast_nonneg ℤ _ a]

[Yakov Pechersky]

I can never get linarith to work:

import algebra.monoid_algebra.basic
import data.int.succ_pred

variables (Z : Type*) (b : ℕ)
  [nonempty Z]
  [conditionally_complete_linear_order Z]
  [no_max_order Z]
  [no_min_order Z]
  [succ_order Z]
  [pred_order Z]
  [is_succ_archimedean Z]

def formal_series : Type* := Z → fin (b + 1)

variables {Z} {b}

example
  (z : Z)
  [hb : fact (b.succ > 0)]
  (f g : formal_series Z b.succ)
  (h : f z < g z)
  (this : ↑(g z) < b.succ + 1) :
  0 ≤ (((f z) : ℕ) : ℤ) - ((g z) : ℕ) + (b + 1 + 1) :=
begin
  have : ((g z : ℕ) : ℤ) < b + 1 + 1 := sorry,
  simp at *,
  linarith, -- please, linarith!
end