Positivity extension for Finset.card

Stream: metaprogramming / tactics

[Yaël Dillies]

Would someone kindly explain me how to use Qq in positivity extensions? Every time I try to write an extension, I'm fairly confident I can adapt an existing extension, and every time I hit a different stumbling block.

[Yaël Dillies]

Here's my attempt at an extension for docs#Finset.card, which fails because I don't know how to tell Qq that e is Finset.card s, which I can't do because e is supposed to have type β2 : Type u while Finset.card s is supposed to have type ℕ : Type:

import Mathlib.Data.Fintype.Card
import Mathlib.Tactic.Positivity.Core

open Finset

open Qq Lean Meta
#check @Finset.card
@[positivity Finset.card _]
def Mathlib.Meta.Positivity.evalFinsetCard : PositivityExt where eval {u β2} zβ pβ e := do
  let ⟨_v, _l, _r⟩ ← inferTypeQ' <| (Expr.getAppArgs (← withReducible (whnf e))).get! 1
  let .app (.app _f (α : Q(Type u))) (s : Q(Finset $α)) ← withReducible (whnf e) | throwError "not `Finset.card`"

  haveI' : $e =Q Finset.card $s := ⟨⟩
  /-
  type mismatch
    card «$s»
  has type
    ℕ : Type
  but is expected to have type
    «$β2» : Type u
  -/
  let so : Option Q(Finset.Nonempty $s) ← do -- TODO: if I make a typo it doesn't complain?
    try {
      let _fi ← synthInstanceQ (q(Fintype $α) : Q(Type u))
      let _no ← synthInstanceQ (q(Nonempty $α) : Q(Prop))
      match s with
      | ~q(@univ _ $fi) => pure (some q(Finset.univ_nonempty (α := $α)))
      | _ => pure none }
    catch _e => do
      let .some fv ← findLocalDeclWithType? q(Finset.Nonempty $s) | pure none
      pure (some (.fvar fv))
  match so with
  | .some (fi : Q(Finset.Nonempty $s)) => do
    pure (.positive q(@Finset.Nonempty.card_pos.{u} $α $s $fi))
    /-
    type mismatch
      Nonempty.card_pos «$fi»
    has type
      0 < card «$s» : Prop
    but is expected to have type
      0 < «$e» : Prop
    -/
  | _ => pure .none

[Yaël Dillies]

I must say I am confounded by the fiercely displayed "intuitive" in the description of https://github.com/leanprover-community/quote4 :sad:

[Patrick Massot]

It says "the intuitiveness of modal sequent calculus". I've always interpreted that as a very fine example of Gabriel's sense of humor.

[Patrick Massot]

As far as I'm concerned, it could just as well say "the intuitiveness of $\infty$-categories".

[Yaël Dillies]

:bulb: It pays to lie

[Yaël Dillies]

import Mathlib.Data.Fintype.Card
import Mathlib.Tactic.Positivity.Core

open Finset
open Qq Lean Meta

@[positivity Finset.card _]
def Mathlib.Meta.Positivity.evalFinsetCard : PositivityExt where eval _ _ e := do
  let ⟨v, _l, _r⟩ ← inferTypeQ' <| (Expr.getAppArgs (← withReducible (whnf e))).get! 1
  let .app (.app _f (α : Q(Type v))) (s : Q(Finset $α)) ← withReducible (whnf e) | throwError "not `Finset.card`"

  let so : Option Q(Finset.Nonempty $s) ← do -- TODO: if I make a typo it doesn't complain?
    try {
      let _fi ← synthInstanceQ (q(Fintype $α) : Q(Type v))
      let _no ← synthInstanceQ (q(Nonempty $α) : Q(Prop))
      match s with
      | ~q(@univ _ $fi) => pure (some q(Finset.univ_nonempty (α := $α)))
      | _ => pure none }
    catch _e => do
      let .some fv ← findLocalDeclWithType? q(Finset.Nonempty $s) | pure none
      pure (some (.fvar fv))
  match so with
  | .some (fi : Q(Finset.Nonempty $s)) => do
    return .positive (q(@Finset.Nonempty.card_pos.{v} $α $s $fi) : Expr)
  | _ => pure .none

example {α : Type*} {s : Finset α} (hs : s.Nonempty) : 0 < s.card := by positivity
example {α : Type*} [Fintype α] [Nonempty α] : 0 < (univ : Finset α).card := by positivity

[Yaël Dillies]

This is bad, but type-ascripting with : Expr unblocks me at least.

[Thomas Murrills]

Instead of Expr, you can simply use the correct Q type: Q(0 < card $s)!

[Yaël Dillies]

:open_mouth: Where do you learn your tricks?

[Thomas Murrills]

norm_num :grinning_face_with_smiling_eyes:

[Yaël Dillies]

We, as a community, have a documentation issue :face_palm:

[Thomas Murrills]

(Just kidding, we actually lie a lot there to make the refl proofs work!) What tipped me off here was the presence of $e.

[Mario Carneiro]

you just noticed? I'm hoping that if I do enough oral teaching eventually someone will write the docs :D

[Yaël Dillies]

Oh that's certainly not news to me! I've been a big advocate of docs in the past and I've written a lot myself. But here I had no idea what repo to even look into.

[Mario Carneiro]

most examples of use of Qq are in mathlib tactics

[Yaël Dillies]

Yeah but I was hoping I could find something in the metaprogramming book, typically.

[Mario Carneiro]

I don't think it covers Qq

[Yaël Dillies]

... or the Qq readme

[Yaël Dillies]

Mario, while you are here, how do I extract the u from an expression e whose type is {ι : Type u} → {α : Type v} → [Semifield α] → Finset ι → (ι → α) → α?

[Yaël Dillies]

I tried let ⟨v, _l, _r⟩ ← inferTypeQ' <| (Expr.getAppArgs (← withReducible (whnf e))).get! 1 but it doesn't seem to work

[Mario Carneiro]

(<- whnf (<- whnf (<- inferType e)).bindingDomain!).sortLevel! maybe?

[Mario Carneiro]

it's a bit of a weird situation to be in

[Yaël Dillies]

Mario Carneiro said:

(<- whnf (<- inferType (<- whnf e).bindingDomain!)).sortLevel! maybe?

Wait sorry to be dump but what is the full line supposed to look like?

[Mario Carneiro]

let u := (<- whnf (<- whnf (<- inferType e)).bindingDomain!).sortLevel!

[Yaël Dillies]

Okay, this does not seem to work because it does not cooperate nicely with Qq. I assume this is what inferTypeQ' is about.

[Mario Carneiro]

you can coerce the types once you have all the exprs and levels you need

[Yaël Dillies]

Sorry, you will to be more precise. I'm a Lean 4 noob and I learn by seeing code.

[Mario Carneiro]

I assume you are talking about the code you posted above... but then what is this function of type {ι : Type u} → {α : Type v} → [Semifield α] → Finset ι → (ι → α) → α you are referring to?

[Mario Carneiro]

you can do this:

@[positivity Finset.card _]
def Mathlib.Meta.Positivity.evalFinsetCard : PositivityExt where eval _ _ e := do
  let .app (.app (.const _ [u]) (α : Q(Type u))) (s : Q(Finset $α)) ← withReducible (whnf e)
    | throwError "not `Finset.card`"
  let so ← do
    try
      let _fi ← synthInstanceQ (q(Fintype $α) : Q(Type u))
      let _no ← synthInstanceQ (q(Nonempty $α) : Q(Prop))
      match s with
      | ~q(@univ _ $fi) => pure (some q(Finset.univ_nonempty (α := $α)))
      | _ => pure none
    catch _e => do
      let .some fv ← findLocalDeclWithType? q(Finset.Nonempty $s) | pure none
      pure (some (.fvar fv))
  match so with
  | .some (fi : Q(Finset.Nonempty $s)) => do
    return .positive (q(@Finset.Nonempty.card_pos.{u} $α $s $fi) : Q(0 < card $s))
  | _ => pure .none

[Yaël Dillies]

Mario Carneiro said:

I assume you are talking about the code you posted above... but then what is this function of type {ι : Type u} → {α : Type v} → [Semifield α] → Finset ι → (ι → α) → α you are referring to?

Sorry, this is referring to this message where the function is basically docs#Finset.sum (except that I divide by the cardinality of the finset to get an average).

[Yaël Dillies]

Oh I see! Is this a general solution?

[Mario Carneiro]

at the beginning of one of these matches you usually know that the input is a constant applied to some stuff so you can use that to get the main universe levels

[Yaël Dillies]

because it seems

let ⟨v, _l, _r⟩ ← inferTypeQ' <| (Expr.getAppArgs (← withReducible (whnf e))).get! some_small_number

does actually work, except that I have no way other than trial and error to figure out some_small_number.

[Mario Carneiro]

some_small_number should be the arity of the constant

[Yaël Dillies]

What's a constant in that context?

[Mario Carneiro]

?

[Mario Carneiro]

.const

[Mario Carneiro]

in this case, it is Finset.sum.{u}

[Mario Carneiro]

and we use that to nab the u

[Yaël Dillies]

Yes but does correspond to a declaration in the environment, a variable in the local context... ?

[Mario Carneiro]

it's a level expression, whatever level happens to be used on this Finset.sum application found in the goal or whatever

[Yaël Dillies]

Okay so what if I have a declaration with two universe variables and I want to nab the second one?

[Mario Carneiro]

you would use a list with two elements

[Mario Carneiro]

The length of the list should match the constant's number of universes

[Mario Carneiro]

if you mouse over Finset.card you can see it has one universe argument

[Yaël Dillies]

Okay great! This was very instructive. I shall come back to complain if need arises.

[Yaël Dillies]

Here I am again with a MWE (that I've already shown to @Alex J. Best):

import Mathlib.Analysis.Normed.Group.Basic

open scoped ENNReal NNReal

namespace Mathlib.Meta.Positivity
open Lean Meta Qq Function

def lp {ι : Type*} [Fintype ι] {α : ι → Type*} [∀ i, NormedAddCommGroup (α i)] (p : ℝ≥0∞)
    (f : ∀ i, α i) : ℝ := sorry

lemma lp_nonneg {ι : Type*} [Fintype ι] {α : ι → Type*} [∀ i, NormedAddCommGroup (α i)] {p : ℝ≥0∞}
    {f : ∀ i, α i} : 0 ≤ lp p f := sorry

lemma lp_pos {ι : Type*} [Fintype ι] {α : ι → Type*} [∀ i, NormedAddCommGroup (α i)] {p : ℝ≥0∞}
    {f : ∀ i, α i} (hf : f ≠ 0) : 0 < lp p f := sorry

lemma lp_pos_of_pos {ι : Type*} [Fintype ι] {α : ι → Type*} [∀ i, NormedAddCommGroup (α i)]
    [∀ i, Preorder (α i)] {p : ℝ≥0∞} {f : ∀ i, α i} (hf : 0 < f) : 0 < lp p f := lp_pos hf.ne'

/-- The `positivity` extension which identifies expressions of the form `lp p f`. -/
@[positivity lp _ _] def evalLp : PositivityExt where eval z p e := do
  let .app (.app (.app (.app (.app (.app (.const _ [u, v]) (ι : Q(Type v))) (fi : Q(Fintype $ι)))
    (α : Q($ι → Type u))) (no : Q(∀ i, NormedAddCommGroup ($α i)))) (p : Q(ℝ≥0∞)))
      (f : Q(∀ i, $α i)) ← withReducible (whnf e)
    | throwError "not lp"
  try {
    let zα ← synthInstanceQ (q(Zero (∀ i, $α i)) : Q(Type (max u v)))
    let pα ← synthInstanceQ (q(PartialOrder (∀ i, $α i)) : Q(Type (max u v)))
    let pα' ← synthInstanceQ (q(∀ i, Preorder ($α i)) : Q(Type (max u v)))
    assumeInstancesCommute
    match ← core zα pα f with
    | .positive pf => return .positive (q(@lp_pos_of_pos $ι $fi $α $no $pα' $p $f $pf) : Expr)
    | .nonzero pf => return .positive (q(@lp_pos $ι $fi $α $no $p $f $pf) : Expr)
    | _ => return .nonnegative (q(@lp_nonneg $ι $fi $α $no $p $f) : Expr)
  } catch _ => try {
    let pf ← findLocalDeclWithType? q($f ≠ 0)
    let pf ← pf
    return .positive (← mkAppM ``lp_pos #[.fvar pf])
  } catch _ =>
    return .nonnegative (q(@lp_nonneg $ι $fi $α $no $p $f) : Expr)

variable {ι : Type*} [Fintype ι] {α : ι → Type*} [∀ i, NormedAddCommGroup (α i)] {w : ι → ℝ≥0}
  {f : ∀ i, α i}

-- All of these are expected to work
example {p : ℝ≥0∞} : 0 ≤ lp p f := by positivity
example {p : ℝ≥0∞} (hf : f ≠ 0) : 0 < lp p f := by positivity
example {p : ℝ≥0∞} {f : ι → ℝ} (hf : 0 < f) : 0 < lp p f := by positivity
example {p : ℝ≥0} : 0 ≤ ‖f‖_[p, w] := by positivity

[Yaël Dillies]

I don't know how to tell Qq that the PartialOrder (∀ i, α i) and ∀ i, Preorder (α i) instances result in the same Preorder (∀ i, α i) instance. I would have hoped assumeInstancesCommute does this, but maybe that only works for instances existing in the local context, not derived ones?

[Eric Wieser]

Not answering the question directly, but here's how to avoid all the app stuff:

/-- The `positivity` extension which identifies expressions of the form `lp p f`. -/
@[positivity lp _ _] def evalLp : PositivityExt where eval {u} α z p e := do
  if let 0 := u then do -- lean4#3060 means we can't use `|` here
    let ~q(ℝ) := α | throwError "not lp"
    let ~q(@lp $ι $instι $αi $instnorm $p $f) := e | throwError "not lp"
    sorry
  else
    throwError "not lp"

[Eric Wieser]

Here's an error-free version:

/-- The `positivity` extension which identifies expressions of the form `lp p f`. -/
@[positivity lp _ _] def evalLp : PositivityExt where eval {u} α _z _p e := do
  if let 0 := u then do -- lean4#3060 means we can't combine this with the match below
    match α, e with
    | ~q(ℝ), ~q(@lp $ι $instι $α $instnorm $p $f) =>
      try {
        let _pα ← synthInstanceQ (q(∀ i, PartialOrder ($α i)) : Q(Type (max u_1 u_2)))
        assumeInstancesCommute
        match ← core q(inferInstance) q(inferInstance) f with
        | .positive pf => return .positive q(lp_pos_of_pos $pf)
        | .nonzero pf => return .positive q(lp_pos $pf)
        | _ => return .nonnegative (q(lp_nonneg))
      } catch _ =>
        assumeInstancesCommute
        if let some pf ← findLocalDeclWithType? q($f ≠ 0) then
          let pf : Q($f ≠ 0) := .fvar pf
          return .positive q(lp_pos $pf)
        else
          return .nonnegative q(lp_nonneg)
    | _ => throwError "not lp"
  else
    throwError "not lp"

[Eric Wieser]

Note the trick here: only use synthInstanceQ for when you need new instances that require a global isntance lookup; if the instance you want is a consequence of a local instance, then use q(inferInstance) instead

[Yaël Dillies]

And now what if I want to pattern-match on whether my type is a pi-type?

import Mathlib.Algebra.Ring.Defs
import Mathlib.Data.Fintype.Basic
import Mathlib.Tactic.Positivity.Core

def conv {α β : Type*} [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β]
    (f g : α → β) : α → β := sorry

namespace Mathlib.Meta.Positivity
open Lean Meta Qq

@[positivity conv _ _] def evalConv : PositivityExt where eval {u α} zα pα e := do
  match α, e with
  /-
  stuck at solving universe constraint
    imax ?u.573 ?u.575 =?= u+1
  while trying to unify
    Sort (imax ?u.573 ?u.575) : Type (imax ?u.573 ?u.575)
  with
    Type u : Type (u + 1)
  -/
  | ~q($β → $γ), ~q(@conv _ _ $instβfin $instβdec $instβgroup $instγring) =>
      sorry
  | _ => throwError "not conv"

[Eric Wieser]

Does this work?

abbrev TypeFunction (α β : Type*) := α → β

@[positivity conv _ _] def evalConv : PositivityExt where eval {u α} zα pα e := do
  let u1 ← mkFreshLevelMVar
  let u2 ← mkFreshLevelMVar
  let _ : u =QL max u1 u2 := ⟨⟩
  match α, e with
  | ~q(TypeFunction.{u2,u1} $α $β), ~q(@conv _ _ $instβfin $instβdec $instβgroup $instγring $f $g) =>
      sorry
  | _ => throwError "not conv"

[Eric Wieser]

I think this raises that matching on universes is a bad idea, because max 1 1 is not equal to 1

[Yaël Dillies]

Here's a non-working minimal example based off your idea:

import Mathlib.Algebra.Ring.Defs
import Mathlib.Data.Fintype.Basic
import Mathlib.Tactic.Positivity.Core

section Defs
variable {α β : Type*}

def conv [Fintype α] [DecidableEq α] [AddCommGroup α] [CommSemiring β] (f g : α → β) : α → β :=
  sorry

section OrderedCommSemiring
variable [Fintype α] [DecidableEq α] [AddCommGroup α] [OrderedCommSemiring β] {f g : α → β}

lemma conv_nonneg (hf : 0 ≤ f) (hg : 0 ≤ g) : 0 ≤ conv f g := sorry
lemma conv_nonneg_of_pos_of_nonneg (hf : 0 < f) (hg : 0 ≤ g) : 0 ≤ conv f g := conv_nonneg hf.le hg
lemma conv_nonneg_of_nonneg_of_pos (hf : 0 ≤ f) (hg : 0 < g) : 0 ≤ conv f g := conv_nonneg hf hg.le

end OrderedCommSemiring

section StrictOrderedCommSemiring
variable [Fintype α] [DecidableEq α] [AddCommGroup α] [StrictOrderedCommSemiring β] {f g : α → β}

lemma conv_pos (hf : 0 < f) (hg : 0 < g) : 0 < conv f g := sorry

end StrictOrderedCommSemiring
end Defs

private abbrev TypeFunction (α β : Type*) := α → β

namespace Mathlib.Meta.Positivity
open Lean Meta Qq

@[positivity conv _ _] def evalConv : PositivityExt where eval {u π} zπ pπ e := do
  let u1 ← mkFreshLevelMVar
  let u2 ← mkFreshLevelMVar
  let _ : u =QL max u1 u2 := ⟨⟩
  match π, e with
  | ~q(TypeFunction.{u2, u1} $α $β),
    ~q(@conv _ _ $instαfin $instαdec $instαgrp $instβring $f $g) =>
    let instβstrictring ← synthInstanceQ (q(StrictOrderedCommSemiring $β) : Q(Type u2))
    let instβordring : Q(OrderedCommSemiring $β) := q(inferInstance)
    assumeInstancesCommute
    let ra ← core zπ pπ f
    let rb ← core zπ pπ g
    match ra, rb with -- unknown free variable '_uniq.3469'
    | .positive pa, .positive pb =>
       return .positive q(@conv_pos $α $β $instαfin $instαdec $instαgrp $instβstrictring $f $g $pa $pb)
    -- | .positive pa, .nonnegative pb => return .nonnegative q(conv_nonneg_of_pos_of_nonneg $pa $pb)
    -- | .nonnegative pa, .positive pb => return .nonnegative q(conv_nonneg_of_nonneg_of_pos $pa $pb)
    -- | .nonnegative pa, .nonnegative pb => return .nonnegative q(conv_nonneg $pa $pb)
    | _, _ => pure .none
  | _ => throwError "not conv"

end Mathlib.Meta.Positivity

section Examples
variable {α β : Type*}


section OrderedCommSemiring
variable [Fintype α] [DecidableEq α] [AddCommGroup α] [OrderedCommSemiring β] {f g : α → β}

example (hf : 0 ≤ f) (hg : 0 ≤ g) : 0 ≤ conv f g := by positivity
example (hf : 0 < f) (hg : 0 ≤ g) : 0 ≤ conv f g := by positivity
example (hf : 0 ≤ f) (hg : 0 < g) : 0 ≤ conv f g := by positivity

end OrderedCommSemiring

section StrictOrderedCommSemiring
variable [Fintype α] [DecidableEq α] [AddCommGroup α] [StrictOrderedCommSemiring β] {f g : α → β}

example (hf : 0 < f) (hg : 0 < g) : 0 < conv f g := by positivity

end StrictOrderedCommSemiring
end Examples

[Yaël Dillies]

If you uncomment the three branches, you instead get a timeout.

[Eric Wieser]

let zπ : Q(Zero ($α → $β)) := zπ seems to help