Taming positivity

Stream: metaprogramming / tactics

[Yaël Dillies]

I am faced with awful goals in #15440 that are in the scope of positivity. For it to work there, it needs to know that 0 ≤ ((n : ℕ) : α) so I tried writing an extension and failed miserably.

[Yaël Dillies]

import tactic.positivity

namespace tactic
variables {α : Type*}

open positivity

private lemma nat_cast_nonneg [ordered_semiring α] (n : ℕ) : 0 ≤ (n : α) := n.cast_nonneg

private lemma nat_cast_pos [ordered_semiring α] [nontrivial α] {n : ℕ} (hn : 0 < n) : 0 < (n : α) :=
nat.cast_pos.2 hn

private lemma int_cast_nonneg [ordered_ring α] {n : ℤ} (hn : 0 ≤ n) : 0 ≤ (n : α) :=
by { rw ←int.cast_zero, exact int.cast_mono hn }

private lemma int_cast_pos [ordered_ring α] [nontrivial α] {n : ℤ} : 0 < n → 0 < (n : α) :=
int.cast_pos.2

private lemma rat_cast_nonneg [linear_ordered_field α] {q : ℚ} : 0 ≤ q → 0 ≤ (q : α) :=
rat.cast_nonneg.2

private lemma rat_cast_pos [linear_ordered_field α] {q : ℚ} : 0 < q → 0 < (q : α) := rat.cast_pos.2

/-- Extension for the `positivity` tactic: cast of a natural is nonnegative. -/
@[positivity]
meta def positivity_coe : expr → tactic strictness
| `(lift_t %%a) := do
  typ_a ← infer_type a,
  strictness_a ← core a,
  match typ_a, strictness_a with
  | `(ℕ), positive p := positive <$> mk_app ``nat_cast_pos [p]
  | `(ℕ), nonnegative p := nonnegative <$> mk_app ``nat_cast_nonneg [a]
  | `(ℤ), positive p := positive <$> mk_app ``int_cast_pos [p]
  | `(ℤ), nonnegative p := nonnegative <$> mk_app ``int_cast_nonneg [a]
  | `(ℚ), positive p := positive <$> mk_app ``rat_cast_pos [p]
  | `(ℚ), nonnegative p := nonnegative <$> mk_app ``rat_cast_nonneg [a]
  | _, _ := failed
  end
| _ := failed

end tactic

example {α : Type*} [ordered_semiring α] (n : ℕ) : 0 ≤ (n : α) := by positivity -- fails

[Yaël Dillies]

What did I do wrong?

[Yaël Dillies]

cc @Heather Macbeth, @Mario Carneiro

[Mario Carneiro]

I don't think the function is called lift_t

[Yaël Dillies]

coe doesn't work either at least.

[Mario Carneiro]

it definitely needs to be coe, if you add a trace you can see your function doesn't even get called otherwise

[Yaël Dillies]

How do I add a trace?

[Mario Carneiro]

trace a, in the do block

[Mario Carneiro]

the other issue is that you are failing if core a fails, which means that the nat_cast_nonneg case doesn't work

[Yaël Dillies]

Aaah, I know. core a fails.

[Yaël Dillies]

So I should another extension that proves that all naturals are nonnegative?

[Mario Carneiro]

You need to wrap it with try_core to handle the error

@[positivity]
meta def positivity_coe : expr → tactic strictness
| `(coe %%a) := do
  typ_a ← infer_type a,
  strictness_a ← try_core (core a),
  match typ_a, strictness_a with
  | `(ℕ), some (positive p) := positive <$> mk_app ``nat_cast_pos [p]
  | `(ℕ), _ := nonnegative <$> mk_app ``nat_cast_nonneg [a]
  | `(ℤ), some (positive p) := positive <$> mk_app ``int_cast_pos [p]
  | `(ℤ), some (nonnegative p) := nonnegative <$> mk_app ``int_cast_nonneg [a]
  | `(ℚ), some (positive p) := positive <$> mk_app ``rat_cast_pos [p]
  | `(ℚ), some (nonnegative p) := nonnegative <$> mk_app ``rat_cast_nonneg [a]
  | _, _ := failed
  end
| _ := failed

end tactic

example {α : Type*} [ordered_semiring α] (n : ℕ) : 0 ≤ (n : α) := by positivity -- ok

[Yaël Dillies]

Also, is this design alright or should I write a different extension for each coercion? For example, this doesn't handle nnreal.

[Mario Carneiro]

checking the types is not very robust. For instance this will fail if you are using the nat -> int coercion

[Mario Carneiro]

you should pattern match on the coe instance itself

[Mario Carneiro]

like (@coe %%typ_a _ %%inst %%a) and then match on inst

[Mario Carneiro]

it's fine that this doesn't do all coes; there is no requirement that this is the only coe extension

[Yaël Dillies]

Are you sure? That's part of what Gabriel is changing.

[Mario Carneiro]

not sure what you are referring to

[Yaël Dillies]

docs#add_comm_group_with_one

[Yaël Dillies]

In particular, in docs#int.comm_ring you can see that the coercion is implemented using docs#int.of_nat.

[Yaël Dillies]

@Mario Carneiro, what am I doing wrong now?

import tactic.positivity

namespace tactic
variables {α : Type*}

open positivity

private lemma nonneg_of_canon {α : Type*} [canonically_ordered_add_monoid α] (a : α) : 0 ≤ a :=
zero_le _

/-- Extension for the `positivity` tactic: Any elemeny of a canonically ordered additive monoid is
nonnegative. -/
@[positivity]
meta def positivity_canon : expr → tactic strictness
| `(%%a) := nonnegative <$> mk_app ``nonneg_of_canon [a]

private lemma nat_cast_nonneg [ordered_semiring α] (n : ℕ) : 0 ≤ (n : α) := n.cast_nonneg

private lemma nat_cast_pos [ordered_semiring α] [nontrivial α] {n : ℕ} (hn : 0 < n) : 0 < (n : α) :=
nat.cast_pos.2 hn

private lemma int_coe_nat_nonneg (n : ℕ) : 0 ≤ (n : ℤ) := n.cast_nonneg
private lemma int_coe_nat_pos {n : ℕ} : 0 < n → 0 < (n : ℤ) := nat.cast_pos.2

private lemma int_cast_nonneg [ordered_ring α] {n : ℤ} (hn : 0 ≤ n) : 0 ≤ (n : α) :=
by { rw ←int.cast_zero, exact int.cast_mono hn }

private lemma int_cast_pos [ordered_ring α] [nontrivial α] {n : ℤ} : 0 < n → 0 < (n : α) :=
int.cast_pos.2

private lemma rat_cast_nonneg [linear_ordered_field α] {q : ℚ} : 0 ≤ q → 0 ≤ (q : α) :=
rat.cast_nonneg.2

private lemma rat_cast_pos [linear_ordered_field α] {q : ℚ} : 0 < q → 0 < (q : α) := rat.cast_pos.2

/-- Extension for the `positivity` tactic: casts from `ℕ`, `ℤ`, `ℚ`. -/
@[positivity]
meta def positivity_coe : expr → tactic strictness
| `(@coe %%typ_a _ %%inst %%a) := do
  strictness_a ← core a,
  trace a,
  match inst, strictness_a with
  | `(@coe_to_lift _ _ nat.cast_coe), positive p := positive <$> mk_app ``nat_cast_pos [p]
  | `(@coe_to_lift _ _ nat.cast_coe), nonnegative p := nonnegative <$> mk_app ``nat_cast_nonneg [a]
  | `(@coe_to_lift _ _ $ @coe_base _ _ int.has_coe), positive p := positive <$> mk_app ``int_coe_nat_pos [p]
  | `(@coe_to_lift _ _ $ @coe_base _ _ int.has_coe), nonnegative p := nonnegative <$> mk_app ``int_coe_nat_nonneg [a]
  | `(@coe_to_lift _ _ int.cast_coe), positive p := positive <$> mk_app ``int_cast_pos [p]
  | `(@coe_to_lift _ _ int.cast_coe), nonnegative p := nonnegative <$> mk_app ``int_cast_nonneg [p]
  | `(@coe_to_lift _ _ rat.cast_coe), positive p := positive <$> mk_app ``rat_cast_pos [p]
  | `(@coe_to_lift _ _ rat.cast_coe), nonnegative p := nonnegative <$> mk_app ``rat_cast_nonneg [p]
  | _, _ := failed -- TODO: Handle `coe : nnreal → real`
  end
| _ := failed

end tactic

-- work
example (n : ℕ) : 0 ≤ (n : ℤ) := by show_term { by positivity }
example (n : ℤ) : 0 ≤ n ^ 2 := by show_term { by positivity }
example {α : Type*} [ordered_semiring α] (n : ℕ) : 0 ≤ (n : α) := by show_term { by positivity }

-- fail
example {α : Type*} [ordered_ring α] (n : ℤ) : 0 ≤ ((n ^ 2 : ℤ) : α) :=
by show_term { by positivity }
example {α : Type*} [linear_ordered_field α] (n : ℚ) : 0 ≤ ((n ^ 2 : ℚ) : α) :=
by show_term { by positivity }

/-
equation compiler failed, maximum number of steps (2048) exceeded (possible solution: use
'set_option eqn_compiler.max_steps <new-threshold>') (use
'set_option trace.eqn_compiler.elim_match true' for additional details)
-/

[Yaël Dillies]

Ah, it just looks like I was matching on too much at once.

[Yaël Dillies]

#16141

[Eric Wieser]

pattern matching on the coercion (edit: instance) feels like a bad idea; you don't want a syntactic math, you want one that unifies

[Yaël Dillies]

Mario was the one suggesting this. What alternative do you offer? I was originally pattern-matching on the type, but that fails to distinguish docs#nat.cast_coe from docs#int.has_coe.

[Eric Wieser]

What do you mean by pattern matching on the type?

[Yaël Dillies]

Matching on the expr of the type of the variable that's being cast.

[Eric Wieser]

You want to pattern match on the type, and not the instance. I suspect if you leave the instance as a _ then lean uses typeclass inference and the end result is actually that you do end up matching on the instance

[Yaël Dillies]

Yeah, so that fails to distinguish coe : ℕ → ℤ from coe : ℕ → ℚ.

[Eric Wieser]

Does matching (@coe %%src %%dest %%inst %%a), then matching on src, dest pairs not work?

[Yaël Dillies]

Sure that's an option.

[Eric Wieser]

It's the right option, because it doesn't try to compare typeclass instances syntactically

[Eric Wieser]

Matching (@coe ℕ ℚ %%inst %%a) etc at the top level should work too

[Yaël Dillies]

Here I am again, but this time in Lean 4. I have a binary operation op : (ι → R) → (ι → R) → ι → R which is positive/nonnegative/nonzero on positive/nonnegative/nonzero inputs. I want to encode this in a positivity extension because I use those facts > 50 times combined with other facts in LeanAPAP.

[Yaël Dillies]

The problem now is that ι → R is neither a free variable nor a concrete type. I somehow need to pattern-match on the α in docs#Mathlib.Meta.Positivity.PositivityExt.eval to get ι and R. But it seems that Qq doesn't support pattern-matching on types (cc @Gabriel Ebner), so am I stuck?

[Yaël Dillies]

MWE:

import Mathlib.Tactic.Positivity

variable {ι R : Type*} [Zero R] [Preorder R] {f g : ι → R}

def op : (ι → R) → (ι → R) → ι → R := sorry

lemma op_pos (hf : 0 < f) (hg : 0 < g) : 0 < op f g := sorry
lemma op_nonneg (hf : 0 ≤ f) (hg : 0 ≤ g) : 0 ≤ op f g := sorry
lemma op_ne_zero (hf : f ≠ 0) (hg : g ≠ 0) : op f g ≠ 0 := sorry

namespace Mathlib.Meta.Positivity
open Lean Meta Qq Function

/-- The `positivity` extension which identifies expressions of the form `op f g`,
such that `positivity` successfully recognises both `f` and `g`. -/
@[positivity op _ _] def evalOp : PositivityExt where eval {u α} zα pα e := do
  -- What do I do here? I can't pattern-match on `α`, which I know is of the form `ι → R`.
  sorry

end Mathlib.Meta.Positivity

[Eric Wieser]

Right, I guess you want one of let ~q($ι → $R) := α | throwError "oh no" or let ~q(@op $ι $R $f $g) := e | throwError "oh no", both of which seem illegal

[Yaël Dillies]

As an emergency measure, I'm currently going with

section
variable {α : Type*} [Zero α] [PartialOrder α] {a b c : α}

lemma dummy_pos_pos (ha : 0 < a) (hb : 0 < b) : 0 < c := sorry
lemma dummy_pos_nng (ha : 0 < a) (hb : 0 ≤ b) : 0 ≤ c := sorry
lemma dummy_nng_pos (ha : 0 ≤ a) (hb : 0 < b) : 0 ≤ c := sorry
lemma dummy_nng_nng (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ c := sorry
lemma dummy_pos_nzr (ha : 0 < a) (hb : b ≠ 0) : c ≠ 0 := sorry
lemma dummy_nzr_pos (ha : a ≠ 0) (hb : 0 < b) : c ≠ 0 := sorry
lemma dummy_nzr_nzr (ha : a ≠ 0) (hb : b ≠ 0) : c ≠ 0 := sorry

end

-- TODO: Fix :(
/-- The `positivity` extension which identifies expressions of the form `op f g`,
such that `positivity` successfully recognises both `f` and `g`. -/
@[positivity op _ _] def evalConv : PositivityExt where eval {u α} zα pα e := do
  let .app (.app (_f : Q($α → $α → $α)) (a : Q($α))) (b : Q($α)) ← withReducible (whnf e)
    | throwError "not op"
  let ra ← core zα pα a; let rb ← core zα pα b
  match ra, rb with
  | .positive pa, .positive pb => return .positive q(dummy_pos_pos $pa $pb)
  | .positive pa, .nonnegative pb => return .nonnegative q(dummy_pos_nng $pa $pb)
  | .nonnegative pa, .positive pb => return .nonnegative q(dummy_nng_pos $pa $pb)
  | .nonnegative pa, .nonnegative pb => return .nonnegative q(dummy_nng_nng $pa $pb)
  | .positive pa, .nonzero pb => return .nonzero q(dummy_pos_nzr $pa $pb)
  | .nonzero pa, .positive pb => return .nonzero q(dummy_nzr_pos $pa $pb)
  | .nonzero pa, .nonzero pb => return .nonzero q(dummy_nzr_nzr $pa $pb)
  | _, _ => pure .none

[Yaël Dillies]

That avoids

• breaking existing proofs
• accidentally making the proofs think they don't need some positivity assumption

[Yaël Dillies]

Is there any hope of porting docs3#tactic.positivity_smul? I'm not sure how I can access the type that's acting on the other one...

[Gabriel Ebner]

But it seems that Qq doesn't support pattern-matching on types

You should be able to pattern-match on the type separately. Something like:

match α with
| ~q($ι → $R) =>
  -- ^^ This adds `$α =Q $ι → $R` to the context.
  match  e with ...

[Eric Wieser]

I think I tried that with let above and it didn't work

[Eric Wieser]

Maybe because the universes need to be matched first?