weird Dtype for non-Dtypes using Pi.instCompleteLattice

Stream: lean4

[Ira Fesefeldt]

I instantiated a complete lattice for a pointwise but non-dependent defined type using Pi.instCompleteLattice. This worked nicely. However, now that I would like to prove something on it, I get a weird dependent-looking type in the proofview. I think this is only cosmetic, it still bugs me, however. Is there maybe an easy solution to make the type look neat?

An MWE looks like this, where b has the weird dependent type:

import Mathlib.Data.ENNReal.Basic

def state (α : Type) : Type := α → ℕ

def myType (α : Type) : Type := (state α) → ENNReal

noncomputable instance cl {α : Type} : CompleteLattice (myType α) := Pi.instCompleteLattice

def sideCondition (s₁ s₂ s₂ : state α) : Prop := sorry

noncomputable def myMul (P Q : myType Var) : myType Var :=
  fun s => sSup { x | ∃ s₁ s₂ : state Var, sideCondition s s₁ s₂ ∧ x = P s₁ * Q s₂}

example {P₁ P₂ Q₁ Q₂ : myType Var} (hP : P₁ ≤ P₂) (hQ : Q₁ ≤ Q₂): myMul P₁ Q₁ ≤ myMul P₂ Q₂  := by
  intro s
  apply sSup_le
  intro b
  sorry

[Kevin Buzzard]

You can do dsimp at b to see that b : ENNReal and then you can change the intro line to intro (b : ENNReal) if you like.

[Kevin Buzzard]

But assuming you want to do more intros you might want to instead do

  rintro - ⟨s₁, s₂, h, rfl⟩

which just removes b from the picture completely.

[Jovan Gerbscheid]

This seems to be a problem with the definitions of Pi.preorder Pi.partialOrder Pi.instSemilatticeSup Pi.instLattice Pi.instCompleteLattice. They all contain terms of the form fun i => a i:

import Mathlib.Order.CompleteLattice

set_option pp.explicit true
/-
def Pi.partialOrder.{u_2, u_1} : {ι : Type u_1} →
  {π : ι → Type u_2} → [inst : (i : ι) → PartialOrder (π i)] → PartialOrder ((i : ι) → π i) :=
fun {ι} {π} [inst : (i : ι) → PartialOrder (π i)] =>
  let __spread.0 := @Pi.preorder ι (fun i => π i) fun i => @PartialOrder.toPreorder (π i) (inst i);
  @PartialOrder.mk ((i : ι) → π i) __spread.0 ⋯
-/
#print Pi.partialOrder

[Jovan Gerbscheid]

Here's a minimal example of this going badly in a definition:

import Mathlib

set_option trace.Meta.isDefEq true

variable {ι : Type u} {α : ι → Type v} [inst : (i : ι) → LE (α i)]
#check @Pi.hasLe _ _ inst

The second _ gets instantiated as fun i => α i, instead of α.
The subset of the trace that instantiates the metavariable is:

    [] ✅ ?m.30 i =?= α i ▼
      [] ?m.30 i [assignable] =?= α i [nonassignable]
      [] ✅ ι → Type ?u.27 =?= ι → Type v ▼
        [] ✅ ι =?= ι
        [] ✅ Type ?u.27 =?= Type v

I think this is an inefficiency in the unification algorithm, not being able to properly deal with the unification problem ?m.30 i =?= α i.

[Jovan Gerbscheid]

I've had a crack at fixing this problem, and made an issue for it (lean4#4386).

I made a modification to the mkLambdaFVars function, adding a etaReduce : Bool parameter that determines whether a new lambda of the form fun x => f x should instead become f. I then set this option to true at isDefEq when processing metavariable assignments.

Quite a number of proof in mathlib broke. Many of these involve removing a now unnecessary simp only. In other cases, a simp or rewrite doesn't work anymore because it relied on the bound variable that existed due to the eta expanded form, such as a simp_rw [mul_comm] that was used to rewrite fun x => 2*x, but now this term has turned into HMul.hMul 2. There were two strange cases where I had to replace a proof h with by exact h, because this changes the order in which metavariables are instantiated, avoiding a weird error.

After fixing all the proofs, the change leads to a 0.6% improvement in build instructions (#13601). Most notably, Mathlib.Algebra.DirectLimit, previously a top 50 slowest file, has sped up by 40%.

[Jovan Gerbscheid]

After looking more closely at Mathlib.Algebra.DirectLimit, my best guess for where the dramatic speedup comes from is that there are unifications where the two expressions are the same big complicated expression, but on one side G has been replaced with fun i => G i.