Zulip Chat Archive

Stream: maths

Topic: sensitivity conjecture


view this post on Zulip Johan Commelin (Aug 02 2019 at 05:54):

The sensitivity conjecture was 30 years old, and recently resolved. Can we formalise this? https://www.scottaaronson.com/blog/?p=4229
See also Donald Knuth's condensation of the proof: https://www.cs.stanford.edu/~knuth/papers/huang.pdf

view this post on Zulip Johan Commelin (Aug 02 2019 at 06:16):

@Chris Hughes You've been doing a lot with matrices lately. Did you do things like row/column rank?

view this post on Zulip Johan Commelin (Aug 02 2019 at 06:17):

And how far did you get with the inverse matrix?

view this post on Zulip Chris Hughes (Aug 02 2019 at 07:55):

I used a noncomputable inverse in the end. I didn't use row and column rank either, but used the predicates has_left_inverse and has_right_inverse as well. Both of these look good enough for the sensitivity proof.

view this post on Zulip Johan Commelin (Aug 02 2019 at 07:58):

But this isn't in mathlib yet, right?

view this post on Zulip Chris Hughes (Aug 02 2019 at 07:59):

No.

view this post on Zulip Chris Hughes (Aug 02 2019 at 08:24):

It's a bit unfinished, that's why. It would be nicer to have a pseudoinverse that worked on rectangular matrices.

view this post on Zulip Reid Barton (Aug 02 2019 at 11:54):

I thought about this also. How easy is it to do these block matrix calculations appearing in the proof that An=nIA_n = nI (and in the definition of AnA_n)?
This is another example where it's natural to consider a matrix with rows and columns indexed by a general finite type (in this case, the hypercube).

view this post on Zulip Reid Barton (Aug 02 2019 at 11:55):

Given what we have at the moment it might be easier to formulate the Knuth proof in terms of linear maps everywhere instead of matrices

view this post on Zulip Kevin Buzzard (Aug 02 2019 at 11:56):

@Chris Hughes the matrices in Knuth's proof are indexed by {0,1}^n

view this post on Zulip Chris Hughes (Aug 02 2019 at 12:06):

My matrix pequiv thing might help with the block matrix computations. You can concatenate matrices algebraically using something like
(ab)(1000)+(cd)(0001)=(abcd) \begin{pmatrix} a & b \end{pmatrix} \begin{pmatrix} 1 & 0 \\0 & 0 \end{pmatrix} + \begin{pmatrix} c & d \end{pmatrix} \begin{pmatrix} 0 & 0 \\0 & 1 \end{pmatrix} = \begin{pmatrix} a & b \\c & d \end{pmatrix}

view this post on Zulip Chris Hughes (Aug 02 2019 at 12:12):

In the proof you'll probably end up with some big ugly sum, but with some terms like (1000)(0001) \begin{pmatrix} 1 & 0 \\0 & 0 \end{pmatrix} \begin{pmatrix} 0 & 0 \\0 & 1 \end{pmatrix} , which cancel quite easily.

view this post on Zulip Reid Barton (Aug 02 2019 at 12:18):

I'm writing up a translation of Knuth's version into linear maps to compare

view this post on Zulip Reid Barton (Aug 02 2019 at 12:58):

https://gist.github.com/rwbarton/ed50d4340e2f654b9d778ccb3ec93442

view this post on Zulip Reid Barton (Aug 02 2019 at 13:00):

I haven't used the relevant parts of mathlib much but as far as I could tell while writing this everything ought to be fairly straightforward

view this post on Zulip Chris Hughes (Aug 02 2019 at 13:05):

Is there an easy way to see the pdf version?

view this post on Zulip Kevin Buzzard (Aug 02 2019 at 13:05):

rofl kids these days

view this post on Zulip Reid Barton (Aug 02 2019 at 13:06):

One sec

view this post on Zulip Reid Barton (Aug 02 2019 at 13:06):

sensitivity.pdf

view this post on Zulip Johan Commelin (Aug 02 2019 at 13:14):

That looks quite formalisable, I think.

view this post on Zulip Johan Commelin (Aug 02 2019 at 13:16):

After all, Kenny formalised the dimension formula, and Fabian did the dual basis.

view this post on Zulip Johan Commelin (Aug 02 2019 at 13:16):

Anything else that we need?

view this post on Zulip Johan Commelin (Aug 02 2019 at 13:18):

@Reid Barton How far are you with the Lean version?

view this post on Zulip Reid Barton (Aug 02 2019 at 13:18):

Haven't started

view this post on Zulip Reid Barton (Aug 02 2019 at 13:18):

The only other general fact which gets used is the triangle inequality for summing over a finite set, do we have that?

view this post on Zulip Johan Commelin (Aug 02 2019 at 13:19):

If we do, it should be finset.abs_sum, right? I don't think I've seen it.

view this post on Zulip Reid Barton (Aug 02 2019 at 13:19):

Then there is going to be some possibly tricky business relating the hypercube graph to the matrix entries of the fnf_n, but that would also appear in the matrix version

view this post on Zulip Johan Commelin (Aug 02 2019 at 13:22):

Right, that final calc block seems the most tricky part.

view this post on Zulip Johan Commelin (Aug 02 2019 at 13:22):

The rest is straight-forward, I think.

view this post on Zulip Rob Lewis (Aug 02 2019 at 13:26):

This looks super doable. It's obviously a different kind of proof, but somehow it reminds me of the cap set proof in spirit.

view this post on Zulip Reid Barton (Aug 02 2019 at 13:32):

I guess I'll just start typing and see at what point I get stuck.

view this post on Zulip Johan Commelin (Aug 02 2019 at 14:30):

@Reid Barton How are things going so far? I finally have time to look at this

view this post on Zulip Reid Barton (Aug 02 2019 at 14:32):

So far I created a new repository and did other things while building mathlib :slight_smile:

view this post on Zulip Reid Barton (Aug 02 2019 at 14:33):

I was about to get started actually

view this post on Zulip Johan Commelin (Aug 02 2019 at 14:34):

Why do you build mathlib?

view this post on Zulip Johan Commelin (Aug 02 2019 at 14:34):

I haven't built mathlib in 3 months

view this post on Zulip Reid Barton (Aug 02 2019 at 14:34):

I haven't been indoctrinated in the new ways yet and I had other things to do anyways

view this post on Zulip Reid Barton (Aug 02 2019 at 14:48):

Does this look sensible so far?

import data.real.basic
import linear_algebra.dimension

noncomputable theory

/-- The free vector space on vertices of a hypercube, defined inductively. -/
def V :   Type
| 0 := 
| (n+1) := V n × V n

instance : Π n, add_comm_group (V n) :=
begin
  apply nat.rec,
  { dunfold V, apply_instance },
  { introsI n IH, dunfold V, apply_instance }
end

instance : Π n, vector_space  (V n) :=
begin
  apply nat.rec,
  { dunfold V, apply_instance },
  { introsI n IH, dunfold V, apply_instance }
end

lemma dim_V {n : } : vector_space.dim  (V n) = 2^n :=
begin
  induction n with n IH,
  { apply dim_of_field },
  { dunfold V,
    rw [dim_prod, IH, pow_succ, two_mul] }
end

/-- The linear operator f_n corresponding to Huang's matrix A_n. -/
def f : Π n, V n [] V n
| 0 := 0
| (n+1) := sorry

view this post on Zulip Reid Barton (Aug 02 2019 at 14:50):

And is there any special support for linear maps into/out of binary direct sums?

view this post on Zulip Rob Lewis (Aug 02 2019 at 14:52):

Heh, I just started playing around with this and got to exactly the same place. Not that I saw (at a quick glance).

view this post on Zulip Reid Barton (Aug 02 2019 at 14:52):

Ah yes, linear_map.fst/snd/prod

view this post on Zulip Reid Barton (Aug 02 2019 at 14:56):

/-- The linear operator f_n corresponding to Huang's matrix A_n. -/
noncomputable def f : Π n, V n [] V n
| 0 := 0
| (n+1) :=
  linear_map.pair
    (linear_map.copair (f n) linear_map.id)
    (linear_map.copair linear_map.id (-f n))

This definition needs an explicit noncomputable even though I have noncomputable theory at the top, is that supposed to happen?

view this post on Zulip Chris Hughes (Aug 02 2019 at 15:00):

Is noncomputable theory inside a section?

view this post on Zulip Rob Lewis (Aug 02 2019 at 15:00):

noncomputable theory doesn't always propogate to aux decls.

view this post on Zulip Reid Barton (Aug 02 2019 at 15:32):

/-- The linear operator f_n corresponding to Huang's matrix A_n. -/
noncomputable def f : Π n, V n [] V n
| 0 := 0
| (n+1) :=
  linear_map.pair
    (linear_map.copair (f n) linear_map.id)
    (linear_map.copair linear_map.id (-f n))

lemma f_squared {n : } :  v, (f n) (f n v) = (n : )  v :=
-- The (n : ℝ) is necessary since `n • v` refers to the multiplication defined
-- using only the addition of V.
begin
  induction n with n IH,
  { intro v, dunfold f, simp, refl },
  { rintro v, v',
    ext,
    { dunfold f V,
      conv_rhs { change ((n : ) + 1)  v, rw add_smul },
      simp [IH] },
    { dunfold f V,
      conv_rhs { change ((n : ) + 1)  v', rw add_smul },
      have : Π (x y : V n), -x + (y + x) = y := by { intros, abel }, -- ugh
      simp [IH, this] } }
end

view this post on Zulip Reid Barton (Aug 02 2019 at 15:32):

Maybe I'll put up a repository under leanprover-community?

view this post on Zulip Rob Lewis (Aug 02 2019 at 15:37):

This was weirdly hard to make it go through, I got caught on the (n : R) thing too for a bit.

lemma fn2 :  n v, f n (f n v) = (n : )  v
| 0 v := by { rw (show f 0 = 0, from rfl), norm_cast, simp, refl }
| (k+1) v1, v2 :=
begin
  rw [f, nat.cast_add, add_smul],
  simp [fn2], rw [add_comm],
  convert add_sub_cancel _ _
end

view this post on Zulip Reid Barton (Aug 02 2019 at 15:38):

Okay, I made https://github.com/leanprover-community/lean-sensitivity. I don't know how the permissions work by default, but anyone who can add collaborators should feel free to do so.

view this post on Zulip Floris van Doorn (Aug 02 2019 at 15:46):

My gut feeling says that defining V n := (fin n -> bool) -> real would be nicer to work with. Then V is defined directly instead of recursively. You can use the following to go between fin n and fin (n+1):

universe variable u
variables {α : Type u} {n : }
def tail (p : fin (n+1)  α) : fin n  α := λ i, p i.succ
def cons (x : α) (v : fin n  α) : fin (n+1)  α :=
λ j, fin.cases x v j

view this post on Zulip Reid Barton (Aug 02 2019 at 15:51):

I thought defining V recursively would be more convenient for defining and proving things about f and g--and it seems pretty convenient so far. I was thinking of defining the hypercube as fin n -> bool though (in part because it seems a bit cheating to define it recursively).

view this post on Zulip Rob Lewis (Aug 02 2019 at 15:52):

I've started with the hypercube as fin n -> bool but I'm not sure about the cleanest way to define the basis of e_ps.

view this post on Zulip Floris van Doorn (Aug 02 2019 at 15:53):

Ok. Maybe that's right. Why do you say it feels like cheating?

view this post on Zulip Johan Commelin (Aug 02 2019 at 15:53):

I thought defining V recursively would be more convenient for defining and proving things about f and g--and it seems pretty convenient so far. I was thinking of defining the hypercube as fin n -> bool though (in part because it seems a bit cheating to define it recursively).

Why would that be cheating?

view this post on Zulip Johan Commelin (Aug 02 2019 at 15:54):

I've started with the hypercube as fin n -> bool but I'm not sure about the cleanest way to define the basis of e_ps.

Dual basis is in mathlib

view this post on Zulip Reid Barton (Aug 02 2019 at 15:55):

Well just because it's part of the "interface" of the overall theorem and fin n -> bool feels a bit more canonical. For example if the hypercube is defined recursively then it's not obvious how to construct the action of the symmetric group.

view this post on Zulip Floris van Doorn (Aug 02 2019 at 15:55):

Isn't the basis e just

def V (n : ℕ) : Type := (fin n → bool) → ℝ
def e (p : fin n → bool) : V n := λ q, if q = p then 1 else 0

view this post on Zulip Reid Barton (Aug 02 2019 at 15:55):

I agree it's not cheating by much.

view this post on Zulip Johan Commelin (Aug 02 2019 at 15:57):

@Floris van Doorn But you changed the definition of V

view this post on Zulip Reid Barton (Aug 02 2019 at 15:58):

If you assume that the hypercube must be represented by fin n -> bool, then at some point you have to make a recursive decomposition of building something for n+1 out of two somethings for n. I suggest doing that when we define the basis e

view this post on Zulip Reid Barton (Aug 02 2019 at 15:58):

Which is I think what Rob was going to do

view this post on Zulip Floris van Doorn (Aug 02 2019 at 15:58):

I was responding to Rob, who said (as I understood it) that he was interested in the basis using this definition of V

view this post on Zulip Reid Barton (Aug 02 2019 at 15:59):

Probably it doesn't matter very much where you do it

view this post on Zulip Johan Commelin (Aug 02 2019 at 16:00):

Do we want to define e directly?

view this post on Zulip Johan Commelin (Aug 02 2019 at 16:00):

I don't really care.

view this post on Zulip Johan Commelin (Aug 02 2019 at 16:00):

I just thought that we would first define the basis for V.

view this post on Zulip Reid Barton (Aug 02 2019 at 16:01):

So something like e (n+1) p := if p 0 then prod.inr (e n p.tail) else prod.inl (e n p.tail)

view this post on Zulip Rob Lewis (Aug 02 2019 at 16:01):

@Floris van Doorn That looks way cleaner than what I was doing, I was using the other definition of V though.

view this post on Zulip Rob Lewis (Aug 02 2019 at 16:01):

def e : Π n : , Q n  V n
| 0 p := (1 : )
| (k+1) p :=
  match p 0 with
  | tt := (e k (drop p), 0)
  | ff := (0, e k (drop p))
  end

or something like that, I don't think it's gonna be convenient.

view this post on Zulip Floris van Doorn (Aug 02 2019 at 16:01):

The recursive decomposition is easy:

def tail (p : fin (n+1) → α) : fin n → α := λ i, p i.succ
def tuple (x : α) (v : α → (fin n → α) → β) : (fin (n+1) → α) → β :=
λ p, v (p 0) (tail p)

So if you have an element of bool -> V n you get an element of V (n+1)

view this post on Zulip Reid Barton (Aug 02 2019 at 16:04):

I'm just worried that you will end up with only a linear isomorphism (not a definitional equality) between V (n+1) and bool -> V n or V n x V n and that will make the computations involving f and g a lot more involved unless you can manage to cancel the isomorphisms automatically

view this post on Zulip Floris van Doorn (Aug 02 2019 at 16:05):

Ok, that might be a problem if we have to translate a lot between these two representations. I think it will be doable though.

view this post on Zulip Floris van Doorn (Aug 02 2019 at 16:06):

but maybe in that aspect the recursive definition is easier.

view this post on Zulip Johan Commelin (Aug 02 2019 at 16:06):

How about

/-- The hypercube.-/
def Q (n) : Type := fin n  bool

/-- The basis of V indexed by the hypercube.-/
def b : Π n, Q n  V n
| 0     := λ _, (1:)
| (n+1) := λ v, if v n = tt
           then (b n (v  fin.succ), 0)
           else (0, b n (v  fin.succ))

view this post on Zulip Reid Barton (Aug 02 2019 at 16:07):

The alternative is to write down the basis and probably also the dual basis separately by this kind of recursive formula and then check that the dual basis is really dual and also the formula for εq(fnep)\varepsilon_q (f_n e_p), by induction

view this post on Zulip Rob Lewis (Aug 02 2019 at 16:09):

@Johan Commelin That's probably slightly more convenient than the match, yeah.

view this post on Zulip Johan Commelin (Aug 02 2019 at 16:12):

Ok, but now we need to prove that this is a basis...

view this post on Zulip Johan Commelin (Aug 02 2019 at 16:12):

It should suffice to prove linear independence

view this post on Zulip Reid Barton (Aug 02 2019 at 16:13):

something like

noncomputable def ε : Π {n : } (p : fin n  bool), V n [] 
| 0 _ := linear_map.id
| (n+1) p :=
  match p 0 with
  | ff := (ε (p  fin.succ)).comp (linear_map.fst _ _ _)
  | tt := (ε (p  fin.succ)).comp (linear_map.snd _ _ _)
  end

view this post on Zulip Reid Barton (Aug 02 2019 at 16:13):

Ok, but now we need to prove that this is a basis...

Yeah that's true

view this post on Zulip Johan Commelin (Aug 02 2019 at 16:14):

@Reid Barton Is there a reason you don't want to use mathlibs dual basis?

view this post on Zulip Reid Barton (Aug 02 2019 at 16:14):

I fear you might get stuck when you need to calculate the matrix entries but I don't really know

view this post on Zulip Reid Barton (Aug 02 2019 at 16:15):

because you won't have a formula for the dual basis like the one above

view this post on Zulip Reid Barton (Aug 02 2019 at 16:16):

Unless there are already theorems that say if we have bases of V and W, then we get a basis of V x W and the formula for the dual basis is the expected one

view this post on Zulip Johan Commelin (Aug 02 2019 at 16:17):

Aha, but wouldn't it be better/easier to prove those formulas?

view this post on Zulip Johan Commelin (Aug 02 2019 at 16:17):

Because otherwise you have to reprove that this thing is actually a dual basis.

view this post on Zulip Reid Barton (Aug 02 2019 at 16:18):

I guess we must already have a theorem about a basis of V x W so that we can compute its dimension

view this post on Zulip Reid Barton (Aug 02 2019 at 16:18):

You mean we should prove a mathlib theorem about the dual basis of V x W that comes from bases of V and W?

view this post on Zulip Reid Barton (Aug 02 2019 at 16:20):

I haven't seen the dual basis stuff in mathlib at all yet, let me take a look.

view this post on Zulip Reid Barton (Aug 02 2019 at 16:23):

So, there is

lemma is_basis_inl_union_inr {v : ι  β} {v' : ι'  γ}
  (hv : is_basis α v) (hv' : is_basis α v') : is_basis α (sum.elim (inl α β γ  v) (inr α β γ  v')) :=

view this post on Zulip Johan Commelin (Aug 02 2019 at 16:23):

Also, more trivialities:

/-- The hypercube.-/
def Q (n) : Type := fin n  bool

instance Q.fintype (n) : fintype (Q n) := by delta Q; apply_instance

def Q.card (n) : fintype.card (Q n) = 2^n :=
calc _ = _ : fintype.card_fun
   ... = _ : by simp only [fintype.card_fin, fintype.card_bool]

view this post on Zulip Johan Commelin (Aug 02 2019 at 16:24):

Ooh, that def should be a simp-lemma

view this post on Zulip Reid Barton (Aug 02 2019 at 16:25):

Maybe the right way to do all this is to just define the hypercube recursively after all, and then tack a translation onto fin n -> bool at the end if we want to.

view this post on Zulip Reid Barton (Aug 02 2019 at 16:26):

Then we can use that is_basis_inl_union_inr and add a formula to linear_algebra.dual about its dual basis

view this post on Zulip Reid Barton (Aug 02 2019 at 16:27):

Q (n+1) := Q n ⊕ Q n and whatever definition of "adjacent" is the most convenient

view this post on Zulip Johan Commelin (Aug 02 2019 at 16:28):

Or should we just prove that Q n →₀ ℝ is linearly equivelent to V n?

view this post on Zulip Johan Commelin (Aug 02 2019 at 16:28):

Or maybe we should redefine V n to be that space?

view this post on Zulip Reid Barton (Aug 02 2019 at 16:29):

Or should we just prove that Q n →₀ ℝ is linearly equivelent to V n?

This one sounds good

view this post on Zulip Reid Barton (Aug 02 2019 at 16:32):

Maybe by first providing Q (n+1) ≃ Q n ⊕ Q n

view this post on Zulip Johan Commelin (Aug 02 2019 at 16:36):

Aha, that also sounds like a good idea. And then use is_basis.comp?

view this post on Zulip Johan Commelin (Aug 02 2019 at 16:38):

Need to feed some kids :children_crossing: brb

view this post on Zulip Johan Commelin (Aug 02 2019 at 16:54):

Huh, there is no has_xor typeclass??

view this post on Zulip Johan Commelin (Aug 02 2019 at 17:32):

namespace Q
variable (n : )

instance : fintype (Q n) := by delta Q; apply_instance

variable {n}

def xor (x y : Q n) : Q n :=
λ i, bxor (x i) (y i)

@[symm] lemma xor_comm (x y : Q n) : x.xor y = y.xor x :=
funext $ λ i, bool.bxor_comm _ _

/-- The distance between two vertices of the hypercube.-/
def dist (x y : Q n) :  :=
(finset.univ : finset (fin n)).sum $ λ i, cond (x.xor y i) 1  0

@[simp] lemma dist_self (x : Q n) : x.dist x = 0 :=
finset.sum_eq_zero $ λ i hi, by simp only [xor, bxor_self, bool.cond_ff]

@[symm] lemma dist_symm (x y : Q n) : x.dist y = y.dist x :=
congr_arg ((finset.univ : finset (fin n)).sum) $
by { funext i, simp [xor_comm] }

/-- Two vertices of the hypercube are adjacent if their distance is 1.-/
def adjacent (x y : Q n) : Prop := x.dist y = 1

/-- The set of n-/
def neighbours (x : Q n) : set (Q n) := {y | x.adjacent y}

variable (n)

/-- The cardinality of the hypercube.-/
@[simp] lemma card : fintype.card (Q n) = 2^n :=
calc _ = _ : fintype.card_fun
   ... = _ : by simp only [fintype.card_fin, fintype.card_bool]

theorem sensitivity (H : set (Q n)) (x) (h : x  H) :
  real.sqrt n  fintype.card (H  (neighbours x) : set (Q n)) :=
sorry

end Q

Lean isn't yet happy with the theorem statement

view this post on Zulip Johan Commelin (Aug 02 2019 at 17:54):

Voila: that's a statement that Lean likes:

theorem sensitivity (H : finset (Q n)) (x) (h : x  H) :
  real.sqrt n  (H.filter (neighbours x)).card :=
sorry

view this post on Zulip Patrick Massot (Aug 02 2019 at 18:28):

Hi everybody. I'd like to play this game too. Can we somehow distribute efforts? Where are you now?

view this post on Zulip Reid Barton (Aug 02 2019 at 18:34):

Hi Patrick! I just got back to this, currently trying to add a recursive definition of the hypercube and associated basis.

view this post on Zulip Reid Barton (Aug 02 2019 at 18:35):

After that, I think there are some independent pieces to do

view this post on Zulip Patrick Massot (Aug 02 2019 at 18:35):

Do you think you could push something and give me lemmas to prove?

view this post on Zulip Johan Commelin (Aug 02 2019 at 18:36):

This is what I have now:

/-- The cardinality of the hypercube.-/
@[simp] lemma card : fintype.card (Q n) = 2^n :=
calc _ = _ : fintype.card_fun
   ... = _ : by simp only [fintype.card_fin, fintype.card_bool]

def equiv_sum : Q (n+1)  Q n  Q n :=
{ to_fun := λ x, cond (x 0)
                   (sum.inl (x  fin.succ))
                   (sum.inr (x  fin.succ)),
  inv_fun := λ x, sum.rec_on x
                   (λ y i, if h : i = 0 then tt else y (i.pred h))
                   (λ y i, if h : i = 0 then ff else y (i.pred h)),
  left_inv :=
  begin
    intro x, dsimp only, cases h : x 0;
    { funext i, dsimp only [bool.cond_tt, bool.cond_ff], split_ifs with H,
      { rw [H, h] },
      { rw [function.comp_app, fin.succ_pred] } }
  end,
  right_inv :=
  begin

  end }

view this post on Zulip Patrick Massot (Aug 02 2019 at 18:36):

Johan, which definition of Q n is this using?

view this post on Zulip Patrick Massot (Aug 02 2019 at 18:36):

Did you agree on the definitions of Q n and V n?

view this post on Zulip Reid Barton (Aug 02 2019 at 18:37):

Maybe I will just push something using a lot of constant and axiom as a starting point

view this post on Zulip Reid Barton (Aug 02 2019 at 18:38):

then perhaps we can distribute the representation decisions

view this post on Zulip Patrick Massot (Aug 02 2019 at 18:39):

It seems hard to decide independently the representations of V n and Q n

view this post on Zulip Johan Commelin (Aug 02 2019 at 18:42):

This is with Q n := fin n → bool

view this post on Zulip Reid Barton (Aug 02 2019 at 18:43):

I think https://github.com/leanprover-community/lean-sensitivity/commit/c2d0b69cbe175f3125c2719f3b87f2f6f626f424 is enough to make the rest of the proof go through

view this post on Zulip Reid Barton (Aug 02 2019 at 18:44):

Except with a correct statement of f_matrix_nonadjacent

view this post on Zulip Johan Commelin (Aug 02 2019 at 18:49):

@Reid Barton @Patrick Massot Shall I fill in the Q and adjacent constants?

view this post on Zulip Reid Barton (Aug 02 2019 at 18:50):

Feel free, I'm going to try to continue to sketch out the rest of the proof

view this post on Zulip Johan Commelin (Aug 02 2019 at 18:51):

@Patrick Massot @Floris van Doorn I've given you write permissions on the repo

view this post on Zulip Patrick Massot (Aug 02 2019 at 18:55):

thanks!

view this post on Zulip Patrick Massot (Aug 02 2019 at 18:58):

Reid I see you defined epsilon as the dual basis, but I liked the recursive definition

view this post on Zulip Patrick Massot (Aug 02 2019 at 18:59):

I'd like to work on the fact about |epsilon_q f_n e_p|

view this post on Zulip Rob Lewis (Aug 02 2019 at 18:59):

@Johan Commelin mind giving me access too? I was looking at this for a bit before dinner, might try to do a bit more.

view this post on Zulip Johan Commelin (Aug 02 2019 at 18:59):

Sure!

view this post on Zulip Reid Barton (Aug 02 2019 at 19:00):

I was intending that we'd add a lemma to mathlib that says that the dual basis element on inl i is given by projecting to the first factor, then applying the dual basis of the original basis

view this post on Zulip Johan Commelin (Aug 02 2019 at 19:00):

With this definition:

/-- The basis of V indexed by the hypercube.-/
def e : Π n, Q n  V n
| 0     := λ _, (1:)
| (n+1) := λ v, cond (v 0) (e n (v  fin.succ), 0) (0, e n (v  fin.succ))

I can't make {n} implicit...

view this post on Zulip Johan Commelin (Aug 02 2019 at 19:01):

@Rob Lewis Done, although I guess you also have admin rights by default...

view this post on Zulip Johan Commelin (Aug 02 2019 at 19:01):

Since you are admin of leanprover-community, right?

view this post on Zulip Reid Barton (Aug 02 2019 at 19:02):

Gah, I keep running into "maximum class-instance resolution depth has been reached" issues, I think they are related to decidable_eq somehow...

view this post on Zulip Rob Lewis (Aug 02 2019 at 19:02):

Oh, maybe. But thanks anyway!

view this post on Zulip Rob Lewis (Aug 02 2019 at 19:05):

I can't make {n} implicit...

Why not?

def e : Π {n}, Q n  V n
| 0     := λ _, (1:)
| (n+1) := λ v, cond (v 0) (e (v  fin.succ), 0) (0, e (v  fin.succ))

view this post on Zulip Reid Barton (Aug 02 2019 at 19:05):

@Patrick Massot That proof will depend on the definition of Q and e, though

view this post on Zulip Reid Barton (Aug 02 2019 at 19:07):

I pushed another commit about g

view this post on Zulip Patrick Massot (Aug 02 2019 at 19:07):

I'm using the definition of e that Rob just pasted

view this post on Zulip Patrick Massot (Aug 02 2019 at 19:08):

(which I indeed modified from Johan's message)

view this post on Zulip Jesse Michael Han (Aug 02 2019 at 19:11):

i'm also happy to contribute

what needs to be done besides the two sorrys Reid just pushed?

view this post on Zulip Reid Barton (Aug 02 2019 at 19:11):

Oh dang, H is not a great name

view this post on Zulip Reid Barton (Aug 02 2019 at 19:13):

@Jesse Michael Han I'll be pushing a couple more sorrys soon to complete the proof outline

view this post on Zulip Johan Commelin (Aug 02 2019 at 19:17):

I'm inductively proving that e is a basis.

view this post on Zulip Johan Commelin (Aug 02 2019 at 19:18):

See the jmc branch

view this post on Zulip Patrick Massot (Aug 02 2019 at 19:22):

As I wrote earlier, I'm inductively calculating epsilon q e p

view this post on Zulip Patrick Massot (Aug 02 2019 at 19:22):

I guess it should prove that e is a basis right?

view this post on Zulip Reid Barton (Aug 02 2019 at 19:24):

Lean isn't yet happy with the theorem statement

@Johan Commelin were you having trouble with type classes?

view this post on Zulip Johan Commelin (Aug 02 2019 at 19:24):

Well, sets weren't finsets and such

view this post on Zulip Johan Commelin (Aug 02 2019 at 19:25):

There is a working statement on the jmc branch

view this post on Zulip Johan Commelin (Aug 02 2019 at 19:25):

I'm almost done with the proof that e is a basis

view this post on Zulip Reid Barton (Aug 02 2019 at 19:28):

Okay, I pushed a couple more bits (theorem statement adapted from your Johan--but it should be an exists)

view this post on Zulip Reid Barton (Aug 02 2019 at 19:29):

Not sure if the next-to-last statement is phrased optimally

view this post on Zulip Patrick Massot (Aug 02 2019 at 19:34):

In those terms, I'm working on f_matrix_adjacent and f_matrix_nonadjacent

view this post on Zulip Jesse Michael Han (Aug 02 2019 at 19:35):

g_injective was easy:

lemma g_injective {m : } : function.injective (g m) :=
begin
  rw[g], intros x₁ x₂ H_eq, simp at *, exact H_eq.right
end

view this post on Zulip Reid Barton (Aug 02 2019 at 19:35):

I'm going to tackle the inequality that's the last sentence of the PDF I posted

view this post on Zulip Reid Barton (Aug 02 2019 at 19:35):

that leaves f_image_g and exists_eigenvalue

view this post on Zulip Johan Commelin (Aug 02 2019 at 19:36):

I'll push what I have now.

view this post on Zulip Johan Commelin (Aug 02 2019 at 19:38):

Ok, I pushed

view this post on Zulip Johan Commelin (Aug 02 2019 at 19:38):

It does contain a sorry. Will work on that soon.

view this post on Zulip Jesse Michael Han (Aug 02 2019 at 19:38):

i doubt f_image_g will be as easy but i can start on that. @Johan Commelin could i get push access as well?

view this post on Zulip Johan Commelin (Aug 02 2019 at 19:39):

afk

view this post on Zulip Reid Barton (Aug 02 2019 at 19:42):

What's your github username again?

view this post on Zulip Jesse Michael Han (Aug 02 2019 at 19:42):

jesse-michael-han

view this post on Zulip Reid Barton (Aug 02 2019 at 19:42):

Cool, added

view this post on Zulip Patrick Massot (Aug 02 2019 at 19:46):

Do we have a nice way to define the two injections from fin n -> bool to fin n+1 -> bool that differ on the zeroth element of fin n+1?

view this post on Zulip Patrick Massot (Aug 02 2019 at 19:46):

I guess I should use pattern matching

view this post on Zulip Johan Commelin (Aug 02 2019 at 19:47):

Check what I did

view this post on Zulip Johan Commelin (Aug 02 2019 at 19:47):

I've used cond (x 0) stuff

view this post on Zulip Patrick Massot (Aug 02 2019 at 19:48):

This is not quite the same question, is it?

view this post on Zulip Johan Commelin (Aug 02 2019 at 19:48):

Maybe not

view this post on Zulip Patrick Massot (Aug 02 2019 at 19:48):

You're going i the easier direction (decreasing n)

view this post on Zulip Johan Commelin (Aug 02 2019 at 19:49):

Right, I was too fast... sorry

view this post on Zulip Reid Barton (Aug 02 2019 at 19:52):

In principle I like building the equivalence Q (n+1) ≃ Q n ⊕ Q n out of stuff in data.equiv.basic/data.equiv.fin though it would be kind of verbose

view this post on Zulip Patrick Massot (Aug 02 2019 at 19:53):

I found the library bit I was missing

view this post on Zulip Patrick Massot (Aug 02 2019 at 19:53):

I can now write Q n → Q (n+1) := λ p, λ k, if h : k = 0 then tt else p (k.pred h)

view this post on Zulip Johan Commelin (Aug 02 2019 at 19:53):

That's what I used

view this post on Zulip Patrick Massot (Aug 02 2019 at 19:53):

I was missing pred

view this post on Zulip Johan Commelin (Aug 02 2019 at 19:53):

I already pushed that equiv @Reid Barton

view this post on Zulip Patrick Massot (Aug 02 2019 at 19:54):

Sorry Johan, I focused on your cond and missed pred

view this post on Zulip Reid Barton (Aug 02 2019 at 19:54):

Oh I see, just defined manually yeah

view this post on Zulip Reid Barton (Aug 02 2019 at 20:09):

I changed H from a finset back to a set though I'm not yet entirely sure whether it was a good idea

view this post on Zulip Johan Commelin (Aug 02 2019 at 20:18):

Ooh, you should also feel free to refactor Q.equiv_sum

view this post on Zulip Johan Commelin (Aug 02 2019 at 20:19):

If you want to use more fancy library functions (-;

view this post on Zulip Chris Hughes (Aug 02 2019 at 20:23):

finsets ftw.

view this post on Zulip Floris van Doorn (Aug 02 2019 at 20:33):

@Patrick Massot: I would suggest

def cons (x : α) (v : fin n → α) : fin (n+1) → α :=
λ j, fin.cases x v j

view this post on Zulip Patrick Massot (Aug 02 2019 at 20:34):

What is that?

view this post on Zulip Floris van Doorn (Aug 02 2019 at 20:36):

To define the maps Q n → Q (n+1), fin.cases is there exactly for that purpose.

view this post on Zulip Patrick Massot (Aug 02 2019 at 20:37):

Oh I see

view this post on Zulip Patrick Massot (Aug 02 2019 at 20:41):

It's still totally mysterious to me that your definition cannot be rewritten as fin.cases x v

view this post on Zulip Floris van Doorn (Aug 02 2019 at 20:56):

Lean is pretty bad at these kind of unification problems, unless it uses the [elab_as_eliminator] attribute. With that attribute it is hardcoded to look at the third explicit argument of fin.cases, and then figure out what to do using the type of the third argument. If you don't give it 3 arguments, it will do the standard unification procedure, which fails.

view this post on Zulip Patrick Massot (Aug 02 2019 at 20:57):

What do you get from using this definition rather than mine?

view this post on Zulip Patrick Massot (Aug 02 2019 at 20:57):

It seems harder to prove lemmas about it

view this post on Zulip Patrick Massot (Aug 02 2019 at 20:57):

but probably I'm missing library lemmas

view this post on Zulip Johan Commelin (Aug 02 2019 at 21:07):

I'm calling it a day

view this post on Zulip Johan Commelin (Aug 02 2019 at 21:07):

Unfortunately e is still not a basis

view this post on Zulip Johan Commelin (Aug 02 2019 at 21:08):

I pushed the mess that I have so far.

view this post on Zulip Patrick Massot (Aug 02 2019 at 21:08):

This is all very frustrating. I'm trying to learn how to make weird inductions in Lean

view this post on Zulip Patrick Massot (Aug 02 2019 at 21:08):

And I'm very bad at it

view this post on Zulip Jesse Michael Han (Aug 02 2019 at 21:14):

i'm halfway done with f_image_g

view this post on Zulip Floris van Doorn (Aug 02 2019 at 21:20):

My hope was that the lemmas you needed were already in the library. Although I don't see anything other than cases_zero and cases_succ. What else do you need?

view this post on Zulip Jesse Michael Han (Aug 02 2019 at 22:27):

i'm done with f_image_g except for these two annoying lemmas:

lemma cast_lemma_1 {m : } : 0  (1 + (nat.cast m) : ) := sorry

lemma cast_lemma_2 {m : } : (nat.cast (nat.succ m) : ) = (1 + nat.cast m : ) := sorry

view this post on Zulip Jesse Michael Han (Aug 02 2019 at 22:30):

oh nevermind, i just needed to make a change:

lemma cast_lemma_1 {m : } : 0  (1 + (nat.cast m) : ) :=
by {change (0 : )  (1 + m : ), suffices this : 0  (m : ), by {linarith}, simp}

lemma cast_lemma_2 {m : } : (nat.cast (nat.succ m) : ) = (1 + nat.cast m : ) :=
by change (nat.succ m) = (1 + m : ); simp

view this post on Zulip Jesse Michael Han (Aug 02 2019 at 22:57):

[edited] oops i missed the invite link

view this post on Zulip Patrick Massot (Aug 02 2019 at 23:53):

I'm done computing the matrix

view this post on Zulip Patrick Massot (Aug 02 2019 at 23:58):

I haven't use @Johan Commelin xor adjacency definition, see https://github.com/leanprover-community/lean-sensitivity/blob/058def458c9a4023ec95aaf211c0f7a22f77a05d/src/sensitivity.lean#L232-L235. I hope my definition is the same as his. At least I can compute the matrix using it

view this post on Zulip Patrick Massot (Aug 02 2019 at 23:59):

I also used the explicit inductive definition of the dual basis, and proved the duality equations.

view this post on Zulip Patrick Massot (Aug 03 2019 at 00:00):

Note that I spent most of my time trying to prove fancy induction principle on Q n, messing around with elab_as_eliminator and induction ... using .... But nothing worked, so I reverted to good old cases.

view this post on Zulip Patrick Massot (Aug 03 2019 at 00:18):

Is there any reason we use bool everywhere instead of Prop?

view this post on Zulip Johan Commelin (Aug 03 2019 at 05:44):

@Patrick Massot You don't need bool_cases. You can just write cases h : x p.

view this post on Zulip Patrick Massot (Aug 03 2019 at 09:51):

Nice trick! I tried by_cases hp : x p = tt but this gave an inconvenient second case. I'm a bit disappointed that the proof wasn't finished while I slept. I'll be again away from Lean for the next 9 hours, so maybe this will be enough. Otherwise I'll play again tonight. Have fun!

view this post on Zulip Patrick Massot (Aug 03 2019 at 17:48):

@Jesse Michael Han I think you have slightly too much love for tidy. What about

lemma f_image_g' {m : } (w : V (m + 1)) (hv :  v, w = g m v) :
  (f (m + 1) : V (m + 1)  V (m + 1)) w = real.sqrt (m + 1)  w :=
begin
  rcases hv with v, rfl,
  dsimp [g],
  erw f,
  simp [f_squared],
  rw [smul_add, smul_smul, real.mul_self_sqrt (by exact_mod_cast zero_le _ : 0  (1 : ) + m), add_smul, one_smul],
  abel,
end

view this post on Zulip Patrick Massot (Aug 03 2019 at 17:49):

Do you mind if I replace your proof by this one? I looks closer to the paper proof

view this post on Zulip Jesse Michael Han (Aug 03 2019 at 17:50):

oh, i didn't see f_squared

yeah that looks much better

view this post on Zulip Patrick Massot (Aug 03 2019 at 17:51):

Did you look at the pdf proof?

view this post on Zulip Jesse Michael Han (Aug 03 2019 at 17:53):

yes, but i took a longer route in proving the left-side equality (because i essentially rederived f_squared)

view this post on Zulip Patrick Massot (Aug 03 2019 at 17:54):

Anyway, is anybody working on the next lemma?

view this post on Zulip Patrick Massot (Aug 03 2019 at 17:54):

I mean exists_eigenvalue

view this post on Zulip Patrick Massot (Aug 03 2019 at 17:55):

I know nothing about dimension in mathlib, but it looks like a good opportunity to learn

view this post on Zulip Jesse Michael Han (Aug 03 2019 at 17:56):

i'm not working on it

i was going to wait to hear back from reid

view this post on Zulip Patrick Massot (Aug 03 2019 at 18:05):

exists_mem_ne_zero_of_dim_pos looks very promising

view this post on Zulip Jesse Michael Han (Aug 03 2019 at 20:50):

i started a bit on degree_theorem; feel free to overwrite or build on what's there

i'm not sure if finsupp.mem_span_if_total is the correct way to extract a linear combination from a proof of membership in a span, but it reduces to a finset.sum which seems to be what we want.

view this post on Zulip Patrick Massot (Aug 03 2019 at 20:55):

I finished e_is_basis that @Johan Commelin almost did yesterday

view this post on Zulip Patrick Massot (Aug 03 2019 at 20:56):

Wait. @Jesse Michael Han did you proof start timeout?

view this post on Zulip Patrick Massot (Aug 03 2019 at 20:56):

I tried to merge and I see it times out

view this post on Zulip Patrick Massot (Aug 03 2019 at 20:58):

https://github.com/leanprover-community/lean-sensitivity/commit/0f1468180a143ba8d40276b2bf7198fc2c250093 is my attempt at the dimension argument

view this post on Zulip Patrick Massot (Aug 03 2019 at 20:58):

But I don't know enough cardinal theory to do finite dimensional linear algebra :sad:

view this post on Zulip Jesse Michael Han (Aug 03 2019 at 20:58):

i'll take a look

view this post on Zulip Patrick Massot (Aug 03 2019 at 20:59):

For instance I need to prove:

n : 
 2 ^ n < cardinal.omega

view this post on Zulip Patrick Massot (Aug 03 2019 at 20:59):

and

n : ,
 2 ^ n = 2 ^ n

Where at least some of this stuff is in cardinals

view this post on Zulip Patrick Massot (Aug 03 2019 at 21:05):

I won't do more tonight.

view this post on Zulip Jesse Michael Han (Aug 03 2019 at 21:14):

OK, leanpkg test succeeds at my commit, but indeed times out after the merge. i'll fix it i fixed it

view this post on Zulip Chris Hughes (Aug 03 2019 at 21:21):

If you know everything is finite dimensional, you probably shouldn't be using cardinals. Everything about infinite dimension should be transferred to findim really, or you have to faff with coercions

view this post on Zulip Patrick Massot (Aug 03 2019 at 21:32):

Chris, the problem is we seem to have a lot more lemmas about dim than findim

view this post on Zulip Patrick Massot (Aug 03 2019 at 21:35):

For instance, do you have dim_sup_add_dim_inf_eq for findim?

view this post on Zulip Patrick Massot (Aug 03 2019 at 21:36):

Or do you have a nice way to import such theorems into the finite dimensional world?

view this post on Zulip Chris Hughes (Aug 03 2019 at 21:37):

I have virtually nothing. I guess when transfer comes along it will be easier. But they'll just be simp [nat.cast_add] or something.

view this post on Zulip Patrick Massot (Aug 03 2019 at 21:39):

Was this mirroring discussed with @Mario Carneiro? It seems a bit sad to duplicate all this, but we really want to be able to use finite dimensions as natural numbers

view this post on Zulip Mario Carneiro (Aug 03 2019 at 21:40):

most facts about numbers being equivalent to finite cardinals are proven

view this post on Zulip Patrick Massot (Aug 03 2019 at 21:41):

what do you mean?

view this post on Zulip Chris Hughes (Aug 03 2019 at 21:43):

Like cast is monotonic etc. Unfortunately, cardinals are not an ordered semiring, so the generic lemmas don't work.

view this post on Zulip Patrick Massot (Aug 03 2019 at 21:43):

Are they tagged for use by norm_cast?

view this post on Zulip Patrick Massot (Aug 03 2019 at 21:44):

For instance attribute [elim_cast] cardinal.nat_cast_in seems to be missing

view this post on Zulip Jesse Michael Han (Aug 03 2019 at 22:06):

i think the version of 2^n < omega you stated is parsed by Lean as monoid.pow, which is more annoying to deal with

but if you ensure it's the cardinal pow of casted nats, it's 2 lemmas away:

import set_theory.cardinal

universe u

example {n : } : (2) ^ (n : cardinal.{u}) < (cardinal.omega : cardinal.{u}) :=
 by rw[<-cardinal.nat_cast_pow]; exact cardinal.nat_lt_omega _

view this post on Zulip Patrick Massot (Aug 03 2019 at 22:15):

Do we know that the restriction of linear_independent family to a subtype is linear_independent?

view this post on Zulip Patrick Massot (Aug 03 2019 at 22:24):

Anyway, I said I would stop more than one hour ago, so I should really stop now

view this post on Zulip Patrick Massot (Aug 03 2019 at 22:25):

Modulo the restriction thing, the proof of the dimension argument is reduced to these 2^n < omega things

view this post on Zulip Patrick Massot (Aug 03 2019 at 22:26):

see https://github.com/leanprover-community/lean-sensitivity/commit/af0e391f1d39d5448e3aff901f1dbe7eb10d3e32

view this post on Zulip Jesse Michael Han (Aug 03 2019 at 22:26):

the monoid.pow is annoying because you have to do an induction, but it's not bad:

example {n : } : (2 ^ n : cardinal) = (2 ^ (n : cardinal.{u}) : cardinal.{u}) :=
begin
  induction n with n ih,
    {simp},
    {rw[nat.cast_succ, cardinal.power_add, <-ih, cardinal.power_one, mul_comm], refl },
end

you can get the first one from this one, i believe

view this post on Zulip Patrick Massot (Aug 03 2019 at 22:27):

I followed Chris's advice to get rid of dim as soon as I applied the lemmas

view this post on Zulip Patrick Massot (Aug 03 2019 at 22:28):

Nice, feel free to remove those sorries and push. I'll go to bed

view this post on Zulip Patrick Massot (Aug 03 2019 at 22:29):

Maybe you can even finish the whole thing while I sleep

view this post on Zulip Patrick Massot (Aug 03 2019 at 22:30):

Or maybe @Reid Barton will come back and cross the finish line for us

view this post on Zulip Patrick Massot (Aug 03 2019 at 22:31):

Zulip says his local time is 6:30pm

view this post on Zulip Patrick Massot (Aug 03 2019 at 22:31):

This leaves him the whole evening and night

view this post on Zulip Patrick Massot (Aug 03 2019 at 22:31):

and same for you!

view this post on Zulip Patrick Massot (Aug 03 2019 at 22:32):

Have fun!

view this post on Zulip Yao Liu (Aug 04 2019 at 04:46):

As a spectator, I was looking around and found (via Terry Tao's blog post) this interpretation https://arxiv.org/abs/1907.11175
namely, the 2n2^n-dimensional space ought to be the exterior algebra (or Clifford algebra) of an nn-dimensional vector space.

view this post on Zulip Jesse Michael Han (Aug 04 2019 at 21:07):

i'm trying to import analysis.normed_space.basic to use the triangle inequality, but this causes Lean on both my machines to start complaining about "equation compiler failed to generate bytecode for e._main", and something not being a rfl lemma, etc. the errors appear iff i have that import.

does anyone know why this would happen?

view this post on Zulip Kevin Buzzard (Aug 04 2019 at 21:12):

equation compiler failed to generate bytecode for 'e._main'
nested exception message:
code generation failed, VM does not have code for 'real.normed_field'

view this post on Zulip Kevin Buzzard (Aug 04 2019 at 21:16):

The entire file analysis.normed_space.basic is marked noncomputable so maybe it's no surprise the VM doesn't have code for real.normed_field

view this post on Zulip Kevin Buzzard (Aug 04 2019 at 21:17):

If you mark e noncomputable then most of the errors go away

view this post on Zulip Jesse Michael Han (Aug 04 2019 at 21:19):

indeed, but i was alarmed that previous proofs which were by refl were somehow no longer so after adding noncomputable

view this post on Zulip Jesse Michael Han (Aug 04 2019 at 21:19):

but that error can be fixed by changing rfl to by rw e...

view this post on Zulip Kevin Buzzard (Aug 04 2019 at 21:20):

you golfed me, I just found by unfold e :-)

view this post on Zulip Johan Commelin (Aug 05 2019 at 06:35):

Can someone give a status update? Is the only thing that needs to be done the tying together of some loose ends?

view this post on Zulip Chris Hughes (Aug 05 2019 at 06:42):

Looks like two sorries right now.

view this post on Zulip Chris Hughes (Aug 05 2019 at 06:42):

Neither are that hard.

view this post on Zulip Johan Commelin (Aug 05 2019 at 06:44):

I'm tackling adjacent_symm

view this post on Zulip Chris Hughes (Aug 05 2019 at 06:46):

I just proved that.

view this post on Zulip Chris Hughes (Aug 05 2019 at 06:46):

There are two sorries in the final theorem. I'm doing the first.

view this post on Zulip Chris Hughes (Aug 05 2019 at 06:59):

One sorry left now.

view this post on Zulip Johan Commelin (Aug 05 2019 at 08:17):

@Chris Hughes Are you still working on this?

view this post on Zulip Johan Commelin (Aug 05 2019 at 08:17):

I connected adjacent back to my definition that used dist.

view this post on Zulip Chris Hughes (Aug 05 2019 at 08:59):

I'm not. The last sorry looked like you needed to understand what was going on. Everything else I proved did not require that.

view this post on Zulip Johan Commelin (Aug 05 2019 at 09:01):

Ok, I see.

view this post on Zulip Patrick Massot (Aug 05 2019 at 09:42):

Johan, is there any use to the distance you defined, and relating it to adjacent? I'm not sure it makes adjacent so much more related to the usual definition. Maybe we could define a general graph class, and then adjacency in this context, and relate. But the real question is: what is the usual definition of the graph structure on Q n? Maybe the simplest answer goes through defining the (Z/2)^n action on Q n. For instance we could redefine Q n to be (Z/2)^n instead of this weird CS bool thing. Then define the canonical basis b for (Z/2)^n (it should already be in mathlib) and define adjacent x y by exists i, b i bul x = y.

view this post on Zulip Johan Commelin (Aug 05 2019 at 09:49):

I'm almost done with the final sorry.

view this post on Zulip Johan Commelin (Aug 05 2019 at 09:49):

I'll push what I have. Lunch time now.

view this post on Zulip Patrick Massot (Aug 05 2019 at 09:50):

Oh, I was starting on this final sorry

view this post on Zulip Patrick Massot (Aug 05 2019 at 09:51):

Do you mind if I finish during your lunch?

view this post on Zulip Patrick Massot (Aug 05 2019 at 09:56):

@Johan Commelin should I push?

view this post on Zulip Patrick Massot (Aug 05 2019 at 09:57):

Ok, let's say he was really having lunch

view this post on Zulip Patrick Massot (Aug 05 2019 at 09:57):

https://github.com/leanprover-community/lean-sensitivity/commit/f7be6abb34eafcd01df9417c99df34f8076362b9

view this post on Zulip Patrick Massot (Aug 05 2019 at 09:58):

Now we have a lot of cleanup to do before telling people about it

view this post on Zulip Johan Commelin (Aug 05 2019 at 10:22):

Nice, well done!

view this post on Zulip Johan Commelin (Aug 05 2019 at 10:22):

@Reid Barton @Rob Lewis @Jesse Michael Han @Chris Hughes @Floris van Doorn We have a theorem!

view this post on Zulip Kevin Buzzard (Aug 05 2019 at 10:25):

Well done!

I really like these "oh look here's some relatively simple-looking maths, how hard is it actually to formalise?" questions. A year or so ago my impression was "in Lean, it's probably going to be tough". Now my impression is turning to "it might be not too bad". We have cubing the cube, the IMO questions, working out pi to 7 decimal places, and now this.

view this post on Zulip Patrick Massot (Aug 05 2019 at 10:26):

It's still a lot harder than it should be

view this post on Zulip Kevin Buzzard (Aug 05 2019 at 10:26):

But I suspect it's a lot easier than it was.

view this post on Zulip Patrick Massot (Aug 05 2019 at 10:26):

Unless you already know perfectly all the relevant part of mathlib

view this post on Zulip Patrick Massot (Aug 05 2019 at 10:26):

Oh yes of course

view this post on Zulip Kevin Buzzard (Aug 05 2019 at 10:26):

It's almost getting to the point where it's as easy as I thought it would be before I knew anything about how this stuff worked.

view this post on Zulip Johan Commelin (Aug 05 2019 at 10:27):

Let's see if we can write transfer lemmas for this little project, to make things shorter

view this post on Zulip Kevin Buzzard (Aug 05 2019 at 10:27):

What does that mean?

view this post on Zulip Johan Commelin (Aug 05 2019 at 10:28):

Because we have Q n →₀ ℝ and V n, and they are canonically isomorphic.

view this post on Zulip Kevin Buzzard (Aug 05 2019 at 10:28):

for sure

view this post on Zulip Johan Commelin (Aug 05 2019 at 10:28):

Some proofs are easy on one side, others on the other.

view this post on Zulip Patrick Massot (Aug 05 2019 at 10:28):

What do you think about starting the refactor with:

notation `Z/2` := zmodp 2 nat.prime_two

def Q (n : ) := fin n  Z/2

view this post on Zulip Johan Commelin (Aug 05 2019 at 10:28):

This might be a good test case for the existing transfer api.

view this post on Zulip Johan Commelin (Aug 05 2019 at 10:28):

@Patrick Massot Why would that help?

view this post on Zulip Kevin Buzzard (Aug 05 2019 at 10:29):

I think your suggestion is a really worthwhile one Johan.

view this post on Zulip Patrick Massot (Aug 05 2019 at 10:29):

And then try to understand that std_basis thing, and define adjacency as I wrote it should be defined?

view this post on Zulip Johan Commelin (Aug 05 2019 at 10:29):

What does Z/2 have that bool doesn't have?

view this post on Zulip Kevin Buzzard (Aug 05 2019 at 10:29):

Looks

view this post on Zulip Patrick Massot (Aug 05 2019 at 10:29):

A group structure

view this post on Zulip Patrick Massot (Aug 05 2019 at 10:29):

Johan, is there any use to the distance you defined, and relating it to adjacent? I'm not sure it makes adjacent so much more related to the usual definition. Maybe we could define a general graph class, and then adjacency in this context, and relate. But the real question is: what is the usual definition of the graph structure on Q n? Maybe the simplest answer goes through defining the (Z/2)^n action on Q n. For instance we could redefine Q n to be (Z/2)^n instead of this weird CS bool thing. Then define the canonical basis b for (Z/2)^n (it should already be in mathlib) and define adjacent x y by exists i, b i bul x = y.

See above

view this post on Zulip Patrick Massot (Aug 05 2019 at 10:30):

I think this would give a much more recognizable adjacency relation

view this post on Zulip Kevin Buzzard (Aug 05 2019 at 10:30):

instead of this weird CS bool thing

Mathematicians still failing to come to terms with weird CS stuff

view this post on Zulip Patrick Massot (Aug 05 2019 at 10:31):

It's hard to express the fact that x and y are two different elements of a two elements sets in a nicer way than x = y +1

view this post on Zulip Johan Commelin (Aug 05 2019 at 10:31):

@Patrick Massot Ok, that seems fine.

view this post on Zulip Kevin Buzzard (Aug 05 2019 at 10:31):

x \ne y?

view this post on Zulip Patrick Massot (Aug 05 2019 at 10:32):

If I understand correctly mathlib still don't have the canonical basis of K^n (it has a more general std_basis for pi). It's time we fix that

view this post on Zulip Johan Commelin (Aug 05 2019 at 10:32):

Anyway, I have a meeting scheduled in 10 minutes... so I can't help too much with the refactor now.

view this post on Zulip Patrick Massot (Aug 05 2019 at 10:32):

I also need to go

view this post on Zulip Patrick Massot (Aug 05 2019 at 10:32):

Something easy that anyone can do is to collect all lemmas from that file that should be in mathlib and PR them

view this post on Zulip Patrick Massot (Aug 05 2019 at 10:33):

We should do that before refactoring because some of them will turn out to be unneeded for the sensitivity proof and will disappear if we don't rescue them first

view this post on Zulip Rob Lewis (Aug 05 2019 at 11:47):

I was away from Lean for the weekend and it looks like I missed all the fun. Nice job, guys!

view this post on Zulip Reid Barton (Aug 05 2019 at 12:04):

We should do that before refactoring because some of them will turn out to be unneeded for the sensitivity proof and will disappear if we don't rescue them first

I'm going to start by moving them to their own file

view this post on Zulip Reid Barton (Aug 05 2019 at 12:04):

Rob I think there's still plenty of clean up that would be nice to do. You had a shorter proof of f_squared right?

view this post on Zulip Rob Lewis (Aug 05 2019 at 12:05):

I just pushed it 20 seconds ago...

view this post on Zulip Rob Lewis (Aug 05 2019 at 12:05):

Looking at a few other proofs now that should be easy to clean up.

view this post on Zulip Reid Barton (Aug 05 2019 at 12:06):

Give me a couple minutes to push what I have simplified already

view this post on Zulip Rob Lewis (Aug 05 2019 at 12:08):

Sure thing.

view this post on Zulip Reid Barton (Aug 05 2019 at 12:10):

OK, pushed

view this post on Zulip Reid Barton (Aug 05 2019 at 12:11):

Next I was going to try to replace the definition of adjacent by def adjacent' {n : ℕ} (p q : Q n) : Prop := ∃! i, p i ≠ q i and get rid of the dist stuff

view this post on Zulip Reid Barton (Aug 05 2019 at 12:12):

Although I guess this means proving something similar to adjacent_iff_dist

view this post on Zulip Reid Barton (Aug 05 2019 at 12:13):

By the way, what is this run_cmd tactic.skip magic about?

view this post on Zulip Rob Lewis (Aug 05 2019 at 12:14):

I suspect that will be nicer, but I'm not sure... I'm gonna try some more local cleanup toward the bottom.

view this post on Zulip Rob Lewis (Aug 05 2019 at 12:14):

I was editing the theorem below, which was causing the one above to recompile constantly, and it was really slow. Putting no-op code in between makes it stop recompiling the one above.

view this post on Zulip Rob Lewis (Aug 05 2019 at 12:15):

It wasn't meant to be pushed though, I deleted it.

view this post on Zulip Kevin Buzzard (Aug 05 2019 at 12:15):

You're giving away your secrets!

view this post on Zulip Kevin Buzzard (Aug 05 2019 at 12:15):

Isn't there supposed to be some way of doing this with a .?

view this post on Zulip Rob Lewis (Aug 05 2019 at 12:16):

. might have the same effect. Not sure.

view this post on Zulip Johan Commelin (Aug 05 2019 at 12:19):

I always use .

view this post on Zulip Reid Barton (Aug 05 2019 at 12:25):

I'm constantly getting "excessive memory consumption" errors, is there some way to deal with these?

view this post on Zulip Reid Barton (Aug 05 2019 at 12:25):

The dependencies are definitely built

view this post on Zulip Johan Commelin (Aug 05 2019 at 12:36):

I added some foo_apply lemmas and golfed f_image_g.

view this post on Zulip Rob Lewis (Aug 05 2019 at 12:40):

I'm constantly getting "excessive memory consumption" errors, is there some way to deal with these?

Hmm, something's funny with the simp set. It's spending over two seconds in the simp only in the 0 case of f_squared, that seems excessive.

view this post on Zulip Rob Lewis (Aug 05 2019 at 12:41):

Or, maybe not the simp set. Even the definition of f takes a while. Probably a big type class search.

view this post on Zulip Reid Barton (Aug 05 2019 at 12:41):

I don't understand how anyone could have written any of this interactively. Did I break everything?

view this post on Zulip Rob Lewis (Aug 05 2019 at 12:42):

It's a little slow but it works fine for me.

view this post on Zulip Kevin Buzzard (Aug 05 2019 at 12:42):

restart Lean?

view this post on Zulip Rob Lewis (Aug 05 2019 at 12:46):

Adding this short-circuit helps in a few places:

def Vn_module {n} : module  (V n) := by apply_instance
local attribute [instance, priority 10000] Vn_module

view this post on Zulip Reid Barton (Aug 05 2019 at 12:50):

Now leanpkg build has started printing goals and failing without printing any error message

view this post on Zulip Reid Barton (Aug 05 2019 at 12:51):

(not related to that module instance)

view this post on Zulip Kevin Buzzard (Aug 05 2019 at 12:51):

reboot your computer??

view this post on Zulip Patrick Massot (Aug 05 2019 at 12:59):

I don't understand how anyone could have written any of this interactively. Did I break everything?

I noticed it was very slow, but wasn't sure whether it was because I'm using my laptop. Anyway, I was doing the usual sorry dance (every have that is proved is replaced by a commented out proof and sorry).

view this post on Zulip Patrick Massot (Aug 05 2019 at 13:00):

I'd love to help refactoring but I'm on beach duty

view this post on Zulip Reid Barton (Aug 05 2019 at 13:03):

I found out how to increase the default memory limit for lean in emacs, so now I can load the whole file again

view this post on Zulip Johan Commelin (Aug 05 2019 at 13:04):

Why does Lean not understand what I mean when I write

def RQ_equiv_V : Π (n : ), (Q n  ) ≃ₗ[] V n
| 0     := _
| (n+1) := _

view this post on Zulip Johan Commelin (Aug 05 2019 at 13:04):

It takes ages to parse/elaborate/tc this

view this post on Zulip Johan Commelin (Aug 05 2019 at 13:04):

Result: 4 deterministic timeouts

view this post on Zulip Rob Lewis (Aug 05 2019 at 13:04):

Does adding this before help?

def Vn_module {n} : module  (V n) := by apply_instance
def acg {n} : add_comm_semigroup (V n) := by apply_instance
def acm {n} : add_comm_monoid (V n) := by apply_instance
def hsr {n} : has_scalar  (V n) := by apply_instance
def hav {n} : has_add (V n) := by apply_instance

local attribute [instance, priority 100000] acg acm hsr hav Vn_module

view this post on Zulip Rob Lewis (Aug 05 2019 at 13:05):

I'm timing right now, but it feels like a very significant speedup on the whole file.

view this post on Zulip Rob Lewis (Aug 05 2019 at 13:05):

Yeah, those short circuits reduce the compile time by more than 50%.

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

Doesn't help for this thing :sad:

view this post on Zulip Johan Commelin (Aug 05 2019 at 13:06):

Btw, should we even use real numbers?

view this post on Zulip Johan Commelin (Aug 05 2019 at 13:06):

For this problem nat.sqrt is just as good as real.sqrt, isn't it?

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

So we could do the whole thing with -modules

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

Anyway, I don't mind using real.

view this post on Zulip Johan Commelin (Aug 05 2019 at 13:08):

Without this RQ_equiv_V I don't think we can get very far with "transfer"-like techniques.

view this post on Zulip Johan Commelin (Aug 05 2019 at 13:24):

@Reid Barton Have your problems gone away?

view this post on Zulip Reid Barton (Aug 05 2019 at 13:25):

Some of them

view this post on Zulip Rob Lewis (Aug 05 2019 at 13:27):

Do you have local changes that are causing this? It compiles with -T20000 for me, so there shouldn't be any memory issues.

view this post on Zulip Jesse Michael Han (Aug 05 2019 at 13:29):

I don't understand how anyone could have written any of this interactively.

in the case of degree_theorem, very painfully...

what is this "insert no-op code" magic? do i put a . or run_cmd tactic.skip above the current declaration i'm working on to stop recompilation of previous theorems?

view this post on Zulip Rob Lewis (Aug 05 2019 at 13:29):

The only suspicious thing I see in the profiling is that simp is spending a long time in tactic.join_user_simp_lemmas.

view this post on Zulip Johan Commelin (Aug 05 2019 at 13:30):

@Jesse Michael Han Yes. . is gold.

view this post on Zulip Reid Barton (Aug 05 2019 at 13:37):

I used to have some local changes but I still had problems when I got rid of them

view this post on Zulip Reid Barton (Aug 05 2019 at 13:37):

Is the default memory limit different in VS code maybe?

view this post on Zulip Kevin Buzzard (Aug 05 2019 at 13:38):

It's 100000 in VS Code I believe

view this post on Zulip Kevin Buzzard (Aug 05 2019 at 13:38):

The T50000 challenge was what happened when I halved it

view this post on Zulip Reid Barton (Aug 05 2019 at 13:44):

That's the "time" limit I thought

view this post on Zulip Kevin Buzzard (Aug 05 2019 at 13:44):

oh apologies. Memory limit is...

view this post on Zulip Kevin Buzzard (Aug 05 2019 at 13:45):

4096 megs

view this post on Zulip Reid Barton (Aug 05 2019 at 13:46):

Ah okay, that explains some things. In emacs it's 1024 megs

view this post on Zulip Jesse Michael Han (Aug 05 2019 at 13:52):

looks like something we should patch in the community version of lean-mode

4096 megs and constantly swapping

view this post on Zulip Johan Commelin (Aug 05 2019 at 14:23):

@Rob Lewis Did you manage to clean things up at the bottom of the file?

view this post on Zulip Johan Commelin (Aug 05 2019 at 14:24):

Do we have some sort of "cleaning up" roadmap?

view this post on Zulip Johan Commelin (Aug 05 2019 at 14:26):

The reason I wrote my dist function is that I imagined that we might rename Q to hypercube and put it in mathlib, and show that it is a (discrete) metric space, etc....

view this post on Zulip Johan Commelin (Aug 05 2019 at 14:27):

Not sure if we want to do things like that.

view this post on Zulip Rob Lewis (Aug 05 2019 at 14:28):

I got distracted by trying to speed things up. I have no major changes right now.

view this post on Zulip Rob Lewis (Aug 05 2019 at 14:29):

But performance-wise, I don't see any more obvious places to optimize. It seems to behave pretty reasonably.

view this post on Zulip Johan Commelin (Aug 05 2019 at 14:30):

Can you get the statement of RQ_equiv_V to work?

view this post on Zulip Johan Commelin (Aug 05 2019 at 14:30):

@Reid Barton What do you think of @Patrick Massot's suggestion for adjacency?

view this post on Zulip Johan Commelin (Aug 05 2019 at 14:31):

It's quite similar to your ∃! i, x i ≠ y i suggestion, but it exploits a bit of group structure.

view this post on Zulip Rob Lewis (Aug 05 2019 at 14:56):

local attribute [instance, priority 10000] finsupp.module classical.prop_decidable makes it work. The decidable instance isn't necessary but it speeds things up a little bit.

view this post on Zulip Rob Lewis (Aug 05 2019 at 14:56):

Once again, the type classes here are kind of a mess.

view this post on Zulip Johan Commelin (Aug 05 2019 at 14:58):

It's really sad that this creates a mess. It doesn't feel like we are doing something horrible.

view this post on Zulip Johan Commelin (Aug 05 2019 at 14:58):

I just pushed a compression of duality.

view this post on Zulip Jesse Michael Han (Aug 05 2019 at 15:34):

i'm working on turning degree_theorem into a calc proof after the existential instantiation of q

also thank you johan for the cleanup :^)

view this post on Zulip Reid Barton (Aug 05 2019 at 15:37):

i'm working on turning degree_theorem into a calc proof after the existential instantiation of q

Oh cool, I wanted to do this as well but currently I'm trying to simplify exists_eigenvalue a bit

view this post on Zulip Rob Lewis (Aug 05 2019 at 15:40):

Have you made any structural changes to exists_eigenvalue? I have a few cosmetic updates local, but nothing important.

view this post on Zulip Rob Lewis (Aug 05 2019 at 15:40):

I won't touch degree_theorem if Jesse is on it now.

view this post on Zulip Reid Barton (Aug 05 2019 at 15:43):

I'm trying to do all the conversion between cardinals and naturals at once

view this post on Zulip Reid Barton (Aug 05 2019 at 15:46):

Pushed, I think it is somewhat better now...

view this post on Zulip Rob Lewis (Aug 05 2019 at 15:49):

Nice.

view this post on Zulip Jesse Michael Han (Aug 05 2019 at 16:07):

also pushed my calcification

not sure what the correct style is for long calc proofs but i tried to prettify it

view this post on Zulip Johan Commelin (Aug 05 2019 at 16:47):

Nice work @Reid Barton and @Jesse Michael Han

view this post on Zulip Johan Commelin (Aug 05 2019 at 16:47):

I think that maybe we should just use begin ... end instead of by { .. } for the longer proofs in the calc block

view this post on Zulip Johan Commelin (Aug 05 2019 at 16:49):

Of course that's a very minor issue

view this post on Zulip Reid Barton (Aug 05 2019 at 17:01):

Going to head out for a while, but I feel it should somehow be easier to show that l q = ε q y

view this post on Zulip Johan Commelin (Aug 05 2019 at 17:07):

Yep... that's the kind of "transfer" thing that I wanted to do

view this post on Zulip Johan Commelin (Aug 05 2019 at 17:07):

But showing Q n ->0 R =_l V n is already non-trivial...

view this post on Zulip Johan Commelin (Aug 05 2019 at 17:08):

It seems that Rob found a fix.

view this post on Zulip Johan Commelin (Aug 05 2019 at 17:08):

@Jesse Michael Han what do you think of the following style?

theorem degree_theorem :
   q, q  H  real.sqrt (m + 1)  (H  q.adjacent).to_finset.card :=
begin
  rcases exists_eigenvalue H _ with y, ⟨⟨H_mem', H_mem'', H_nonzero⟩⟩,
  rcases (finsupp.mem_span_iff_total _).mp H_mem' with l, H_l₁, H_l₂,
  have hHe : H   ,
  { contrapose! hH, rw [hH, set.empty_card'], exact nat.zero_lt_succ _ },
  obtain q, H_mem_H, H_max :  q, q  H   q', q'  H  abs (l q')  abs (l q),
  { cases set.exists_mem_of_ne_empty hHe with r hr,
    cases @finset.max_of_mem _ _ (H.to_finset.image (λ q', abs (l q')))
      (abs (l r)) (finset.mem_image_of_mem _ (set.mem_to_finset.2 hr)) with x hx,
    rcases finset.mem_image.1 (finset.mem_of_max hx) with q, hq, rfl,
    refine q, set.mem_to_finset.1 hq, λ q' hq', _⟩⟩,
    exact (finset.le_max_of_mem (finset.mem_image_of_mem _ (set.mem_to_finset.2 hq')) hx : _) },
  have H_q_pos : 0 < abs (l q),
  { rw [abs_pos_iff],
    assume h,
    rw [finsupp.mem_supported'] at H_l₁,
    have H_max' :  q', l q' = 0,
    { intro q',
      by_cases hq' : q'  H,
      { revert q', simpa [h] using H_max },
      { exact H_l₁ _ hq' } },
    have hl0 : l = 0,
    { ext, rw [H_max', finsupp.zero_apply] },
    simp [hl0] at H_l₂,
    exact H_nonzero H_l₂.symm },
  refine q, _, _⟩⟩,
  suffices : real.sqrt (m + 1) * abs (l q)  (_) * abs (l q),
    by { exact (mul_le_mul_right H_q_pos).mp _ },

  calc
    real.sqrt (m + 1) * (abs (l q))
         abs (real.sqrt (m + 1) * l q) : by conv_lhs { rw [ abs_sqrt_nat,  abs_mul] }
    ...  abs (ε q (real.sqrt (m + 1)  y)) :
        begin rw [linear_map.map_smul, smul_eq_mul, abs_mul, abs_mul],
          apply mul_le_mul_of_nonneg_left _ _,
            { apply le_of_eq, congr' 1, rw [ H_l₂, finsupp.total_apply, finsupp.sum, linear_map.map_sum],
              rw [finset.sum_eq_single q],
              { rw [linear_map.map_smul, smul_eq_mul, duality, if_pos rfl, mul_one], },
              { intros p hp hne,
                simp [linear_map.map_smul, duality, hne.symm] },
              { intro h_q_ne_supp,
                simp [finsupp.not_mem_support_iff.mp h_q_ne_supp] } },
          { exact abs_nonneg _ }
        end
    ...  l.support.sum (λ x : Q (m + 1), abs (l x) * abs ((ε q) ((f (m + 1) : _) (e x)))) :
        begin
          rw [ f_image_g y (by simpa using H_mem''),  H_l₂, finsupp.total_apply,
            finsupp.sum, linear_map.map_sum, linear_map.map_sum],
          refine le_trans abs_triangle_sum _,
          conv_lhs { congr, skip, simp [abs_mul] }
        end
    ...  finset.sum (l.support  set.to_finset H  set.to_finset (Q.adjacent q))
            (λ (x : Q (m + 1)), abs (l x) * abs ((ε q) ((f (m + 1) : _) (e x)))) :
        begin
          rw [ finset.sum_subset],
          { intros x Hx, simp[-finsupp.mem_support_iff] at Hx, exact Hx.left },
          { intros x H_mem H_not_mem,
            by_cases x  H,
              { simp at H_mem H_not_mem, rw[f_matrix], have := (H_not_mem _ _),
                change ¬ Q.adjacent _ _ at this, simp [Q.adjacent_comm, this] },
              { suffices : (l x) = 0, by {simp [this]},
                rw [finsupp.mem_supported'] at H_l₁, exact H_l₁ _ _ } }
        end
    ...  (finset.card (l.support  set.to_finset H  set.to_finset (Q.adjacent q))) * abs (l q) :
        begin
          refine le_trans (finset.sum_le_sum _) _,
          { exact λ p, abs (l q) },
          { intros x Hx, rw [f_matrix], simp at Hx,
            have := Hx.right.right, change Q.adjacent _ _ at this,
            rw [if_pos this.symm, mul_one], exact H_max x Hx.2.1 },
          { simp only [mul_one, finset.sum_const, add_monoid.smul_one, add_monoid.smul_eq_mul] }
        end
    ...  (finset.card (set.to_finset (H  Q.adjacent q))) * abs (l q) :
        begin
          refine (mul_le_mul_right _).mpr _, norm_cast,
          refine finset.card_le_of_subset (finset.coe_subset.mp _),
          simpa only [finset.coe_inter, finset.coe_to_finset', set.inter_assoc]
            using set.inter_subset_right _ _
        end
end

view this post on Zulip Rob Lewis (Aug 05 2019 at 17:13):

A fix to what? I'm playing around with changing the definition of adjacent right now.

view this post on Zulip Johan Commelin (Aug 05 2019 at 17:24):

Oh, to Lean not parsing RQ_equiv_V.

view this post on Zulip Johan Commelin (Aug 05 2019 at 17:25):

So I'll get back to filling in that definition now.

view this post on Zulip Johan Commelin (Aug 05 2019 at 17:25):

@Rob Lewis What do you propose as new definition of adjacent?

view this post on Zulip Rob Lewis (Aug 05 2019 at 17:27):

I was hoping def adjacent {n : ℕ} (p : Q n) : set (Q n) := λ q, ∃! i, p i ≠ q i would simplify things a bit. It basically exchanges the difficulty of adjacent_iff_dist for adjacent_succ_iff though.

view this post on Zulip Rob Lewis (Aug 05 2019 at 17:28):

My (not quite complete) proof of adjacent_succ_iff is a bit longer but arguably a bit simpler, and I don't think it's optimized.

view this post on Zulip Johan Commelin (Aug 05 2019 at 17:45):

For some reason

def equiv_unique {α : Type*} {β : Type*} [unique α] [discrete_field β] :
  (α  β) ≃ₗ[β] β :=
{ to_fun := λ f, f (default α),
  inv_fun := finsupp.single (default α),
  add := λ f g, finsupp.add_apply,
  smul := λ b f, rfl,
  left_inv := λ f, (finsupp.unique_single _).symm,
  right_inv := λ b, finsupp.single_eq_same }

is also extremely slow.

view this post on Zulip Johan Commelin (Aug 05 2019 at 17:47):

And if I change discrete_field to comm_ring it doesn't find add_comm_group for the LHS.

view this post on Zulip Johan Commelin (Aug 05 2019 at 17:47):

Even after importing algebra.pi_instances

view this post on Zulip Jesse Michael Han (Aug 05 2019 at 17:48):

yeah that looks good

my original version actually had begin .. end instead of by {} as well, but i thought that mathlib style forbids nested begin end blocks

view this post on Zulip Johan Commelin (Aug 05 2019 at 17:51):

What's this??

equation type mismatch, term
  equiv_unique (Q 0) 
has type
  (Q 0  ) ≃ₗ[] 
but is expected to have type
  (Q 0  ) ≃ₗ[] V 0

view this post on Zulip Johan Commelin (Aug 05 2019 at 17:51):

V 0 is defeq to real.

view this post on Zulip Johan Commelin (Aug 05 2019 at 17:51):

Why doesn't it see that?

view this post on Zulip Chris Hughes (Aug 05 2019 at 17:55):

Is the module structure defeq?

view this post on Zulip Johan Commelin (Aug 05 2019 at 17:56):

I think so.

view this post on Zulip Rob Lewis (Aug 05 2019 at 17:56):

https://github.com/leanprover-community/lean-sensitivity/tree/new_adj

view this post on Zulip Johan Commelin (Aug 05 2019 at 17:57):

noncomputable instance : Π n, add_comm_group (V n) :=
begin
  apply nat.rec,
  { dunfold V, apply_instance },
  { introsI n IH, dunfold V, apply_instance }
end

noncomputable instance : Π n, vector_space  (V n) :=
begin
  apply nat.rec,
  { dunfold V, apply_instance },
  { introsI n IH, dunfold V, apply_instance }
end

view this post on Zulip Rob Lewis (Aug 05 2019 at 17:57):

Not thrilled with the proof of adjacent_succ_iff. I'm not sure this is an improvement.

view this post on Zulip Rob Lewis (Aug 05 2019 at 17:57):

But I need to head home and eat dinner now.

view this post on Zulip Johan Commelin (Aug 05 2019 at 19:31):

I pushed another cleanup of degree_theorem

view this post on Zulip Johan Commelin (Aug 05 2019 at 19:32):

Maybe some parts at the top of the proof should be factored out into separate lemmas.

view this post on Zulip Floris van Doorn (Aug 05 2019 at 20:41):

(deleted - wrong topic)

view this post on Zulip Patrick Massot (Aug 05 2019 at 23:53):

Who could try to add the following lines after the definition of epsilon, and see if the commented lines timeout?

variables (n : ) (v : V n)
local notation `Ψ` := finsupp.equiv_fun_on_fintype.inv_fun

/-
This following fails with `by apply_instance`, but defining it doesn't seem to help.
instance tata : vector_space ℝ (Q n →₀ ℝ) :=
{..finsupp.module (Q n) ℝ, .. }
 -/

def coeffs {n : } (v : V n) : Q n   := Ψ (λ p : Q n, ε p v)
def somme {n : } := (finsupp.total (Q n) (V n)  e)

#check coeffs v -- coeffs v : Q n →₀ ℝ
#check @somme n  -- somme : (Q n →₀ ℝ) →ₗ[ℝ] V n
#check linear_map.to_fun somme  -- somme.to_fun : (Q ?M_1 →₀ ℝ) → V ?M_1

-- The following lines timeout
--#check linear_map.to_fun somme (coeffs v)
--#check linear_map.to_fun (@somme n)
--#check (Q n →₀ ℝ) →ₗ[ℝ] V n

view this post on Zulip Patrick Massot (Aug 05 2019 at 23:57):

Independently of this, I still think that the way we prove e is a basis is not optimal. What we really care about is the decomposition of vectors v : V n as a sum over p in Q n of (ε p v) • (e p) (the issues above were met while trying to write down this formula using the linear algebra library). In our current proof of the main theorem, this formula is somewhat hidden, because we use the fact e is a basis to get a mysterious sequence of coefficients unrelated to ε. One improvement could be to prove ε is equal to dual_basis e and use stuff in dual.lean. But we could just as well directly prove the decomposition formula

view this post on Zulip Patrick Massot (Aug 05 2019 at 23:57):

The key is:

view this post on Zulip Patrick Massot (Aug 05 2019 at 23:57):

lemma epsilon_total {n : } {v : V n} (h :  p : Q n, (ε p) v = 0) : v = 0 :=
begin
  induction n with n ih,
  { dsimp [ε] at h, exact h (λ _, tt) },
  { cases v with v₁ v₂,
    ext ; change _ = (0 : V n) ; simp only [] ; apply ih ; intro p ;
    [ let q : Q (n+1) := λ i, if h : i = 0 then tt else p (i.pred h),
      let q : Q (n+1) := λ i, if h : i = 0 then ff else p (i.pred h)],
    all_goals {
      specialize h q,
      rw [ε, show q 0 = tt, from rfl, cond_tt] at h <|> rw [ε, show q 0 = ff, from rfl, cond_ff] at h,
      rwa show p = q  fin.succ, by { ext, simp [q, fin.succ_ne_zero] } } }
end

view this post on Zulip Patrick Massot (Aug 05 2019 at 23:58):

Which we can apply to a vector minus its intended decomposition (using the duality lemma).

view this post on Zulip Patrick Massot (Aug 05 2019 at 23:59):

If we insist on keeping that e is a basis then the above lemma (together with the duality lemma) reproves it

view this post on Zulip Patrick Massot (Aug 05 2019 at 23:59):

(this is all assuming we can use lemmas about sums over finsupp...)

view this post on Zulip Patrick Massot (Aug 06 2019 at 00:02):

Another thing that is surprisingly painful is the proof of have H_q_pos : 0 < abs (l q), in the main theorem. I think we should use that fintype.normed_group is using the supremum norm. So abs (l q) is actually the norm of y, hence positive using norm_pos_iff

view this post on Zulip Patrick Massot (Aug 06 2019 at 00:05):

And then I think the big calc at the end should have more steps and use more general lemmas about linear maps and dual bases.

view this post on Zulip Rob Lewis (Aug 06 2019 at 13:03):

I didn't think of a nice way to optimize the proof of adj_succ_iff with the "exists unique" definition of adjacent. But I did notice that the detour through dist is completely unnecessary. This is all we need about adjacent:

def adjacent : Π {n : }, Q n  (set $ Q n)
| 0 p q := false
| (n+1) p q := (p 0 = q 0  adjacent (p  fin.succ) (q  fin.succ))  (p 0  q 0  p  fin.succ = q  fin.succ)

lemma adjacent.symm :  {n} {p q : Q n}, p.adjacent q  q.adjacent p
| (n+1) p q (or.inl h_eq, h_adj) := or.inl h_eq.symm, h_adj.symm
| (n+1) p q (or.inr h_ne, h_eq) := or.inr h_ne.symm, h_eq.symm

lemma adjacent_comm {p q : Q n} : p.adjacent q  q.adjacent p :=
adjacent.symm, adjacent.symm

lemma adjacent_succ_iff {p q : Q (n+1)} :
  p.adjacent q  (p 0 = q 0  adjacent (p  fin.succ) (q  fin.succ))  (p 0  q 0  p  fin.succ = q  fin.succ) :=
iff.refl _

lemma not_adjacent_zero (p q : Q 0) : ¬ p.adjacent q :=
by rintros v, _⟩; apply fin_zero_elim v

Using an inductive prop for adjacent looks very slightly cleaner, I think, but forces some packing and unpacking in adjacent_succ_iff.

inductive adjacent :  {n}, Q n  Q n  Prop
| zero {n} {p q : Q (n+1)} : p 0  q 0  p  fin.succ = q  fin.succ  adjacent p q
| nonzero {n} {p q : Q (n+1)} : p 0 = q 0  adjacent (p  fin.succ) (q  fin.succ)  adjacent p q

view this post on Zulip Patrick Massot (Aug 06 2019 at 13:04):

I'm currently playing with this adjacent_succ_iff thing

view this post on Zulip Patrick Massot (Aug 06 2019 at 13:04):

Using my proposed definition of adjacent

view this post on Zulip Rob Lewis (Aug 06 2019 at 13:05):

Which definition is that?

view this post on Zulip Patrick Massot (Aug 06 2019 at 13:05):

/-- `flip i p` flips the i-th bit of p -/
def flip {n : } (i : fin n) : Q n  Q n :=
λ p k, if i = k then bnot (p k) else p k

def adjacent {n : } : Q n  (set $ Q n) := λ p, {q |  i : fin n, q = flip i p}

view this post on Zulip Patrick Massot (Aug 06 2019 at 13:05):

This is my proposal but still phrased in terms of bool rather than Z/2

view this post on Zulip Patrick Massot (Aug 06 2019 at 13:06):

I think this is a pretty clean definition, very close to what you would say when explaining the statement

view this post on Zulip Patrick Massot (Aug 06 2019 at 13:07):

But I'm not claiming it makes the proof of adjacent_succ_iff as short as we'd like it to be

view this post on Zulip Patrick Massot (Aug 06 2019 at 13:08):

(deleted)

view this post on Zulip Patrick Massot (Aug 06 2019 at 14:11):

I returned to this and finished this proof. I add the following trivial preliminaries:

lemma ne_iff_eq_bnot {b b' : bool} : b  b'  b = bnot b' :=
by cases b ; cases b' ; simp

@[simp]
lemma not_eq_bnot :  b : bool, ¬ b = bnot b
| tt := λ h, bool.no_confusion h
| ff := λ h, bool.no_confusion h

lemma fin.eq_succ_iff_pred_eq {n : } {i : fin (n + 1)} {l : fin n}
(h : i  0) : i = fin.succ l  (fin.pred i h = l) :=
begin
  split ; intro H,
  { simp only [H, h, fin.pred_succ] },
  { simp only [H.symm, fin.succ_pred] }
end

view this post on Zulip Patrick Massot (Aug 06 2019 at 14:13):

And then the adjacency stuff becomes:

/-- `flip i p` flips the i-th bit of p -/
def flip {n : } (i : fin n) : Q n  Q n :=
λ p k, if i = k then bnot (p k) else p k

/-- The adjacency relation on Q^n: two vertices of the hypercube are adjacent if they differ at one bit. -/
def adjacent {n : } : Q n  (set $ Q n) := λ p, {q |  i : fin n, q = flip i p}

@[simp] lemma not_adjacent_zero (p q : Q 0) : p.adjacent q = false :=
begin
  rw eq_false,
  rintro i, h,
  fin_cases i
end

lemma adjacent_succ_iff {p q : Q (n+1)} :
  p.adjacent q  (p 0 = q 0  adjacent (p  fin.succ) (q  fin.succ))  (p 0  q 0  p  fin.succ = q  fin.succ) :=
begin
  split,
  { rintros i, h,
    rw h,
    by_cases hi : i = 0,
    { right,
      rw [hi, flip],
      split ; simp,
      ext l,
      simp [(fin.succ_ne_zero _).symm] },
    { left,
      split,
      { simp [hi, flip] },
      { use i.pred hi,
        ext l,
        dsimp [flip],
        congr' 1,
        rw fin.eq_succ_iff_pred_eq } } },
  { rintro (h₀, i, h⟩⟩ | h₀, h),
    { use i.succ,
      ext l,
      by_cases hl : l = 0,
      { simp only [hl, flip, fin.succ_ne_zero, h₀, bnot, if_false] },
      { have := congr_fun h (l.pred hl),
        simp at this,
        rw this,
        dsimp [flip], simp only [fin.succ_pred],
        have := fin.eq_succ_iff_pred_eq hl,
        conv_lhs at this { rw eq_comm },
        conv_rhs at this { rw eq_comm },
        congr' 1,
        rw  this } },
    { use 0,
      ext l,
      by_cases hl : l = 0,
      { simp [flip, hl, ne_iff_eq_bnot.1 h₀] },
      { rw  fin.succ_pred l hl,
        have := congr_fun h (l.pred hl),
        simp only [function.comp_app] at this,
        rw  this,
        simp [flip, ne.symm hl] } } }
end

view this post on Zulip Patrick Massot (Aug 06 2019 at 14:13):

It seems there is some kind of pain conservation law here

view this post on Zulip Patrick Massot (Aug 06 2019 at 14:13):

@Rob Lewis

view this post on Zulip Patrick Massot (Aug 06 2019 at 14:14):

Maybe that solution is a bit orthogonal to the general design of our proof since it doesn't use induction on n at all

view this post on Zulip Patrick Massot (Aug 06 2019 at 14:32):

I forget symmetry:

lemma flip_flip {n : } (i : fin n) (p : Q n) : flip i (flip i p) = p :=
begin
  ext l,
  dsimp [flip],
  split_ifs,
  simp
end

@[symm] lemma adjacent_comm {p q : Q n} : p.adjacent q  q.adjacent p :=
by split ; rintro i, h ; rw h ; use i ; rw flip_flip

view this post on Zulip Patrick Massot (Aug 06 2019 at 14:44):

Who could try to add the following lines after the definition of epsilon, and see if the commented lines timeout?

variables (n : ) (v : V n)
local notation `Ψ` := finsupp.equiv_fun_on_fintype.inv_fun

/-
This following fails with `by apply_instance`, but defining it doesn't seem to help.
instance tata : vector_space ℝ (Q n →₀ ℝ) :=
{..finsupp.module (Q n) ℝ, .. }
 -/

def coeffs {n : } (v : V n) : Q n   := Ψ (λ p : Q n, ε p v)
def somme {n : } := (finsupp.total (Q n) (V n)  e)

#check coeffs v -- coeffs v : Q n →₀ ℝ
#check @somme n  -- somme : (Q n →₀ ℝ) →ₗ[ℝ] V n
#check linear_map.to_fun somme  -- somme.to_fun : (Q ?M_1 →₀ ℝ) → V ?M_1

-- The following lines timeout
--#check linear_map.to_fun somme (coeffs v)
--#check linear_map.to_fun (@somme n)
--#check (Q n →₀ ℝ) →ₗ[ℝ] V n

Does anyone has any explanation for the above mystery?

view this post on Zulip Rob Lewis (Aug 06 2019 at 14:50):

You're right that the induction isn't necessary. Ultimately we need these two facts; everything below goes through fine with just these. These proofs are for the "exists unique" definition of adjacent.

lemma adj_succ {p q : Q (n+1)} (h0 : p 0  q 0) : p  fin.succ = q  fin.succ  p.adjacent q :=
begin
  split,
  { intro heq,
    use [0, h0],
    intros y hy,
    contrapose! hy,
    rw fin.succ_pred _ hy,
    apply congr_fun heq },
  { rintros i, h_eq, h_uni,
    ext x, by_contradiction hx,
    apply fin.succ_ne_zero x,
    rw [h_uni _ hx, h_uni _ h0] }
end

lemma adj_succ_of_zeq {p q : Q (n+1)} (h0 : p 0 = q 0) :
  Q.adjacent (p  fin.succ) (q  fin.succ)  p.adjacent q :=
begin
  split,
  { rintros i, h_eq, h_uni,
    use [i.succ, h_eq],
    intros y hy,
    rw [fin.pred_inj, fin.pred_succ],
    { apply h_uni, change p (fin.pred _ _).succ  q (fin.pred _ _).succ, simp [hy] },
    { contrapose! hy, rw [hy, h0] },
    { apply fin.succ_ne_zero } },
  { rintros i, h_eq, h_uni,
    have h_i : i  0, from λ h_i, absurd h0 (by rwa h_i at h_eq),
    use [i.pred h_i, show p (fin.succ (fin.pred i _))  q (fin.succ (fin.pred i _)), by rwa [fin.succ_pred]],
    intros y hy, simp [eq.symm (h_uni _ hy)] }
end

view this post on Zulip Patrick Massot (Aug 06 2019 at 14:53):

I don't have a strong opinion about this exists_unique vs flip. I think both definition directly relate to the intuitive definition.

view this post on Zulip Patrick Massot (Aug 06 2019 at 14:53):

Why do you separate those two lemmas? Does it make later things easier?

view this post on Zulip Patrick Massot (Aug 06 2019 at 14:54):

Could you try my finsupp.total mystery?

view this post on Zulip Rob Lewis (Aug 06 2019 at 14:54):

I don't have time to debug the type class thing right now, but you can look at the trace here and see if you can make any sense:

set_option trace.class_instances true
include v
example := by try_for 10000 {exact  linear_map.to_fun somme (coeffs v)}

view this post on Zulip Rob Lewis (Aug 06 2019 at 14:55):

I think it ended up being a bit cleaner with them separate. But I generally try to avoid disjunctions, so that's why this feels cleaner to me.

view this post on Zulip Patrick Massot (Aug 06 2019 at 15:13):

(message too long, truncated at 262144 characters)

view this post on Zulip Patrick Massot (Aug 06 2019 at 15:21):

It seems adding the shortcut

instance toto : module  (Q n  ) :=
finsupp.module (Q n) 

helps a lot

view this post on Zulip Patrick Massot (Aug 06 2019 at 15:21):

Although the coercion from linear_map to function still doesn't kick in

view this post on Zulip Rob Lewis (Aug 06 2019 at 15:23):

Yes, the messages get truncated, but 262144 characters is usually plenty to find the problem...

view this post on Zulip Rob Lewis (Aug 06 2019 at 15:23):

Unsurprisingly there are type class issues in this whole development. You can add that to the short circuit instances for V.

view this post on Zulip Johan Commelin (Aug 06 2019 at 15:24):

Why "unsurprisingly"?

view this post on Zulip Rob Lewis (Aug 06 2019 at 15:24):

https://github.com/leanprover-community/lean-sensitivity/tree/new_adj is about as clean as I can get the adjacent stuff for now.

view this post on Zulip Johan Commelin (Aug 06 2019 at 15:24):

To me this is quite a surprise

view this post on Zulip Rob Lewis (Aug 06 2019 at 15:26):

I think it's been clear for a while that we're kind of abusing type class search. Whether it's our setup, or the inference algorithm itself, these kinds of issues are showing up a lot.

view this post on Zulip Patrick Massot (Aug 06 2019 at 15:26):

It's pretty clear that either we are doing it wrong, or Lean 3's type class is doing it wrong

view this post on Zulip Patrick Massot (Aug 06 2019 at 15:26):

Rob was quicker...

view this post on Zulip Patrick Massot (Aug 06 2019 at 15:28):

Rob, I think you can merge into master, I don't think anyone has a much better idea

view this post on Zulip Kevin Buzzard (Aug 06 2019 at 15:54):

Can someone summarise the problems you're having?

view this post on Zulip Patrick Massot (Aug 06 2019 at 16:21):

Kevin, there are several problems. The one I was discussing with Rob is to get a definition of the adjacency relation on the hypercube which is both easily recognizable and convenient for the proofs. I think we sort of settled that.

view this post on Zulip Patrick Massot (Aug 06 2019 at 16:23):

Then I went outside to help my youngest daughter training to ride a bicycle without side wheels. She's making progress but was tired. So i returned, and took up the big problem.

view this post on Zulip Patrick Massot (Aug 06 2019 at 16:23):

Which is the sum manipulation and basis and dual basis things.

view this post on Zulip Patrick Massot (Aug 06 2019 at 16:23):

Now that instances work, here is my proposal:

view this post on Zulip Patrick Massot (Aug 06 2019 at 16:23):

instance coeffs_module (n) : module  (Q n  ) :=
finsupp.module (Q n) 

def coeffs {n : } (v : V n) : Q n   := finsupp.equiv_fun_on_fintype.inv_fun (λ p : Q n, ε p v)

def somme {n : } :  (Q n  )  V n := finsupp.total (Q n) (V n)  e

/-- For any v : V n, \sum_{p ∈ Q n} (ε p v) • e p = v -/
lemma decomposition {n : } (v : V n) : somme (coeffs v) = v :=
begin
  suffices :  (p : Q n), ε p (somme $ coeffs v) = ε p v,
  { refine eq_of_sub_eq_zero (epsilon_total _),
    intros p,
    rw [linear_map.map_sub, sub_eq_zero_iff_eq, this] },
  intro p,
  erw [somme, finsupp.total_apply, linear_map.map_sum],
  simp only [duality, map_smul, smul_eq_mul],
  rw finset.sum_eq_single p,
  { simp, refl },
  { intros q q_in q_ne,
    simp [q_ne.symm] },
  { intro p_not_in,
    simp [finsupp.not_mem_support_iff.1 p_not_in] }
end

view this post on Zulip Patrick Massot (Aug 06 2019 at 16:25):

Note how this doesn not use e.is_basis or equiv_sum

view this post on Zulip Patrick Massot (Aug 06 2019 at 16:25):

I think this is going more straightly to the point

view this post on Zulip Patrick Massot (Aug 06 2019 at 16:27):

Modulo all the finsupp weirdness, it says exactly what the docstring claims

view this post on Zulip Patrick Massot (Aug 06 2019 at 16:27):

I think this could be the basis for a refactor of the main proof

view this post on Zulip Rob Lewis (Aug 06 2019 at 16:28):

What's somme? I keep reading that as a misspelling of some...

view this post on Zulip Patrick Massot (Aug 06 2019 at 16:28):

Oh sorry

view this post on Zulip Patrick Massot (Aug 06 2019 at 16:28):

It's French for sum

view this post on Zulip Rob Lewis (Aug 06 2019 at 16:28):

Aha.

view this post on Zulip Patrick Massot (Aug 06 2019 at 16:29):

At some point I wanted to avoid name clash

view this post on Zulip Patrick Massot (Aug 06 2019 at 16:29):

Of course it uses epsilon_total that I posted earlier

view this post on Zulip Patrick Massot (Aug 06 2019 at 16:29):

lemma epsilon_total {n : } {v : V n} (h :  p : Q n, (ε p) v = 0) : v = 0 :=
begin
  induction n with n ih,
  { dsimp [ε] at h, exact h (λ _, tt) },
  { cases v with v₁ v₂,
    ext ; change _ = (0 : V n) ; simp only [] ; apply ih ; intro p ;
    [ let q : Q (n+1) := λ i, if h : i = 0 then tt else p (i.pred h),
      let q : Q (n+1) := λ i, if h : i = 0 then ff else p (i.pred h)],
    all_goals {
      specialize h q,
      rw [ε, show q 0 = tt, from rfl, cond_tt] at h <|> rw [ε, show q 0 = ff, from rfl, cond_ff] at h,
      rwa show p = q  fin.succ, by { ext, simp [q, fin.succ_ne_zero] } } }
end

view this post on Zulip Patrick Massot (Aug 06 2019 at 16:31):

and duality. Together those lemmas are equivalent to the fact that e and epsilon are dual bases.

view this post on Zulip Patrick Massot (Aug 06 2019 at 16:31):

What do you think about this?

view this post on Zulip Rob Lewis (Aug 06 2019 at 16:35):

I haven't worked through your earlier posts very carefully, but if there's a chance this could clean up the bottom of the file, I'm in favor of trying...

view this post on Zulip Patrick Massot (Aug 07 2019 at 00:58):

Ok, I pushed something. The main goal is to shorten the final proof, make it easier to read, and transfer as much as possible into for_mathlib.lean. I followed my plan of using the duality as outline in my previous messages. Maybe I went too far, and I'm actually fighting the linear algebra library. But I still like how the final proof looks like. And I guess that Lean night already lasted too long (looks like it's now almost 3am...)

view this post on Zulip Rob Lewis (Aug 07 2019 at 09:33):

Nice, I think it looks great!

view this post on Zulip Patrick Massot (Aug 07 2019 at 10:39):

What I think it the final big thing is to generalize and move to mathlib https://github.com/leanprover-community/lean-sensitivity/blob/19c2800c9330ddf7130dac4ce22b7d2eb51afcfd/src/sensitivity.lean#L193-L247. It should connect with https://github.com/leanprover-community/mathlib/blob/master/src/linear_algebra/dual.lean. We could have a lemma characterizing pairs of dual bases (taking as input our statements duality and epsilon_total and outputting the conjunction that e is a basis and epsilon is its dual basis). And then replace the rest of the what I outlined in the first link by general lemmas about dual bases. Or, maybe more flexibly, we could have a duality predicate about two families of vector saying they form dual bases, and then state all lemmas in dual.lean in term of this predicate. As usual with predicate vs construction, the gain appears in exactly the situation we are in, when we want an alternative construction for some reason.

view this post on Zulip Patrick Massot (Aug 07 2019 at 10:42):

Honestly, I spent way too much time working on this sensitivity thing. Maybe someone who understands linear algebra in mathlib (and especially dual.lean) should take over (@Johan Commelin?). Today I'll bring my son to Penhir for climbing.

view this post on Zulip Patrick Massot (Aug 09 2019 at 21:23):

I'm frustrated that we can't advertise our sensitivity conjecture formalization so I tried again. I wrote https://github.com/leanprover-community/lean-sensitivity/commit/ed3d288f0fe696cc5a8049cad612f503ae2f4da3 about pairs of maps constituting a dual basis. It was a nightmare because elaboration was failing everywhere. And when I try to use it in the main file I get random mismatches of decidable_whatever. Maybe I was wrong when I wrote that function coercions were the main issue. It seems that decidability classes are there each time we really suffer in mathlib (see also polynomials). I give up.

view this post on Zulip Patrick Massot (Aug 09 2019 at 21:23):

I guess Rob is our last hope.

view this post on Zulip David Michael Roberts (Aug 10 2019 at 10:35):

working out pi to 7 decimal places,

where was that done? I can't find it after a little look here in the chat.

view this post on Zulip Mario Carneiro (Aug 10 2019 at 10:46):

see https://github.com/leanprover-community/mathlib/blob/master/src/data/real/pi.lean#L193-L229 and the linked gist at https://gist.github.com/fpvandoorn/5b405988bc2e61953d56e3597db16ecf

view this post on Zulip Mario Carneiro (Aug 10 2019 at 10:46):

I think it was our pi day activity

view this post on Zulip Kevin Buzzard (Aug 10 2019 at 11:18):

They worked it out to a million decimal places in Coq once, but I would imagine the process took more than 24 hours in total. What has been interesting recently is that questions have come up and then a group of people have worked on them and within a day or two the code is up and running.

view this post on Zulip David Michael Roberts (Aug 10 2019 at 13:27):

Though the seven decimal places include the 3., that's still pretty nice.

view this post on Zulip Reid Barton (Aug 10 2019 at 14:13):

I also have the impression that decidable_eq requirements are somehow responsible for a lot of pain, though I have no data or understanding of why that would be.

view this post on Zulip Rob Lewis (Aug 21 2019 at 09:54):

@Patrick Massot What were the issues you were having here? It seems like things compile, and I don't see any nightmares in the file right now.

view this post on Zulip Rob Lewis (Aug 21 2019 at 09:54):

I was planning to try to move some of the lemmas to mathlib and put this in the archive. Are there still major changes you want to make?

view this post on Zulip Patrick Massot (Aug 21 2019 at 10:59):

I think I've explained it in previous messages. This minor nightmare is https://github.com/leanprover-community/lean-sensitivity/blob/lean-3.4.2/src/sensitivity.lean#L154-L247 which was meant to be replaced by calling https://github.com/leanprover-community/lean-sensitivity/blob/lean-3.4.2/src/for_mathlib.lean#L25-L103 but I couldn't make it work because of conflicting decidable instances (mixing actual instances and classical.prop_decidable I guess). Also https://github.com/leanprover-community/lean-sensitivity/blob/lean-3.4.2/src/sensitivity.lean#L117-L140 looks stupid since we then explicitly describe a basis.

view this post on Zulip Patrick Massot (Aug 21 2019 at 11:00):

I would really love it if you could have a look at this decidability nightmare

view this post on Zulip Patrick Massot (Aug 21 2019 at 11:01):

When we rushed to prove this theorem I thought that within one week we would be able to post comments to all blogs discussing this theorem to point out it was very quickly formalized. Instead we have one more proof that formalization is not practicable for stupid reasons.

view this post on Zulip Rob Lewis (Aug 21 2019 at 11:13):

I'll see what I can do.

view this post on Zulip Kevin Buzzard (Aug 21 2019 at 11:28):

I wasn't involved but I thought that it was indeed quickly formalised

view this post on Zulip Rob Lewis (Aug 21 2019 at 11:32):

It was quickly formalized but it's not a perfect formalization. To brag about something this short, it kind of has to be done canonically, and the problem (I think) is that Patrick struggled to get the canonical proof to work.

view this post on Zulip Patrick Massot (Aug 21 2019 at 11:33):

We don't need it to be perfect, but I'd like it to be recognizable maths

view this post on Zulip Rob Lewis (Aug 21 2019 at 13:44):

@Patrick Massot I just pushed an update. Is this what you had in mind? The decidability issues were nothing major. We were missing a decidable_eq instance for V n, which was confusing things in a few places.

view this post on Zulip Rob Lewis (Aug 21 2019 at 13:52):

In fact, the specific dec_eq instance I gave it isn't necessary. Defining it using classical.dec_eq is fine too. But without the explicit instance, it seems to be inferring different dec_eqs in different places.

view this post on Zulip Rob Lewis (Aug 21 2019 at 13:52):

It's all kind of ironic since V definitely isn't decidable. There are non-defeq ways to pretend that it is.

view this post on Zulip Patrick Massot (Aug 21 2019 at 14:54):

Yes, it looks good. I'm happy you found it easy. I'm so upset by those kinds of problems that my mind refuse to work on them.

view this post on Zulip Patrick Massot (Aug 21 2019 at 14:54):

What is the point of getting calc_lemma out of the theorem proof?

view this post on Zulip Kevin Buzzard (Aug 21 2019 at 14:54):

We mathematicians just instinctively deny that such (decidability) issues can exist, because we've been ignoring them for centuries.

view this post on Zulip Patrick Massot (Aug 21 2019 at 14:55):

I think https://github.com/leanprover-community/lean-sensitivity/blob/a4b69d68217b7b8319a03f3406f4fba6147b2f91/src/sensitivity.lean#L194-L202 are not needed, we can use their proofs where we need them

view this post on Zulip Patrick Massot (Aug 21 2019 at 14:57):

And we still have that silly dimension computation. We should have a mathlib lemma stating that if V has a basis index by a finite type then its findim is the cardinal of this finite type, and of course a lemma computing the cardinal of fin n to bool

view this post on Zulip Rob Lewis (Aug 21 2019 at 14:59):

What is the point of getting calc_lemma out of the theorem proof?

That calc block is a memory hog. I moved it out to make it easier to fix, it doesn't have to stay out. Also gave me a chance to try extract_goal, which stumbles a bit with let statements.

view this post on Zulip Rob Lewis (Aug 21 2019 at 15:00):

I think https://github.com/leanprover-community/lean-sensitivity/blob/a4b69d68217b7b8319a03f3406f4fba6147b2f91/src/sensitivity.lean#L194-L202 are not needed, we can use their proofs where we need them

Yeah. Again, just slightly easier to put them there while making the updates.

view this post on Zulip Rob Lewis (Aug 21 2019 at 16:02):

And we still have that silly dimension computation. We should have a mathlib lemma stating that if V has a basis index by a finite type then its findim is the cardinal of this finite type, and of course a lemma computing the cardinal of fin n to bool

This is more annoying than it should be because of cardinal universes.

view this post on Zulip Patrick Massot (Aug 21 2019 at 16:03):

I really think mathlib should hide this to users who manipulate only finite-dimensional vector spaces (as we do in this proof)

view this post on Zulip Patrick Massot (Aug 21 2019 at 16:03):

If we can't do that then the linear algebra library has a serious issue

view this post on Zulip Rob Lewis (Aug 21 2019 at 16:09):

I think this is what linear_algebra/finite_dimensional.lean is trying to do, but there's still some glue missing.

view this post on Zulip Rob Lewis (Aug 21 2019 at 16:12):

fg doesn't seem to be linked up with the existence of a finite basis, as far as I can tell.

view this post on Zulip Rob Lewis (Aug 21 2019 at 23:26):

Turns out I work better late at night and this was much easier than I thought. https://github.com/leanprover-community/lean-sensitivity/commit/af28ecfab7f412f7d451a4ff4cf328aad322eae3

view this post on Zulip Patrick Massot (Aug 22 2019 at 15:16):

Thanks Rob! I finally had some time to look at it. I would still prefer to hide cardinal even more (or at least have only one of dim_V or dim_V') but it's already much better. I feel sufficiently confident that we are close to something we could share (and I feel sufficiently confident I don't want to write that referee report I should be writing) that I made a cosmetic pass on the whole file: https://github.com/leanprover-community/lean-sensitivity/commit/4feaed5a407676a45327854595bd3e4b319c4f7e I hope there aren't too many controversial changes (especially for equation compiler addicts). Everyone is free to tweak it.

view this post on Zulip Patrick Massot (Aug 22 2019 at 15:18):

I also reintegrated the calc block in the main proof.

view this post on Zulip Patrick Massot (Aug 22 2019 at 15:32):

And now we can go on removing stuff that just got merged in mathlib, and continue emptying for_mathlib.lean

view this post on Zulip Rob Lewis (Aug 22 2019 at 16:00):

It looks good! I just pushed an update that gets rid of dim_V'. But updating mathlib breaks the assumption_mod_castin findim_V, I'm not sure why.

view this post on Zulip Rob Lewis (Aug 22 2019 at 16:12):

Fixed. https://github.com/leanprover-community/lean-sensitivity/tree/upgraded_mathlib on a branch for now so it doesn't interfere with update-mathlib. After the next nightly comes out, we can upgrade to that and merge to master.

view this post on Zulip Rob Lewis (Aug 22 2019 at 16:15):

@Paul-Nicolas Madelaine At https://github.com/leanprover-community/mathlib/blob/master/src/set_theory/cardinal.lean#L589, is nat_cast_pow (and nat_cast_le) a good elim_cast lemma? Maybe I was wrong to add that.

view this post on Zulip Patrick Massot (Aug 23 2019 at 08:16):

Rob, do you understand the crazy https://github.com/leanprover-community/lean-sensitivity/commit/658b12067f73e85fe27e6108bed92b2148c454da or is it the result of random desperate modifications?

view this post on Zulip Rob Lewis (Aug 23 2019 at 08:45):

That commit in particular, or the short circuits more generally? They were local to the namespace V before, which ended right after they were declared, so they were doing absolutely nothing.

view this post on Zulip Patrick Massot (Aug 23 2019 at 08:46):

Oh ok

view this post on Zulip Patrick Massot (Aug 23 2019 at 08:46):

I'm sorry I messed up that

view this post on Zulip Patrick Massot (Aug 23 2019 at 08:47):

I just pushed some more tweaks to make statements look nicer (at least to my eye)

view this post on Zulip Patrick Massot (Aug 23 2019 at 08:47):

Did you make progress on the mathlib bump issue?

view this post on Zulip Rob Lewis (Aug 23 2019 at 08:48):

No worries. It was obvious something was wrong when I opened it on my laptop, the extra 25 seconds to compile are noticeable.

view this post on Zulip Rob Lewis (Aug 23 2019 at 08:49):

I think the next mathlib nightly goes up once the next PR gets merged and built, right?

view this post on Zulip Rob Lewis (Aug 23 2019 at 08:49):

Then we run leanpkg upgrade on the upgraded_mathlib branch and rebase.

view this post on Zulip Patrick Massot (Aug 23 2019 at 08:50):

I think the remaining ugliness in statements now all come from elaboration issues (the obvious ones like (f (m + 1) : _) w = √(m + 1) • w but also the sneaky ones like being forced to write √(m + 1) ≤ Card (H ∩ q.adjacent) instead of switching sides to match the way we would say it).

view this post on Zulip Patrick Massot (Aug 23 2019 at 08:51):

Oh, I thought you had trouble with the question you asked PN

view this post on Zulip Rob Lewis (Aug 23 2019 at 08:52):

Oh, that's fixed locally, I was just wondering if it should be a global change.

view this post on Zulip Patrick Massot (Aug 23 2019 at 08:52):

apply' just got merged so we should get a new nightly soon

view this post on Zulip Patrick Massot (Aug 23 2019 at 08:53):

Of course we can always trigger a new nightly build by hand if we are in a hurry

view this post on Zulip Patrick Massot (Aug 23 2019 at 08:54):

Back to mathematics, I wonder why the theorem is stated (in our formalization and in the original paper) for positive n. Isn't the statement obviously true when n = 0?

view this post on Zulip Rob Lewis (Aug 23 2019 at 08:54):

I'll need to run soon, got a friend in town visiting. But your changes look fine. There's dead code on lines 344-345.

view this post on Zulip Patrick Massot (Aug 23 2019 at 08:55):

oops, forgot to delete that. I'll do it right now

view this post on Zulip Paul-Nicolas Madelaine (Aug 23 2019 at 09:31):

@Rob Lewis nat_cast_le is a good elim_cast lemma and nat_cast_pow should be a move_cast lemma.
something to keep in mind that I should also write explicitely in the documentation is that move_cast lemmas are going to be used from right to left.
so in that case, the nat_cast_pow lemma will turn ↑n ^ m into ↑(pow n m), which can be a bit weird if the ^ notation is defined on cardinals.
I'll add these notes to the documentation as soon as I am done with the report.

view this post on Zulip Patrick Massot (Aug 23 2019 at 11:12):

Ok, we are up to date with mathlib, and ready for the next round of PR

view this post on Zulip Jesse Michael Han (Aug 24 2019 at 19:11):

on the reduction branch i started on the reduction of the original sensitivity conjecture to the degree theorem we formalized

view this post on Zulip Jesse Michael Han (Aug 24 2019 at 19:12):

it looks manageable except that the proof of gotsman_linial_equivalence uses Fourier transforms

view this post on Zulip Patrick Massot (Aug 24 2019 at 19:59):

That sounds like a big "except"

view this post on Zulip Daniel Donnelly (Aug 24 2019 at 20:09):

Why can't Lean handle FT? Not that I need it for my app or anything...

view this post on Zulip Patrick Massot (Aug 24 2019 at 20:14):

Oh, it can. But someone needs to explain it to Lean.

view this post on Zulip Patrick Massot (Aug 24 2019 at 20:14):

And analysis is not mathlib's strong point

view this post on Zulip Scott Morrison (Aug 24 2019 at 22:59):

It's not really Fourier transforms in the Gotsman-Linial argument --- it's just the Z/2Z valued version, no analysis involved at all.

view this post on Zulip Scott Morrison (Aug 24 2019 at 22:59):

In fact the proof is just a few lines, even easier than Huang's recent argument.

view this post on Zulip Daniel Donnelly (Aug 24 2019 at 23:05):

I can attest to that. Has to do with sums of roots of unity in any field.

view this post on Zulip Jesse Michael Han (Aug 24 2019 at 23:06):

oh, good

then maybe soon we can say that we really formalized the sensitivity conjecture

view this post on Zulip Scott Morrison (Aug 24 2019 at 23:32):

The Gotsman-Linial argument is in https://www.sciencedirect.com/science/article/pii/0097316592900608, which is free online. There's also a restatement of the proof at https://blog.computationalcomplexity.org/2019/07/degree-and-sensitivity.html.

view this post on Zulip Scott Morrison (Aug 24 2019 at 23:34):

I'm not sure what EnjoysMath meant, but there's nothing in the argument about sums of roots of unity, it's just counting signs in the GL argument.

view this post on Zulip Rob Lewis (Aug 27 2019 at 07:30):

I was trying to figure out why this project was so slow to compile on my laptop. Looks like we have another performance issue when we get deep into the mathlib file hierarchy: building the default simp set at the beginning of for_mathlib.lean takes 1.5 sec (on my laptop, 1 sec on my desktop). This happens once in every declaration that uses simp without only.

view this post on Zulip Johan Commelin (Aug 27 2019 at 07:34):

/me hears Kenny rolling on the floor lauging out loud

view this post on Zulip Johan Commelin (Aug 27 2019 at 07:35):

@Kenny Lau In how many different languages do you know the word “Schadenfreude”?

view this post on Zulip Scott Morrison (Aug 27 2019 at 08:20):

Wow, that’s really bad.

view this post on Zulip Scott Morrison (Aug 27 2019 at 08:20):

Like, maybe this enterprise is actually doomed, bad. :-)

view this post on Zulip Chris Hughes (Aug 27 2019 at 08:28):

I think this is maybe a case for being careful about minimising imports. It won't improve speed for everyone, but certainly it will improve speed a lot of the time. I think there were a lot of unnecessary imports for that proof.

view this post on Zulip Johan Commelin (Aug 27 2019 at 08:41):

[…] building the default simp set at the beginning of for_mathlib.lean takes 1.5 sec (on my laptop, 1 sec on my desktop). This happens once in every declaration that uses simp without only.

Isn't this something that can be cached?

view this post on Zulip Rob Lewis (Aug 27 2019 at 08:51):

It's not like it's an inherent problem -- I don't think Isabelle has the same behavior. Caching the simp set is probably pretty complicated because of multithreading. There's maybe something to be done there, but definitely not doable from mathlib.

view this post on Zulip Rob Lewis (Aug 27 2019 at 08:52):

It's the best case I've heard yet for minimizing imports. But I'm not sure how much it will really buy in the end. Maybe it helps this specific proof, but it will be a recurring issue.

view this post on Zulip Rob Lewis (Aug 27 2019 at 08:54):

It's fairly slow even just importing analysis.normed_space.basic.

view this post on Zulip Scott Morrison (Aug 27 2019 at 09:03):

I wonder if we should also be using local attribute [simp] more, or custom simp sets.

view this post on Zulip Floris van Doorn (Aug 27 2019 at 15:35):

I was always wondering whether the amount of simp declarations would cause performance issues. Limiting the number of imports might help a bit, but that is not a sustainable solution. Other potential solutions:

  • Can we write a user command at the top of a file that generates and caches the standard simp set, which all declarations in that file can then use? (Potentially modifying them a little bit, since some new simp-lemmas might be added).
  • As Scott said, make extensive use of simp-sets: instead of marking everything with @[simp] we mark things as topology_simp and linear_algebra_simp and with simp with topology_simp. Obviously this is a less nice user experience.
  • Be more restrictive with marking declarations as simp. Maybe not every simplification should be a simp-lemma. This will probably not make a big enough impact, since most simp-lemmas should remain simp-lemmas.

view this post on Zulip Rob Lewis (Aug 27 2019 at 16:53):

Can we write a user command at the top of a file that generates and caches the standard simp set, which all declarations in that file can then use? (Potentially modifying them a little bit, since some new simp-lemmas might be added).

And define a new tactic simp' to use our cache? That would probably be doable. I'm not sure how efficiently we can generate a cache compared to the built in methods. And I think it's pretty common to progressively prove a bunch of simp lemmas in a file, which may use each other, and then a lot of theorems that use these simp rules right after. We'd have to modify a lot of proofs and/or regenerate the cache a bunch of times per file.

view this post on Zulip Rob Lewis (Aug 27 2019 at 16:54):

I wonder if we should also be using local attribute [simp] more, or custom simp sets.

This seems like the most effective way to speed things up, and also a huge pain.

view this post on Zulip Rob Lewis (Aug 27 2019 at 16:54):

The alternative, of course, is to not change anything for now and see how things look in :four_leaf_clover: .

view this post on Zulip Rob Lewis (Aug 27 2019 at 16:58):

There are some simp sets that are pretty self-contained. I'm thinking of all the rules for making sense of filters. That would be a pretty natural thing to factor out of the default simp set.

view this post on Zulip Johan Commelin (Aug 27 2019 at 16:59):

Why is this not an issue in Isabelle?

view this post on Zulip Patrick Massot (Aug 27 2019 at 17:31):

Johan, did you ever read https://github.com/leanprover/lean/wiki/Simplifier-Features to see what the simplifier could look like?

view this post on Zulip Johan Commelin (Aug 27 2019 at 17:42):

Patrick, nope, I didn't.

view this post on Zulip Johan Commelin (Aug 27 2019 at 17:45):

It's an inspiring wiki page, thanks for the link!


Last updated: May 06 2021 at 18:20 UTC