fact_finiteDimensional_of_finrank_eq_succ

Stream: mathlib4

[Patrick Massot]

The following works in Lean 3:

import linear_algebra.finite_dimensional

variables (R: Type*) [field R](E : Type _) [add_comm_group E] [module R E]

open finite_dimensional

local attribute [instance] fact_finite_dimensional_of_finrank_eq_succ

example [fact (finrank R E = 3)] : finite_dimensional R E := by
apply_instance

It is producing the proof fact_finiteDimensional_of_finrank_eq_succ 2. But in Lean 4 the translated code is:

import Mathlib.LinearAlgebra.FiniteDimensional

variable (R: Type*) [Field R](E : Type _) [AddCommGroup E] [Module R E]

open FiniteDimensional

attribute [local instance] fact_finiteDimensional_of_finrank_eq_succ

example [Fact (finrank R E = 3)] : FiniteDimensional R E :=  by
  infer_instance

which complains with

cannot find synthesization order for instance @fact_finiteDimensional_of_finrank_eq_succ with type
  ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (n : ℕ)
    [inst_3 : Fact (finrank K V = n + 1)], FiniteDimensional K V
all remaining arguments have metavariables:
  Fact (finrank K V = ?n + 1)

Using set_option synthInstance.checkSynthOrder false in removes the error on the instance declaration but then infer_instance fails. Is this a known issue?

[Matthew Ballard]

I think this is a case of in creating a section and local not surviving past it

[Matthew Ballard]

Both

set_option synthInstance.checkSynthOrder false in
attribute [local instance] fact_finiteDimensional_of_finrank_eq_succ in
example [Fact (finrank R E = 3)] : FiniteDimensional R E :=  by
  infer_instance

and

set_option synthInstance.checkSynthOrder false
attribute [local instance] fact_finiteDimensional_of_finrank_eq_succ

example [Fact (finrank R E = 3)] : FiniteDimensional R E :=  by
  infer_instance

work for example

[Patrick Massot]

Indeed!

[Patrick Massot]

I've read about that "feature" before, but it's really hard to avoid being surprised anyway!

[Matthew Ballard]

I don't remember if there was a satisfying workaround

[Patrick Massot]

Should I write

set_option synthInstance.checkSynthOrder false
attribute [local instance] fact_finiteDimensional_of_finrank_eq_succ
set_option synthInstance.checkSynthOrder true

[Matthew Ballard]

I think that is the best I've seen :) Others might know better

[Patrick Massot]

Next issue is actually a lot worse. You know this legend saying simp only is nice for proof maintenance? When the Lean 3 proof is

lemma inner_cross_product_apply (u v w : E) : ⟪u ×₃ v, w⟫ = ω.volume_form ![u, v, w] :=
by simp only [cross_product, to_dual, linear_equiv.trans_symm, linear_equiv.symm_symm,
  linear_isometry_equiv.to_linear_equiv_symm, alternating_map.curry_left_linear_map_apply,
  linear_map.coe_comp, function.comp_app, linear_map.llcomp_apply,
  linear_equiv.coe_coe, linear_equiv.trans_apply, linear_isometry_equiv.coe_to_linear_equiv,
  linear_isometry_equiv.norm_map, submodule.coe_norm,
  inner_product_space.to_dual_symm_apply, alternating_map.curry_left_apply_apply,
  alternating_map.const_linear_equiv_of_is_empty_symm_apply,
  eq_self_iff_true, linear_map.coe_to_continuous_linear_map', matrix.zero_empty]

and Lean 4 answers:

unsolved goals
E: Type u_1
inst✝²: NormedAddCommGroup E
inst✝¹: InnerProductSpace ℝ E
inst✝: Fact (finrank ℝ E = 3)
ω: Orientation ℝ E (Fin 3)
uvw: E
⊢ inner
    (↑(LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E))
      (↑LinearMap.toContinuousLinearMap
        (↑(↑(LinearMap.llcomp ℝ E (AlternatingMap ℝ E ℝ (Fin 0)) ℝ)
              ↑(LinearEquiv.symm AlternatingMap.constLinearEquivOfIsEmpty))
          (↑{
                toAddHom :=
                  { toFun := fun f => AlternatingMap.curryLeft f,
                    map_add' :=
                      (_ :
                        ∀ (f g : AlternatingMap ℝ E ℝ (Fin (Nat.succ 0))),
                          AlternatingMap.curryLeft (f + g) = AlternatingMap.curryLeft f + AlternatingMap.curryLeft g) },
                map_smul' :=
                  (_ :
                    ∀ (r : ℝ) (f : AlternatingMap ℝ E ℝ (Fin (Nat.succ 0))),
                      AlternatingMap.curryLeft (r • f) = r • AlternatingMap.curryLeft f) }
            (↑(↑{
                      toAddHom :=
                        { toFun := fun f => AlternatingMap.curryLeft f,
                          map_add' :=
                            (_ :
                              ∀ (f g : AlternatingMap ℝ E ℝ (Fin (Nat.succ 1))),
                                AlternatingMap.curryLeft (f + g) =
                                  AlternatingMap.curryLeft f + AlternatingMap.curryLeft g) },
                      map_smul' :=
                        (_ :
                          ∀ (r : ℝ) (f : AlternatingMap ℝ E ℝ (Fin (Nat.succ 1))),
                            AlternatingMap.curryLeft (r • f) = r • AlternatingMap.curryLeft f) }
                  (↑(↑{
                            toAddHom :=
                              { toFun := fun f => AlternatingMap.curryLeft f,
                                map_add' :=
                                  (_ :
                                    ∀ (f g : AlternatingMap ℝ E ℝ (Fin (Nat.succ 2))),
                                      AlternatingMap.curryLeft (f + g) =
                                        AlternatingMap.curryLeft f + AlternatingMap.curryLeft g) },
                            map_smul' :=
                              (_ :
                                ∀ (r : ℝ) (f : AlternatingMap ℝ E ℝ (Fin (Nat.succ 2))),
                                  AlternatingMap.curryLeft (r • f) = r • AlternatingMap.curryLeft f) }
                        (volumeForm ω))
                    u))
              v)))))
    w =
  ↑(volumeForm ω) ![u, v, w]

[Kevin Buzzard]

yeah I guess sections is a natural way to make in work but you really have to remember that this is what's going on in order to understand these initially counterintuitive errors!

[Matthew Ballard]

Can one make local set_option or something that hides the toggle on/off?

[Patrick Massot]

Fortunately git blame says @Heather Macbeth will be delighted to fix that proof :grinning_face_with_smiling_eyes:

[Kevin Buzzard]

As for the much worse issue, yeah, these would come up during porting. The only solution I ever found was to bite the bullet and figure out what wasn't firing. It might be one of those situations where simp [X] fails but rw [X] works, there is a thread here where I whine about this. If you want to see if you're lucky you could randomly add _ to the end of some of the lemmas in the list :-/

[Matthew Ballard]

What if you delete only?

[Kevin Buzzard]

bet that doesn't fix it

[Kevin Buzzard]

there's a chance that adding a random _ at the end of one of the lemma statements fixes it

[Matthew Ballard]

I see eq_self_iff_true which I never see except from a working simp [...]that got squeezed

[Patrick Massot]

I know, I've already being doing this a lot, although it usually doesn't get that bad outside the manifold library.

[Patrick Massot]

Conveniently enough, I no longer have time to work on this now, so I pushed a fix for the whole file except for this monster simp only.

[Kevin Buzzard]

One thing I've done in the past is to make rw do the job instead in lean 3, and then port the rw proof to lean 4

[Kevin Buzzard]

then you can change it back to simp and find the rw which can't be simped and then you can moan about it on the lean 4 thread.