iInf_pi_sum (was: Failure of pattern matching)

Stream: new members

[Igor Khavkine]

Could somebody please shed light on why pattern matching fails in the following example? The sorry'd identity says that the many-indexed inf over a sum of independently indexed functions is the sum of the single-indexed infs of the individual functions. Once defined, the failure comes when trying to match it to a simple concrete example.

import Mathlib

open BigOperators ENNReal

theorem iInf_pi_sum {ι α : Type*} {κ : ι → Type*}
    [Fintype ι] [CompleteLattice α] [OrderedAddCommMonoid α]
    (f : (i : ι) → (κ i) → α) :
    ⨅ k : (i : ι) → (κ i), ∑ i : ι, f i (k i) = ∑ i : ι, ⨅ k : (κ i), f i k := by
  sorry

example (n : ℕ) : ⨅ k : Fin n → ℕ, ∑ i : Fin n, (1 / (k i) : ℝ≥0∞)
    = ∑ i : Fin n, ⨅ ki : ℕ, (1 / ki : ℝ≥0∞) := by
  -- fails to unify with goal
  --apply iInf_pi_sum _
  -- fails to unify with goal
  --apply @iInf_pi_sum (Fin n) ℝ≥0∞ (fun _ => ℕ) _ _ _ _
  -- this works
  --apply @iInf_pi_sum (Fin n) ℝ≥0∞ (fun _ => ℕ) _ _ _ (fun i ki => 1 / ki)
  -- this also works
  apply @iInf_pi_sum _ _ _ _ _ _ (fun i (ki : ℕ) => (1 / ki : ℝ≥0∞))

In practice, I expect that the most tedious part of the matching would be typing in the functions that are being summed over, but that's the only way it works now. Is there any approach that would make the matching succeed automatically?

[Alex J. Best]

  apply iInf_pi_sum (fun i (ki : ℕ) => (1 / ki : ℝ≥0∞))

also works btw, lean just needs help to infer the function f here

[Igor Khavkine]

There is a further rabbit hole when one tries to prove the general identity. I suspect that it could be done using docs#Finset.induction_on, based on the following pattern.

theorem iInf₂_add /-{α : Type*}-/ {κ : Type*}
    /-[CompleteLattice α] [OrderedAddCommMonoid α]-/
    (f₁ : κ → ℝ≥0∞ /-α-/) (f₂ : κ → ℝ≥0∞ /-α-/) :
    ⨅ k₁ : κ, ⨅ k₂ : κ, f₁ k₁ + f₂ k₂ = (⨅ k₁ : κ, f₁ k₁) + (⨅ k₂ : κ, f₂ k₂) := by
  simp_rw [← ENNReal.add_iInf]
  rw [← ENNReal.iInf_add]

However, right now I can't even prove that when generalizing from ENNReal in the way that I commented out. It seems that the appropriate general add_iInf and iInf_add are not defined. Generalizing a copy paste of the proof from ENNReal fails with a mysterious typeclass resolution error.

-- typeclass resolution failure on α!
theorem iInf_add' {ι : Sort*} {α : Type*} {a : α} {f : ι → α}
    [OrderedAddCommMonoid α] [CompleteLattice α] : iInf f + a = ⨅ i, f i + a :=
  le_antisymm (le_iInf fun _ => add_le_add (iInf_le _ _) <| le_rfl)
    (tsub_le_iff_right.1 <| le_iInf fun _ => tsub_le_iff_right.2 <| iInf_le _ _)

Any idea of what's missing here?

[Yaël Dillies]

[CompleteLattice α] [OrderedAddCommMonoid α] declares two (a priori unrelated) orders on α

[Igor Khavkine]

Alex J. Best said:

  apply iInf_pi_sum (fun i (ki : ℕ) => (1 / ki : ℝ≥0∞))

also works btw, lean just needs help to infer the function f here

Of course, thanks. But matching the function is obviously the hard part also for the human. It could be quite an involved expression to type out (or copy from the Infoview). Any way here to make the computer do the hard work?

[Yaël Dillies]

Theorems of this form are usually pretty hard to prove.

[Igor Khavkine]

Yaël Dillies said:

[CompleteLattice α] [OrderedAddCommMonoid α] declares two (a priori unrelated) orders on α

Aha, I see. But without the CompleteLattice property, the iInfs don't make sense. Is there a way to ask for the order from OrderedAddCommMonoid to be complete?

[Yaël Dillies]

That's where things start getting hard. There are many different ways algebraic operations can interact with the order, so I can't give you a one size fits all answer.

[Igor Khavkine]

I guess the main use case is α = ENNReal where it can be made to work. But it would be nice if the proof worked also more generally, say in the presence of extra parameters like α = X -> ENNReal.

[Yaël Dillies]

I understand that, but it's pretty hard to axiomatise

[Yaël Dillies]

Basically, the proof needs that one-sided addition is a map preserving the infimum. I don't think we have a way to state that in mathlib right now.

[Igor Khavkine]

OK, I understand. Thanks.

[Igor Khavkine]

Anyway, my main question was about the pattern matching failure in the iInf_pi_sum example. Any way to figure out the point of failure and supply extra hints to make it succeed that doesn't involve manually supplying the function f?

[Igor Khavkine]

Aha! Here's something that works. Specializing to ENNReal and exchanging the lhs and rhs of the identity gives a successful match.

theorem iInf_pi_sum {ι /-α-/ : Type*} {κ : ι → Type*}
    [Fintype ι] /-[CompleteLattice α] [OrderedAddCommMonoid α]-/
    (f : (i : ι) → (κ i) → ℝ≥0∞ /-α-/) :
    ∑ i : ι, ⨅ ki : (κ i), f i ki = ⨅ k : (i : ι) → (κ i), ∑ i : ι, f i (k i)
    := by
  sorry

example (n : ℕ) :
    ∑ i : Fin n, ⨅ ki : ℕ, (1 / ki : ℝ≥0∞) = ⨅ k : Fin n → ℕ, ∑ i : Fin n, (1 / (k i) : ℝ≥0∞)
    := by
  apply iInf_pi_sum _

[Igor Khavkine]

I guess the matching is done from right to left and Lean is confused by the double dependence of f i (k i) on i. It feels like there should be a way to hint Lean to make the match succeed in the other direction as well, which is obviously the important direction in practice (for rw or simp). A case for some metacode maybe? Something I know next to nothing about at the moment, unfortunately.

[Mario Carneiro]

rw [← iInf_pi_sum] works too

[Mario Carneiro]

This is called a higher order unification problem, and higher order unification is in general undecidable. The restrictions that lean has here were added deliberately, because they used to not exist (in lean 2) and this lead to unpredictable timeouts and difficult to understand behavior

[Igor Khavkine]

OK, thanks for the explanation. I understand why it doesn't work out of the box. Still the higher unification problem here is very specific (to match f i (k i), first isolate any occurrence of k, make sure each one occurs in the form k i, replace the combination by a dummy ki, then match against f i ki). And this is a pretty common pattern in mathematics.

I hope someone takes up the challenge to make something like rw [iInf_pi_sum (special_way_to_extract_f)] to work on expressions that involve the complicated side of the identity. :pray:

[Igor Khavkine]

For anyone who's curious, I've managed to prove the version of iInf_pi_sum that I wanted.

import Mathlib.Order.CompleteLattice
import Mathlib.Algebra.Order.Sub.Prod
import Mathlib.Data.Fintype.BigOperators

/-- Pass a multi-indexed ⨅ through a ∑, to get a ∑ of single-indexed ⨅s. -/
theorem iInf_pi_sum {ι α : Type*} [hι : Fintype ι] {κ : ι → Type*}
    [CompleteLattice α]
    [AddCommMonoid α]
    [CovariantClass α α (· + ·) (· ≤ ·)]
    [CovariantClass α α (Function.swap (· + ·)) (· ≤ ·)]
    [Sub α] [OrderedSub α]
    (f : (i : ι) → (κ i) → α) :
    ⨅ k : (i : ι) → (κ i), ∑ i : ι, f i (k i) = ∑ i : ι, ⨅ ki : (κ i), f i ki
    := sorry

The only interaction between + and ≤ that was needed is handled by CovariantClass. I modeled this solution on how add_le_add does it.

[Igor Khavkine]

Would this belong somewhere in Mathlib?

[Igor Khavkine]

Here's the full code with some intermediate lemmas of their own interest.

import Mathlib.Order.CompleteLattice
import Mathlib.Algebra.Order.Sub.Prod
import Mathlib.Data.Fintype.BigOperators

import Mathlib.Data.Real.ENNReal

open Classical BigOperators

-- generalized replacement for ENNReal.iInf_add
theorem iInf_add {ι : Sort*} {α : Type*} {a : α} {f : ι → α}
    [CompleteLattice α]
    [Add α]
    [CovariantClass α α (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1]
    [CovariantClass α α (Function.swap fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1]
    [Sub α] [OrderedSub α] :
    iInf f + a = ⨅ i, f i + a := by
  apply and_self_iff.mp _; constructor -- two proofs: one compact, one human readable
  · exact le_antisymm (le_iInf fun _ => add_le_add (iInf_le _ _) <| le_rfl)
      (tsub_le_iff_right.1 <| le_iInf fun _ => tsub_le_iff_right.2 <| iInf_le _ _)
  · apply le_antisymm _ _
    · { calc
        iInf f + a ≤ ⨅ i, f i + a := by apply le_iInf _; intro j; { calc
        iInf f + a ≤      f j + a := by apply add_le_add _ le_rfl; { calc
        iInf f     ≤      f j     := iInf_le _ j } } }
    · { calc
        (⨅ i, f i + a)     ≤ iInf f   + a := by rw [← tsub_le_iff_right]; exact by { calc
        (⨅ i, f i + a) - a ≤ iInf f       := by apply le_iInf _; intro j; { calc
        (⨅ i, f i + a) - a ≤      f j     := by rw [tsub_le_iff_right]; { calc
        ⨅ i, (f i + a)     ≤      f j + a := iInf_le _ j } } } }

-- generalized replacement for ENNReal.add_iInf
theorem add_iInf {ι : Sort*} {α : Type*} {a : α} {f : ι → α}
    [CompleteLattice α]
    [AddCommMagma α]
    [CovariantClass α α (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1]
    [CovariantClass α α (Function.swap fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1]
    [Sub α] [OrderedSub α] :
    a + iInf f = ⨅ i, a + f i := by
  rw [add_comm, iInf_add]; simp [add_comm]

-- check that the ENNReal versions are special cases
example {a : ENNReal} {ι : Sort*} {f : ι → ENNReal} :
  @ENNReal.iInf_add a ι f = iInf_add := rfl
example {ι : Sort*} {f : ι → ENNReal} {a : ENNReal} :
  @ENNReal.add_iInf ι f a = add_iInf := rfl

-- try a proper generalization
example (β : Type) {a : β → ENNReal} {ι : Sort*} {f : ι → β → ENNReal} :=
  iInf_add (α := β → ENNReal) (a := a) (f := f)

/-- Pass a double ⨅ through a sum, to get a sum of independent ⨅s. -/
theorem iInf₂_add {α : Type*} {κ : Type*}
    [CompleteLattice α]
    [AddCommMagma α]
    [CovariantClass α α (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1]
    [CovariantClass α α (Function.swap fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1]
    [Sub α] [OrderedSub α]
    (f₁ : κ → α) (f₂ : κ → α) :
    ⨅ k₁ : κ, ⨅ k₂ : κ, f₁ k₁ + f₂ k₂ = (⨅ k₁ : κ, f₁ k₁) + (⨅ k₂ : κ, f₂ k₂) := by
  simp_rw [← add_iInf]
  rw [← iInf_add]

/-- Factorize dependent function type over an Option. -/
theorem Equiv.piOptionEquivProdPi (α : Type*) (β : Option α → Type*) :
    ((y : Option α) → β y) ≃ ((x : α) → β (some x)) × (β none) := by
  calc
    ((y : Option α) → β y)
      ≃ _ := Equiv.piCongrLeft' _ (Equiv.optionEquivSumPUnit α)
    ((y : α ⊕ Unit) → β _)
      ≃ _ := Equiv.sumPiEquivProdPi _
    ((x : α)        → β (some x)) × (Unit → β none)
      ≃ ((x : α)    → β (some x)) × (       β none)
          := Equiv.prodCongrRight fun _ =>
              (Equiv.piUnique fun (_ : Unit) ↦ β none)

/-- Pass a multi-indexed ⨅ through a ∑, to get a ∑ of single-indexed ⨅s. -/
theorem iInf_pi_sum {ι α : Type*} [hι : Fintype ι] {κ : ι → Type*}
    [CompleteLattice α]
    [AddCommMonoid α]
    [CovariantClass α α (· + ·) (· ≤ ·)]
    [CovariantClass α α (Function.swap (· + ·)) (· ≤ ·)]
    [Sub α] [OrderedSub α]
    (f : (i : ι) → (κ i) → α) :
    ⨅ k : (i : ι) → (κ i), ∑ i : ι, f i (k i) = ∑ i : ι, ⨅ ki : (κ i), f i ki
    := by
  -- proof by an induction principle on Fintype
  revert ι
  apply Fintype.induction_empty_option
  case h_empty => -- base case: empty type
    intro κ f
    calc -- simplify both empty sums to 0
      _ = _ := by exact congr_arg _ (funext fun k => Finset.sum_of_empty Finset.univ)
      _ = _ := by exact iInf_const
      _ = _ := by exact (Finset.sum_of_empty _).symm
  case h_option => -- inductive step: from α to Option α
    intro ι hι h_ind κ f
    -- factorize parameter space of the multi-indexed ⨅
    let hprod := Equiv.piOptionEquivProdPi ι κ
    -- expand ∑ over Option α
    simp_rw [Fintype.sum_option]
    -- rewrite ⨅ as an iterated ⨅
    rw [← Equiv.iInf_comp hprod.symm]
    rw [iInf_prod]
    -- get the result ready for final simplification
    unfold_let hprod
    unfold Equiv.piOptionEquivProdPi
    simp only [Equiv.instTransSortSortSortEquivEquivEquiv_trans, Equiv.optionEquivSumPUnit_symm_inl,
      Equiv.optionEquivSumPUnit_symm_inr, id_eq, Equiv.trans_refl, Equiv.symm_trans_apply,
      Equiv.piCongrLeft'_symm_apply, Equiv.optionEquivSumPUnit_none, Equiv.optionEquivSumPUnit_some]
    -- XXX: did not find better simplification that deeply nested `whnf`
    conv =>
      enter [1, 1, i, 1, j, 1, 2]
      whnf
      rfl
    conv =>
      enter [1, 1, i, 1, j, 2, 2, x, 2]
      whnf
      rfl
    -- pass ⨅ through ∑ and finish
    simp only [← iInf_add]
    simp only [← add_iInf]
    congr
    exact h_ind _
  case of_equiv => -- covariance with respect to type equivalence
    intro ι' ι hι hι'ι h_orig κ f
    have hι' : Fintype ι' := Fintype.ofEquiv _ hι'ι.symm
    let hpiι'ι : ((i : ι) → κ i) ≃ ((i' : ι') → κ (hι'ι i')) := (Equiv.piCongrLeft _ hι'ι).symm
    -- reindex ∑ and ⨅
    simp only [← Equiv.sum_comp hι'ι]
    simp only [← Equiv.iInf_comp hpiι'ι.symm]
    -- simplify and finish
    simp only [Equiv.symm_symm, Equiv.piCongrLeft_apply_apply]
    first
    | exact h_orig _  -- fails to unify with goal (XXX: expected behavior?)
    | exact Iff.mp (by congr!) (h_orig _)  -- congr! succeeds to prove Iff with goal

example (n : ℕ) :
    ∑ i : Fin n, ⨅ ki : ℕ, (1 / ki : ENNReal) = ⨅ k : Fin n → ℕ, ∑ i : Fin n, (1 / (k i) : ENNReal)
    := by
  first
  | apply iInf_pi_sum _  -- fails to unify with goal
  | rw [  iInf_pi_sum _] -- fails to match lhs to goal lhs
  | rw [← iInf_pi_sum _] -- matches rhs to goal rhs
  | exact iInf_pi_sum (fun i (ki : ℕ) => (1 / ki : ENNReal)) -- succeeds with explicit `f`
  | sorry

[Igor Khavkine]

Comments welcome, as I'm still in the learning stages with Lean.