proving a concrete equation

Stream: new members

[Alex Zhang]

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]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

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]

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

[Eric Wieser]

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]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

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

[Alex Zhang]

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]

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

[Yakov Pechersky]

Probably easier to do via the polynomial definition

[Alex Zhang]

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]

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]

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

[Alex Zhang]

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]

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

[Yakov Pechersky]

Eric, you can use fintype.card iota maybe?

[Alex Zhang]

Yakov Pechersky said:

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

Good point!

[Alex Zhang]

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

[Alex Zhang]

@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]

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]

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]

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

[Yakov Pechersky]

Any fintype that has the appropriate order

[Alex Zhang]

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

[Alex Zhang]

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]

Is that part done by you? @Yakov Pechersky

[Yakov Pechersky]

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

[Alex Zhang]

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

[Alex Zhang]

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]

#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]

Can you reduce it to a statement about numbers?

[Mario Carneiro]

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

[Alex Zhang]

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]

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]

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

[Alex Zhang]

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]

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

[Alex Zhang]

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

[Eric Wieser]

What specifically did you eval?

[Alex Zhang]

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]

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

[Mario Carneiro]

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

[Alex Zhang]

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]

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

[Mario Carneiro]

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

[Alex Zhang]

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]

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]

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]

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

[Eric Wieser]

I don't think norm_fin knows about subtraction

[Mario Carneiro]

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]

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

[Alex Zhang]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

there aren't any tactics specifically designed for matrix computations

[Mario Carneiro]

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]

since we know that rfl closes the goal

[Alex Zhang]

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]

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]

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]

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

[Alex Zhang]

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]

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

[Yakov Pechersky]

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]

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]

and actually 23 lemmas for each vector that I need.

[Yakov Pechersky]

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

[Eric Wieser]

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]

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]

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]

Then you won't need any tactic

[Eric Wieser]

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

[Alex Zhang]

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]

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]

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]

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

[Alex Zhang]

#eval does correct evaluations, doesn't it?

[Alex Zhang]

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]

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]

Try that

[Alex Zhang]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

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]

(deleted)

[Eric Wieser]

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]

Did you add something like

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

[Alex Zhang]

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]

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]

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

[Yakov Pechersky]

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]

And there, you know that the subtraction nat friendly.

[Eric Wieser]

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]

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]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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