Decidability clash

Stream: lean4

[Sophie Morel]

I hope that this is the right stream for my question, since it's not really a math question but, as far as I can tell, a problem with different decidability instances fighting it out.

Context: I'm trying to prove that continuous multilinear maps are differentiable. So there is a type ι indexing the product on which the map is defined, with a Fintype instance on it. Some of my lemmas require a DedicableEq instance on ι, and some require a LinearOrder instance; when I tried to call the second kind of lemma in the first kind of lemma, the DecidableEq instance coming from the LinearOrder fights the already existing DecidableEq instance and it blocks everything with one of Lean's trademark confusing messages. Here is a MWE so you can see if I interpreted the situation correctly:

import Mathlib.Tactic
import Mathlib.Analysis.NormedSpace.Multilinear
import Mathlib.Order.Extension.Well

namespace MultilinearMap

variable {R : Type uR} [Semiring R]  {ι : Type uι} {M : ι → Type v} {N : Type w}
[∀ (i : ι), AddCommGroup (M i)] [AddCommGroup N] [∀ (i : ι), Module R (M i)]
[Module R N] {n : ℕ}

lemma apply_sub [LinearOrder ι]
(f : MultilinearMap R M N) (a b v : (i : ι) → (M i)) (s : Finset ι)
(hs : Finset.card s = n) :
f (s.piecewise a v) - f (s.piecewise b v) = Finset.sum Finset.univ (fun (i : Fin n) =>
f (fun j => if h : j ∈ s then (if (s.orderIsoOfFin hs).symm ⟨j, h⟩ < i then a j
else if (s.orderIsoOfFin hs).symm ⟨j, h⟩ = i then a j - b j else b j) else v j)) := by sorry

end MultilinearMap

namespace ContinuousMultilinearMap

variable {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {ι : Type v} [Fintype ι] [DecidableEq ι]
{E : ι → Type w₁} {F : Type w₂}
[(i : ι) → NormedAddCommGroup (E i)] [NormedAddCommGroup F] [(i : ι) → NormedSpace 𝕜 (E i)]
[NormedSpace 𝕜 F]


noncomputable def deriv (f : ContinuousMultilinearMap 𝕜 E F)
(x : (i : ι) → E i) : ((i : ι) → E i) →L[𝕜] F :=
Finset.sum Finset.univ (fun (i : ι) => (f.toContinuousLinearMap x i).comp (ContinuousLinearMap.proj i))

lemma sub_piecewise_bound (f : ContinuousMultilinearMap 𝕜 E F) (x : (i : ι) → E i)
(h : (((i : ι) → (E i)) × ((i : ι) → E i)))
{s : Finset ι} (hs : 2 ≤ s.card) :
‖f (s.piecewise h.1 x) - f (s.piecewise h.2 x)‖ ≤ s.card • (‖f‖ *
‖x‖ ^ sᶜ.card * ‖h‖ ^ (s.card - 1) * ‖h.1 - h.2‖) := by
  letI : LinearOrder ι := WellFounded.wellOrderExtension emptyWf.wf
  erw [MultilinearMap.apply_sub f.toMultilinearMap h.1 h.2 x s rfl]
    -- Error message: tactic 'rewrite' failed, did not find instance of the pattern in the target expression
     -- f.toMultilinearMap (Finset.piecewise s h.1 x) - f.toMultilinearMap (Finset.piecewise s h.2 x)

end ContinuousMultilinearMap

My interpretation of the error message is that Lean doesn't think the Finset.piecewise do the same thing, since the Finset.decidableMem instances that they call come from different sources. But since I'm a mathematician and I don't care about these decidability things, of course the functions do the same thing !

I thought about just taking my ι to be Fin n throughout, but it's a bit unsatisfying to my mathematical mind (because it shouldn't be necessary), and also I'm not even sure it would solve the problem.

[Andrew Yang]

This works:

convert (congr_arg norm (MultilinearMap.apply_sub f.toMultilinearMap h.1 h.2 x s rfl)).trans_le _

[Sophie Morel]

Thanks ! Though it made a strange seemingly unrelated error appear later in my real code, and I have no idea what's happening. (No MWE yet as I'm still trying to fix things myself, but I may be back soon.)

[Sophie Morel]

Okay, so I pawned myself by trying to streamline the MWE too much. :confounded: My actual file had an open Classical at the beginning instead of a DecidableEq instance for my specific type ι, and I don't even know why or how, but your solution has introduced a problem with the complement function on Finset ι. New MWE:

import Mathlib.Tactic
import Mathlib.Analysis.NormedSpace.Multilinear
import Mathlib.Order.Extension.Well

namespace MultilinearMap

variable {R : Type uR} [Semiring R]  {ι : Type uι} {M : ι → Type v} {N : Type w}
[∀ (i : ι), AddCommGroup (M i)] [AddCommGroup N] [∀ (i : ι), Module R (M i)]
[Module R N] {n : ℕ}

lemma apply_sub [LinearOrder ι]
(f : MultilinearMap R M N) (a b v : (i : ι) → (M i)) (s : Finset ι)
(hs : Finset.card s = n) :
f (s.piecewise a v) - f (s.piecewise b v) = Finset.sum Finset.univ (fun (i : Fin n) =>
f (fun j => if h : j ∈ s then (if (s.orderIsoOfFin hs).symm ⟨j, h⟩ < i then a j
else if (s.orderIsoOfFin hs).symm ⟨j, h⟩ = i then a j - b j else b j) else v j)) := by sorry

end MultilinearMap

namespace ContinuousMultilinearMap

open Classical

variable {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {ι : Type v} [Fintype ι]
{E : ι → Type w₁} {F : Type w₂}
[(i : ι) → NormedAddCommGroup (E i)] [NormedAddCommGroup F] [(i : ι) → NormedSpace 𝕜 (E i)]
[NormedSpace 𝕜 F]


noncomputable def deriv (f : ContinuousMultilinearMap 𝕜 E F)
(x : (i : ι) → E i) : ((i : ι) → E i) →L[𝕜] F :=
Finset.sum Finset.univ (fun (i : ι) => (f.toContinuousLinearMap x i).comp (ContinuousLinearMap.proj i))

lemma sub_piecewise_bound (f : ContinuousMultilinearMap 𝕜 E F) (x : (i : ι) → E i)
(h : (((i : ι) → (E i)) × ((i : ι) → E i)))
{s : Finset ι} (hs : 2 ≤ s.card) :
‖f (s.piecewise h.1 x) - f (s.piecewise h.2 x)‖ ≤ s.card • (‖f‖ *
‖x‖ ^ sᶜ.card * ‖h‖ ^ (s.card - 1) * ‖h.1 - h.2‖) := by
  letI : LinearOrder ι := WellFounded.wellOrderExtension emptyWf.wf
  set n := s.card
  convert (congr_arg norm (MultilinearMap.apply_sub f.toMultilinearMap h.1 h.2 x s rfl)).trans_le _
  refine le_trans (norm_sum_le _ _) ?_
  have heq : (Finset.univ (α := Fin n)).card = n := by simp only [Finset.card_fin]
  rw [←heq, ←(Finset.sum_const (α := Fin n))]
  apply Finset.sum_le_sum
  intro i _
  refine le_trans (ContinuousMultilinearMap.le_op_norm f _) ?_
  rw [mul_assoc, mul_assoc]
  refine mul_le_mul_of_nonneg_left ?_ (norm_nonneg _)
  rw [←(Finset.prod_compl_mul_prod s)]
  set m := s.orderIsoOfFin rfl i
  rw [←(Finset.mul_prod_erase s _ m.2)]
  simp only [m.2, dite_true]
  conv => lhs
          congr
          rfl
          congr
          rw [OrderIso.symm_apply_apply]
          simp only [lt_irrefl i, ite_false, ite_true]
          rfl
  have hle1aux : ∀ (j : ι), j ∈ sᶜ →
    (fun k => ‖if hk : k ∈ s then
          if (OrderIso.symm (Finset.orderIsoOfFin s rfl)) ⟨k, hk⟩ < i then h.1 k
          else
            if (OrderIso.symm (Finset.orderIsoOfFin s rfl)) ⟨k, hk⟩ = i then h.1 k - h.2 k
            else h.2 k
        else x k‖) j ≤ ‖x‖ := by
    intro j hj
    rw [Finset.mem_compl] at hj
    simp only [hj, dite_false]
    apply norm_le_pi_norm
  have hle1 := Finset.prod_le_prod (s := sᶜ) (fun j _ => norm_nonneg _) hle1aux
  rw [Finset.prod_const] at hle1
  have hle2aux : ∀ (j : ι), j ∈ Finset.erase s m →
    (fun k =>  ‖if hk : k ∈ s then
    if (OrderIso.symm (Finset.orderIsoOfFin s rfl)) ⟨k, hk⟩ < i then h.1 k
    else
    if (OrderIso.symm (Finset.orderIsoOfFin s rfl)) ⟨k, hk⟩ = i then h.1 k - h.2 k
    else h.2 k
    else x k‖) j ≤ ‖h‖ := by
    intro j hj
    set hj' := Finset.mem_of_mem_erase hj
    simp only [hj', dite_true]
    by_cases hj'' : (s.orderIsoOfFin rfl).symm ⟨j, hj'⟩ < i
    . simp only [hj'', ite_true]
      refine le_trans ?_ (norm_fst_le h)
      apply norm_le_pi_norm
    . simp only [hj'', ite_false]
      have hj''' : (s.orderIsoOfFin rfl).symm ⟨j, hj'⟩ ≠ i := by
        by_contra habs
        rw [Finset.mem_erase] at hj
        simp only at hj
        rw [←habs] at hj
        simp only [OrderIso.apply_symm_apply, ne_eq, not_true_eq_false, false_and] at hj
      simp only [hj''', ite_false, ge_iff_le]
      refine le_trans ?_ (norm_snd_le h)
      apply norm_le_pi_norm
  have hle2 := Finset.prod_le_prod (s := s.erase m) (fun j _ => norm_nonneg _) hle2aux
  rw [Finset.prod_const, Finset.card_erase_of_mem m.2] at hle2
  refine le_trans (mul_le_mul_of_nonneg_right hle1 (mul_nonneg (norm_nonneg _)
    (Finset.prod_nonneg (fun _ _ => norm_nonneg _)))) ?_
  apply mul_le_mul
  . apply le_refl (‖x‖ ^ sᶜ.card)
  /- Error message:
  tactic 'apply' failed, failed to unify
  ‖x‖ ^ Finset.card sᶜ ≤ ‖x‖ ^ Finset.card sᶜ
with
  ‖x‖ ^ Finset.card sᶜ ≤ ‖x‖ ^ Finset.card sᶜ-/

end ContinuousMultilinearMap

The error message is not so helpful, but if I unwrap it I find that the problem seems to come from Finset.booleanAlgebra, which calls on two separate decidability instances on ι. So the problem has only been displaced further. :man_facepalming:

[Yaël Dillies]

Yes, simply don't use open Classical. This is what's introducing the problematic DecidableEq instance.

[Sophie Morel]

If I don't use open Classical, every lemma before that that involved Function.update and Finset.piecewise starts having problems.

[Sophie Morel]

Look at this for example:

import Mathlib.Tactic
import Mathlib.Analysis.NormedSpace.Multilinear
import Mathlib.Analysis.Calculus.ContDiff.Basic
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Order.Extension.Well
import ExteriorPowers.MultilinearMap


open Filter Asymptotics ContinuousLinearMap Set Metric
open Topology NNReal Asymptotics ENNReal
open NormedField


namespace ContinuousMultilinearMap


variable {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {ι : Type v} [Fintype ι]
{E : ι → Type w₁} {F : Type w₂}
[(i : ι) → NormedAddCommGroup (E i)] [NormedAddCommGroup F] [(i : ι) → NormedSpace 𝕜 (E i)]
[NormedSpace 𝕜 F] [DecidableEq ι]


noncomputable def deriv (f : ContinuousMultilinearMap 𝕜 E F)
(x : (i : ι) → E i) : ((i : ι) → E i) →L[𝕜] F :=
Finset.sum Finset.univ (fun (i : ι) => (f.toContinuousLinearMap x i).comp (ContinuousLinearMap.proj i))



@[simp]
lemma deriv_apply (f : ContinuousMultilinearMap 𝕜 E F)
(x y : (i : ι) → E i) :
  f.deriv x y = Finset.sum Finset.univ (fun (i : ι) => f (Function.update x i (y i))) := by
  unfold deriv toContinuousLinearMap
  simp only [ContinuousLinearMap.coe_sum', ContinuousLinearMap.coe_comp',
    ContinuousLinearMap.coe_mk', LinearMap.coe_mk, LinearMap.coe_toAddHom, Finset.sum_apply,
    Function.comp_apply, ContinuousLinearMap.proj_apply, MultilinearMap.toLinearMap_apply, coe_coe]

@[simp]
lemma deriv_coe_apply (f : ContinuousMultilinearMap 𝕜 E F) (x y: (i : ι) → (E i)):
f.deriv x y = f.toMultilinearMap.linearDeriv x y := by
  simp only [deriv_apply, MultilinearMap.linearDeriv_apply, coe_coe]
  -- Goal: (Finset.sum Finset.univ fun x_1 ↦ f (Function.update x x_1 (y x_1))) =
  --        Finset.sum Finset.univ fun x_1 ↦ f (Function.update x x_1 (y x_1))
  rfl /-Error nmessage: type mismatch
  HEq.rfl
has type
  HEq ?m.22983 ?m.22983 : Prop
but is expected to have type
  (Finset.sum Finset.univ fun x_1 ↦ f (Function.update x x_1 (y x_1))) =
    Finset.sum Finset.univ fun x_1 ↦ f (Function.update x x_1 (y x_1)) : Prop-/

If I sorry this lemma, the next one has a similar problem !

[Sophie Morel]

Oops, there's an import from a local file in my MWE. The local file also had an open Classical, I changed it to a DedicableEq instance and that problem vanished.

[Sophie Morel]

But I'm a mathematician, I want to use open Classical so I don't have to worry about decidability all the time... :sob:

[Sebastien Gouezel]

Lesson learned the hard way: never ever open Classical, because it creates much more problems than it solves. Instead, whenever a lemma complains that the statement doesn't make sense because it lacks decidability assumptions, add them to the statement of the lemma.

[Sophie Morel]

Sebastien, the first open Classical came because I copied the preamble of Mathlib.Analysis.Calculus.FDeriv.Bilinear and it was there. (Since that's the file I'm trying to generalize.)

[Yaël Dillies]

Feel free to remove it from there too!

[Sophie Morel]

Uhhhh, I haven't dared PR my shiny new lemmas to mathlib yet, I'm not at the level where I'm going to fiddle with the assumptions of already-existing files.

[Sophie Morel]

(Also one day maybe I'll understand how to use calc and my life will become beautiful. Don't hold your breath.)

[Yaël Dillies]

Both of those are things you should try. I'm still eagerly awaiting your shellability work :wink:

[Sophie Morel]

There were other people who wanted to contribute abstract simplicial complex stuff to mathlib so I was waiting to hear from them. But it's been a few months and they seem to have vanished.

[Yaël Dillies]

There is https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/AbstractSimplicialComplex from two days ago.

[Yaël Dillies]

Out of everyone here, you have the most advanced use of ASC so far. I have very detailed ideas about the basic theory, but I don't know much about the rest. You should PR your material, then I can polish the basic parts and review the harder parts in depth.

[Sophie Morel]

I hadn't seen that. (Every time I log on to Zulip, it tells me I have ten zillion unread messages, and I run away again.) I have to ruin lives give an exam early next week, then I should have a little time to PR this stuff.

[Sophie Morel]

It's an oral exam, so at least I won't spend my holiday grading. (I will, however, spend it reading postdoc applications...)

[Sophie Morel]

Well, continuous multilinear maps are now officially differentiable, thanks to Andrew Yang's fix ! Now I have to prove that they are infinitely differentiable by an "obvious induction". I look forward eagerly to the wrenches that Lean is going to throw into said obvious induction.

[Patrick Massot]

Sophie Morel said:

Every time I log on to Zulip, it tells me I have ten zillion unread messages, and I run away again.

Do you know you can use the stream menu to mark messages as read even if you didn't read them?

[Patrick Massot]

Wew are sorry about the open Classical trap. It used to be a good idea a long time ago. This is no longer true but you may still find places recommending it, or old files using it. It is really a historical accident.

[Patrick Massot]

Sophie Morel said:

Well, continuous multilinear maps are now officially differentiable, thanks to Andrew Yang's fix ! Now I have to prove that they are infinitely differentiable by an "obvious induction". I look forward eagerly to the wrenches that Lean is going to throw into said obvious induction.

Please read comments containing the word universe in https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Analysis/Calculus/ContDiff/Bounds.lean for instance.

[Eric Wieser]

open scoped Classical in is still occasionally a good idea, but only for defs and never for theorems

[Sophie Morel]

Patrick Massot said:

Sophie Morel said:

Well, continuous multilinear maps are now officially differentiable, thanks to Andrew Yang's fix ! Now I have to prove that they are infinitely differentiable by an "obvious induction". I look forward eagerly to the wrenches that Lean is going to throw into said obvious induction.

Please read comments containing the word universe in https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Analysis/Calculus/ContDiff/Bounds.lean for instance.

Hahaha, I ran into exactly that issue, you wizard. :sweat_smile: Thanks for the link !

[Sophie Morel]

Patrick Massot said:

Sophie Morel said:

Every time I log on to Zulip, it tells me I have ten zillion unread messages, and I run away again.

Do you know you can use the stream menu to mark messages as read even if you didn't read them?

Yes, I know. It goes against my completionist instincts but I will have to use this feature if I want to continue frequenting Zulip.

[Sophie Morel]

Whew, the induction is done. I had extra fun with the change of universe because ContinuousMultilinearMap.domDomCongr only works if all the components of the product are the same space, so I had to reduce to that case first. (Well first I tried to generalize domDomCongr and quickly understood why the restriction was there. Ouch.)

[Sophie Morel]

Okayyy, I made my first PR of the "continuous multilinear maps are infinitely differentiable" project, which is a definition and a couple lemmas in Mathlib.LinearAlgebra.Multilinear.Basic, and I labelled it with awaiting-review. Should I now go to PR reviews to discuss it ? I've been trying to follow the instructions of https://leanprover-community.github.io/contribute/index.html so far, but I didn't see a mention of the PR reviews Zulip channel.

[Patrick Massot]

This review stream is used only for PRs that require too much discussion for GitHub, and sometimes also to point out PRs that seem neglected on GitHub.

[Sophie Morel]

Ok, I'll wait then.

[Eric Wieser]

It is usually a good idea to mention the PR number when noting that you made a PR, so that interested but lazy people can click it and look at it! (Zulip autolinks things that look like #NNNN to github PRs)

[Sophie Morel]

Here, for interested but lazy people: #9130

[Sophie Morel]

Wow, magical autolink !

[Eric Wieser]

I left some initial comments; the obvious one is that you're writing Finset.sum instead of ∑, and the latter is usually much easier to read!

[Sophie Morel]

You're right, I almost never use notation in my own files but I guess I should. I've committed all your changes.