fun with binport

Stream: mathlib4

[Daniel Selsam]

This compiles in Lean4, importing binported oleans:

import Mathlib.RingTheory.Nullstellensatz

namespace MvPolynomial.Playground
open Ideal

variable {k : Type u} [instField : Field k]
variable {σ : Type v}
variable [instIAC : IsAlgClosed k] [instF : Fintype σ]

theorem vanishing_ideal_zero_locus_eq_radical (I : Ideal (MvPolynomial σ k)) : vanishingIdeal (ZeroLocus I) = I.radical := by
  rw [I.radical_eq_jacobson]
  refine le_antisymm (le_Inf ?x) (@λ p hp x hx => ?y)
  case x =>
    intro J ⟨hJI, hJ⟩
    let ⟨x, hx⟩ := (is_maximal_iff_eq_vanishing_ideal_singleton J).1 hJ
    refine hx.symm ▸ vanishing_ideal_anti_mono (@λ y hy p hp => ?z)
    case z =>
      rw [← mem_vanishing_ideal_singleton_iff, Set.mem_singleton_iff.1 hy, ← hx]
      refine hJI hp
  case y =>
    rw [← mem_vanishing_ideal_singleton_iff x p]
    refine (mem_Inf.mp hp) ⟨@le_trans _ _ _ _ _ (le_vanishing_ideal_zero_locus (I := I))
      (vanishing_ideal_anti_mono (@λ y hy => hy.symm ▸ hx)),
        MvPolynomial.vanishing_ideal_singleton_is_maximal⟩

end MvPolynomial.Playground

It is very close to what synport would produce automatically.

[Floris van Doorn]

Just curious, what would synport product automatically?

[Kevin Buzzard]

For comparison, here is the Lean 3 code.

[Mario Carneiro]

oof, it tripped on the rintros

-- error: Mathport/Syntax/Translate/Basic.lean:221:16: unsupported tactic `rintros
/-- Main statement of the Nullstellensatz -/
@[simp]
theorem vanishing_ideal_zero_locus_eq_radical
(I : ideal (mv_polynomial σ k)) : «expr = »(vanishing_ideal (zero_locus I), I.radical) :=
begin
  rw [I.radical_eq_jacobson] [],
  refine [le_antisymm (le_Inf _) (λ p hp x hx, _)],
  { rintros [J, "⟨", hJI, ",", hJ, "⟩"],
    obtain ["⟨", x, ",", hx, "⟩", ":=", (is_maximal_iff_eq_vanishing_ideal_singleton J).1 hJ],
    refine [«expr ▸ »(hx.symm, vanishing_ideal_anti_mono (λ y hy p hp, _))],
    rw ["[", "<-", mem_vanishing_ideal_singleton_iff, ",", set.mem_singleton_iff.1 hy, ",", "<-", hx, "]"] [],
    refine [hJI hp] },
  { rw ["<-", mem_vanishing_ideal_singleton_iff x p] [],
    refine [mem_Inf.mp hp ⟨le_trans (le_vanishing_ideal_zero_locus I) (vanishing_ideal_anti_mono (λ
        y hy, «expr ▸ »(hy.symm, hx))), mv_polynomial.vanishing_ideal_singleton_is_maximal⟩] }
end

might be a while before we have full coverage on these proofs

[Mario Carneiro]

what you see there is the reconstructed lean 3 syntax, which is what it prints on a fatal error

[Mario Carneiro]

After adding the rcases/rintros/obtain parsers, synport makes it through this proof. Here's what it looks like without editing:

/-- Main statement of the Nullstellensatz -/
@[simp]
theorem vanishing_ideal_zero_locus_eq_radical (I : ideal (mv_polynomial σ k)) :
  «expr = » (vanishing_ideal (zero_locus I)) I.radical :=
  by
    rw [I.radical_eq_jacobson]
    refine' le_antisymm (le_Inf _) fun p hp x hx => _
    ·
      rintro J ⟨hJI, hJ⟩
      obtain⟨x, hx⟩ := (is_maximal_iff_eq_vanishing_ideal_singleton J).1 hJ
      refine' «expr ▸ » hx.symm (vanishing_ideal_anti_mono fun y hy p hp => _)
      rw [←mem_vanishing_ideal_singleton_iff, set.mem_singleton_iff.1 hy, ←hx]
      refine' hJI hp
    ·
      rw [←mem_vanishing_ideal_singleton_iff x p]
      refine'
        mem_Inf.mp hp
          ⟨le_trans (le_vanishing_ideal_zero_locus I) (vanishing_ideal_anti_mono fun y hy => «expr ▸ » hy.symm hx),
            mv_polynomial.vanishing_ideal_singleton_is_maximal⟩

[Mario Carneiro]

actually the «expr = » in the statement is because I'm too lazy to run this on all previous files to build up the set of notations. Daniel's been running the full builds, which should resolve those so that it appears like normal

[Daniel Selsam]

Could somebody please recommend a few Mathlib theorems for me to play with using binport that will stress-test either typeclass resolution or the simplifier?

[Yakov Pechersky]

The old way of proving the formula for a 2x2 det:

import data.matrix.notation
import linear_algebra.determinant
import group_theory.perm.fin

example {α : Type*} [comm_ring α] {a b c d : α} :
  matrix.det ![![a, b], ![c, d]] = a * d - b * c :=
begin
  -- TODO: can we make this require less steering?
  simp [matrix.det_apply', finset.univ_perm_fin_succ, ←finset.univ_product_univ, finset.sum_product,
        fin.sum_univ_succ, fin.prod_univ_succ],
  ring
end

and the new way for a 3x3:

example {α : Type*} [comm_ring α] (A : matrix (fin 3) (fin 3) α) {a b c d e f g h i : α} :
        matrix.det ![![a, b, c], ![d, e, f], ![g, h, i]] =
          a * e * i - a * f * h - b * d * i + b * f * g + c * d * h - c * e * g :=
begin
  simp [matrix.det_succ_row_zero, fin.sum_univ_succ],
  /-
  Try this: simp only [det_succ_row_zero, fin.sum_univ_succ, neg_mul_eq_neg_mul_symm, cons_append,
  mul_one, fin.default_eq_zero, fin.coe_zero, cons_vec_bit0_eq_alt0, one_mul, cons_val_one,
  cons_vec_alt0, fin.succ_succ_above_one, fin.coe_succ, univ_unique, minor_apply, pow_one,
  fin.zero_succ_above, fin.succ_zero_eq_one, fin.succ_succ_above_zero, nat.neg_one_sq,
  finset.sum_singleton, cons_val_zero, cons_val_succ, det_fin_zero, head_cons, pow_zero]
   -/
  ring
end

[Floris van Doorn]

For type-class inference maybe docs#units.is_scalar_tower' (at least there are a lot of type-class assumptions)
For simp, I mostly think of the manifold and category theory library. Maybe docs#structure_groupoid.compatible_of_mem_maximal_atlas or docs#Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_inverse_obj.
Others might have better suggestions.

[Heather Macbeth]

There are several heavy simps in docs#measure_theory.simple_func.exists_le_lower_semicontinuous_lintegral_ge, for example

simpa only [hs, hc, lt_top_iff_ne_top, true_and, simple_func.coe_const, function.const_apply,
  lintegral_const, ennreal.coe_indicator, set.univ_inter, ennreal.coe_ne_top,
  measurable_set.univ, with_top.mul_eq_top_iff, simple_func.const_zero, or_false,
  lintegral_indicator, ennreal.coe_eq_zero, ne.def, not_false_iff, simple_func.coe_zero,
  set.piecewise_eq_indicator, simple_func.coe_piecewise, false_and, restrict_apply] using h

[Eric Wieser]

docs#exists_extension_norm_eq has hit typeclass timeouts for me in multiple attempted refactors

[Daniel Selsam]

Eric Wieser said:

docs#exists_extension_norm_eq has hit typeclass timeouts for me in multiple attempted refactors

This is perfect, thank you. Just trying to elaborate the type exposed another issue :)

[Eric Wieser]

If you want more timeouts, I have plenty of stale refactor branches that I could update to match master to get fresh timeouts on

[Daniel Selsam]

Timeouts are a luxury I rarely have yet -- there are still a lot of relatively fast elaboration errors. There are many complicated dynamics that only emerge deep in mathlib, and so we are just hitting them for the first time in lean4.

[Sebastien Gouezel]

If you want to try out a weird behavior, you can have a look at measure_theory/arithmetic.lean, especially the proof of the lemma has_measurable_gpow where Lean 3 does something crazy (there is probably a bug lurking somewhere): replacing the last line of the proof of this lemma exact has_measurable_gpow_aux G with the proof of the auxiliary lemma has_measurable_gpow_aux fails badly, for no reason I can understand. If Lean 4 could behave more properly on this one, this would be pretty nice!

[Eric Wieser]

Some other weird typeclass behavior is in #8547. Does lean4 require this instance that PR adds in order to remove the @s in the other part of the PR?

[Daniel Selsam]

Good news: I added lean-liquid to the mathport pipeline and it worked fine. I will include liquid in the uploads from now on (https://github.com/dselsam/mathport/releases/tag/v0.0.0.0). There is still a long way to go before the binaries can be used effectively, but at least the proof-term porting seems very robust now.

[Kevin Buzzard]

I had only recently internalised that porting large-ish projects which depended on mathlib like this one was on your radar. This is really good news!

[Daniel Selsam]

Kevin Buzzard said:

I had only recently internalised that porting large-ish projects which depended on mathlib like this one was on your radar. This is really good news!

Yes, there is no obstacle to applying mathport to any lean3 project that depends on an up-to-date mathlib. Mathport takes a list of modules to port, e.g. ./mathport config.json Lean3::all Mathlib::all Liquid::all.

[Scott Morrison]

No library left behind!

[Scott Morrison]

The alternative take on this is that it increases moral hazard, encouraging people to do maths outside of mathlib. :-)

[Floris van Doorn]

@Daniel Selsam If you are interested in another gruesome type-class problem, here is one that takes 8.6 to fail on yesterday's mathlib (it is supposed to fail):

--after running scripts/mk_all.sh
import all -- import all files of mathlib

open topological_space measure_theory

set_option profiler true
example {α E : Type*} {m0 : measurable_space α} {p : ennreal} {μ : measure α}
  [measurable_space E] [normed_group E] [borel_space E]
  [second_countable_topology E] [hp : fact (1 ≤ p)] :
  complete_space (measure_theory.Lp E p μ) :=
by apply_instance

I tried to port this to the binported mathlib you posted a while back.

import Mathlib.All

open MeasureTheory TopologicalSpace

-- this should succeed
example {α : Type u} {E : Type v} {m0 : MeasurableSpace α} {p : Ennreal} {μ : Measure α}
  [MeasurableSpace E] [NormedGroup E] [BorelSpace E]
  [SecondCountableTopology E] [hp : Fact (1 ≤ p)] :
  UniformSpace (lp E p μ) :=
by inferInstance

-- this should fail
example {α : Type u} {E : Type v} {m0 : MeasurableSpace α} {p : Ennreal} {μ : Measure α}
  [MeasurableSpace E] [NormedGroup E] [BorelSpace E]
  [SecondCountableTopology E] [hp : Fact (1 ≤ p)] :
  CompleteSpace (lp E p μ) :=
by inferInstance

However, I'm getting some type-class problems, that are caused by the redefinition of docs#coe_trans, which makes instances like docs#add_units.has_coe looping. Can I disable instances locally (the equivalent of Lean 3's local attribute [-instance])?

[Leonardo de Moura]

@Floris van Doorn Thanks for looking into this stuff. I just pushed support for temporarily disabling instances. Here is an example:

structure Foo where
  a : Nat

instance fooAdd : Add Foo where
  add x y := ⟨x.a + y.a⟩

def f1 (a b : Foo) := a + b -- Works

section
attribute [-instance] fooAdd

def f2 (a b : Foo) := a + b -- Error
end

def f3 (a b : Foo) := a + b -- Works

[Floris van Doorn]

Thanks!