Zulip Chat Archive

Stream: new members

Topic: proving a concrete equation


Alex Zhang (Jul 28 2021 at 20:18):

Could anyone give me a way to proving the following equation, which I need to establish first for a later theorem?
As far as I know, the "proof" has largely to be a brute force computation. The vectors a b c d were also firstly found by a computer.

import data.matrix.notation

def circulant {α : Type*} {n : } (v : fin n  α) : matrix (fin n) (fin n) α
| i j := v (i - j)

def a : fin 23   :=
![ 1,  1, -1, -1, -1,  1, -1, -1, -1,  1, -1,  1,  1, -1,  1, -1, -1, -1,  1, -1, -1, -1,  1]
def b : fin 23   :=
![ 1, -1,  1,  1, -1,  1,  1, -1, -1,  1,  1,  1,  1,  1,  1, -1, -1,  1,  1, -1,  1,  1, -1]
def c : fin 23   :=
![ 1,  1,  1, -1, -1, -1,  1,  1, -1,  1, -1,  1,  1, -1,  1, -1,  1,  1, -1, -1, -1,  1,  1]
def d : fin 23   :=
![ 1,  1,  1, -1,  1,  1,  1, -1,  1, -1, -1, -1, -1, -1, -1,  1, -1,  1,  1,  1, -1,  1,  1]

local notation `A` := circulant a
local notation `B` := circulant b
local notation `C` := circulant c
local notation `D` := circulant d

lemma want : A^2 + B^2 + C^2 + D^2 = (92 : matrix (fin 23) (fin 23) ) :=
begin
  sorry
end

Alex Zhang (Jul 28 2021 at 20:29):

Perhaps split a big computation task into several small computation tasks?

Yakov Pechersky (Jul 28 2021 at 20:35):

You could do "ext i j, fin_cases i; fin_cases j; simp [circulant]". That would be the most brute force.

Yakov Pechersky (Jul 28 2021 at 20:36):

You would want to prove some helper lemmas that proving that a matrix equal to some numeral coerced to a matrix requires solely proving it along the diagonal and zero values along nondiagonal entries.

Eric Wieser (Jul 28 2021 at 20:37):

Why don't you instead prove that the product of circulant matrices is a circulant matrix?

Eric Wieser (Jul 28 2021 at 20:38):

Then you only have to show a vector of 23 elements is ![1, 0, 0, ...] rather than having to show equality of a matrix of 529 elements

Eric Wieser (Jul 28 2021 at 20:39):

@Yakov Pechersky, any ideas for generalizing circulant matrices away from fin using permutations?

Yakov Pechersky (Jul 28 2021 at 20:41):

According to Wikipedia, using the matrix polynomial of the cyclic permutation matrix P

Yakov Pechersky (Jul 28 2021 at 20:42):

But that P is still over fin n, because of how it's sparse definition is.

Alex Zhang (Jul 28 2021 at 20:43):

Eric Wieser said:

Then you only have to show a vector of 23 elements is ![1, 0, 0, ...] rather than having to show equality of a matrix of 529 elements

Yeah! That's what I thought. I am trying to express A^2 and etc as a circulant v for some v first.

Yakov Pechersky (Jul 28 2021 at 20:44):

Alex, Wikipedia says that circulant matrices form a commutative algebra. Can you give it that instance?

Yakov Pechersky (Jul 28 2021 at 20:44):

Probably easier to do via the polynomial definition

Alex Zhang (Jul 28 2021 at 20:45):

Yakov Pechersky said:

Probably easier to do via the polynomial definition

Not quite sure about this. I considered using this as the definition. But used the direct one enventually.

def circulant {α : Type*} {n : } (v : fin n  α) : matrix (fin n) (fin n) α
| i j := v (i - j)

Eric Wieser (Jul 28 2021 at 20:46):

Yakov, does using any permutation matrix that is an nth root of the identity work, rather than needing the cyclic permutation on fin n?

Eric Wieser (Jul 28 2021 at 20:47):

Ah, I guess n has to match the cardinality of the index type

Alex Zhang (Jul 28 2021 at 20:50):

Eric Wieser said:

Yakov, does using any permutation matrix that is an nth root of the identity work, rather than needing the cyclic permutation on fin n?

I don't think so. For example, (1 2) ( 3 4 5) has order 6, but is not a cyclic permutation of order 6.

Yakov Pechersky (Jul 28 2021 at 20:54):

The polynomial definitions leads directly to the proof about the algebra. And encodes the sparsity better.

Yakov Pechersky (Jul 28 2021 at 20:55):

Eric, you can use fintype.card iota maybe?

Alex Zhang (Jul 28 2021 at 20:55):

Yakov Pechersky said:

The polynomial definitions leads directly to the proof about the algebra. And encodes the sparsity better.

Good point!

Alex Zhang (Jul 28 2021 at 20:56):

I think I am to prove those things if I have time, and then add them into mathlib.

Alex Zhang (Jul 28 2021 at 20:57):

@Yakov Pechersky Btw, I have already tried to run

ext i j, fin_cases i,
  any_goals {fin_cases j},

to see what happens,
but it hasn't finished yet.....

Yakov Pechersky (Jul 28 2021 at 20:58):

We have some stuff around matrix polynomials (because of proofs of cayley Hamilton) but not too much. I'm working on pushing some in, but have not been able to do any mathlib work due to real-life job. Just zulip.

Yakov Pechersky (Jul 28 2021 at 20:59):

Try to see if it works for just the first case on i first. That'll be 23 (+ 22) goals, instead of 23 squared.

Eric Wieser (Jul 28 2021 at 20:59):

I think I'm resigned to the fact that this only makes sense for fin n

Yakov Pechersky (Jul 28 2021 at 21:00):

Any fintype that has the appropriate order

Alex Zhang (Jul 28 2021 at 21:01):

Ah, I will have a look at the matrix polynomial part implemented.

Alex Zhang (Jul 28 2021 at 21:01):

Alex Zhang said:

Yakov Pechersky Btw, I have already tried to run

ext i j, fin_cases i,
  any_goals {fin_cases j},

to see what happens,
but it hasn't finished yet.....

It hasn't finished... I am to kill it.

Alex Zhang (Jul 28 2021 at 21:02):

Is that part done by you? @Yakov Pechersky

Yakov Pechersky (Jul 28 2021 at 21:05):

I don't have mathlib access to run it for a week

Alex Zhang (Jul 28 2021 at 21:11):

ext i j, fin_cases i, fin_cases j, is ok

Alex Zhang (Jul 28 2021 at 21:12):

If I am facing the goal (A * A + B * B + C * C + D * D) 0 0 = 92 0 0 or changing the * to pow_two, are there any tactics that will close such a goal in one or two steps?

Alex Zhang (Jul 28 2021 at 21:22):

#eval (A * A + B * B + C * C + D * D) 0 0 prints 92. But I am not able to use #eval in the proof. Does anyone know whether there is any alternative tactic that will be helpful if the goal is
example : (A * A + B * B + C * C + D * D) 0 0 = 92 := sorry

Mario Carneiro (Jul 28 2021 at 21:24):

Can you reduce it to a statement about numbers?

Mario Carneiro (Jul 28 2021 at 21:25):

simp should be able to do most of the heavy lifting here

Alex Zhang (Jul 28 2021 at 21:27):

If using simp, I will kind of be stuck here

example : (A * A + B * B + C * C + D * D) 0 0 = 92 :=
begin
  simp [mul_apply, circulant, a, b, c, d],
  sorry
end

Alex Zhang (Jul 29 2021 at 09:19):

Could anyone give some suggestions on proving a goal which is a direct computation that #eval can do? Is it possible to expand finset.sum as the form...+...+...+...?

import data.matrix.notation
import tactic.gptf

open matrix

def circulant {α : Type*} {n : } (v : fin n  α) : matrix (fin n) (fin n) α
| i j := v (i - j)

def a : fin 23   :=
![ 1,  1, -1, -1, -1,  1, -1, -1, -1,  1, -1,  1,  1, -1,  1, -1, -1, -1,  1, -1, -1, -1,  1]
def b : fin 23   :=
![ 1, -1,  1,  1, -1,  1,  1, -1, -1,  1,  1,  1,  1,  1,  1, -1, -1,  1,  1, -1,  1,  1, -1]
def c : fin 23   :=
![ 1,  1,  1, -1, -1, -1,  1,  1, -1,  1, -1,  1,  1, -1,  1, -1,  1,  1, -1, -1, -1,  1,  1]
def d : fin 23   :=
![ 1,  1,  1, -1,  1,  1,  1, -1,  1, -1, -1, -1, -1, -1, -1,  1, -1,  1,  1,  1, -1,  1,  1]

local notation `A` := circulant a
local notation `B` := circulant b
local notation `C` := circulant c
local notation `D` := circulant d

example :
  dot_product
      (λ (i : fin 23),
         ![(1 : ), 1, -1, -1, -1, 1, -1, -1, -1, 1, -1, 1, 1, -1, 1, -1, -1, -1, 1, -1, -1, -1, 1]
           (-i))
      (λ (i : fin 23),
         ![(1 : ), 1, -1, -1, -1, 1, -1, -1, -1, 1, -1, 1, 1, -1, 1, -1, -1, -1, 1, -1, -1, -1, 1]
           (i - 1)) =
    -1 :=
begin
  sorry,
end

example : (A * A) 0 1 = -1 :=
begin
  sorry,
end

Eric Wieser (Jul 29 2021 at 09:31):

simp only [dot_product, fin.sum_univ_succ], expands the sum for you

Alex Zhang (Jul 29 2021 at 09:34):

A way I can solve the first example without expanding the sum is

example :
  dot_product
      (λ (i : fin 23),
         ![(1 : ), 1, -1, -1, -1, 1, -1, -1, -1, 1, -1, 1, 1, -1, 1, -1, -1, -1, 1, -1, -1, -1, 1]
           (-i))
      (λ (i : fin 23),
         ![(1 : ), 1, -1, -1, -1, 1, -1, -1, -1, 1, -1, 1, 1, -1, 1, -1, -1, -1, 1, -1, -1, -1, 1]
           (i - 1)) =
    -1 :=
begin
  have :
  dot_product
  ![(1 : ), 1, -1, -1, -1, 1, -1, -1, -1, 1, -1, 1, 1, -1, 1, -1, -1, -1, 1, -1, -1, -1, 1]
  ![1, 1, 1, -1, -1, -1, 1, -1, -1, -1, 1, -1, 1, 1, -1, 1, -1, -1, -1, 1, -1, -1, -1]
  = -1,
  {norm_num},
  nth_rewrite_rhs 0 [ this],
  congr;
  dec_trivial!,
end

Alex Zhang (Jul 29 2021 at 09:36):

I first use #eval outside the proof, and then copy the result into the proof to simplify terms.

Alex Zhang (Jul 29 2021 at 09:36):

Is it possible to add a tactic that does #eval? @Eric Wieser

Eric Wieser (Jul 29 2021 at 09:37):

What specifically did you eval?

Alex Zhang (Jul 29 2021 at 09:39):

I did

#eval
(λ (i : fin 23),
         ![(1 : ), 1, -1, -1, -1, 1, -1, -1, -1, 1, -1, 1, 1, -1, 1, -1, -1, -1, 1, -1, -1, -1, 1]
           (-i))

and the other.

Eric Wieser (Jul 29 2021 at 09:45):

It would certainly be helpful if there was a tactic to convert ![a, b, c, d] (-i) into ![a, d, c, b]

Mario Carneiro (Jul 29 2021 at 09:47):

You can use norm_fin to turn -12 : fin 23 into 11

Alex Zhang (Jul 29 2021 at 09:48):

It is not hard to prove that
example : ![(1 : ℚ), 1, -1, -1, -1, 1, -1, -1, -1, 1, -1, 1, 1, -1, 1, -1, -1, -1, 1, -1, -1, -1, 1] (-1) = 1 := rfl
But I don't know how to simplify or rewrite the LHS as the RHS in a more complicated expression.
Do you have a clue?

Mario Carneiro (Jul 29 2021 at 09:49):

doesn't simp prove that ![a, b, c, d] 3 = d?

Mario Carneiro (Jul 29 2021 at 09:49):

I'm aware that rfl does it but the goal here is for simp to discover the rhs on its own

Alex Zhang (Jul 29 2021 at 09:51):

Ah, simp closes that example {α} (a b c d : α): ![a, b, c, d] 3 = d := by simp. Perhaps I should first use norm_fin.

Alex Zhang (Jul 29 2021 at 09:53):

example :
![(1 : ), 1, -1, -1, -1, 1, -1, -1, -1, 1, -1, 1, 1, -1, 1, -1, -1, -1, 1, -1, -1, -1, 1] (-1) = 1 :=
by {norm_fin,}

norm_fin won't change -1 in the goal :cry:

Alex Zhang (Jul 29 2021 at 09:54):

1 goal
 ![1, 1, -1, -1, -1, 1, -1, -1, -1, 1, -1, 1, 1, -1, 1, -1, -1, -1, 1, -1, -1, -1, 1] (-1) = 1

@Mario Carneiro

Alex Zhang (Jul 29 2021 at 09:56):

example : (-1 : fin 23) = 22 := by norm_fin This also dose not work.

Eric Wieser (Jul 29 2021 at 09:58):

I don't think norm_fin knows about subtraction

Mario Carneiro (Jul 29 2021 at 09:58):

Hm, it seems to be a gap in norm_fin, probably because @Eric Wieser informed me only yesterday that fin subtraction isn't broken anymore

Mario Carneiro (Jul 29 2021 at 09:59):

that's awkward; you can use change (-1 : fin 23) with 22 but that's kind of verbose

Alex Zhang (Jul 29 2021 at 10:01):

Yes, in a more involved computation. Doing all the change (-1 : fin 23) with 22type things manually is not practical.

Mario Carneiro (Jul 29 2021 at 10:02):

well, you should have more lemmas to simplify this to something not using subtraction anyway

Mario Carneiro (Jul 29 2021 at 10:03):

rather than just trying to power through the whole thing with simp et al

Mario Carneiro (Jul 29 2021 at 10:03):

there aren't any tactics specifically designed for matrix computations

Mario Carneiro (Jul 29 2021 at 10:04):

so you will have to either wait for the existing tactics to be upgraded, write them yourself, or write a lemma that says what you want

Mario Carneiro (Jul 29 2021 at 10:04):

since we know that rfl closes the goal

Alex Zhang (Jul 29 2021 at 10:05):

Mario Carneiro said:

well, you should have more lemmas to simplify this to something not using subtraction anyway

That is a good suggestions. I will try to write more lemmas first.

Alex Zhang (Aug 04 2021 at 14:47):

Eric Wieser said:

It would certainly be helpful if there was a tactic to convert ![a, b, c, d] (-i) into ![a, d, c, b]

Can we extend norm_num to do so somehow? @Eric Wieser

Yakov Pechersky (Aug 04 2021 at 14:48):

Usually, norm_num extensions deal with normalizing numerical values, which can indicate many different types (as long as there is a 0 and +, in fact).

Yakov Pechersky (Aug 04 2021 at 14:49):

And norm_num is helpful because it does VM calculation to help it decide what proofs to create.

Alex Zhang (Aug 04 2021 at 14:51):

Is it possible to add some lemma or extend simp or norm_num to rewrite things like
(λ (j : fin 23), ![a, b, c, d, ...] (i - j)), where i is a given number (e.g. 0 or 1 or 4)?

Yakov Pechersky (Aug 04 2021 at 14:51):

In this matrix rearrangement case, there are no calculations, just rewrites. So you could write a lemma to do so.

Yakov Pechersky (Aug 04 2021 at 14:52):

Ah, I see, you want to do it for arbitrary vectors, and just have a rearrangement of terms. And the underlying calculation is some modular arithmetic.

Alex Zhang (Aug 04 2021 at 14:54):

Yes, otherwise I need to write 23

lemma A_0_dot_a : dot_product (λ (j : fin 23), a (0 - j)) a = 23 :=
by sorry

where def a : fin 23 → ℚ := ![ 1, 1, -1, -1, -1, 1, -1, -1, -1, 1, -1, 1, 1, -1, 1, -1, -1, -1, 1, -1, -1, -1, 1]

Alex Zhang (Aug 04 2021 at 14:54):

and actually 23 lemmas for each vector that I need.

Yakov Pechersky (Aug 04 2021 at 14:54):

I guess first step would be to extend norm_fin to deal with negatives

Eric Wieser (Aug 04 2021 at 14:59):

Alex Zhang said:

Eric Wieser said:

It would certainly be helpful if there was a tactic to convert ![a, b, c, d] (-i) into ![a, d, c, b]

Can we extend norm_num to do so somehow? Eric Wieser

In my opinion the way to solve this would be to have a tactic that converts f where f : fin n → A and n is a numeric literal into ![f 0, f 1, ..., f (n - 1)], at which point norm_fin could likely simplify f 0 etc.

Alex Zhang (Aug 04 2021 at 14:59):

There may be a way that uses norm_fin, but my proof does not

lemma A_5_dot_a : dot_product (λ (j : fin 23), a (5 - j)) a = -1 :=
begin
  have :
  (λ (j : fin 23), a (5 - j)) =
  ![1, -1, -1, -1, 1, 1, 1, -1, -1, -1, 1, -1, -1, -1, 1, -1, 1, 1, -1, 1, -1, -1, -1],
  {dec_trivial},
  rw [this, a],
  norm_num,
end

Yakov Pechersky (Aug 04 2021 at 15:00):

Can you write the correct form for this lemma?

lemma vec_cons_apply_neg {m : } (x : α) (u : fin m  α) (i : fin (m + 1)) :
  vec_cons x u (-i) = _ := sorry

Yakov Pechersky (Aug 04 2021 at 15:00):

Then you won't need any tactic

Eric Wieser (Aug 04 2021 at 15:01):

Writing an expand_fin f tactic that does as I describe above might be a good exercise in metaprogramming

Alex Zhang (Aug 04 2021 at 15:03):

Yakov Pechersky said:

Can you write the correct form for this lemma?

lemma vec_cons_apply_neg {m : } (x : α) (u : fin m  α) (i : fin (m + 1)) :
  vec_cons x u (-i) = _ := sorry

I don't quite understand why this can be helpful. There has not to be (-i), it can be (5-i) for example.

Yakov Pechersky (Aug 04 2021 at 15:04):

Yes, I understand that you have (j - i) in your case. If you write the correct (-i) lemma then you will be able to use that to show the (j - i) case.

Alex Zhang (Aug 04 2021 at 15:05):

I currently don't know how to write a tactic. I guess having a tactic that does #eval may be more helpful in general.

Yakov Pechersky (Aug 04 2021 at 15:05):

The tactic doing #eval doesn't help if it can't also provide a proof term that the evaluation is correct.

Alex Zhang (Aug 04 2021 at 15:06):

#eval does correct evaluations, doesn't it?

Alex Zhang (Aug 04 2021 at 15:12):

Yakov Pechersky said:

Can you write the correct form for this lemma?

lemma vec_cons_apply_neg {m : } (x : α) (u : fin m  α) (i : fin (m + 1)) :
  vec_cons x u (-i) = _ := sorry

I am not sure what is the correct term (in the sense that it makes the lemma helpful for the following problems) for the underscore.

Yakov Pechersky (Aug 04 2021 at 15:13):

inductive acc' {α} (r : α  α  Prop) : α  Prop
| intro (x : α) (h :  y : α, r y x  acc' y) : acc' x

def foo : string :=
@acc'.rec_on string (λ _ _, false) (λ _, string) "" _, by cc $ λ x h IH, x

#eval foo

Yakov Pechersky (Aug 04 2021 at 15:13):

Try that

Alex Zhang (Aug 04 2021 at 15:16):

#eval reports error vm check failed: is_external(o) (possibly due to incorrect axioms, or sorry)

Yakov Pechersky (Aug 04 2021 at 15:17):

So #eval doesn't always work, even if the definitions are accepted by the kernel

Yakov Pechersky (Aug 04 2021 at 15:18):

lemma vec_cons_apply_neg_zero {m : } (x : α) (u : fin m  α) (i : fin (m + 1)) :
  vec_cons x u (-0) = x :=
by simp

lemma vec_cons_apply_neg_one {m : } (x : α) (u : fin (m + 1)  α) (i : fin (m + 2)) :
  vec_cons x u (-1) = u (-1) := sorry

Eric Wieser (Aug 04 2021 at 15:22):

(deleted)

Eric Wieser (Aug 04 2021 at 15:23):

I just tried to fix norm_fin; my conclusion is that the easiest way to do so is probably to normalize fin to an integer instead of to a natural

Yakov Pechersky (Aug 04 2021 at 15:24):

Did you add something like

| `(@_root_.has_neg.neg ._ (@fin.has_neg %%n) %%a) := some (neg n a)

Alex Zhang (Aug 04 2021 at 15:25):

Would norm_fin be helpful for proving

lemma A_5_dot_a : dot_product (λ (j : fin 23), a (5 - j)) a = -1 :=
begin
  have :
  (λ (j : fin 23), a (5 - j)) =
  ![1, -1, -1, -1, 1, 1, 1, -1, -1, -1, 1, -1, -1, -1, 1, -1, 1, 1, -1, 1, -1, -1, -1],
  {dec_trivial},
  rw [this, a],
  norm_num,
end

?
As j is a variable, I didn't see what norm_fin can do for us.

Alex Zhang (Aug 04 2021 at 15:34):

Yakov Pechersky said:

So #eval doesn't always work, even if the definitions are accepted by the kernel

I understand that #eval can fail in some cases, but when it fails, I think it just means we shouldn't use it in that case.

Eric Wieser (Aug 04 2021 at 15:35):

@Yakov Pechersky, normalize_fin.sub is hard to express with naturals

Yakov Pechersky (Aug 04 2021 at 15:37):

Use the following:

lemma fin.neg_succ_eq {m : } (i : fin m) :
  (-i.succ) = fin.last _ - i.cast_succ :=
begin
  simp only [fin.ext_iff, fin.coe_neg, fin.coe_sub, nat.succ_sub_succ_eq_sub, fin.coe_last,
             fin.coe_succ, fin.coe_cast_succ],
  rw [nat.add_sub_assoc (nat.le_succ_of_le i.is_lt.le), add_comm,
      nat.add_sub_assoc i.is_lt.le, nat.add_mod, nat.mod_self,
      zero_add, nat.mod_mod]
end

Yakov Pechersky (Aug 04 2021 at 15:38):

And there, you know that the subtraction nat friendly.

Eric Wieser (Aug 04 2021 at 15:49):

I don't know whether that was aimed at me or Alex. I pushed my half-baked attempt at branch#eric-wieser/norm_fin_sub, but do not intend to continue trying

Alex Zhang (Aug 04 2021 at 15:53):

Alex Zhang said:

Would norm_fin be helpful for proving

lemma A_5_dot : dot_product (λ (j : fin 23), a (5 - j)) a = -1 :=
begin
  have :
  (λ (j : fin 23), a (5 - j)) =
  ![1, -1, -1, -1, 1, 1, 1, -1, -1, -1, 1, -1, -1, -1, 1, -1, 1, 1, -1, 1, -1, -1, -1],
  {dec_trivial},
  rw [this, a],
  norm_num,
end

?
As j is a variable, I didn't see what norm_fin can do for us.

Eric, would norm_fin be useful for lemmas like this? @Eric Wieser
I currently have to write 23 lemmas for each a.

Alex Zhang (Aug 04 2021 at 15:58):

things like #eval (cir a) a take an amazingly long time.

Mario Carneiro (Aug 04 2021 at 16:27):

Using integers will cause problems with the other reductions. Instead, I was thinking of reducing a - b in fin to a - b as naturals when a >= b, and when a < b then just fully reduce it to c := ((a - b : fin n) : nat) and prove a + c = b + k * n

Yakov Pechersky (Aug 04 2021 at 16:28):

Will this work with (-a) - (-b)?

Mario Carneiro (Aug 04 2021 at 16:28):

it goes one step at a time. -a would get reduced the same as 0 - a


Last updated: Dec 20 2023 at 11:08 UTC