witt vectors

Stream: maths

[Johan Commelin]

Anyone interested in sharpening his teeth on polynomials is encouraged to look here: https://gist.github.com/jcommelin/77240367c2815ca0c45da188ba78be19

[Johan Commelin]

A bunch of stuff from the preamble will be obsolete as soon as Mario pushes his latest mathlib edits.

[Johan Commelin]

In the final lemma there are a bunch of sorrys. The proof is extremely slow, and I am continuously struggling with deterministic timeouts.

[Johan Commelin]

I have no idea why. It didn't feel to me like I was pushing limits.

[Johan Commelin]

So there is about 180 lines of preamble. And then about 50 lines of interesting stuff :wink:

[Johan Commelin]

(A bit of motivation for these crazy polynomials: They are useful for defining rings of Witt vectors, and those show up all over the place in number theory. For example, the ring of p-adic integers turns out to be the ring of Witt vectors of the finite field with p elements.)

[Kevin Buzzard]

In the final lemma there are a bunch of sorrys. The proof is extremely slow, and I am continuously struggling with deterministic timeouts.

There is sometimes a reason for this ("your code is crappy for a reason which you didn't realise") but typically you have to get lucky with an expert looking at it and spotting what you did wrong. My valuation stuff got slow recently and I don't know why, but I didn't even bother posting 200 lines of Lean code and saying "why does this take three seconds to compile and I had to put some type class thing up to 100 to make it work?" because it's such a boring question; if I really cared I would try and minimise; currently I just grit my teeth and work around it.

[Johan Commelin]

So how do you work around deterministic timeouts? What determines such a timeout? Can I set some option to let Lean work harder?

[Kevin Buzzard]

Did you see the 1 <= k <= n example? That one seemed to debate some discussion from the experts

[Kevin Buzzard]

Here's a conjecture: these things are almost always caused by the type class inference system. @Mario Carneiro what do you think about my conjecture?

[Mario Carneiro]

that's a bit of a general claim. Another way to make lean take a long time is to use lots of definitional equality or kernel computation, possibly on accident; and elaboration can often take a suspiciously long time to complete (not crazy but like 10-15 seconds for a term proof) for reasons I don't well understand

[Kevin Buzzard]

There's a file in the perfectoid repo which takes 10 seconds to compile and I was half-thinking about trying to work out why so really I was looking for clues here.

[Johan Commelin]

Anyone care to take a look at https://github.com/jcommelin/mathlib/blob/witt/algebra/witt_vector.lean#L107 ? That file is self-contained, but depends on the latest mathlib.

[Kevin Buzzard]

I don't know what the type of anything is, but the lemma you're applying needs that the things you're applying it to are in a multiplicative group and the elements you're talking about look suspicious to me

[Kevin Buzzard]

A field is not a group under multiplication. Are you using the right lemma?

[Mario Carneiro]

oh, good call

[Mario Carneiro]

there are mirror versions of all the group lemmas for fields with namespace division_ring or field

[Kevin Buzzard]

This has happened to me so many times :-)

[Kevin Buzzard]

"I can't find an instance of exactly what it says in the goal" usually for me means "the thing you want me to match with doesn't match because of something in square brackets"

[Mario Carneiro]

heh, I remember so many questions from you like that

[Johan Commelin]

I'm slowly making progress... conv is still confusing me.

[Johan Commelin]

conv in (λ _, _) gives an error:

invalid mk_pattern, #1 expr parameter does not occur in the target or (other) expr parameter types
state:
_inst_1 : nat.Prime,
n n : ℕ,
H : ∀ (m : ℕ), m < n → eval₂ C witt_polynomial (X_in_terms_of_W m) = X m
⊢ witt_polynomial n =
      C (↑p ^ (n + 1)) * X n +
        finset.sum finset.univ
          (λ (x : fin n),
             eval₂ C witt_polynomial (C ↑p ^ x.val) *
               eval₂ C witt_polynomial (X_in_terms_of_W (x.val) ^ p ^ (n - x.val))) =
    ?m_1

[Johan Commelin]

But there is clearly a lambda in there...

[Johan Commelin]

Ok, I navigated to the lambda by hand.

[Johan Commelin]

Then I did some rewrites using ring homomorphisms, but Lean couldn't find an instance for them, nor for some rings.

[Johan Commelin]

Outside the conv, Lean found those instances without any trouble.

[Johan Commelin]

Is this a known issue?

[Kevin Buzzard]

I have this gut feeling that I've gone from never using conv (because I had no idea how it worked or what it did, before Patrick and I pushed the experts to explain it and then Patrick wrote conv.md) to over-using it. I tend to use it to do rewrites under a lambda -- but remember that simp does this too, so perhaps simp only will do what you're trying to do without having to use conv. One problem with conv is that if you're trying to find f x = g x in some lam x, f x = g x then conv won't match f x because it complains it doesn't know what x is. I don't know what your problem is but I look at pretty much every Lean function and it's some sort of lambda, so trying to match a lambda with so many holes sounds a bit scary to me, and trying to fill in the holes also looks hard for the reason I just mentioned above. Will simp not work for you?

[Johan Commelin]

"I worked my way around it..."

[Johan Commelin]

@Mario Carneiro I have the feeling that I can not extract sublemmas for this proof. Yet I'm constantly plagued with deterministic timeouts. https://github.com/jcommelin/mathlib/blob/witt/algebra/witt_vector.lean#L108

[Johan Commelin]

I fought the mess (and the mess won)

[Mario Carneiro]

I wanted to ask: why are you using a finset.univ.sum over fin n when the function to sum over does not depend on the assumption x.2?

[Mario Carneiro]

It would be much easier to use (finset.range n).sum (\lam x, ...)

[Johan Commelin]

Ok. The answer is: I've never used finset.range before, and didn't know about it.

[Kevin Buzzard]

deterministic time-outs usually mean that you've made a mistake in your code and Lean, instead of saying "look an error", is trying to coerce an int into a nat or something else that it can't do but is unfortunately bad at spotting that it can't do.

[Kevin Buzzard]

bad coercions, and trying to prove things which aren't refl by refl, are sometimes the cause

[Kevin Buzzard]

(even if they look refl)

[Johan Commelin]

@Mario Carneiro Ok, in the definition after the witt_polynomial I am using i.2.

[Johan Commelin]

So now I need some hackery to make that recursive definition work.

[Mario Carneiro]

I see that... I'm working on the hackery

[Mario Carneiro]

This should get you started:

theorem range_sum_eq_fin_univ_sum {α} [add_comm_monoid α] (f : ℕ → α) (n) :
  (finset.range n).sum f = finset.univ.sum (λ i : fin n, f i.1) :=
show _ = @multiset.sum α _ ↑(list.map _ _),
by rw [list.map_pmap, list.pmap_eq_map]; refl

def witt_polynomial (n : ℕ) : mv_polynomial ℕ R :=
(finset.range (n+1)).sum (λ i, (C p ^ i * X i ^ (p^(n-i))))

def X_in_terms_of_W : ℕ → mv_polynomial ℕ ℚ
| n := (X n - (finset.sum finset.univ (λ i : fin n,
  have _ := i.2, (C p^i.val * (X_in_terms_of_W i.val)^(p^(n-i.val)))))) * C (1/p^n)

lemma X_in_terms_of_W_eq {n : ℕ} : X_in_terms_of_W n =
    (X n - (finset.range n).sum (λ i, C p ^ i * X_in_terms_of_W i ^ p ^ (n - i))) *
      C (1 / ↑p ^ n) :=
by rw [X_in_terms_of_W, range_sum_eq_fin_univ_sum]

[Mario Carneiro]

@Kevin Buzzard Hey look, a nontrivial equation lemma

[Johan Commelin]

Thanks!

[Johan Commelin]

That's a really sweet example of equation lemma hackery!

[Kevin Buzzard]

finset.sum finset.univ (λ i : fin (n+1), (C p^i.val * (X i.val)^(p^(n-i.val))))

Is this really still the best way to sum from 0 to n? It's the constant mentioning of .val which is a bit irritating. Is there some big operator or something which makes this better-looking?

[Chris Hughes]

No, the best way is (range (n+1)).sum ...

[Johan Commelin]

@Kevin Buzzard Mario suggested a better way. I'll push my current file.

[Kevin Buzzard]

Oh yes I see the post now. I ignored it initially because I'd not even begun to look at the file, but I have WiFi for the next 10 minutes so I downloaded the version on GH and am now looking through it.

[Johan Commelin]

https://github.com/jcommelin/mathlib/blob/witt/algebra/witt_vector.lean#L114

[Johan Commelin]

Ok, make sure you download again (-;

[Johan Commelin]

I've all sorts of rewrites that are failing, and it is beyond me why they fail...

[Kevin Buzzard]

I see! Range is nice to look at, but summing over fin n is cool because i.2 is exactly what you need to make the equation compiler swallow it. Then you switch back to get the equation lemma you really want.

[Johan Commelin]

Yes. Pretty cool stuff, right? Kudos to Mario.

[Johan Commelin]

I feel I've made progress today.

[Johan Commelin]

But the proof is still extremely slow. And it is fragile beyond imagination.

[Kevin Buzzard]

on line 135 or so you have two different n's.

[Mario Carneiro]

that's from the first two lines. You can ignore the first n after the first line

[Johan Commelin]

Yes, I don't know why strong_induction introduces a new n

[Johan Commelin]

I'll clear the first one

[Kevin Buzzard]

Inserting repeat {sorry},end #exit on line 124 and the proof still takes forever to compile (a second or two). I can't work with Lean when it's like this. Something you're doing is taking far longer than it should, and rather than biting the bullet nowadays I try to fix it.

[Kevin Buzzard]

It's line 119

[Kevin Buzzard]

simp only [eval₂_mul, eval₂_add, eval₂_sub, eval₂_neg, eval₂_C, eval₂_X],

[Johan Commelin]

How do you figure out which line it is?

[Kevin Buzzard]

elaboration: tactic execution took 3.44s.

[Kevin Buzzard]

I just keep cutting and pasting repeat {sorry}, end #exit higher and higher up the file until I find it

[Kevin Buzzard]

Nowadays when I write Lean code I notice it straight away and deal with the problem when it appears.

[Johan Commelin]

Ok... so somehow I need to speed up that line...

[Johan Commelin]

In mathspeak it says that the eval2 is a ring homomorphism, and that it therefore commutes with mul and add.

[Johan Commelin]

And thus the ring hom can be moved "inside".

[Johan Commelin]

  rw [eval₂_mul, eval₂_C],
  simp only [eval₂_sub],
  rw eval₂_X,

[Johan Commelin]

Somehow simp only succeeds, while rw doesn't...

[Johan Commelin]

Ok, it is still really ugly... but progress: https://github.com/jcommelin/mathlib/blob/witt/algebra/witt_vector.lean#L115

[Johan Commelin]

Now I need i.property but I no longer have access to it :sad:

[Johan Commelin]

And the proof is still relatively slow.

[Johan Commelin]

Anyway, I need to go home now. See you later!

[Mario Carneiro]

After lots of testing, I think I know the problem: eval₂_* is a bad simp lemma, not because it is written incorrectly, but because it is too expensive to instantiate. It takes a second or so to figure out if one of these rules even applies, and simp has to go through tons of them at all parts of the expression

[Kevin Buzzard]

I've just been dropping these sorry,end #exit lines in near the beginning and even the rewrites are taking time. simp only [eval₂_sub] seems to take about 200ms but rw @eval₂_sub _ _ _ _ _ _ (X n) (finset.sum (finset.range n) (λ (i : ℕ), C ↑p ^ i * X_in_terms_of_W i ^ p ^ (n - i))) _ _ C _ witt_polynomial also takes about 200ms

[Kevin Buzzard]

and then rw eval₂_X takes about 600ms

[Mario Carneiro]

For me the eval2_sub proof works provided I have the foobar instance:

instance foobar : comm_ring (mv_polynomial ℕ ℚ) := by apply_instance

[Kevin Buzzard]

definition inst_1 : decidable_eq ℕ := by apply_instance
definition inst_2 : decidable_eq ℚ := by apply_instance
definition inst_3 : comm_ring ℚ := by apply_instance
definition inst_4 : decidable_eq (mv_polynomial ℕ ℚ) := by apply_instance
definition inst_5 : comm_ring (mv_polynomial ℕ ℚ) := by apply_instance
definition inst_6 : is_ring_hom (C : ℚ → (mv_polynomial ℕ ℚ)) := by apply_instance

lemma X_in_terms_of_W_prop (n : ℕ) : (X_in_terms_of_W n).eval₂ C witt_polynomial = X n :=
begin
  apply nat.strong_induction_on n,
  clear n,
  intros n H,
  rw X_in_terms_of_W_eq,
  rw [eval₂_mul, eval₂_C],
  rw @eval₂_sub ℚ (mv_polynomial ℕ ℚ) ℕ inst_1 inst_2 inst_3
    (X n)
    (finset.sum (finset.range n) (λ (i : ℕ), C ↑p ^ i * X_in_terms_of_W i ^ p ^ (n - i)))
    inst_4 inst_5 C inst_6 witt_polynomial,
  sorry,end #exit

That last rw is taking 150ms. Is that a long time for a rewrite?

[Kevin Buzzard]

I filled in every field.

[Kevin Buzzard]

and rw @eval₂_X ℚ (mv_polynomial ℕ ℚ) ℕ inst_1 inst_2 inst_3' inst_4' C inst_5' witt_polynomial n (the line after) is taking over 300ms.

[Kevin Buzzard]

definition inst_3' : comm_semiring ℚ := by apply_instance
definition inst_4' : comm_semiring (mv_polynomial ℕ ℚ) := by apply_instance
definition inst_5' : is_semiring_hom (C : ℚ → (mv_polynomial ℕ ℚ)) := by apply_instance

I thought that rw looked at the head of the expression, and it's not hard to find eval_2, there's only two possibilities, and one of them fits perfectly. I don't understand why these rewrites are taking so long.

[Johan Commelin]

That's exactly what I was thinking.

[Mario Carneiro]

By the way, in the expression (X_in_terms_of_W n).eval₂ C witt_polynomial = X n are you aware that the R variable of witt_polynomial is instantiated as Q?

[Mario Carneiro]

if you try to assert that it has type mv_polynomial ℕ R it doesn't typecheck

[Mario Carneiro]

Oh wow, this has a 1000% improvement in speed:

generalize e : eval₂ C witt_polynomial = f,
haveI : is_ring_hom f := by subst f; apply eval₂.is_ring_hom,

Most of the proof only uses that f is a ring hom. For the rest, you can use the equality to recover the eval

[Johan Commelin]

Mario, yes, I was aware of that. In the end, we want some identity over \Z. I only wrote the general definition of witt_polynomial so that I didn't constantly have to map them to other rings.

[Johan Commelin]

Ok, so I put that bit of code somewhere in the beginning of my proof? And then I get massive speedups, and afterwards it is recovered/unfolded towards the end?

[Johan Commelin]

@Mario Carneiro Does your suggestion classify as best practice or is it a fragile hack? Is this a sign that we need to improve eval2, or is there nothing to worry about?

[Mario Carneiro]

It is a hack, although not that fragile, it's just a weird workaround for inexplicable slowdown

[Mario Carneiro]

I found another weird way to speed things up:

set_option profiler true

instance eval_witt_hom : is_ring_hom (eval₂ C (witt_polynomial R)) :=
@mv_polynomial.eval₂.is_ring_hom _ _ _ _ _ _ _ _ _
  (@C.is_ring_hom R ℕ _ (λ a b, _inst_2 a b) _) _

lemma X_in_terms_of_W_prop (n : ℕ) : (X_in_terms_of_W n).eval₂ C (witt_polynomial ℚ) = X n :=
begin
  apply nat.strong_induction_on n,
  intros n H,
  rw [X_in_terms_of_W_eq],
  simp,
end

the simp application runs fine as long as you have that instance. The elaboration of eval_witt_hom takes about 500 ms written like this, but if I write _inst_2 instead of eta expanded, elaboration jumps to 8.3 s. If I use by apply_instance it takes about 1 s

[Mario Carneiro]

@Sebastian Ullrich This stuff is closer to your area of expertise than mine, although I am not sure how easy it is to separate mathlib from this issue

[Mario Carneiro]

Okay, here's a complete proof with no unreasonable slowdowns:

instance eval_witt_hom : is_ring_hom (eval₂ C (witt_polynomial R)) :=
@mv_polynomial.eval₂.is_ring_hom _ _ _ _ _ _ _ _ _
  (@C.is_ring_hom R ℕ _ (λ a b, _inst_2 a b) _) _

lemma X_in_terms_of_W_prop'
  (f : mv_polynomial ℕ ℚ → mv_polynomial ℕ ℚ) [is_ring_hom f]
  (fC : ∀ (a : ℚ), f (C a) = C a)
  (fX : ∀ (n : ℕ), f (X n) = witt_polynomial ℚ n)
  (n : ℕ) : f (X_in_terms_of_W n) = X n :=
begin
  apply nat.strong_induction_on n,
  clear n, intros n H,
  rw [X_in_terms_of_W_eq],
  simp only [is_ring_hom.map_mul f, is_ring_hom.map_sub f, fC, fX, ring_hom_sum.finset f],
  rw [finset.sum_congr rfl, (_ : witt_polynomial ℚ n -
    (finset.range n).sum (λ i, C p ^ i * X i ^ p ^ (n - i)) = C (p ^ n) * X n)],
  { rw [mul_right_comm, ← C_mul, mul_one_div_cancel, C_1, one_mul],
    exact pow_ne_zero _ (nat.cast_ne_zero.2 $ ne_of_gt pp.pos) },
  { simp [witt_polynomial, nat.sub_self],
    rw ring_hom_powers (@C ℚ ℕ _ _ _) },
  { intros i h,
    simp [is_ring_hom.map_mul f, ring_hom_powers f, fC] at h ⊢,
    rw H _ h }
end

lemma X_in_terms_of_W_prop (n : ℕ) : (X_in_terms_of_W n).eval₂ C (witt_polynomial ℚ) = X n :=
begin
  letI : is_ring_hom (@C ℚ ℕ _ _ _) := by apply_instance,
  haveI H := @eval_witt_hom _ ℚ _ _,
  have fC := eval₂_C C (witt_polynomial ℚ),
  have fX := eval₂_X C (witt_polynomial ℚ),
  revert H fC fX, generalize : eval₂ C (witt_polynomial ℚ) = f,
  introsI, exact X_in_terms_of_W_prop' f fC fX n
end

[Johan Commelin]

Wow! Thanks for your help Mario! I wouldn't have been able to come up with this myself.

[Johan Commelin]

@Mario Carneiro Is it ok that your proof explicitly mentions _inst_2? I always assumed that was "forbidden".

[Mario Carneiro]

You should see if λ a b, by apply_instance also works without slowdown. If not, you can just name the instance and refer to it

[Johan Commelin]

Ok, I'll merge this into my file as soon as I'm back at work.

[Johan Commelin]

@Mario Carneiro You also changed the definition of witt_polynomial to make the ring R explicit, didn't you?

[Mario Carneiro]

I did, it was making things a bit confusing. You don't have to

[Johan Commelin]

Is there a way to tease more information out of Lean when it gives the error command expected?

[Mario Carneiro]

that means that the parser was reset, you are between definitions or something, and you give a non-keyword

[Mario Carneiro]

Or it means you have checking visible lines mode enabled and you should scroll down to refresh the parser

[Johan Commelin]

I see... a very descriptive error message :rolling_on_the_floor_laughing:

[Kevin Buzzard]

Or it means you have checking visible lines mode enabled and you should scroll down to refresh the parser

Johan -- we're talking about the little message in the blue bar at the bottom of the VS Code window which says something like "checking visible lines and above". I constantly refer to this as "evil mode" and it used to be the case that whenever I see a student whose blue bar said this, I would tell them to click on the blue bar and change it to "checking visible files". There is a place for the "visible lines and above" choice, but for my users it causes more trouble than it solves, because it means that sometimes the answer to "there's a red line -- what is wrong with my code?" is "nothing is wrong with your code, it's just that Lean isn't reading all of it". Nowadays I just show my students how to make it say "checking visible files" by selecting File->Preferences->Settings (ctrl-, on linux), then searching for linesandabove in the default user settings, hovering over "lean.roiModeDefault": "linesAndAbove" (if it says that -- you want it to say visible, clicking the little pencil just to the left of it [thus moving the variable into the part of the settings which you can edit], and then making sure it says "lean.roiModeDefault": "visible" in user settings.

[Gabriel Ebner]

Nowadays I just show my students how to make it say "checking visible files"

BTW, this is the default now.

[Kevin Buzzard]

Thanks for switching it back Gabriel. It's fine if you know what you're doing, but experience indicated that it was confusing for new users. I love the way that you just sit there in the background occasionally making things better for me.

[Johan Commelin]

Thanks for the explanation Kevin!

[Johan Commelin]

Aaaaahrg. I'm completely stuck again!

lemma quux {A : Type*} [add_comm_group A] (n : ℕ) (f : ℕ → A) : (finset.range (n+1)).sum f = f n + (finset.range n).sum f := by simp

lemma X_in_terms_of_W_prop₂ (k : ℕ) : (witt_polynomial k).eval X_in_terms_of_W = X k :=
begin
  apply nat.strong_induction_on k,
  clear k, intros k H,
  dsimp only [witt_polynomial],
  conv
  begin
    to_lhs,
    congr, skip,
    rw quux k (λ (i : ℕ), C ↑p ^ i * X i ^ p ^ (k - i)),
  end,
  -- generalize e : eval X_in_terms_of_W = f,
  -- haveI : is_ring_hom f := by subst f; apply eval.is_ring_hom,
  -- simp only [ring_hom_sum.finset f],
  -- repeat {sorry}, end #exit
  sorry
end

[Johan Commelin]

Yesterday's trick isn't working.

[Johan Commelin]

After this sorry is removed, I think we are mostly good to go for the definition of witt vectors. Meh... I forgot that I still need to convince Lean that I actually get a polynomial over \Z instead of \Q.

[Johan Commelin]

But maybe we first need to figure out why Lean is misbehaving like a toddler...

[Johan Commelin]

I pushed the stuff that I have right now: https://github.com/jcommelin/mathlib/blob/witt/algebra/witt_vector.lean#L135

[Johan Commelin]

Ok, so I have polynomials over \Q, but actually all their coefficients lie in \Z. What is the best way to extract this polynomial over \Z? I currently have the following:

def witt_structure_int (Φ : mv_polynomial bool ℤ) (n : ℕ) : mv_polynomial (bool × ℕ) ℤ :=
finsupp.map_range rat.num (rat.coe_int_num 0) (witt_structure_rat (map int.cast Φ) n)

[Kevin Buzzard]

Your rewrite on line 144 is, for me, trying to rewrite when the goal is | X_in_terms_of_W. But if I add another skip then I see Lean trying to do this:

_inst_1 : nat.Prime,
k : ℕ,
H : ∀ (m : ℕ), m < k → eval₂ C X_in_terms_of_W (witt_polynomial m) = X m
| finset.sum (finset.range (k + 1)) (λ (i : ℕ), C ↑p ^ i * X i ^ p ^ (k - i))
scratch6.lean:145:4: error

rewrite tactic failed, did not find instance of the pattern in the target expression
  finset.sum (finset.range (k + 1)) (λ (i : ℕ), C ↑p ^ i * X i ^ p ^ (k - i))
state:
10 goals
_inst_1 : nat.Prime,
k : ℕ,
H : ∀ (m : ℕ), m < k → eval₂ C X_in_terms_of_W (witt_polynomial m) = X m
⊢ finset.sum (finset.range (k + 1)) (λ (i : ℕ), C ↑p ^ i * X i ^ p ^ (k - i)) = ?m_1

But when you set_option pp.all true I see a whole bunch of typeclass inference stuff which doesn't look like it matches up. The thing you're trying to rewrite has a whole bunch of unsolved metavariables. Your goal looks like this:

 (@finset.sum.{0 0} nat
       (@mv_polynomial.{0 0} nat rat
...

and the thing you're trying to rewrite looks like this:

  @finset.sum.{0 ?l_1} nat (@mv_polynomial.{0 ?l_1} nat ?m_2 ?m_3) ...

Maybe if you are more precise with your rewrite it might help, i.e. throw in some @s and say exactly what the type of some more things are. I am kind of wondering whether the type class inference system doesn't know enough about what your types are, and is making some bad guesses about what instances it should use.

[Kevin Buzzard]

https://gist.github.com/kbuzzard/5254103e5f33b022636a9491fb6719e9

That's the beginning of the set_option pp.all true output. The quux thing is the thing at the top. The goal is the much longer thing at the bottom, most of which I've truncated. The much longer thing at the bottom corresponds to just the first three lines of the top. Lines 3 and 50 match perfectly. Lines 1 and 2 are supposed to match with lines 16 to 49. We have a universe metavariable ?l_1 which can be zero, then a term metavariable ?m_2 which can be rat. What I'm worried about is line 2, which says that type class inference wants to prove something is an add_comm_monoid, and it's going to do this by showing it's an add_comm_group and then it will use an instance called add_comm_group.to_add_comm_monoid. But lines 25 to 42 seem to be showing that the rationals are an add_comm_monoid by showing that they're a field, and then a comm_ring, and then a comm_semiring (note that we have now diverged from the plan, because a comm_semiring isn't an add_comm_group) and then an add_comm_monoid.

Now this might not be the problem, but somehow it looks to me like it might be an obstruction to the rewrite succeeding. Can you somehow tell Lean that you're not working with ?m_2 but with rat?

[Johan Commelin]

Like so?

rw quux k (λ (i : ℕ), ((C ↑p ^ i * X i ^ p ^ (k - i)) : mv_polynomial ℕ ℚ)),

Alas, that still fails.

[Johan Commelin]

Hmm, now the output of pp.all shows an insane amount of similarities between the goal and what the rewrite offers.

[Johan Commelin]

But it is not enough. The rw is using modules :scream: whereas the goal is sane, and just works with rings.

[Kevin Buzzard]

What you're trying to rewrite: https://gist.github.com/kbuzzard/8b4048c89309808fe829c5e59caaa503

Goal: https://gist.github.com/kbuzzard/f515877383946b5eb84f03e31cb988c3

They're not the same. The question perhaps is which differences are superficial and which ones are stopping the rewrite

[Johan Commelin]

I'm scared by https://gist.github.com/kbuzzard/8b4048c89309808fe829c5e59caaa503#file-pattern-lean-L21

[Johan Commelin]

Sorry!!! I messed up. I did not have enough skips in the conv. :sob:

[Kevin Buzzard]

Didn't I mention that? ;-)

[Johan Commelin]

Hmmm, it seems to me that whenever I make any progress using simp or dsimp, afterwards everything breaks, because it cleans up to much.

[Johan Commelin]

So I find my self doing long chains of rws

[Johan Commelin]

And now I have (\lam i, f i) i. And I need f i. How do I do that without dsimp?

[Johan Commelin]

Ok, so I think this is called beta-reduction. Is there a tactic that will do beta-reduction, and nothing else?

[Johan Commelin]

Ok! "I worked my way around it."

[Johan Commelin]

All sorries are gone in this part! :octopus:

[Johan Commelin]

Now I need to figure out how to get some polynomials that are defined over Q to believe that they actually live over Z.

[Johan Commelin]

https://github.com/jcommelin/mathlib/blob/witt/algebra/witt_vector.lean#L218

[Patrick Massot]

You can have a look at https://github.com/leanprover/lean/blob/28f4143be31b7aa3c63a907be5443ca100025ef1/library/init/meta/simp_tactic.lean#L71

[Patrick Massot]

turning off everything but beta

[Kenny Lau]

I think you only need to specify that beta is turned on

[Kenny Lau]

but I'm not sure

[Patrick Massot]

I think we could have a tactic doing only this and unfolding composition (ie rw comp_app)

[Johan Commelin]

After almost a year I took another look at this code. I've almost proven the fundamental theorem about witt polynomials: https://github.com/leanprover-community/mathlib/blob/witt-vectors/src/ring_theory/witt_vector.lean

[Johan Commelin]

theorem witt_structure_int_exists_unique (Φ : mv_polynomial bool ℤ) :
  ∃! (φ : ℕ → mv_polynomial (bool × ℕ) ℤ),
  ∀ (n : ℕ), (witt_polynomial p n).eval₂ C φ =
Φ.eval₂ C (λ b : bool, ((witt_polynomial p n).rename (λ i : ℕ, (b,i)))) :=

[Johan Commelin]

https://github.com/leanprover-community/mathlib/blob/witt-vectors/src/ring_theory/witt_vector.lean#L1199

[Kevin Buzzard]

https://arxiv.org/abs/1906.03583

If you want a goal which looks accessible ;-)

[Johan Commelin]

The only sorry on which that proof depends is on https://github.com/leanprover-community/mathlib/blob/witt-vectors/src/ring_theory/witt_vector.lean#L921 and it says:

p : ℕ,
_inst_3 : nat.prime p,
ι : Type u_1,
_inst_6 : decidable_eq ι,
n : ℤ
⊢ (C n modₑ ↑p) = (C n ^ p modₑ ↑p)

[Johan Commelin]

In other words, I need little Fermat for integers that are viewed as constant polynomials in an arbitrary multi-variate polynomial ring over the integers.

[Johan Commelin]

@Kevin Buzzard I think it makes more sense to first show that Witt vectors form a ring (-;

[Johan Commelin]

(And to clean up the file.)

[Johan Commelin]

There are some extremely crazy things going on, where type class search completely messes up.

[Johan Commelin]

And what is annoying is that you can't even easily switch it off using @s. I wish I could tell Lean:
"Hey, I want to apply this lemma. Try to do that without caring about the type class instances. Just give them to me as goals."
But I'm not sure if it is easy to say that to Lean.

[Kevin Buzzard]

If you want Lean to say that then does this mean that some things are classes which shouldn't be classes?

[Johan Commelin]

Things like add_comm_monoid :stuck_out_tongue_wink:

[Johan Commelin]

It can't figure out that quotient rings are add_comm_monoid, or that quotient.mk is a semiring hom, etc.. etc...

[Johan Commelin]

Probably these issues go away with proper proof engineering... But I'm not a proof engineer.

[Mario Carneiro]

I use by apply when I get the pesky issue with inferred != unified

[Johan Commelin]

@Mario Carneiro With underscores? As in, do you then manually have to fill in the typeclasses? Or does it usually figure out all the type classes itself?

[Mario Carneiro]

no underscores

[Mario Carneiro]

just by apply foo instead of foo _ _ or @foo _ _ _ _ or whatever

[Johan Commelin]

I'll test this

[Johan Commelin]

In the course of this file, I prove:

variables (α : Type u) [decidable_eq α] [comm_ring α]
variables (p : ℕ) [nat.prime p]

lemma dvd_sub_pow_of_dvd_sub (a b : α) (h : (p : α) ∣ a - b) (k : ℕ) :
(p^(k+1) : α) ∣ a^(p^k) - b^(p^k) :=

https://github.com/leanprover-community/mathlib/blob/witt-vectors/src/ring_theory/witt_vector.lean#L261

[Johan Commelin]

This proof is currently quite long and slow.

[Johan Commelin]

But it is completely elementary maths...

[Johan Commelin]

Here is what I currently have:

local attribute [class] nat.prime
variables (α : Type u) [decidable_eq α] [comm_ring α]
variables (p : ℕ) [nat.prime p]

lemma dvd_sub_pow_of_dvd_sub (a b : α) (h : (p : α) ∣ a - b) (k : ℕ) :
  (p^(k+1) : α) ∣ a^(p^k) - b^(p^k) :=
begin
  induction k with k ih, { simpa using h }, clear h,
  simp only [nat.succ_eq_add_one],
  rcases ih with ⟨c, hc⟩,
  rw sub_eq_iff_eq_add' at hc,
  replace hc := congr_arg (λ x, x^p) hc,
  dsimp only at hc,
  rw [← pow_mul, add_pow, finset.sum_range_succ, nat.choose_self, nat.cast_one, mul_one,
    nat.sub_self, pow_zero, mul_one] at hc,
  conv { congr, skip, rw [nat.pow_succ] },
  simp only [nat.pow_eq_pow] at hc,
  rw [hc, pow_mul, add_sub_cancel'], clear hc a,
  apply dvd_sum,
  intros i hi,
  rw finset.mem_range at hi,
  rw mul_pow,
  conv { congr, skip, congr, congr, skip, rw mul_comm },
  repeat { rw mul_assoc, apply dvd_mul_of_dvd_right }, clear c b,
  norm_cast,
  apply coe_nat_dvd,
  by_cases H : i = 0,
  { subst H,
    suffices : p ^ (k + 1 + 1) ∣ (p ^ (k + 1)) ^ p, by simpa,
    rw ← nat.pow_mul,
    apply nat.pow_dvd_pow,
    refine le_trans (add_le_add_left' $ le_add_left $ le_refl _ : k + 1 + 1 ≤ k + 1 + (k + 1)) _,
    refine le_trans (le_of_eq _) (nat.mul_le_mul_left (k+1) $ (nat.prime.ge_two ‹_› : 2 ≤ p)),
    rw mul_two },
  have i_pos := nat.pos_of_ne_zero H, clear H,
  rw nat.pow_succ,
  apply mul_dvd_mul,
  { generalize H : (p^(k+1)) = b,
    have := nat.sub_pos_of_lt hi,
    conv {congr, rw ← nat.pow_one b},
    apply nat.pow_dvd_pow,
    exact this },
  exact nat.prime.dvd_choose i_pos hi ‹_›
end

[Johan Commelin]

If someone is looking for a golfing challenge... voila :up:

[Reid Barton]

It can't figure out that quotient rings are add_comm_monoid

This one in particular seems alarming

[Johan Commelin]

I've done some refactoring, and removed a bunch of sorries.

[Johan Commelin]

Witt vectors are now a comm_ring:
https://github.com/leanprover-community/mathlib/blob/witt-vectors/src/ring_theory/witt_vector.lean#L1339

[Johan Commelin]

I use by apply when I get the pesky issue with inferred != unified

@Mario Carneiro I've been trying this but is doesn't seem to work.

I've cleaned up the code quite a bit. In the course of this, those sorries returned. I have no idea what is wrong, but for some weird reason I'm pushing Leans limits.
If you could take a look at https://github.com/leanprover-community/mathlib/blob/witt-vectors/src/ring_theory/witt_vector.lean#L577 that would be great.

[Johan Commelin]

This branch only changes mv_polynomial.lean and the new file witt_vector.lean.

git pull
git checkout 38d5c12022e001a221e279f035e3cc0734c4a189 # the lean-3.4.2 of yesterday
cache-olean --fetch
git checkout witt-vectors

That should give one a working version of the branch pretty quickly.

[Johan Commelin]

To give an idea of how weird the situation is:

4 goals
p : ℕ,
_inst_3 : nat.prime p,
n : ℕ
⊢ distrib.to_has_add (ideal.quotient (ideal.span {C ↑(p ^ (n + 1))})) =
    add_semigroup.to_has_add (ideal.quotient (ideal.span {C ↑(p ^ (n + 1))}))

p : ℕ,
_inst_3 : nat.prime p,
n : ℕ
⊢ 0 * (X (n + 1) ^ p ^ (n + 1 - (n + 1)) modₑ C ↑(p ^ (n + 1))) = 0

p : ℕ,
_inst_3 : nat.prime p,
n : ℕ
⊢ is_add_monoid_hom (ideal.quotient.mk (ideal.span {C ↑(p ^ (n + 1))}))

p : ℕ,
_inst_3 : nat.prime p,
n : ℕ
⊢ is_add_monoid_hom (ideal.quotient.mk (ideal.span {C ↑(p ^ (n + 1))}))

For none of these goals the "obvious" proof works. I.e. no apply_instance or zero_mul etc...

[Mario Carneiro]

does rfl work for the first?

[Kevin Buzzard]

It does. But Johan you can see something is funny about this code. The 20 or so lines of proof of witt_polynomial_mod_pow_p are taking forever to compile on my machine. There is perhaps some gigantic monster term somewhere in there which needs to be tamed, or something is timing out somewhere...

[Kevin Buzzard]

1 goal
p : nat,
n : nat
⊢ @eq.{1}
    (@ideal.quotient.{0}
       (@mv_polynomial.{0 0} nat int
          (@comm_ring.to_comm_semiring.{0} int
             (@nonzero_comm_ring.to_comm_ring.{0} int
                (@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
       (@mv_polynomial.comm_ring.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
          (λ (a b : int), int.decidable_eq a b)
          (@nonzero_comm_ring.to_comm_ring.{0} int
             (@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
       (@ideal.span.{0}
          (@mv_polynomial.{0 0} nat int
             (@comm_ring.to_comm_semiring.{0} int
                (@nonzero_comm_ring.to_comm_ring.{0} int
                   (@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
          (@mv_polynomial.comm_ring.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
             (λ (a b : int), int.decidable_eq a b)
             (@nonzero_comm_ring.to_comm_ring.{0} int
                (@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
          (@singleton.{0 0}
             (@mv_polynomial.{0 0} nat int
                (@nonzero_comm_semiring.to_comm_semiring.{0} int
                   (@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
                      (@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
             (set.{0}
                (@mv_polynomial.{0 0} nat int
                   (@comm_ring.to_comm_semiring.{0} int
                      (@nonzero_comm_ring.to_comm_ring.{0} int
                         (@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
             (@set.has_emptyc.{0}
                (@mv_polynomial.{0 0} nat int
                   (@comm_ring.to_comm_semiring.{0} int
                      (@nonzero_comm_ring.to_comm_ring.{0} int
                         (@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
             (@set.has_insert.{0}
                (@mv_polynomial.{0 0} nat int
                   (@comm_ring.to_comm_semiring.{0} int
                      (@nonzero_comm_ring.to_comm_ring.{0} int
                         (@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
             (@mv_polynomial.C.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
                (λ (a b : int), int.decidable_eq a b)
                (@nonzero_comm_semiring.to_comm_semiring.{0} int
                   (@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
                      (@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
                (@coe.{1 1} nat int
                   (@coe_to_lift.{1 1} nat int
                      (@coe_base.{1 1} nat int
                         (@nat.cast_coe.{0} int
                            (@mul_zero_class.to_has_zero.{0} int
                               (@semiring.to_mul_zero_class.{0} int
                                  (@comm_semiring.to_semiring.{0} int
                                     (@nonzero_comm_semiring.to_comm_semiring.{0} int
                                        (@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
                                           (@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))))
                            (@monoid.to_has_one.{0} int
                               (@semiring.to_monoid.{0} int
                                  (@comm_semiring.to_semiring.{0} int
                                     (@nonzero_comm_semiring.to_comm_semiring.{0} int
                                        (@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
                                           (@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))))
                            (@distrib.to_has_add.{0} int
                               (@semiring.to_distrib.{0} int
                                  (@comm_semiring.to_semiring.{0} int
                                     (@nonzero_comm_semiring.to_comm_semiring.{0} int
                                        (@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
                                           (@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))))))
                   (@has_pow.pow.{0 0} nat nat nat.has_pow p
                      (@has_add.add.{0} nat nat.has_add n (@has_one.one.{0} nat nat.has_one))))))))
    (@has_mul.mul.{0}
       (@ideal.quotient.{0}
          (@mv_polynomial.{0 0} nat int
             (@comm_ring.to_comm_semiring.{0} int
                (@nonzero_comm_ring.to_comm_ring.{0} int
                   (@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
          (@mv_polynomial.comm_ring.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
             (λ (a b : int), int.decidable_eq a b)
             (@nonzero_comm_ring.to_comm_ring.{0} int
                (@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
          (@ideal.span.{0}
             (@mv_polynomial.{0 0} nat int
                (@comm_ring.to_comm_semiring.{0} int
                   (@nonzero_comm_ring.to_comm_ring.{0} int
                      (@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
             (@mv_polynomial.comm_ring.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
                (λ (a b : int), int.decidable_eq a b)
                (@nonzero_comm_ring.to_comm_ring.{0} int
                   (@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
             (@singleton.{0 0}
                (@mv_polynomial.{0 0} nat int
                   (@nonzero_comm_semiring.to_comm_semiring.{0} int
                      (@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
                         (@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))
                (set.{0}
                   (@mv_polynomial.{0 0} nat int
                      (@comm_ring.to_comm_semiring.{0} int
                         (@nonzero_comm_ring.to_comm_ring.{0} int
                            (@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
                (@set.has_emptyc.{0}
                   (@mv_polynomial.{0 0} nat int
                      (@comm_ring.to_comm_semiring.{0} int
                         (@nonzero_comm_ring.to_comm_ring.{0} int
                            (@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
                (@set.has_insert.{0}
                   (@mv_polynomial.{0 0} nat int
                      (@comm_ring.to_comm_semiring.{0} int
                         (@nonzero_comm_ring.to_comm_ring.{0} int
                            (@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))))
                (@mv_polynomial.C.{0 0} int nat (λ (a b : nat), nat.decidable_eq a b)
                   (λ (a b : int), int.decidable_eq a b)
                   (@nonzero_comm_semiring.to_comm_semiring.{0} int
                      (@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
                         (@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain)))
                   (@coe.{1 1} nat int
                      (@coe_to_lift.{1 1} nat int
                         (@coe_base.{1 1} nat int
                            (@nat.cast_coe.{0} int
                               (@mul_zero_class.to_has_zero.{0} int
                                  (@semiring.to_mul_zero_class.{0} int
                                     (@comm_semiring.to_semiring.{0} int
                                        (@nonzero_comm_semiring.to_comm_semiring.{0} int
                                           (@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
                                              (@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))))
[many more lines cut]

[Kevin Buzzard]

https://gist.github.com/kbuzzard/33fe4da55bcc83199306c133f6c4d865 The goal is nearly 1000 lines long. Is this inevitable when dealing with complex algebraic types or is this an indication that something is wrong?

[Mario Carneiro]

omg we need deduplicating pretty printer so much

[Mario Carneiro]

this definitely isn't inevitable in the abstract

[Mario Carneiro]

not sure how inevitable it is in lean, with the existing typeclass inference mechanism

[Kevin Buzzard]

This subterm

                            (@coe.{1 1} nat int
                               (@coe_to_lift.{1 1} nat int
                                  (@coe_base.{1 1} nat int
                                     (@nat.cast_coe.{0} int
                                        (@mul_zero_class.to_has_zero.{0} int
                                           (@semiring.to_mul_zero_class.{0} int
                                              (@comm_semiring.to_semiring.{0} int
                                                 (@nonzero_comm_semiring.to_comm_semiring.{0} int
                                                    (@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
                                                       (@euclidean_domain.to_nonzero_comm_ring.{0} int
int.euclidean_domain))))))

comes up around 10 times.

[Mario Carneiro]

that's just int.of_nat

[Kevin Buzzard]

It's about 10% of the term in terms of lines of output

[Mario Carneiro]

I don't know why it's fixated on int.euclidean_domain for deriving everything

[Kevin Buzzard]

I thought the whole point of int.of_nat was that it was some primitive which was supposed to be fast

[Mario Carneiro]

it is

[Mario Carneiro]

but that doesn't stop lean from taking a gratuitous path to get there

[Kevin Buzzard]

                  (@coe.{1 1} nat int
                      (@coe_to_lift.{1 1} nat int
                         (@coe_base.{1 1} nat int
                            (@nat.cast_coe.{0} int
                               (@mul_zero_class.to_has_zero.{0} int
                                  (@semiring.to_mul_zero_class.{0} int
                                     (@comm_semiring.to_semiring.{0} int
                                        (@nonzero_comm_semiring.to_comm_semiring.{0} int
                                           (@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
                                              (@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))))
                               (@monoid.to_has_one.{0} int
                                  (@semiring.to_monoid.{0} int
                                     (@comm_semiring.to_semiring.{0} int
                                        (@nonzero_comm_semiring.to_comm_semiring.{0} int
                                           (@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
                                              (@euclidean_domain.to_nonzero_comm_ring.{0} int int.euclidean_domain))))))
                               (@distrib.to_has_add.{0} int
                                  (@semiring.to_distrib.{0} int
                                     (@comm_semiring.to_semiring.{0} int
                                        (@nonzero_comm_semiring.to_comm_semiring.{0} int
                                           (@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
                                              (@euclidean_domain.to_nonzero_comm_ring.{0} int
int.euclidean_domain)))))))))

In fact there's something even bigger which is coming up a lot.

[Mario Carneiro]

oh wait, actually this isn't int.of_nat

[Mario Carneiro]

this is the "wrong" coe from nat to int

[Mario Carneiro]

nat.cast

[Mario Carneiro]

both of them are nat.cast

[Mario Carneiro]

try simp?

[Kevin Buzzard]

                                  (@coe.{1 1} nat int
                                     (@coe_to_lift.{1 1} nat int
                                        (@coe_base.{1 1} nat int
                                           (@nat.cast_coe.{0} int
                                              (@mul_zero_class.to_has_zero.{0} int
                                                 (@semiring.to_mul_zero_class.{0} int
                                                    (@comm_semiring.to_semiring.{0} int
                                                       (@nonzero_comm_semiring.to_comm_semiring.{0} int
                                                          (@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
                                                             (@euclidean_domain.to_nonzero_comm_ring.{0} int
                                                                int.euclidean_domain))))))
                                              (@monoid.to_has_one.{0} int
                                                 (@semiring.to_monoid.{0} int
                                                    (@comm_semiring.to_semiring.{0} int
                                                       (@nonzero_comm_semiring.to_comm_semiring.{0} int
                                                          (@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
                                                             (@euclidean_domain.to_nonzero_comm_ring.{0} int
                                                                int.euclidean_domain))))))
                                              (@distrib.to_has_add.{0} int
                                                 (@semiring.to_distrib.{0} int
                                                    (@comm_semiring.to_semiring.{0} int
                                                       (@nonzero_comm_semiring.to_comm_semiring.{0} int
                                                          (@nonzero_comm_ring.to_nonzero_comm_semiring.{0} int
                                                             (@euclidean_domain.to_nonzero_comm_ring.{0} int
                                                                int.euclidean_domain)))))))))
                                     (@has_pow.pow.{0 0} nat nat nat.has_pow p
                                        (@has_add.add.{0} nat nat.has_add n
                                           (@has_one.one.{0} nat nat.has_one)))))))))))))

There's something slightly bigger. This shows up again and again in the term.

[Kevin Buzzard]

try simp?

[waits 10 seconds] fails to simplify.

[Mario Carneiro]

are there dependencies? What is the pp form of the goal?

[Kevin Buzzard]

The gist I posted above is the pp form of the goal.

[Mario Carneiro]

I mean with regular printing

[Johan Commelin]

Sorry, I got distracted by teaching duties... I've tried dsimp, simp, erw, congr, etc... everything times out.

[Johan Commelin]

1 goal
p : ℕ,
_inst_3 : nat.prime p,
idx : Type u_4,
_inst_10 : decidable_eq idx,
Φ : mv_polynomial idx ℤ,
n : ℕ,
IH : ∀ (m : ℕ), m < n + 1 → map coe (witt_structure_int p Φ m) = witt_structure_rat p (map coe Φ) m,
this :
  eval₂ C (witt_structure_rat p (map coe Φ)) (witt_polynomial p n) =
    eval₂ C (λ (t : ℕ), map coe (witt_structure_int p Φ t)) (witt_polynomial p n)
⊢ eval₂ C (λ (x : idx × ℕ), map coe (X x ^ p))
      (eval₂ C (witt_structure_rat p (map coe Φ)) (witt_polynomial p n)) =
    eval₂ C (λ (x : idx × ℕ), map coe (X x ^ p))
      (eval₂ C (λ (t : ℕ), map coe (witt_structure_int p Φ t)) (witt_polynomial p n))

[Johan Commelin]

I posted the other 4 goals somewhere upstairs.

[Johan Commelin]

You are right that the first one could be closed by refl. Which is weird, because it was produced by congr, I think.

[Johan Commelin]

@Mario Carneiro I feel like I'm bitten by having to work explicitly with integers. But that cannot be avoided. It's crucial to show that these polynomials are defined over int, because int is the initial object in CommRing. And one cannot simply write down these polynomials over an arbitrary ring. Their coefficients are rational numbers that after a lot of work turn out to actually be integers.

[Johan Commelin]

I have no idea how to make the code faster, more well-behaved.

[Mario Carneiro]

mod_e should be a definition

[Johan Commelin]

Can you explain why?

[Mario Carneiro]

you should not make a notation for a very complex term. This increases the difference between what you see and what lean sees

[Johan Commelin]

Do you think it is a reasonable "concept" or is there a better way to do "calculations modulo [ideal/element]"

[Mario Carneiro]

You could use an equivalence relation

[Mario Carneiro]

but I don't know if I should tweak the mathematics aspects too heavily

[Mario Carneiro]

if you need ideals, so be it

[Mario Carneiro]

I think it should be a general definition though; a = b [MOD n] should be generalized

[Johan Commelin]

I think it should be a general definition though; a = b [MOD n] should be generalized

You mean from ℤ to an arbitrary ring?

[Mario Carneiro]

yes

[Mario Carneiro]

and possibly to ideals

[Mario Carneiro]

I see you needed a few variations on this

[Johan Commelin]

Do you think that mod_e is one of the reasons that the file is slow?

[Mario Carneiro]

it's a factor in the huge pp.all terms

[Mario Carneiro]

because mod_e hides an ideal.span and quotient.mk and each of these takes a bunch of typeclass args

[Johan Commelin]

But blur doesn't even use it. And there the rw this still fails... :sad:

[Mario Carneiro]

where do you start sensing problems?

[Johan Commelin]

Should we also build eval_c which is eval₂ C? I'm using eval₂ C a lot.

[Mario Carneiro]

I noticed

[Johan Commelin]

witt_structure_rat_rec_aux is slow

[Mario Carneiro]

I thought that this was one of the eval functions

[Johan Commelin]

And dvd_sub_pow_of_dvd_sub is also incredibly slow, but I think that's completely orthogonal to the others.

[Johan Commelin]

Lines 554–735 are very slow. And that's exactly the part that is hard for mathematicians. The rest is all "math-trivial".

[Johan Commelin]

It is the part where we show that the polynomials have integral coefficients. It takes most textbooks half a page :shock:

[Johan Commelin]

I thought that this was one of the eval functions

No, we don't have a wrapper for eval₂ C.

[Chris Hughes]

Is it the bind operation for mv_polynomial as a monad that you're using?

[Johan Commelin]

I think it is, yes.

[Johan Commelin]

Well, it's not exactly bind. Because I think:

bind : mv_polynomial σ (mv_polynomial σ R) R → mv_polynomial σ R

whereas

eval₂ C : (σ → mv_polynomial σ R) → mv_polynomial σ R → mv_polynomial σ R

[Reid Barton]

It is exactly bind. You're thinking of join

[Johan Commelin]

Aah...

[Johan Commelin]

Crazy names

[Reid Barton]

(Or actually it's bind with the arguments flipped)

[Reid Barton]

The idea is you are binding the result of the non-function argument to the input variable of the function argument

[Reid Barton]

join joins two layers of the monad

[Johan Commelin]

@Mario Carneiro Does this mean we should define bind and join and prove a whole bunch of API about them?

[Mario Carneiro]

sure

[Johan Commelin]

Are there other ways in which I can make my code workable?

[Mario Carneiro]

bind or join - they are interdefinable

[Johan Commelin]

They are all special cases of eval₂

[Mario Carneiro]

I don't think this will do that much to solve the problem, but it seems like a nice definition

[Johan Commelin]

But I also don't think mod_e is the main culprit. The code is also slow in parts where I don't use that.

[Mario Carneiro]

Okay, so here's a minimized version of the first suspiciously slow tactic, on L301:

import data.nat.cast algebra.group_power

lemma foo (p : ℕ) (α) [comm_ring α]
  (P : α → Prop)
  (hc : P (p *
    (@coe nat α
      (@coe_to_lift nat α
        (@coe_base nat α
          (@nat.cast_coe α
            (@mul_zero_class.to_has_zero α
              (@semiring.to_mul_zero_class α
                  (@comm_semiring.to_semiring α _)))
            _ _)))
      p))) : true :=
by try_for 10000 {simp only at hc}; sorry

[Mario Carneiro]

The profiler says all the time (about 22s) is spent in mk_eq_mp. Here's a minimized tactic from the core of simp that triggers the long running mk_eq_mp:

by do
  h ← get_local `hc,
  h_type ← infer_type h,
  pr' ← mk_app `eq.refl [h_type],
  (_, pr) ← simplify simp_lemmas.mk [] h_type {} `eq failed,
  trace pr', trace pr, trace h,
  mk_eq_mp pr h

Replacing pr with the identical hand-rolled proof pr' takes no time at all. Perhaps metavariable instantiations are involved?

[Johan Commelin]

I am totally lost at how you debug these things. The particular lemma that contains L301 seems very innocent. No weird universes or whatever.

[Mario Carneiro]

mk_eq_mp is defined in terms of mk_app, which is also slow along with mk_mapp. Even this is long running:

mk_mapp `eq.mp [h_type, h_type, pr, h]

It's not doing any inference! It's just typechecking

[Mario Carneiro]

I debug this by finding the part that is slow and then delete everything that doesn't matter until almost nothing is left

[Johan Commelin]

Is there an obvious code smell, if you look at that proof?

[Mario Carneiro]

I'm still at the stage where I figure out why lean is stupid. Once I have that I can probably derive an appropriate code smell

[Mario Carneiro]

I'm sure I've hit this bug before but I haven't investigated it in depth

[Mario Carneiro]

the operative aspect here seems to be a slightly noncanonical typeclass path

[Johan Commelin]

Thanks a lot for taking a look. I'm completely handicapped when it comes to debugging things like this. And I'm glad your thinking that Lean is stupid, instead of me being stupid :stuck_out_tongue_wink:

[Johan Commelin]

Feel free to push speed-ups upstream by the way.

[Mario Carneiro]

I don't know how useful adding workarounds on every line will be. I suspect that this issue comes up many many times in the file and that's the major problem

[Johan Commelin]

Ok

[Johan Commelin]

Feel free to push structural speed-ups upstream :grinning:

[Mario Carneiro]

Okay, it's completely barebones now. The problem arises when mk_app and friends are passed a non-canonical instance and asked to unify the results. @Sebastian Ullrich Do you know what's happening here?

set_option profiler true
open tactic

def bar (α) [semiring α] : α := sorry

lemma foo (α) [comm_ring α]
  (h : bar α = @bar α (@comm_semiring.to_semiring α _)) : true :=
by do
  h ← get_local `h,
  ht ← infer_type h,
  `(%%h1 = %%h2) ← return ht,
  ht' ← to_expr ``(%%h2 = %%h2),
  pr ← mk_app `eq.refl [ht],
  pr' ← mk_app `eq.refl [ht'],
  trace [ht, ht, pr', h],
  mk_mapp `eq.mp [ht, ht, pr', h] -- takes 23s

[Johan Commelin]

What is P doing in your example?

[Johan Commelin]

@Mario Carneiro Thanks a lot for stripping this down to a MWE. I would have never managed to do that.

[Mario Carneiro]

oops, don't need P

[Sebastien Gouezel]

Mario, if you're in a debugging mood, chasing stupid Lean behavior, you might have fun looking at https://github.com/leanprover-community/mathlib/blob/d8d25e9adb01c87c355ae1358bba431c1237e2eb/src/analysis/normed_space/operator_norm.lean#L211 (that I already mentioned some time ago, but it was in a private branch then): it looks really strange to me that Lean is not able to infer the instance.

[Sebastian Ullrich]

@Mario Carneiro No idea. Does the defeq trace show something interesting, or does that blow up Lean?

[Johan Commelin]

@Mario Carneiro @Sebastian Ullrich Do I understand correctly that it's not actually type class inference that is creating the problem? Lean should check that certain things are defeq, but it doesn't try hard enough. Is that right?

[Mario Carneiro]

@Sebastian Ullrich Aha, it does show something interesting:

[type_context.is_def_eq_detail] [5]: {add := ring.add (comm_ring.to_ring α),
 add_assoc := _,
 zero := ring.zero α (comm_ring.to_ring α),
 zero_add := _,
 add_zero := _,
 add_comm := _,
 mul := ring.mul (comm_ring.to_ring α),
 mul_assoc := _,
 one := ring.one α (comm_ring.to_ring α),
 one_mul := _,
 mul_one := _,
 left_distrib := _,
 right_distrib := _,
 zero_mul := _,
 mul_zero := _} =?= {add := comm_semiring.add comm_ring.to_comm_semiring,
 add_assoc := _,
 zero := comm_semiring.zero α comm_ring.to_comm_semiring,
 zero_add := _,
 add_zero := _,
 add_comm := _,
 mul := comm_semiring.mul comm_ring.to_comm_semiring,
 mul_assoc := _,
 one := comm_semiring.one α comm_ring.to_comm_semiring,
 one_mul := _,
 mul_one := _,
 left_distrib := _,
 right_distrib := _,
 zero_mul := _,
 mul_zero := _}
[type_context.is_def_eq_detail] [6]: ring.add =?= comm_semiring.add
[type_context.is_def_eq_detail] [6]: ring.add_assoc =?= comm_semiring.add_assoc
[type_context.is_def_eq_detail] [6]: ring.zero α =?= comm_semiring.zero α
[type_context.is_def_eq_detail] [6]: ring.zero_add =?= comm_semiring.zero_add
[type_context.is_def_eq_detail] [6]: ring.add_zero =?= comm_semiring.add_zero
[type_context.is_def_eq_detail] [6]: ring.add_comm =?= comm_semiring.add_comm
[type_context.is_def_eq_detail] [6]: ring.mul =?= comm_semiring.mul
[type_context.is_def_eq_detail] [6]: ring.mul_assoc =?= comm_semiring.mul_assoc
[type_context.is_def_eq_detail] [6]: ring.one α =?= comm_semiring.one α
[type_context.is_def_eq_detail] [6]: ring.one_mul =?= comm_semiring.one_mul
[type_context.is_def_eq_detail] [6]: ring.mul_one =?= comm_semiring.mul_one
[type_context.is_def_eq_detail] [6]: ring.left_distrib =?= comm_semiring.left_distrib
[type_context.is_def_eq_detail] [6]: ring.right_distrib =?= comm_semiring.right_distrib
[type_context.is_def_eq_detail] [6]: ring.zero_mul =?= comm_semiring.zero_mul
[type_context.is_def_eq_detail] unfold left: ring.zero_mul
[type_context.is_def_eq_detail] [7]: λ (a : α),
  have this : 0 * a + 0 = 0 * a + 0 * a, from
    eq.trans
      (eq.mpr
         (id
            (eq.trans
               ((λ (a a_1 : α) (e_1 : a = a_1) (a_2 a_3 : α) (e_2 : a_2 = a_3), congr (congr_arg eq e_1) e_2)
                  (0 * a + 0)
                  (0 * a)
                  (add_zero (0 * a))
                  ((0 + 0) * a)
                  (0 * a)
                  ((λ [c : has_mul α] (a a_1 : α) (e_2 : a = a_1) (a_2 a_3 : α) (e_3 : a_2 = a_3),
                      congr (congr_arg has_mul.mul e_2) e_3)
                     (0 + 0)
                     0
                     (add_zero 0)
                     a
                     a
                     (eq.refl a)))
               (propext (eq_self_iff_true (0 * a)))))
         trivial)
      (eq.mpr (id (eq.rec (eq.refl ((0 + 0) * a = 0 * a + 0 * a)) (right_distrib 0 0 a))) (eq.refl (0 * a + 0 * a))),
  show 0 * a = 0, from eq.symm (add_left_cancel this) =?= comm_semiring.zero_mul
[type_context.is_def_eq_detail] [8]: λ (a : α),
  have this : 0 * a + 0 = 0 * a + 0 * a, from
    eq.trans
      (eq.mpr
         (id
            (eq.trans
               ((λ (a a_1 : α) (e_1 : a = a_1) (a_2 a_3 : α) (e_2 : a_2 = a_3), congr (congr_arg eq e_1) e_2)
                  (0 * a + 0)
                  (0 * a)
                  (add_zero (0 * a))
                  ((0 + 0) * a)
                  (0 * a)
                  ((λ [c : has_mul α] (a a_1 : α) (e_2 : a = a_1) (a_2 a_3 : α) (e_3 : a_2 = a_3),
                      congr (congr_arg has_mul.mul e_2) e_3)
                     (0 + 0)
                     0
                     (add_zero 0)
                     a
                     a
                     (eq.refl a)))
               (propext (eq_self_iff_true (0 * a)))))
         trivial)
      (eq.mpr (id (eq.rec (eq.refl ((0 + 0) * a = 0 * a + 0 * a)) (right_distrib 0 0 a))) (eq.refl (0 * a + 0 * a))),
  show 0 * a = 0, from eq.symm (add_left_cancel this) =?= comm_ring.to_comm_semiring._proof_1
[type_context.is_def_eq_detail] unfold right: comm_ring.to_comm_semiring._proof_1
...

The trace goes for a very long time, but I think this is the important part. It needs to solve @ring.to_semiring α (@comm_ring.to_ring α _inst_1) =?= @comm_semiring.to_semiring α (@comm_ring.to_comm_semiring α _inst_1), so it unfolds both structures, so far so good. It starts confirming each of the fields is equal, until it hits ring.zero_mul =?= comm_semiring.zero_mul, whereupon it decides to unfold both proofs and the subproofs and so on with no end in sight.

[Sebastien Gouezel]

Can anyone explain to me how this can happen? I thought that proofs were discarded right away, and that in any case they are irrelevant so that Lean should never have to check that two proofs are the same. Does it mean that there is a bug in Lean where in some exotic situations proof irrelevance is not used while it should?

[Mario Carneiro]

proofs are not discarded, but under almost all circumstances defeq problems involving them are trivial

[Mario Carneiro]

I think there is a bug in lean somewhere here

[Johan Commelin]

Can this be debugged further inside Lean, or is the next step to run lean in some debugger like gdb?

[Mario Carneiro]

it goes to C++ from here

[Mario Carneiro]

we have to find out why the defeq trace is going into proof terms

[Johan Commelin]

@Mario Carneiro @Sebastian Ullrich Do you think the issues in this file can be reasonable fixed with some version of Lean 3? Or will we not have Witt vectors before Lean 4? (That is certainly an acceptable answer to me.)

[Johan Commelin]

@Sebastian Ullrich Just to get expectations right. Is there any hope/reason to investigate these issues in Lean 3? Or should we just wait till Lean 4?

[Johan Commelin]

More specifically, will Lean 3 have Witt vectors, or should I give up?

[Sebastian Ullrich]

@Johan Commelin @Mario Carneiro Okay, I took a look at this issue and found the following nice comment: https://github.com/leanprover/lean/blob/e6764047a14ce4383d29b2858fa9e2e246d4f13b/src/library/type_context.cpp#L1978
It looks like Leo independently found a performance issue with this code and fixed it for Lean 4: https://github.com/kha/lean4/commit/d85c30fde186b75dd00e04242fb8b05450a8daf8#diff-f56a907e917690c6815e55e0fe8540e9R798
You could try porting it to Lean 3 (using this version: https://github.com/kha/lean4/commit/f8cedb33e70c9d90c9d81a542340bba0b504f8e6), would be interesting to see if anything breaks. But I don't think it can be worked around without changing Lean.

[Johan Commelin]

@Sebastian Ullrich Thanks for looking into this!

[Kevin Buzzard]

Yes, many thanks Sebastian.

[Johan Commelin]

Mario Carneiro said:

Okay, it's completely barebones now. The problem arises when mk_app and friends are passed a non-canonical instance and asked to unify the results. Sebastian Ullrich Do you know what's happening here?

set_option profiler true
open tactic

def bar (α) [semiring α] : α := sorry

lemma foo (α) [comm_ring α]
  (h : bar α = @bar α (@comm_semiring.to_semiring α _)) : true :=
by do
  h ← get_local `h,
  ht ← infer_type h,
  `(%%h1 = %%h2) ← return ht,
  ht' ← to_expr ``(%%h2 = %%h2),
  pr ← mk_app `eq.refl [ht],
  pr' ← mk_app `eq.refl [ht'],
  trace [ht, ht, pr', h],
  mk_mapp `eq.mp [ht, ht, pr', h] -- takes 23s

Now that we have community Lean 3.10.0... can this bug be fixed? I just tried Mario's example, and it still takes 13s on my 16-threaded beastlet.

[Johan Commelin]

Sebastian Ullrich said:

Johan Commelin Mario Carneiro Okay, I took a look at this issue and found the following nice comment: https://github.com/leanprover/lean/blob/e6764047a14ce4383d29b2858fa9e2e246d4f13b/src/library/type_context.cpp#L1978
It looks like Leo independently found a performance issue with this code and fixed it for Lean 4: https://github.com/kha/lean4/commit/d85c30fde186b75dd00e04242fb8b05450a8daf8#diff-f56a907e917690c6815e55e0fe8540e9R798
You could try porting it to Lean 3 (using this version: https://github.com/kha/lean4/commit/f8cedb33e70c9d90c9d81a542340bba0b504f8e6), would be interesting to see if anything breaks. But I don't think it can be worked around without changing Lean.

Sebastian told us what needs to be done.

[Bryan Gin-ge Chen]

I have no understanding of the underlying code here but I just applied the suggested changes on top of 3.10.0c and they seem to solve the issue in Mario's example. Here's the PR: lean#211.

[Johan Commelin]

Fantastic! What time does it need now?

[Johan Commelin]

Note that the "23s" is still in your test code:

[Johan Commelin]

https://github.com/leanprover-community/lean/pull/211/files#diff-40e3406d4b81ffee1556ec817f06e661R17

[Bryan Gin-ge Chen]

Yeah, the test file probably needs more work (how do I wrap the whole thing in try_for?).

Here's a trace from 3.10.0c (tactic execution took 6s):

$ elan run leanprover-community-lean-3.10.0 lean tests/lean/run/mario_type_context.lean
parsing took 0.211ms
elaboration of bar took 0.0243ms
type checking of bar took 0.0118ms
/Users/chb/Documents/lean/lean/tests/lean/run/mario_type_context.lean:4:0: warning: declaration 'bar' uses sorry
compilation of bar took 0.172ms
decl post-processing of bar took 0.241ms
parsing took 0.567ms
type checking of foo took 0.0638ms
compilation of foo took 0.00106ms
decl post-processing of foo took 0.00109ms
elaboration: tactic compilation took 30.3ms
[bar α = bar α, bar α = bar α, eq.refl (bar α = bar α), h]
elaboration: tactic execution took 6s
num. allocated objects:  55
num. allocated closures: 55
 5998ms   100.0%   _interaction._lambda_3
 5998ms   100.0%   scope_trace
 5998ms   100.0%   tactic.mk_mapp
 5998ms   100.0%   _interaction._lambda_2
 5998ms   100.0%   tactic.istep._lambda_1
 5998ms   100.0%   tactic.istep
 5998ms   100.0%   tactic.step
 5998ms   100.0%   _interaction
elaboration of foo took 6.97s
/Users/chb/Documents/lean/lean/tests/lean/run/mario_type_context.lean:6:0: warning: declaration 'foo' uses sorry
cumulative profiling times:
        compilation 0.172ms
        decl post-processing 0.241ms
        elaboration 6.97s
        elaboration: tactic compilation 30.3ms
        elaboration: tactic execution 6s
        parsing 0.778ms
        type checking 0.0749ms

Here's a trace from the PR branch (elaboration: tactic execution took 6ms):

$ elan run local lean tests/lean/run/mario_type_context.lean
parsing took 1.64ms
elaboration of bar took 0.488ms
type checking of bar took 0.0185ms
/Users/chb/Documents/lean/lean/tests/lean/run/mario_type_context.lean:4:0: warning: declaration 'bar' uses sorry
compilation of bar took 1.08ms
decl post-processing of bar took 0.678ms
parsing took 1.41ms
type checking of foo took 0.0687ms
compilation of foo took 0.00192ms
decl post-processing of foo took 0.00173ms
elaboration: tactic compilation took 40ms
[bar α = bar α, bar α = bar α, eq.refl (bar α = bar α), h]
elaboration: tactic execution took 6ms
num. allocated objects:  55
num. allocated closures: 55
    6ms   100.0%   _interaction._lambda_3
    6ms   100.0%   scope_trace
    6ms   100.0%   tactic.mk_mapp
    6ms   100.0%   _interaction._lambda_2
    6ms   100.0%   tactic.istep._lambda_1
    6ms   100.0%   tactic.istep
    6ms   100.0%   tactic.step
    6ms   100.0%   _interaction
elaboration of foo took 78.4ms
/Users/chb/Documents/lean/lean/tests/lean/run/mario_type_context.lean:6:0: warning: declaration 'foo' uses sorry
cumulative profiling times:
        compilation 1.08ms
        decl post-processing 0.679ms
        elaboration 78.9ms
        elaboration: tactic compilation 40ms
        elaboration: tactic execution 6ms
        parsing 3.05ms
        type checking 0.086ms

[Gabriel Ebner]

@Bryan Gin-ge Chen Can you build mathlib with this change to see if it breaks anything?

[Bryan Gin-ge Chen]

Yes, let me try.

[Bryan Gin-ge Chen]

Sadly, it does seem to break mathlib. The first error is:

mathlib/src/algebra/opposites.lean:117:4: error: invalid 'or.cases_on' application, elaborator has special support for this kind of application (it is handled as an "eliminator"), but term
  eq_zero_or_eq_zero_of_mul_eq_zero (op_inj H)
must not contain metavariables because it is used to compute the motive

[Sebastien Gouezel]

Does it break badly, or is it just a few lemmas?

[Kevin Buzzard]

You might be able to just comment out that instance and the one after it...

[Kevin Buzzard]

(just to see how badly it breaks)

[Bryan Gin-ge Chen]

Good idea. Let me take a look.

[Bryan Gin-ge Chen]

The next two errors pop up at some erws in category_theory.opposites, e.g.:

mathlib/src/category_theory/opposites.lean:192:29: error: rewrite tactic failed, did not find instance of the pattern in the target expression
  (functor.op F).map ?m_3 ≫ α.app ?m_2
state:
C : Type u₁,
_inst_1 : category C,
D : Type u₂,
_inst_2 : category D,
F G : C ⥤ D,
α : functor.op F ⟶ functor.op G,
X Y : C,
f : X ⟶ Y
⊢ G.map f ≫ has_hom.hom.unop (α.app (opposite.op Y)) = has_hom.hom.unop (α.app (opposite.op X)) ≫ F.map f

cf.

@[simps] protected definition unop (α : F.op ⟶ G.op) : G ⟶ F :=
{ app         := λ X, (α.app (op X)).unop,
  naturality' := begin tidy, erw α.naturality, refl, end }
----------------------------^ error here

[Kevin Buzzard]

Clearly we have to choose between Witt vectors and opposites...

[Bryan Gin-ge Chen]

Lean seems to have gotten stupider when trying to fill in underscores:

mathlib/src/data/pfun.lean:206:20: error: don't know how to synthesize placeholder
context:
α : Type u_1,
p : Prop,
f : p → roption α,
mem_assert : ∀ {a : α} (h : p), a ∈ f h → a ∈ assert p f,
_x : p,
h : (f _x).dom
⊢ p

theorem mem_bind {f : roption α} {g : α → roption β} :
  ∀ {a b}, a ∈ f → b ∈ g a → b ∈ f.bind g
| _ _ ⟨h, rfl⟩ ⟨h₂, rfl⟩ := ⟨⟨_, _⟩, rfl⟩
-----------------------------^ error here
-- fixed by using `⟨⟨_x, h⟩, rfl⟩` instead

[Bryan Gin-ge Chen]

The build finally finished. It looks like there were < 20 errors in total. edit: see gist

[Bryan Gin-ge Chen]

(not counting the thousands of downstream sorry warnings, of course)

[Johan Commelin]

21 errors doesn't seem too bad. Thanks for all the efforts Bryan!

[Johan Commelin]

Did the build feel significantly slower or faster than usual?

[Johan Commelin]

@Bryan Gin-ge Chen What is your guesstimate? Is this approach hopeless? 21 errors sounds like it can be fixed. I was worried that every other underscore would break, and we would have to abandon this PR. But what do you think?

[Bryan Gin-ge Chen]

Hard to say re: build times since there were lots of errors. I did happen to notice the build took a long time to get through data.real.pi, but maybe that's a slow file for the normal build too.

Since this change is already in Lean 4, I do agree that we should make more of an effort with the PR.

[Johan Commelin]

@Bryan Gin-ge Chen would you mind making a PR to mathlib (with not-ready-to-merge label)?

[Johan Commelin]

But I guess I would need a modified Lean in order to contribute...

[Johan Commelin]

@Gabriel Ebner Do you think it's worth making this a lean-3.10.1?

[Bryan Gin-ge Chen]

I'd be happy to open a new PR when there's a new release (which probably should be 3.11.0 since this a "breaking" change). As of right now, I don't really have anything to PR.

[Johan Commelin]

The code at witt-vectors2 is almost compiling again.

[Johan Commelin]

It's still very ugly, and I need to fix a couple of errors.

[Johan Commelin]

Mostly related to bundling homs

[Johan Commelin]

Already with lean-3.10.0 the code is a lot faster. Looking forward to lean-3.11.0 (-;

[Gabriel Ebner]

lean-3.11.0 will unfortunately still take a while. At the moment the CI is broken, concretely the part that uploads releases. This is because the gothub tool stopped compiling.

[Johan Commelin]

Witt vectors are a ring again!
https://github.com/leanprover-community/mathlib/blob/witt-vectors2/src/ring_theory/witt_vector.lean

[Johan Commelin]

Lots of ugly code is now gone. Lean is much better!

[Johan Commelin]

(And the author maybe also improved a bit.)

[Johan Commelin]

If you want an entertaining read for a Saturday afternoon, you can scroll back in this thread to see the pains I went through about a year ago :stuck_out_tongue_wink:

[Johan Commelin]

There is still a lot of cleanup to be done. But it is now much more straightforward.

[Kevin Buzzard]

This is a huge success story for the community. Witt vectors are just an innocuous piece of algebra in some sense; they could be taught to MSc students. You ran into a brick wall for some reason when formalising them, and this led to isolating fundamental issues with Lean itself, and my understanding is that these have now been fixed.

[Johan Commelin]

One thing that is really annoying, and dissapointing is that there are a lot of convert ring_hom.ext_int _ _ that can't be turned into apply. (This is saying that (f g : int →+* R) implies f = g.)

[Kenny Lau]

@Johan Commelin if I were to define (a ^ p - a) / p in Lean I would use the integer division and then separately prove that p \| (a ^ p - a)

[Kenny Lau]

sure we can pass through \Q but that wouldn't be necessary

[Kenny Lau]

could we do the same thing for the Witt polynomials?

[Kenny Lau]

i.e. use integer division instead of passing through \Q

[Johan Commelin]

I don't think it will make life easier...

[Kenny Lau]

@Johan Commelin have you looked at this construction of (universal) Witt vectors?

[Kenny Lau]

where the set is 1+TA[[T]], the addition is "power series multiplication", and the multiplication is "coefficient-wise multiplication (aka Hadamard product)"

[Johan Commelin]

No I haven't. I'll do that when I have time again (-;

[Kenny Lau]

correction: it's only Hadamard product when one (or both) of the multiplicands is of the form (1-aT)^-1 = sum a^i T^i

[Johan Commelin]

Together with @Rob Lewis I've finished (as in, sorry-free, not cleaned up yet) the ring isomorphism witt_vector p (zmod p) →+* Z_[p] .
Expect some PR soonish (-;

[Kenny Lau]

how did you define the Teichmuller lift?

[Johan Commelin]

def teichmuller_fun (r : R) : 𝕎 R
| 0 := r
| (n+1) := 0

[Johan Commelin]

noncomputable def teichmuller : R →* 𝕎 R :=
{ to_fun := teichmuller_fun p,
  map_one' :=
  begin
    ext ⟨⟩,
    { rw one_coeff_zero, refl },
    { rw one_coeff_pos _ _ _ (nat.succ_pos n), refl }
  end,
  map_mul' :=
  begin
    intros x y,
    rcases counit_surjective R x with ⟨x, rfl⟩,
    rcases counit_surjective R y with ⟨y, rfl⟩,
    simp only [← map_teichmuller_fun, ← ring_hom.map_mul, teichmuller_mul_aux₂],
  end }

[Johan Commelin]

@Kenny Lau We have Teichmuller, Verschiebung, and Frobenius.

[Johan Commelin]

Frobenius isn't a ring hom yet, but that shouldn't be too hard.

[Adam Topaz]

Is Ver additive?

[Johan Commelin]

Yes

[Kenny Lau]

but you don't need Techimuller (in Zp) to define the isom?

[Johan Commelin]

Nope

[Johan Commelin]

W (F_p) is the projective limit of truncated witt vector rings, which have cardinality p ^ n.

[Johan Commelin]

And 1 has order p ^ n in those rings. Hence done.

[Johan Commelin]

The other proof is too analytical for me. (I'm scared of tsum.)

[Kenny Lau]

this sounds a bit suspicious. I mean, what is ((2, 0, 0, ...) : W (F_p)) sent to?

[Johan Commelin]

What do you mean "suspicious"?

We have a freaking formal proof, lol

[Johan Commelin]

   406 src/ring_theory/witt_vector/basic.lean
    90 src/ring_theory/witt_vector/compare.lean
   265 src/ring_theory/witt_vector/frobenius.lean
   145 src/ring_theory/witt_vector/ideal.lean
   155 src/ring_theory/witt_vector/init_tail.lean
    90 src/ring_theory/witt_vector/is_poly.lean
   108 src/ring_theory/witt_vector/mul_p.lean
   549 src/ring_theory/witt_vector/structure_polynomial.lean
    94 src/ring_theory/witt_vector/teichmuller.lean
   488 src/ring_theory/witt_vector/truncated2.lean
   166 src/ring_theory/witt_vector/verschiebung.lean
   330 src/ring_theory/witt_vector/witt_polynomial.lean
   631 src/ring_theory/witt_vector/witt_vector_preps.lean
  3517 total

[Johan Commelin]

Anyway, if you have a ring that is the projective limit of rings R n, and R n has cardinality p ^ n, and 1 : R n has order p ^ n, then this projective limit is isomorphic to Z_p.

[Johan Commelin]

That's not too surprising, right?

[Johan Commelin]

But of course this isom doesn't tell you where Teichmuller lifts are mapped.

[Johan Commelin]

It would be a nice application of Hensel's lemma. But I would like a better API for Henselian rings first.

[Kenny Lau]

why does 1 have order p^n?

[Adam Topaz]

additive order.

[Kenny Lau]

yeah, why does 1 have additive order p^n?

[Johan Commelin]

lemma frobenius_fun_verschiebung (x : 𝕎 R) :
  frobenius_fun (verschiebung x) = x * p :=
congr_fun (frobenius_fun_comp_verschiebung p) x

lemma verschiebung_zmod (x : 𝕎 (zmod p)) :
  verschiebung x = x * p :=
begin
  rw [← frobenius_fun_verschiebung, frobenius_fun_zmodp],
end

-- this should be true not just for `char_p R p` but for general `nontrivial R`.
lemma coeff_p_pow [char_p R p] (i : ℕ) : is_unit ((p ^ i : 𝕎 R).coeff i) :=
begin
  induction i with i h,
  { simp only [one_coeff_zero, ne.def, pow_zero, is_unit_one] },
  { rw [pow_succ', ← frobenius_fun_verschiebung, coeff_frobenius_fun_char_p, verschiebung_coeff_succ],
    exact is_unit_pow p h, }
end

[Johan Commelin]

The i-th coefficient of p ^ i is a unit. So p ^ i is nonzero in the n-truncated witt vectors, for i < n.

[Kenny Lau]

aha

[Kevin Buzzard]

There's some truncated valuation from W_n(k) to {0,1,...,n-1,top} which has the right behaviour. Unfortunately the corresponding multiplicative object is not a group with zero so we can't use lean's valuation stuff I don't think

[Reid Barton]

I don't have anything intelligent to say about this but this 𝕎 letter looks very cool

[Adam Topaz]

Kevin Buzzard said:

There's some truncated valuation from W_n(k) to {0,1,...,n-1,top} which has the right behaviour. Unfortunately the corresponding multiplicative object is not a group with zero so we can't use lean's valuation stuff I don't think

Isn't this a comm_monoid_with_zero?

[Adam Topaz]

Well, rather $q^{\{0,1,\ldots,n-1,\mathrm{top}\}}$ is :)

[Kevin Buzzard]

Sure -- but valuations take values in a linear_ordered_comm_group_with_zero right now.

[Adam Topaz]

Right. Now I'm thinking it might be really fun to define valuations as morphisms of hypperrings.

[Adam Topaz]

Since $\{0,1,\ldots,n-1,top\}$ is a quotient of the "tropical" hyperring $\mathbb{N}$, and the inverse image of the "ideal" defining this quotient is exactly the ideal in $\mathbb{Z}_p$ which you need to quotient out by to get $\mathbb{Z}/p^n$.

[Johan Commelin]

@Rob Lewis wrote the witt_simp tactic, which allows us to prove in 4 lines:

/-- The “product formula” for Frobenius and Verschiebung. -/
lemma verschiebung_mul_frobenius (x y : 𝕎 R) :
  verschiebung (x * frobenius y) = verschiebung x * y :=
begin
  apply is_poly₂.ext'
    (verschiebung_is_poly.comp₂ ((mul_is_poly₂ p).comp_right (frobenius_is_poly p)))
    ((mul_is_poly₂ p).comp_left verschiebung_is_poly),
  rintro ⟨⟩; witt_simp [mul_assoc]
end

On proving such identities, Hazewinkel wrote:

There are pitfalls in calculating with ghost components as is done here. Such a calculation gives a valid proof of an identity or something else only if it is a universal calculation; that is, makes no use of any properties beyond those that follow from the axioms for a unital commutative ring only.

Note that Rob wrote the tactic after we had 2 or 3 of such proofs done, but before I attempted to prove the product formula above.

It doesn't really do the theory of commutative rings, but we can get pretty close to “universal calculations” and have the short proofs that you would expect on paper.

[Rob Lewis]

@Johan Commelin and I have written a paper about this project! http://robertylewis.com/files/witt-vectors.pdf

We'd love to hear if you have any comments about it.

[Kevin Buzzard]

line 399 do you really mean R : Type and not R : Type u? Not that this will cause any problems with mathematical applications of course.

[Rob Lewis]

That line is taking advantage of the one right before it: the code snippet has been slightly edited for the sake of presentation!

[Rob Lewis]

It would be the only universe mentioned anywhere in the paper, either we'd have to give a totally irrelevant explanation or it would look like a typo.

[Johan Commelin]

#4236 is the first real PR on Witt vectors

[Johan Commelin]

Finally after 1.5 years or something... a first PR :grinning:

[Johan Commelin]

#4268 is the next one. Brace yourself, this is the ugliest part. We need to show that some polynomials are integral, and it's just a nasty job.

[Rob Lewis]

There's now an improved draft of our paper on arxiv: https://arxiv.org/abs/2010.02595

[Patrick Massot]

Oops I missed the opportunity to comment because I wanted to find time to read carefully. The only comment I had after a very quick read was that the section about specialized tactics was frustrating because it was hard to understand what the tactics were doing and there were no hint about how to implement them.

[Rob Lewis]

Luckily we've improved that section quite a bit, I think, although it's still not full of implementation details. Since the math is enough to scare off most of our readers it seemed better not to lose the rest with a bunch of metaprogramming talk!

[Patrick Massot]

The approach we used in the perfectoid spaces paper was: the fact the set of potential readers is empty is a feature, it shows we are doing something really new.

[Jasmin Blanchette]

The typesetting looks great! You must have worked hard.

[Rob Lewis]

Pay no attention to the column break on p7

[Jasmin Blanchette]

Sure. Which page did you say? ;)

[Patrick Massot]

What happened to the real Johan? He wouldn't let that page break happen.

[Rob Lewis]

The bigger question is, what happened to the arxiv tex install, because we built the paper in four different local environments and they all looked right

[Ruben Van de Velde]

There seems to be a stray "S" at the end of the Frobenius section on page 10

[Johan Commelin]

Hooray, another Witt vector PR was merged. The next one is #4332 and it will tell mathlib the ring structure on Witt vectors.

[Johan Commelin]

It's 475 lines of code, features two aux tactics, and a lot of comments.

[Johan Commelin]

I've looked whether I could naturally split this into two smaller PRs, but there isn't an obvious point to split the PR

[Johan Commelin]

Once this PR is merged, the fun will start! As in: no more crazy hard long computations, but juicy tactics that give unexpected results.

[Johan Commelin]

Hmm, I think I did find a way to split the PR.

[Johan Commelin]

#4693 should now be reviewed before #4332. This new PR is rather easy. It moves a bunch of stuff from an old file to a new file.

[Johan Commelin]

I've golfed away more than a 100 lines from #4694

[Johan Commelin]

I think this is now a pretty cute and readable explanation of why Witt vectors are a ring. (And it includes two marvelous helper tactics, thanks to Rob.)

[Johan Commelin]

A happy status update from the Witt project. As you may have heard, our paper got accepted at CPP21. We're very happy about that.

All contents of the Witt project have now been PR'd. The comparison isomorphism between $W(\mathbb{F}_p)$ and $\mathbb{Z}_p$ is #5164
It depends on 4 other PRs. There are currently 6 open PRs from the project (I opened 5 of them this morning). 3 PRs are unblocked, 3 are blocked by others.
The most technical one is #4838 on the Frobenius operator. (That's also the oldest PR, and blocking two of the others, among which the comparison isom.)

[Filippo A. E. Nuccio]

@Johan Commelin What is the state of the art of the proof that $\mathbb{W}(R)$ is the projective limit of truncated Witt vectors on $R$? I read here https://leanprover-community.github.io/mathlib_docs/ring_theory/witt_vector/truncated.html that this will be done in future work, and I was wondering if someone (you and @Rob Lewis ?) is actively working on this.

[Johan Commelin]

@Filippo A. E. Nuccio there's an open PR

[Johan Commelin]

it's about 200 of lines (waiting for review, hint) :stuck_out_tongue_wink:

[Filippo A. E. Nuccio]

Johan Commelin said:

Filippo A. E. Nuccio there's an open PR

Oh great, I'll have a look.

[Filippo A. E. Nuccio]

Johan Commelin said:

it's about 200 of lines (waiting for review, hint) :stuck_out_tongue_wink:

I guess you are speaking about #5162, right?

[Johan Commelin]

Nope, it's #5163

[Johan Commelin]

@Filippo A. E. Nuccio and #5164 shows that $\mathbb{W}(\mathbb{F}_p) = \mathbb{Z}_p$.

[Johan Commelin]

The last Witt PR has been kicked onto the queue! Many thanks to all the reviewers! That certainly improved the code!