# Zulip Chat Archive

## Stream: maths

### Topic: witt vectors

#### Johan Commelin (Jul 24 2018 at 14:52):

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

#### Johan Commelin (Jul 24 2018 at 14:52):

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

#### Johan Commelin (Jul 24 2018 at 14:53):

In the final lemma there are a bunch of `sorry`

s. The proof is extremely slow, and I am continuously struggling with deterministic timeouts.

#### Johan Commelin (Jul 24 2018 at 14:53):

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

#### Johan Commelin (Jul 24 2018 at 14:55):

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

#### Johan Commelin (Jul 24 2018 at 14:58):

(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 (Jul 24 2018 at 16:07):

In the final lemma there are a bunch of

`sorry`

s. 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 (Jul 24 2018 at 16:26):

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 (Jul 24 2018 at 16:27):

Did you see the `1 <= k <= n`

example? That one seemed to debate some discussion from the experts

#### Kevin Buzzard (Jul 24 2018 at 16:28):

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 (Jul 25 2018 at 07:13):

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 (Jul 25 2018 at 08:53):

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 (Aug 07 2018 at 10:07):

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 (Aug 07 2018 at 11:00):

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 (Aug 07 2018 at 11:01):

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

#### Mario Carneiro (Aug 07 2018 at 11:03):

oh, good call

#### Mario Carneiro (Aug 07 2018 at 11:03):

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

or `field`

#### Kevin Buzzard (Aug 07 2018 at 11:06):

This has happened to me so many times :-)

#### Kevin Buzzard (Aug 07 2018 at 11:07):

"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 (Aug 07 2018 at 11:08):

heh, I remember so many questions from you like that

#### Johan Commelin (Aug 07 2018 at 11:36):

I'm slowly making progress... `conv`

is still confusing me.

#### Johan Commelin (Aug 07 2018 at 11:37):

`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 (Aug 07 2018 at 11:38):

But there is clearly a lambda in there...

#### Johan Commelin (Aug 07 2018 at 11:46):

Ok, I navigated to the lambda by hand.

#### Johan Commelin (Aug 07 2018 at 11:47):

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

#### Johan Commelin (Aug 07 2018 at 11:47):

Outside the `conv`

, Lean found those instances without any trouble.

#### Johan Commelin (Aug 07 2018 at 11:47):

Is this a known issue?

#### Kevin Buzzard (Aug 07 2018 at 12:34):

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 (Aug 07 2018 at 12:42):

"I worked my way around it..."

#### Johan Commelin (Aug 07 2018 at 12:50):

@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 (Aug 07 2018 at 12:51):

I fought the mess (and the mess won)

#### Mario Carneiro (Aug 07 2018 at 12:52):

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 (Aug 07 2018 at 12:53):

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

#### Johan Commelin (Aug 07 2018 at 12:55):

Ok. The answer is: I've never used `finset.range`

before, and didn't know about it.

#### Kevin Buzzard (Aug 07 2018 at 13:02):

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 (Aug 07 2018 at 13:03):

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

#### Kevin Buzzard (Aug 07 2018 at 13:03):

(even if they look refl)

#### Johan Commelin (Aug 07 2018 at 13:05):

@Mario Carneiro Ok, in the definition after the `witt_polynomial`

I am using `i.2`

.

#### Johan Commelin (Aug 07 2018 at 13:06):

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

#### Mario Carneiro (Aug 07 2018 at 13:06):

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

#### Mario Carneiro (Aug 07 2018 at 13:12):

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 (Aug 07 2018 at 13:12):

@Kevin Buzzard Hey look, a nontrivial equation lemma

#### Johan Commelin (Aug 07 2018 at 13:14):

Thanks!

#### Johan Commelin (Aug 07 2018 at 13:15):

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

#### Kevin Buzzard (Aug 07 2018 at 14:02):

`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 (Aug 07 2018 at 14:03):

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

#### Johan Commelin (Aug 07 2018 at 14:04):

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

#### Kevin Buzzard (Aug 07 2018 at 14:05):

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 (Aug 07 2018 at 14:05):

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

#### Johan Commelin (Aug 07 2018 at 14:05):

Ok, make sure you download again (-;

#### Johan Commelin (Aug 07 2018 at 14:06):

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

#### Kevin Buzzard (Aug 07 2018 at 14:09):

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 (Aug 07 2018 at 14:10):

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

#### Johan Commelin (Aug 07 2018 at 14:11):

I feel I've made progress today.

#### Johan Commelin (Aug 07 2018 at 14:11):

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

#### Kevin Buzzard (Aug 07 2018 at 14:12):

on line 135 or so you have two different `n`

's.

#### Mario Carneiro (Aug 07 2018 at 14:13):

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

after the first line

#### Johan Commelin (Aug 07 2018 at 14:13):

Yes, I don't know why `strong_induction`

introduces a new `n`

#### Johan Commelin (Aug 07 2018 at 14:13):

I'll clear the first one

#### Kevin Buzzard (Aug 07 2018 at 14:16):

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 (Aug 07 2018 at 14:17):

It's line 119

#### Kevin Buzzard (Aug 07 2018 at 14:17):

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

#### Johan Commelin (Aug 07 2018 at 14:18):

How do you figure out which line it is?

#### Kevin Buzzard (Aug 07 2018 at 14:18):

`elaboration: tactic execution took 3.44s`

.

#### Kevin Buzzard (Aug 07 2018 at 14:18):

I just keep cutting and pasting `repeat {sorry}, end #exit`

higher and higher up the file until I find it

#### Kevin Buzzard (Aug 07 2018 at 14:18):

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

#### Johan Commelin (Aug 07 2018 at 14:19):

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

#### Johan Commelin (Aug 07 2018 at 14:20):

In mathspeak it says that the `eval2`

is a ring homomorphism, and that it therefore commutes with mul and add.

#### Johan Commelin (Aug 07 2018 at 14:20):

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

#### Johan Commelin (Aug 07 2018 at 14:23):

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

#### Johan Commelin (Aug 07 2018 at 14:23):

Somehow `simp only`

succeeds, while `rw`

doesn't...

#### Johan Commelin (Aug 07 2018 at 15:11):

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

#### Johan Commelin (Aug 07 2018 at 15:12):

Now I need `i.property`

but I no longer have access to it :sad:

#### Johan Commelin (Aug 07 2018 at 15:12):

And the proof is still relatively slow.

#### Johan Commelin (Aug 07 2018 at 15:12):

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

#### Mario Carneiro (Aug 07 2018 at 15:24):

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 (Aug 07 2018 at 15:39):

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 (Aug 07 2018 at 15:39):

and then `rw eval₂_X`

takes about 600ms

#### Mario Carneiro (Aug 07 2018 at 16:01):

For me the `eval2_sub`

proof works provided I have the `foobar`

instance:

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

#### Kevin Buzzard (Aug 07 2018 at 16:15):

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 (Aug 07 2018 at 16:16):

I filled in every field.

#### Kevin Buzzard (Aug 07 2018 at 16:23):

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 (Aug 07 2018 at 16:25):

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 (Aug 07 2018 at 16:30):

That's exactly what I was thinking.

#### Mario Carneiro (Aug 07 2018 at 16:31):

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 (Aug 07 2018 at 16:33):

if you try to assert that it has type `mv_polynomial ℕ R`

it doesn't typecheck

#### Mario Carneiro (Aug 07 2018 at 16:54):

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 (Aug 07 2018 at 17:13):

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 (Aug 07 2018 at 17:14):

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 (Aug 07 2018 at 17:36):

@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 (Aug 08 2018 at 02:32):

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

#### Mario Carneiro (Aug 08 2018 at 02:36):

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 (Aug 08 2018 at 02:39):

@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 (Aug 08 2018 at 04:22):

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 (Aug 08 2018 at 05:00):

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

#### Johan Commelin (Aug 08 2018 at 05:03):

@Mario Carneiro Is it ok that your proof explicitly mentions `_inst_2`

? I always assumed that was "forbidden".

#### Mario Carneiro (Aug 08 2018 at 05:05):

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 (Aug 08 2018 at 05:06):

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

#### Johan Commelin (Aug 08 2018 at 06:32):

@Mario Carneiro You also changed the definition of `witt_polynomial`

to make the ring `R`

explicit, didn't you?

#### Mario Carneiro (Aug 08 2018 at 06:32):

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

#### Johan Commelin (Aug 08 2018 at 07:10):

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

?

#### Mario Carneiro (Aug 08 2018 at 07:13):

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

#### Mario Carneiro (Aug 08 2018 at 07:13):

Or it means you have `checking visible lines`

mode enabled and you should scroll down to refresh the parser

#### Johan Commelin (Aug 08 2018 at 07:19):

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

#### Kevin Buzzard (Aug 08 2018 at 09:00):

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 (Aug 08 2018 at 09:03):

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

BTW, this is the default now.

#### Kevin Buzzard (Aug 08 2018 at 09:19):

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 (Aug 08 2018 at 09:25):

Thanks for the explanation Kevin!

#### Johan Commelin (Aug 08 2018 at 11:14):

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 (Aug 08 2018 at 11:14):

Yesterday's trick isn't working.

#### Johan Commelin (Aug 08 2018 at 11:18):

~~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 (Aug 08 2018 at 11:19):

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

#### Johan Commelin (Aug 08 2018 at 11:22):

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

#### Johan Commelin (Aug 08 2018 at 11:40):

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 (Aug 08 2018 at 12:02):

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 (Aug 08 2018 at 12:29):

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 (Aug 08 2018 at 12:32):

Like so?

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

Alas, that still fails.

#### Johan Commelin (Aug 08 2018 at 12:41):

Hmm, now the output of `pp.all`

shows an insane amount of similarities between the goal and what the rewrite offers.

#### Johan Commelin (Aug 08 2018 at 12:42):

But it is not enough. The `rw`

is using modules :scream: whereas the goal is sane, and just works with rings.

#### Kevin Buzzard (Aug 08 2018 at 12:44):

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 (Aug 08 2018 at 12:46):

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

#### Johan Commelin (Aug 08 2018 at 12:49):

Sorry!!! I messed up. I did not have enough `skip`

s in the `conv`

. :sob:

#### Kevin Buzzard (Aug 08 2018 at 13:03):

Didn't I mention that? ;-)

#### Johan Commelin (Aug 08 2018 at 13:21):

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 (Aug 08 2018 at 13:21):

So I find my self doing long chains of `rw`

s

#### Johan Commelin (Aug 08 2018 at 13:22):

And now I have `(\lam i, f i) i`

. And I need `f i`

. How do I do that without `dsimp`

?

#### Johan Commelin (Aug 08 2018 at 13:25):

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

#### Johan Commelin (Aug 08 2018 at 13:34):

Ok! "I worked my way around it."

#### Johan Commelin (Aug 08 2018 at 13:35):

All sorries are gone in this part! :octopus:

#### Johan Commelin (Aug 08 2018 at 13:35):

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 (Aug 08 2018 at 13:35):

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

#### Patrick Massot (Aug 08 2018 at 13:37):

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

#### Patrick Massot (Aug 08 2018 at 13:37):

turning off everything but beta

#### Kenny Lau (Aug 08 2018 at 13:40):

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

#### Kenny Lau (Aug 08 2018 at 13:41):

but I'm not sure

#### Patrick Massot (Aug 08 2018 at 13:42):

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

)

#### Johan Commelin (Jun 13 2019 at 14:39):

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 (Jun 13 2019 at 14:40):

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 (Jun 13 2019 at 14:40):

#### Kevin Buzzard (Jun 13 2019 at 14:40):

https://arxiv.org/abs/1906.03583

If you want a goal which looks accessible ;-)

#### Johan Commelin (Jun 13 2019 at 14:41):

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 (Jun 13 2019 at 14:42):

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 (Jun 13 2019 at 14:42):

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

#### Johan Commelin (Jun 13 2019 at 14:42):

(And to clean up the file.)

#### Johan Commelin (Jun 13 2019 at 14:43):

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

#### Johan Commelin (Jun 13 2019 at 14:44):

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 (Jun 13 2019 at 15:04):

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

#### Johan Commelin (Jun 13 2019 at 15:14):

Things like `add_comm_monoid`

:stuck_out_tongue_wink:

#### Johan Commelin (Jun 13 2019 at 15:15):

It can't figure out that quotient rings are `add_comm_monoid`

, or that `quotient.mk`

is a semiring hom, etc.. etc...

#### Johan Commelin (Jun 13 2019 at 15:15):

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

#### Mario Carneiro (Jun 13 2019 at 15:40):

I use `by apply`

when I get the pesky issue with inferred != unified

#### Johan Commelin (Jun 13 2019 at 17:38):

@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 (Jun 13 2019 at 18:35):

no underscores

#### Mario Carneiro (Jun 13 2019 at 18:36):

just `by apply foo`

instead of `foo _ _`

or `@foo _ _ _ _`

or whatever

#### Johan Commelin (Jun 13 2019 at 18:44):

I'll test this

#### Johan Commelin (Jun 13 2019 at 18:48):

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) :=

#### Johan Commelin (Jun 13 2019 at 18:48):

This proof is currently quite long and slow.

#### Johan Commelin (Jun 13 2019 at 18:48):

But it is completely elementary maths...

#### Johan Commelin (Jun 13 2019 at 18:49):

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 (Jun 13 2019 at 18:49):

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

#### Reid Barton (Jun 13 2019 at 20:10):

It can't figure out that quotient rings are

`add_comm_monoid`

This one in particular seems alarming

#### Johan Commelin (Jun 15 2019 at 18:32):

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

#### Johan Commelin (Jun 15 2019 at 18:32):

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 (Jun 18 2019 at 07:40):

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 (Jun 18 2019 at 07:43):

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 (Jun 18 2019 at 08:05):

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 (Jun 18 2019 at 08:06):

does rfl work for the first?

#### Kevin Buzzard (Jun 18 2019 at 08:24):

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 (Jun 18 2019 at 08:27):

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 (Jun 18 2019 at 08:29):

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 (Jun 18 2019 at 08:29):

omg we need deduplicating pretty printer so much

#### Mario Carneiro (Jun 18 2019 at 08:30):

this definitely isn't inevitable in the abstract

#### Mario Carneiro (Jun 18 2019 at 08:30):

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

#### Kevin Buzzard (Jun 18 2019 at 08:30):

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 (Jun 18 2019 at 08:31):

that's just `int.of_nat`

#### Kevin Buzzard (Jun 18 2019 at 08:31):

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

#### Mario Carneiro (Jun 18 2019 at 08:32):

I don't know why it's fixated on `int.euclidean_domain`

for deriving everything

#### Kevin Buzzard (Jun 18 2019 at 08:32):

I thought the whole point of `int.of_nat`

was that it was some primitive which was supposed to be fast

#### Mario Carneiro (Jun 18 2019 at 08:32):

it is

#### Mario Carneiro (Jun 18 2019 at 08:33):

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

#### Kevin Buzzard (Jun 18 2019 at 08:33):

(@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 (Jun 18 2019 at 08:34):

oh wait, actually this isn't `int.of_nat`

#### Mario Carneiro (Jun 18 2019 at 08:34):

this is the "wrong" coe from nat to int

#### Mario Carneiro (Jun 18 2019 at 08:34):

`nat.cast`

#### Mario Carneiro (Jun 18 2019 at 08:34):

both of them are `nat.cast`

#### Mario Carneiro (Jun 18 2019 at 08:34):

try simp?

#### Kevin Buzzard (Jun 18 2019 at 08:34):

(@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 (Jun 18 2019 at 08:35):

try simp?

[waits 10 seconds] fails to simplify.

#### Mario Carneiro (Jun 18 2019 at 08:38):

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

#### Kevin Buzzard (Jun 18 2019 at 08:39):

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

#### Mario Carneiro (Jun 18 2019 at 08:55):

I mean with regular printing

#### Johan Commelin (Jun 18 2019 at 08:56):

Sorry, I got distracted by teaching duties... I've tried `dsimp`

, `simp`

, `erw`

, `congr`

, etc... everything times out.

#### Johan Commelin (Jun 18 2019 at 08:56):

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 (Jun 18 2019 at 08:56):

I posted the other 4 goals somewhere upstairs.

#### Johan Commelin (Jun 18 2019 at 08:56):

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 (Jun 18 2019 at 09:10):

@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 (Jun 18 2019 at 09:11):

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

#### Mario Carneiro (Jun 18 2019 at 09:19):

`mod_e`

should be a definition

#### Johan Commelin (Jun 18 2019 at 09:20):

Can you explain why?

#### Mario Carneiro (Jun 18 2019 at 09:21):

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 (Jun 18 2019 at 09:21):

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

#### Mario Carneiro (Jun 18 2019 at 09:21):

You could use an equivalence relation

#### Mario Carneiro (Jun 18 2019 at 09:22):

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

#### Mario Carneiro (Jun 18 2019 at 09:22):

if you need ideals, so be it

#### Mario Carneiro (Jun 18 2019 at 09:23):

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

should be generalized

#### Johan Commelin (Jun 18 2019 at 09:24):

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 (Jun 18 2019 at 09:24):

yes

#### Mario Carneiro (Jun 18 2019 at 09:24):

and possibly to ideals

#### Mario Carneiro (Jun 18 2019 at 09:25):

I see you needed a few variations on this

#### Johan Commelin (Jun 18 2019 at 09:26):

Do you think that `mod_e`

is one of the reasons that the file is slow?

#### Mario Carneiro (Jun 18 2019 at 09:26):

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

#### Mario Carneiro (Jun 18 2019 at 09:26):

because `mod_e`

hides an `ideal.span`

and `quotient.mk`

and each of these takes a bunch of typeclass args

#### Johan Commelin (Jun 18 2019 at 09:27):

But `blur`

doesn't even use it. And there the `rw this`

still fails... :sad:

#### Mario Carneiro (Jun 18 2019 at 09:27):

where do you start sensing problems?

#### Johan Commelin (Jun 18 2019 at 09:27):

Should we also build `eval_c`

which is `eval₂ C`

? I'm using `eval₂ C`

a lot.

#### Mario Carneiro (Jun 18 2019 at 09:28):

I noticed

#### Johan Commelin (Jun 18 2019 at 09:28):

`witt_structure_rat_rec_aux`

is slow

#### Mario Carneiro (Jun 18 2019 at 09:28):

I thought that this was one of the eval functions

#### Johan Commelin (Jun 18 2019 at 09:29):

And `dvd_sub_pow_of_dvd_sub`

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

#### Johan Commelin (Jun 18 2019 at 09:30):

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 (Jun 18 2019 at 09:30):

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

#### Johan Commelin (Jun 18 2019 at 09:32):

I thought that this was one of the eval functions

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

.

#### Chris Hughes (Jun 18 2019 at 09:35):

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

#### Johan Commelin (Jun 18 2019 at 10:01):

I think it is, yes.

#### Johan Commelin (Jun 18 2019 at 12:45):

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 (Jun 18 2019 at 12:49):

It is exactly `bind`

. You're thinking of `join`

#### Johan Commelin (Jun 18 2019 at 12:49):

Aah...

#### Johan Commelin (Jun 18 2019 at 12:49):

Crazy names

#### Reid Barton (Jun 18 2019 at 12:49):

(Or actually it's `bind`

with the arguments flipped)

#### Reid Barton (Jun 18 2019 at 12:51):

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

#### Reid Barton (Jun 18 2019 at 12:51):

`join`

joins two layers of the monad

#### Johan Commelin (Jun 18 2019 at 12:53):

@Mario Carneiro Does this mean we should define `bind`

and `join`

and prove a whole bunch of API about them?

#### Mario Carneiro (Jun 18 2019 at 12:54):

sure

#### Johan Commelin (Jun 18 2019 at 12:54):

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

#### Mario Carneiro (Jun 18 2019 at 12:54):

`bind`

or `join`

- they are interdefinable

#### Johan Commelin (Jun 18 2019 at 12:55):

They are all special cases of `eval₂`

#### Mario Carneiro (Jun 18 2019 at 12:56):

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

#### Johan Commelin (Jun 18 2019 at 12:57):

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 (Jun 18 2019 at 13:36):

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 (Jun 18 2019 at 14:00):

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 (Jun 18 2019 at 14:10):

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 (Jun 18 2019 at 14:11):

`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 (Jun 18 2019 at 14:12):

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 (Jun 18 2019 at 14:13):

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

#### Mario Carneiro (Jun 18 2019 at 14:14):

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 (Jun 18 2019 at 14:14):

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

#### Mario Carneiro (Jun 18 2019 at 14:15):

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

#### Johan Commelin (Jun 18 2019 at 14:15):

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 (Jun 18 2019 at 14:16):

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

#### Mario Carneiro (Jun 18 2019 at 14:17):

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 (Jun 18 2019 at 14:17):

Ok

#### Johan Commelin (Jun 18 2019 at 14:18):

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

#### Mario Carneiro (Jun 18 2019 at 14:39):

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 (Jun 18 2019 at 14:40):

What is `P`

doing in your example?

#### Johan Commelin (Jun 18 2019 at 14:43):

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

#### Mario Carneiro (Jun 18 2019 at 14:43):

oops, don't need P

#### Sebastien Gouezel (Jun 18 2019 at 14:50):

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 (Jun 18 2019 at 16:00):

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

#### Johan Commelin (Jun 18 2019 at 19:57):

@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 (Jun 18 2019 at 20:17):

@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 (Jun 19 2019 at 07:35):

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 (Jun 19 2019 at 07:42):

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

#### Mario Carneiro (Jun 19 2019 at 07:42):

I think there is a bug in lean somewhere here

#### Johan Commelin (Jun 19 2019 at 08:04):

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

?

#### Mario Carneiro (Jun 19 2019 at 08:06):

it goes to C++ from here

#### Mario Carneiro (Jun 19 2019 at 08:06):

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

#### Johan Commelin (Jun 22 2019 at 20:41):

@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 (Jun 25 2019 at 17:29):

@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 (Jun 25 2019 at 17:30):

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

#### Sebastian Ullrich (Jun 27 2019 at 11:05):

@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 (Jun 27 2019 at 11:14):

@Sebastian Ullrich Thanks for looking into this!

#### Kevin Buzzard (Jun 27 2019 at 12:08):

Yes, many thanks Sebastian.

#### Johan Commelin (May 03 2020 at 09:14):

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 (May 03 2020 at 09:14):

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 (May 03 2020 at 17:11):

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 (May 03 2020 at 17:13):

Fantastic! What time does it need now?

#### Johan Commelin (May 03 2020 at 17:13):

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

#### Johan Commelin (May 03 2020 at 17:14):

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

#### Bryan Gin-ge Chen (May 03 2020 at 17:18):

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 (May 03 2020 at 17:24):

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

#### Bryan Gin-ge Chen (May 03 2020 at 17:25):

Yes, let me try.

#### Bryan Gin-ge Chen (May 03 2020 at 17:46):

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 (May 03 2020 at 17:48):

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

#### Kevin Buzzard (May 03 2020 at 17:52):

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

#### Kevin Buzzard (May 03 2020 at 17:53):

(just to see how badly it breaks)

#### Bryan Gin-ge Chen (May 03 2020 at 17:55):

Good idea. Let me take a look.

#### Bryan Gin-ge Chen (May 03 2020 at 18:01):

The next two errors pop up at some `erw`

s 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 (May 03 2020 at 18:03):

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

#### Bryan Gin-ge Chen (May 03 2020 at 18:10):

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 (May 03 2020 at 20:24):

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

#### Bryan Gin-ge Chen (May 03 2020 at 20:25):

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

#### Johan Commelin (May 04 2020 at 04:37):

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

#### Johan Commelin (May 04 2020 at 04:37):

Did the build feel significantly slower or faster than usual?

#### Johan Commelin (May 04 2020 at 05:35):

@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 (May 04 2020 at 05:48):

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 (May 04 2020 at 06:17):

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

label)?

#### Johan Commelin (May 04 2020 at 06:18):

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

#### Johan Commelin (May 04 2020 at 06:18):

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

?

#### Bryan Gin-ge Chen (May 04 2020 at 06:33):

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 (May 07 2020 at 19:46):

The code at `witt-vectors2`

is almost compiling again.

#### Johan Commelin (May 07 2020 at 19:46):

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

#### Johan Commelin (May 07 2020 at 19:46):

Mostly related to bundling homs

#### Johan Commelin (May 07 2020 at 19:47):

Already with `lean-3.10.0`

the code is a lot faster. Looking forward to `lean-3.11.0`

(-;

#### Gabriel Ebner (May 07 2020 at 19:49):

`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 (May 30 2020 at 10:12):

Witt vectors are a ring again!

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

#### Johan Commelin (May 30 2020 at 10:12):

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

#### Johan Commelin (May 30 2020 at 10:12):

(And the author maybe also improved a bit.)

#### Johan Commelin (May 30 2020 at 10:13):

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 (May 30 2020 at 10:13):

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

#### Kevin Buzzard (May 30 2020 at 10:13):

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 (May 30 2020 at 10:15):

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 (Jun 07 2020 at 13:53):

@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 (Jun 07 2020 at 13:54):

sure we can pass through `\Q`

but that wouldn't be necessary

#### Kenny Lau (Jun 07 2020 at 13:54):

could we do the same thing for the Witt polynomials?

#### Kenny Lau (Jun 07 2020 at 13:54):

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

#### Johan Commelin (Jun 07 2020 at 14:17):

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

#### Kenny Lau (Jun 08 2020 at 09:55):

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

#### Kenny Lau (Jun 08 2020 at 09:55):

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 (Jun 08 2020 at 09:57):

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

#### Kenny Lau (Jun 08 2020 at 10:09):

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 (Sep 10 2020 at 20:46):

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 (Sep 10 2020 at 20:47):

how did you define the Teichmuller lift?

#### Johan Commelin (Sep 10 2020 at 20:48):

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

#### Johan Commelin (Sep 10 2020 at 20:48):

```
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 (Sep 10 2020 at 20:52):

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

#### Johan Commelin (Sep 10 2020 at 20:52):

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

#### Adam Topaz (Sep 10 2020 at 20:53):

Is Ver additive?

#### Johan Commelin (Sep 10 2020 at 20:53):

Yes

#### Kenny Lau (Sep 10 2020 at 20:53):

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

#### Johan Commelin (Sep 10 2020 at 20:54):

Nope

#### Johan Commelin (Sep 10 2020 at 20:54):

`W (F_p)`

is the projective limit of truncated witt vector rings, which have cardinality `p ^ n`

.

#### Johan Commelin (Sep 10 2020 at 20:54):

And `1`

has order `p ^ n`

in those rings. Hence done.

#### Johan Commelin (Sep 10 2020 at 20:55):

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

.)

#### Kenny Lau (Sep 10 2020 at 20:58):

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

sent to?

#### Johan Commelin (Sep 10 2020 at 20:59):

What do you mean "suspicious"?

We have a freaking formal proof, lol

#### Johan Commelin (Sep 10 2020 at 20:59):

```
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 (Sep 10 2020 at 21:00):

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 (Sep 10 2020 at 21:00):

That's not too surprising, right?

#### Johan Commelin (Sep 10 2020 at 21:01):

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

#### Johan Commelin (Sep 10 2020 at 21:02):

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

#### Kenny Lau (Sep 10 2020 at 21:05):

why does 1 have order p^n?

#### Adam Topaz (Sep 10 2020 at 21:05):

additive order.

#### Kenny Lau (Sep 10 2020 at 21:06):

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

#### Johan Commelin (Sep 10 2020 at 21:06):

```
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 (Sep 10 2020 at 21:07):

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 (Sep 10 2020 at 21:07):

aha

#### Kevin Buzzard (Sep 10 2020 at 21:22):

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 (Sep 10 2020 at 21:26):

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

#### Adam Topaz (Sep 10 2020 at 22:00):

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 (Sep 10 2020 at 22:01):

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

#### Kevin Buzzard (Sep 10 2020 at 22:13):

Sure -- but valuations take values in a `linear_ordered_comm_group_with_zero`

right now.

#### Adam Topaz (Sep 10 2020 at 22:19):

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

#### Adam Topaz (Sep 10 2020 at 22:19):

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 (Sep 17 2020 at 05:43):

@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 (Sep 22 2020 at 11:55):

@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 (Sep 22 2020 at 13:39):

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 (Sep 22 2020 at 13:42):

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 (Sep 22 2020 at 13:43):

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 (Sep 24 2020 at 13:43):

#4236 is the first *real* PR on Witt vectors

#### Johan Commelin (Sep 24 2020 at 13:45):

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

#### Johan Commelin (Sep 25 2020 at 23:30):

#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 (Oct 07 2020 at 07:45):

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

#### Patrick Massot (Oct 07 2020 at 07:49):

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 (Oct 07 2020 at 07:54):

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 (Oct 07 2020 at 08:21):

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 (Oct 07 2020 at 10:56):

The typesetting looks great! You must have worked hard.

#### Rob Lewis (Oct 07 2020 at 10:58):

Pay no attention to the column break on p7

#### Jasmin Blanchette (Oct 07 2020 at 10:58):

Sure. Which page did you say? ;)

#### Patrick Massot (Oct 07 2020 at 11:01):

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

#### Rob Lewis (Oct 07 2020 at 11:02):

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 (Oct 07 2020 at 11:58):

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

#### Johan Commelin (Oct 19 2020 at 14:40):

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 (Oct 19 2020 at 14:41):

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

#### Johan Commelin (Oct 19 2020 at 14:44):

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 (Oct 19 2020 at 14:45):

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 (Oct 19 2020 at 16:54):

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

#### Johan Commelin (Oct 19 2020 at 17:48):

#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 (Oct 23 2020 at 17:21):

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

#### Johan Commelin (Oct 23 2020 at 17:22):

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 (Dec 01 2020 at 06:04):

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 (Dec 14 2020 at 09:43):

@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 (Dec 14 2020 at 09:45):

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

#### Johan Commelin (Dec 14 2020 at 09:45):

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

#### Filippo A. E. Nuccio (Dec 14 2020 at 09:47):

Johan Commelin said:

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

Oh great, I'll have a look.

#### Filippo A. E. Nuccio (Dec 14 2020 at 09:51):

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 (Dec 14 2020 at 09:54):

Nope, it's #5163

#### Johan Commelin (Dec 14 2020 at 09:54):

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

#### Johan Commelin (Dec 23 2020 at 09:52):

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

Last updated: May 11 2021 at 16:22 UTC