Zulip Chat Archive

Stream: maths

Topic: witt vectors


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jul 24 2018 at 14:53):

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

view this post on Zulip Johan Commelin (Jul 24 2018 at 14:53):

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

view this post on Zulip 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:

view this post on Zulip 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.)

view this post on Zulip Kevin Buzzard (Jul 24 2018 at 16:07):

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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Aug 07 2018 at 11:01):

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

view this post on Zulip Mario Carneiro (Aug 07 2018 at 11:03):

oh, good call

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Aug 07 2018 at 11:06):

This has happened to me so many times :-)

view this post on Zulip 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"

view this post on Zulip Mario Carneiro (Aug 07 2018 at 11:08):

heh, I remember so many questions from you like that

view this post on Zulip Johan Commelin (Aug 07 2018 at 11:36):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Aug 07 2018 at 11:38):

But there is clearly a lambda in there...

view this post on Zulip Johan Commelin (Aug 07 2018 at 11:46):

Ok, I navigated to the lambda by hand.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Aug 07 2018 at 11:47):

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

view this post on Zulip Johan Commelin (Aug 07 2018 at 11:47):

Is this a known issue?

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Aug 07 2018 at 12:42):

"I worked my way around it..."

view this post on Zulip 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

view this post on Zulip Johan Commelin (Aug 07 2018 at 12:51):

I fought the mess (and the mess won)

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Aug 07 2018 at 12:53):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Aug 07 2018 at 13:03):

(even if they look refl)

view this post on Zulip Johan Commelin (Aug 07 2018 at 13:05):

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

view this post on Zulip Johan Commelin (Aug 07 2018 at 13:06):

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

view this post on Zulip Mario Carneiro (Aug 07 2018 at 13:06):

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

view this post on Zulip 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]

view this post on Zulip Mario Carneiro (Aug 07 2018 at 13:12):

@Kevin Buzzard Hey look, a nontrivial equation lemma

view this post on Zulip Johan Commelin (Aug 07 2018 at 13:14):

Thanks!

view this post on Zulip Johan Commelin (Aug 07 2018 at 13:15):

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

view this post on Zulip 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?

view this post on Zulip Chris Hughes (Aug 07 2018 at 14:03):

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

view this post on Zulip Johan Commelin (Aug 07 2018 at 14:04):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Aug 07 2018 at 14:05):

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

view this post on Zulip Johan Commelin (Aug 07 2018 at 14:05):

Ok, make sure you download again (-;

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Aug 07 2018 at 14:10):

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

view this post on Zulip Johan Commelin (Aug 07 2018 at 14:11):

I feel I've made progress today.

view this post on Zulip Johan Commelin (Aug 07 2018 at 14:11):

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

view this post on Zulip Kevin Buzzard (Aug 07 2018 at 14:12):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Aug 07 2018 at 14:13):

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

view this post on Zulip Johan Commelin (Aug 07 2018 at 14:13):

I'll clear the first one

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Aug 07 2018 at 14:17):

It's line 119

view this post on Zulip Kevin Buzzard (Aug 07 2018 at 14:17):

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

view this post on Zulip Johan Commelin (Aug 07 2018 at 14:18):

How do you figure out which line it is?

view this post on Zulip Kevin Buzzard (Aug 07 2018 at 14:18):

elaboration: tactic execution took 3.44s.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Aug 07 2018 at 14:19):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Aug 07 2018 at 14:20):

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

view this post on Zulip Johan Commelin (Aug 07 2018 at 14:23):

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

view this post on Zulip Johan Commelin (Aug 07 2018 at 14:23):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Aug 07 2018 at 15:12):

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

view this post on Zulip Johan Commelin (Aug 07 2018 at 15:12):

And the proof is still relatively slow.

view this post on Zulip Johan Commelin (Aug 07 2018 at 15:12):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Aug 07 2018 at 15:39):

and then rw eval₂_X takes about 600ms

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Aug 07 2018 at 16:16):

I filled in every field.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Aug 07 2018 at 16:30):

That's exactly what I was thinking.

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Aug 07 2018 at 16:33):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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".

view this post on Zulip 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

view this post on Zulip Johan Commelin (Aug 08 2018 at 05:06):

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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Aug 08 2018 at 06:32):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Aug 08 2018 at 07:19):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Aug 08 2018 at 09:25):

Thanks for the explanation Kevin!

view this post on Zulip 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

view this post on Zulip Johan Commelin (Aug 08 2018 at 11:14):

Yesterday's trick isn't working.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Aug 08 2018 at 11:19):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Aug 08 2018 at 12:46):

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

view this post on Zulip Johan Commelin (Aug 08 2018 at 12:49):

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

view this post on Zulip Kevin Buzzard (Aug 08 2018 at 13:03):

Didn't I mention that? ;-)

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Aug 08 2018 at 13:21):

So I find my self doing long chains of rws

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Aug 08 2018 at 13:34):

Ok! "I worked my way around it."

view this post on Zulip Johan Commelin (Aug 08 2018 at 13:35):

All sorries are gone in this part! :octopus:

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Aug 08 2018 at 13:35):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Aug 08 2018 at 13:37):

turning off everything but beta

view this post on Zulip Kenny Lau (Aug 08 2018 at 13:40):

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

view this post on Zulip Kenny Lau (Aug 08 2018 at 13:41):

but I'm not sure

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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)))) :=

view this post on Zulip Johan Commelin (Jun 13 2019 at 14:40):

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

view this post on Zulip Kevin Buzzard (Jun 13 2019 at 14:40):

https://arxiv.org/abs/1906.03583

If you want a goal which looks accessible ;-)

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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 (-;

view this post on Zulip Johan Commelin (Jun 13 2019 at 14:42):

(And to clean up the file.)

view this post on Zulip Johan Commelin (Jun 13 2019 at 14:43):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jun 13 2019 at 15:14):

Things like add_comm_monoid :stuck_out_tongue_wink:

view this post on Zulip 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...

view this post on Zulip Johan Commelin (Jun 13 2019 at 15:15):

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

view this post on Zulip Mario Carneiro (Jun 13 2019 at 15:40):

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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jun 13 2019 at 18:35):

no underscores

view this post on Zulip Mario Carneiro (Jun 13 2019 at 18:36):

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

view this post on Zulip Johan Commelin (Jun 13 2019 at 18:44):

I'll test this

view this post on Zulip 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) :=

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

view this post on Zulip Johan Commelin (Jun 13 2019 at 18:48):

This proof is currently quite long and slow.

view this post on Zulip Johan Commelin (Jun 13 2019 at 18:48):

But it is completely elementary maths...

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jun 13 2019 at 18:49):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jun 15 2019 at 18:32):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip Mario Carneiro (Jun 18 2019 at 08:06):

does rfl work for the first?

view this post on Zulip 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...

view this post on Zulip 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]

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jun 18 2019 at 08:29):

omg we need deduplicating pretty printer so much

view this post on Zulip Mario Carneiro (Jun 18 2019 at 08:30):

this definitely isn't inevitable in the abstract

view this post on Zulip Mario Carneiro (Jun 18 2019 at 08:30):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jun 18 2019 at 08:31):

that's just int.of_nat

view this post on Zulip Kevin Buzzard (Jun 18 2019 at 08:31):

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

view this post on Zulip Mario Carneiro (Jun 18 2019 at 08:32):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 18 2019 at 08:32):

it is

view this post on Zulip Mario Carneiro (Jun 18 2019 at 08:33):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jun 18 2019 at 08:34):

oh wait, actually this isn't int.of_nat

view this post on Zulip Mario Carneiro (Jun 18 2019 at 08:34):

this is the "wrong" coe from nat to int

view this post on Zulip Mario Carneiro (Jun 18 2019 at 08:34):

nat.cast

view this post on Zulip Mario Carneiro (Jun 18 2019 at 08:34):

both of them are nat.cast

view this post on Zulip Mario Carneiro (Jun 18 2019 at 08:34):

try simp?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 18 2019 at 08:35):

try simp?

[waits 10 seconds] fails to simplify.

view this post on Zulip Mario Carneiro (Jun 18 2019 at 08:38):

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

view this post on Zulip Kevin Buzzard (Jun 18 2019 at 08:39):

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

view this post on Zulip Mario Carneiro (Jun 18 2019 at 08:55):

I mean with regular printing

view this post on Zulip 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.

view this post on Zulip 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))

view this post on Zulip Johan Commelin (Jun 18 2019 at 08:56):

I posted the other 4 goals somewhere upstairs.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 18 2019 at 09:11):

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

view this post on Zulip Mario Carneiro (Jun 18 2019 at 09:19):

mod_e should be a definition

view this post on Zulip Johan Commelin (Jun 18 2019 at 09:20):

Can you explain why?

view this post on Zulip 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

view this post on Zulip 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]"

view this post on Zulip Mario Carneiro (Jun 18 2019 at 09:21):

You could use an equivalence relation

view this post on Zulip Mario Carneiro (Jun 18 2019 at 09:22):

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

view this post on Zulip Mario Carneiro (Jun 18 2019 at 09:22):

if you need ideals, so be it

view this post on Zulip Mario Carneiro (Jun 18 2019 at 09:23):

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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jun 18 2019 at 09:24):

yes

view this post on Zulip Mario Carneiro (Jun 18 2019 at 09:24):

and possibly to ideals

view this post on Zulip Mario Carneiro (Jun 18 2019 at 09:25):

I see you needed a few variations on this

view this post on Zulip Johan Commelin (Jun 18 2019 at 09:26):

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

view this post on Zulip Mario Carneiro (Jun 18 2019 at 09:26):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jun 18 2019 at 09:27):

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

view this post on Zulip Mario Carneiro (Jun 18 2019 at 09:27):

where do you start sensing problems?

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jun 18 2019 at 09:28):

I noticed

view this post on Zulip Johan Commelin (Jun 18 2019 at 09:28):

witt_structure_rat_rec_aux is slow

view this post on Zulip Mario Carneiro (Jun 18 2019 at 09:28):

I thought that this was one of the eval functions

view this post on Zulip 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.

view this post on Zulip 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".

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip Chris Hughes (Jun 18 2019 at 09:35):

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

view this post on Zulip Johan Commelin (Jun 18 2019 at 10:01):

I think it is, yes.

view this post on Zulip 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

view this post on Zulip Reid Barton (Jun 18 2019 at 12:49):

It is exactly bind. You're thinking of join

view this post on Zulip Johan Commelin (Jun 18 2019 at 12:49):

Aah...

view this post on Zulip Johan Commelin (Jun 18 2019 at 12:49):

Crazy names

view this post on Zulip Reid Barton (Jun 18 2019 at 12:49):

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

view this post on Zulip 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

view this post on Zulip Reid Barton (Jun 18 2019 at 12:51):

join joins two layers of the monad

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jun 18 2019 at 12:54):

sure

view this post on Zulip Johan Commelin (Jun 18 2019 at 12:54):

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

view this post on Zulip Mario Carneiro (Jun 18 2019 at 12:54):

bind or join - they are interdefinable

view this post on Zulip Johan Commelin (Jun 18 2019 at 12:55):

They are all special cases of eval₂

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jun 18 2019 at 14:13):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 18 2019 at 14:15):

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

view this post on Zulip 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:

view this post on Zulip Johan Commelin (Jun 18 2019 at 14:16):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jun 18 2019 at 14:17):

Ok

view this post on Zulip Johan Commelin (Jun 18 2019 at 14:18):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jun 18 2019 at 14:40):

What is P doing in your example?

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jun 18 2019 at 14:43):

oops, don't need P

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jun 19 2019 at 07:42):

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

view this post on Zulip Mario Carneiro (Jun 19 2019 at 07:42):

I think there is a bug in lean somewhere here

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jun 19 2019 at 08:06):

it goes to C++ from here

view this post on Zulip Mario Carneiro (Jun 19 2019 at 08:06):

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

view this post on Zulip 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.)

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jun 25 2019 at 17:30):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 27 2019 at 11:14):

@Sebastian Ullrich Thanks for looking into this!

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 12:08):

Yes, many thanks Sebastian.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 03 2020 at 17:13):

Fantastic! What time does it need now?

view this post on Zulip Johan Commelin (May 03 2020 at 17:13):

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

view this post on Zulip Johan Commelin (May 03 2020 at 17:14):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Bryan Gin-ge Chen (May 03 2020 at 17:25):

Yes, let me try.

view this post on Zulip 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

view this post on Zulip Sebastien Gouezel (May 03 2020 at 17:48):

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

view this post on Zulip Kevin Buzzard (May 03 2020 at 17:52):

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

view this post on Zulip Kevin Buzzard (May 03 2020 at 17:53):

(just to see how badly it breaks)

view this post on Zulip Bryan Gin-ge Chen (May 03 2020 at 17:55):

Good idea. Let me take a look.

view this post on Zulip Bryan Gin-ge Chen (May 03 2020 at 18:01):

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

view this post on Zulip Kevin Buzzard (May 03 2020 at 18:03):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Bryan Gin-ge Chen (May 03 2020 at 20:25):

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

view this post on Zulip Johan Commelin (May 04 2020 at 04:37):

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

view this post on Zulip Johan Commelin (May 04 2020 at 04:37):

Did the build feel significantly slower or faster than usual?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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)?

view this post on Zulip Johan Commelin (May 04 2020 at 06:18):

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

view this post on Zulip Johan Commelin (May 04 2020 at 06:18):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 07 2020 at 19:46):

The code at witt-vectors2 is almost compiling again.

view this post on Zulip Johan Commelin (May 07 2020 at 19:46):

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

view this post on Zulip Johan Commelin (May 07 2020 at 19:46):

Mostly related to bundling homs

view this post on Zulip 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 (-;

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 30 2020 at 10:12):

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

view this post on Zulip Johan Commelin (May 30 2020 at 10:12):

(And the author maybe also improved a bit.)

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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)

view this post on Zulip Kenny Lau (Jun 07 2020 at 13:54):

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

view this post on Zulip Kenny Lau (Jun 07 2020 at 13:54):

could we do the same thing for the Witt polynomials?

view this post on Zulip Kenny Lau (Jun 07 2020 at 13:54):

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

view this post on Zulip Johan Commelin (Jun 07 2020 at 14:17):

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

view this post on Zulip Kenny Lau (Jun 08 2020 at 09:55):

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

view this post on Zulip 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)"

view this post on Zulip Johan Commelin (Jun 08 2020 at 09:57):

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

view this post on Zulip 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

view this post on Zulip 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 (-;

view this post on Zulip Kenny Lau (Sep 10 2020 at 20:47):

how did you define the Teichmuller lift?

view this post on Zulip Johan Commelin (Sep 10 2020 at 20:48):

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

view this post on Zulip 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 }

view this post on Zulip Johan Commelin (Sep 10 2020 at 20:52):

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

view this post on Zulip Johan Commelin (Sep 10 2020 at 20:52):

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

view this post on Zulip Adam Topaz (Sep 10 2020 at 20:53):

Is Ver additive?

view this post on Zulip Johan Commelin (Sep 10 2020 at 20:53):

Yes

view this post on Zulip Kenny Lau (Sep 10 2020 at 20:53):

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

view this post on Zulip Johan Commelin (Sep 10 2020 at 20:54):

Nope

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 10 2020 at 20:54):

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

view this post on Zulip Johan Commelin (Sep 10 2020 at 20:55):

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

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Sep 10 2020 at 20:59):

What do you mean "suspicious"?

We have a freaking formal proof, lol

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 10 2020 at 21:00):

That's not too surprising, right?

view this post on Zulip Johan Commelin (Sep 10 2020 at 21:01):

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

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Sep 10 2020 at 21:05):

why does 1 have order p^n?

view this post on Zulip Adam Topaz (Sep 10 2020 at 21:05):

additive order.

view this post on Zulip Kenny Lau (Sep 10 2020 at 21:06):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Sep 10 2020 at 21:07):

aha

view this post on Zulip 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

view this post on Zulip Reid Barton (Sep 10 2020 at 21:26):

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

view this post on Zulip 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?

view this post on Zulip Adam Topaz (Sep 10 2020 at 22:01):

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

view this post on Zulip Kevin Buzzard (Sep 10 2020 at 22:13):

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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Sep 10 2020 at 22:19):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 24 2020 at 13:43):

#4236 is the first real PR on Witt vectors

view this post on Zulip Johan Commelin (Sep 24 2020 at 13:45):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Jasmin Blanchette (Oct 07 2020 at 10:56):

The typesetting looks great! You must have worked hard.

view this post on Zulip Rob Lewis (Oct 07 2020 at 10:58):

Pay no attention to the column break on p7

view this post on Zulip Jasmin Blanchette (Oct 07 2020 at 10:58):

Sure. Which page did you say? ;)

view this post on Zulip Patrick Massot (Oct 07 2020 at 11:01):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Oct 19 2020 at 14:41):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Oct 19 2020 at 16:54):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Oct 23 2020 at 17:21):

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

view this post on Zulip 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.)

view this post on Zulip 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(Fp)W(\mathbb{F}_p) and Zp\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.)

view this post on Zulip Filippo A. E. Nuccio (Dec 14 2020 at 09:43):

@Johan Commelin What is the state of the art of the proof that W(R)\mathbb{W}(R) is the projective limit of truncated Witt vectors on RR? 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.

view this post on Zulip Johan Commelin (Dec 14 2020 at 09:45):

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

view this post on Zulip Johan Commelin (Dec 14 2020 at 09:45):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Dec 14 2020 at 09:54):

Nope, it's #5163

view this post on Zulip Johan Commelin (Dec 14 2020 at 09:54):

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

view this post on Zulip 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