I wonder how to calculate matrix mul and invertible

Stream: new members

[Nick_adfor]

A(x) =

⎡ x - 1 3 -4 ⎤

⎢ -4 x + 7 -8 ⎥

⎣ -6 7 x - 7⎦

P(x) =

⎡ 1 0 0 ⎤

⎢(-x - 7)/3 1 0 ⎥

⎣(x² + 7)/(4x + 4) (-3x - 7)/(4x + 4) 1 ⎦

Q(x) =

⎡ 0 0 1 ⎤

⎢ 1 4⁄3 2 ⎥

⎣ 0 1 (x + 5)/4 ⎦

D(x) =

⎡ 3 0 0 ⎤

⎢ 0 (4x + 4)/3 0 ⎥

⎣ 0 0 (x² - 2x - 3)/4 ⎦

Prove that P(x) · A(x) · Q(x) = D(x), and also P(x) and Q(x) are invertible.
(diagonal divisibility form, Smith)

[Eric Wieser]

Please edit your message in place to use #backticks (the language goes after the opening ``` not before)

[Nick_adfor]

Eric Wieser said:

Please edit your message in place to use #backticks (the language goes after the opening ``` not before)

Thank you! I'm now refreshing.

[Nick_adfor]

import Mathlib

open Matrix Polynomial

variable (x : Polynomial ℚ)

noncomputable def A : Matrix (Fin 3) (Fin 3) (Polynomial ℚ) :=
  !![
    x - 1, 3, -4;
    -4, x + 7, -8;
    -6, 7, x - 7
  ]

noncomputable def Q : Matrix (Fin 3) (Fin 3) (Polynomial ℚ) :=
  !![
    0, 0, 1;
    1, 4 / 3, 2;
    0, 1, (x + 5) / 4
  ]

noncomputable def P : Matrix (Fin 3) (Fin 3) (Polynomial ℚ) :=
  !![
    4 * x + 4, 0, 0;
    -(4 / 3) * x^2 - (32 / 3) * x - (28 / 3), 4 * x + 4, 0;
    x^2 + 7, -3 * x - 7, 4 * x + 4
  ]

noncomputable def D : Matrix (Fin 3) (Fin 3) (Polynomial ℚ) :=
  !![
    12 * x + 12, 0, 0;
    0, (16 / 3) * x^2 + (32 / 3) * x + (16 / 3), 0;
    0, 0, x^3 - x^2 - 5 * x - 3
  ]

noncomputable def AQ : Matrix (Fin 3) (Fin 3) (Polynomial ℚ) :=
  !![
    3, 0, 0;
    x + 7, (4 * x + 4) / 3, 0;
    7, (3 * x + 7) / 3, (x^2 - 2 * x - 3) / 4
  ]

theorem PAQ_eq_D : P x * A x * Q x = D x := by
  have hAQ : A x * Q x =
  !![
    (x - 1) * 0 + 3 * 1 + (-4) * 0, (x - 1) * 0 + 3 * (4 / 3) + (-4) * 1, (x - 1) * 1 + 3 * 2 + (-4) * ((x + 5) / 4);
    (-4) * 0 + (x + 7) * 1 + (-8) * 0, (-4) * 0 + (x + 7) * (4 / 3) + (-8) * 1, (-4) * 1 + (x + 7) * 2 + (-8) * ((x + 5) / 4);
    (-6) * 0 + 7 * 1 + (x - 7) * 0, (-6) * 0 + 7 * (4 / 3) + (x - 7) * 1, (-6) * 1 + 7 * 2 + (x - 7) * ((x + 5) / 4)
  ] := by
      unfold A Q
      rw [Matrix.mul_fin_three]
  have hAQ' : A x * Q x = AQ x := by
    rw [hAQ]
    unfold AQ
    apply Matrix.ext
    intros i j
    fin_cases i; fin_cases j
    · simp [Matrix.cons_val_zero]
    · simp [Matrix.cons_val_one]
      ring_nf
      norm_num
    · simp [Matrix.cons_val_two, Matrix.tail_cons, Matrix.head_cons]
    · simp [Matrix.cons_val_zero]
      ring_nf
      fin_cases j
      · simp [Matrix.cons_val_zero]

      · simp [Matrix.cons_val_one]
        field_simp
        ring
      · simp [Matrix.cons_val_two, Matrix.tail_cons, Matrix.head_cons]
        field_simp
        ring

[Nick_adfor]

I don't know why lean cannot do the calculation. In line 60, even a trivial calculation cannot be realized automatically.

    · simp [Matrix.cons_val_one]
      ring_nf
      norm_num --⊢ -4 + 4 / 3 * 3 = 0

[Junyan Xu]

I don't think there's any tactic to deal with division in the Euclidean domain Q[X]. I'd recommend that you perform divisions in Q, e.g. you can turn 4 / 3 into C (1 / 3) * 4 or C (4 / 3), and (x + 5) / 4 into C (1 / 4) * (x + 5), etc.

[Nick_adfor]

import Mathlib

open Matrix Polynomial

variable (x : Polynomial ℚ)

noncomputable def A : Matrix (Fin 3) (Fin 3) (Polynomial ℚ) :=
  !![
    x - C 1, C 3, C (-4);
    C (-4), x + C 7, C (-8);
    C (-6), C 7, x - C 7
  ]

noncomputable def Q : Matrix (Fin 3) (Fin 3) (Polynomial ℚ) :=
  !![
    C 0, C 0, C 1;
    C 1, C (4/3 : ℚ), C 2;
    C 0, C 1, (x + C 5) * C (1/4 : ℚ)
  ]

noncomputable def P : Matrix (Fin 3) (Fin 3) (Polynomial ℚ) :=
  !![
    C 4 * x + C 4, C 0, C 0;
    -C (4/3 : ℚ) * x^2 - C (32/3 : ℚ) * x - C (28/3 : ℚ), C 4 * x + C 4, C 0;
    x^2 + C 7, -C 3 * x - C 7, C 4 * x + C 4
  ]

noncomputable def D : Matrix (Fin 3) (Fin 3) (Polynomial ℚ) :=
  !![
    C 12 * x + C 12, C 0, C 0;
    C 0, C (16/3 : ℚ) * x^2 + C (32/3 : ℚ) * x + C (16/3 : ℚ), C 0;
    C 0, C 0, x^3 - x^2 - C 5 * x - C 3
  ]

noncomputable def AQ : Matrix (Fin 3) (Fin 3) (Polynomial ℚ) :=
  !![
    C 3, C 0, C 0;
    x + C 7, C (4/3) * x + C (4/3), C 0;
    C 7, x + C (7/3), C (1/4) * x^2 - C (1/2) * x - C (3/4)
  ]

theorem PAQ_eq_D : P x * A x * Q x = D x := by
  have hAQ : A x * Q x =
  !![
    (x - C 1) * C 0 + C 3 * C 1 + C (-4) * C 0,
    (x - C 1) * C 0 + C 3 * C (4/3) + C (-4) * C 1,
    (x - C 1) * C 1 + C 3 * C 2 + C (-4) * ((x + C 5) * C (1/4));

    C (-4) * C 0 + (x + C 7) * C 1 + C (-8) * C 0,
    C (-4) * C 0 + (x + C 7) * C (4/3) + C (-8) * C 1,
    C (-4) * C 1 + (x + C 7) * C 2 + C (-8) * ((x + C 5) * C (1/4));

    C (-6) * C 0 + C 7 * C 1 + (x - C 7) * C 0,
    C (-6) * C 0 + C 7 * C (4/3) + (x - C 7) * C 1,
    C (-6) * C 1 + C 7 * C 2 + (x - C 7) * ((x + C 5) * C (1/4))
  ] := by
      unfold A Q
      rw [Matrix.mul_fin_three]
  have hAQ' : A x * Q x = AQ x := by
    rw [hAQ]
    unfold AQ
    apply Matrix.ext
    intros i j
    fin_cases i; fin_cases j
    · simp [Matrix.cons_val_zero]
    · simp [Matrix.cons_val_one]
      by_eval
    · simp [Matrix.cons_val_two]
      by_eval
    · simp [Matrix.cons_val_zero]
      ring_nf
      fin_cases j
      · simp [Matrix.cons_val_zero]
      · simp [Matrix.cons_val_one]
        rw [← C_mul]
        ring_nf
        rw [← C_sub]
        ring_nf
      · simp [Matrix.cons_val_two]
        field_simp
        repeat rw [← C_mul]
        ring_nf
        rw [← C_neg]
        rw [← C_sub]
        ring_nf
        rw [C_neg]
        rw [add_neg_cancel_right]
        rw [neg_add_eq_zero]
        rw [mul_rotate]
        rw [← C_mul]
        ring_nf
    · simp [Matrix.cons_val_two]
      fin_cases j
      simp [Matrix.cons_val_zero]
      · simp [Matrix.cons_val_one]
        by_eval
      · simp [Matrix.cons_val_two]
        rw [← C_mul]
        rw [← mul_assoc (x - C 7) (x + C 5) (C 4⁻¹)]
        by_eval

[Nick_adfor]

Now this part cannot be done by simp only [Matrix.cons_val_one] : (

[Nick_adfor]

Junyan Xu said:

I don't think there's any tactic to deal with division in the Euclidean domain Q[X]. I'd recommend that you perform divisions in Q, e.g. you can turn 4 / 3 into C (1 / 3) * 4 or C (4 / 3), and (x + 5) / 4 into C (1 / 4) * (x + 5), etc.

This remark really helps. Now the following question comes to fin_cases

[Nick_adfor]

There are two parts using fin_cases j, seeming that I might do something repeatedly and now get stuck : (

[Nick_adfor]

rw [← C_mul] works for the previous line, but not for the last one. I’m unsure why fin_cases cannot be applied to split that row of the matrix.

[Hagb (Junyu Guo)]

Nick_adfor said:

now get stuck : (

It seems that your proof costs too much time and reaches the maximum heart beats (as you can see in the info view). A set_option maxHeartbeats 400000 in line can be added before the declaration to increase the maximum amount for this declaration, or set_option maxHeartbeats 400000 (without in) to set it for all remaining declarations.

[Hagb (Junyu Guo)]

By the way, since the field ℚ used here is infinite, a trick to prove the equality of two polynomials over it is proving the equality of evaluations of them. An evaluation of a polynomial (after rewritten) will be composed of +, -, *, /, and ofNat on the field ℚ, so ring tactic can be used to prove their equality.

macro (name := by_eval) "by_eval" : tactic =>
  `(tactic| (
    apply Polynomial.funext
    intro x
    try simp only [eval_sub, eval_add, eval_X, eval_C, eval_smul, eval_mul, eval_natCast,
        eval_pow, eval_neg, eval_ofNat, eval_one, eval_zero, smul_eq_mul]
    ring) )

example (x : Polynomial ℚ) :
    -(x * C 8 * C (1 / 4)) +
    x * C 2 + C 7 * C 2 + (-(C 8 * C 5 * C (1 / 4)) - C 4) = 0 := by
  by_eval

[Nick_adfor]

Hagb (Junyu Guo) said:

By the way, since the field ℚ used here is infinite, a trick to prove the equality of two polynomials over it is proving the equality of evaluations of them. An evaluation of a polynomial (after rewritten) will be composed of +, -, *, and ofNat on the field ℚ, so ring tactic can be used to prove their equality.

macro (name := by_eval) "by_eval" : tactic =>
  `(tactic| (
    apply Polynomial.funext
    intro x
    try simp only [eval_sub, eval_add, eval_X, eval_C, eval_smul, eval_mul, eval_natCast,
        eval_pow, eval_neg, eval_ofNat, eval_one, eval_zero, smul_eq_mul]
    ring) )

example (x : Polynomial ℚ) :
    -(x * C 8 * C (1 / 4)) +
    x * C 2 + C 7 * C 2 + (-(C 8 * C 5 * C (1 / 4)) - C 4) = 0 := by
  by_eval

I've never tried define a new tactic before. This trick really helps to shorten the code. I don't know if try will cause too much automatic work.

[Nick_adfor]

I write it so long because I only use rw? to generate.

[Nick_adfor]

      · simp [Matrix.cons_val_two, Matrix.tail_cons, Matrix.head_cons]
        field_simp
        repeat rw [← C_mul]
        ring_nf
        rw [← C_neg]
        rw [← C_sub]
        ring_nf
        rw [C_neg]
        rw [add_neg_cancel_right]
        rw [neg_add_eq_zero]
        rw [mul_rotate]
        rw [← C_mul]
        ring_nf

Just look at this part, one can see what rw? will generate. Seems it do not generate eval_, but only C_.

[Hagb (Junyu Guo)]

Nick_adfor said:

I don't know if try will cause too much automatic work.

try should be removed here, I think. I forgot what I was thinking when I wrote it about a month ago.

[Nick_adfor]

Hagb (Junyu Guo) said:

Nick_adfor said:

I don't know if try will cause too much automatic work.

try should be removed here, I think. I forgot what I was thinking when I wrote it about a month ago.

May I ask in which piece of code you applied this tactic?

[Nick_adfor]

import Mathlib

open Matrix Polynomial

variable (x : Polynomial ℚ)

macro "by_eval" : tactic => `(tactic| (
  apply Polynomial.funext
  intro x
  try simp [eval_sub, eval_add, eval_X, eval_C, eval_smul, eval_mul, eval_natCast, eval_pow, eval_neg, eval_ofNat, eval_one, eval_zero, smul_eq_mul]
  ring
))

noncomputable def A : Matrix (Fin 3) (Fin 3) (Polynomial ℚ) :=
  !![
    x - C 1, C 3, C (-4);
    C (-4), x + C 7, C (-8);
    C (-6), C 7, x - C 7
  ]

noncomputable def Q : Matrix (Fin 3) (Fin 3) (Polynomial ℚ) :=
  !![
    C 0, C 0, C 1;
    C 1, C (4/3 : ℚ), C 2;
    C 0, C 1, (x + C 5) * C (1/4 : ℚ)
  ]

noncomputable def P : Matrix (Fin 3) (Fin 3) (Polynomial ℚ) :=
  !![
    C 4 * x + C 4, C 0, C 0;
    -C (4/3 : ℚ) * x^2 - C (32/3 : ℚ) * x - C (28/3 : ℚ), C 4 * x + C 4, C 0;
    x^2 + C 7, -C 3 * x - C 7, C 4 * x + C 4
  ]

noncomputable def D : Matrix (Fin 3) (Fin 3) (Polynomial ℚ) :=
  !![
    C 12 * x + C 12, C 0, C 0;
    C 0, C (16/3 : ℚ) * x^2 + C (32/3 : ℚ) * x + C (16/3 : ℚ), C 0;
    C 0, C 0, x^3 - x^2 - C 5 * x - C 3
  ]

noncomputable def AQ : Matrix (Fin 3) (Fin 3) (Polynomial ℚ) :=
  !![
    C 3, C 0, C 0;
    x + C 7, C (4/3) * x + C (4/3), C 0;
    C 7, x + C (7/3), C (1/4) * x^2 - C (1/2) * x - C (3/4)
  ]

theorem PAQ_eq_D : P x * A x * Q x = D x := by
  have hAQ : A x * Q x =
  !![
    (x - C 1) * C 0 + C 3 * C 1 + C (-4) * C 0,
    (x - C 1) * C 0 + C 3 * C (4/3) + C (-4) * C 1,
    (x - C 1) * C 1 + C 3 * C 2 + C (-4) * ((x + C 5) * C (1/4));

    C (-4) * C 0 + (x + C 7) * C 1 + C (-8) * C 0,
    C (-4) * C 0 + (x + C 7) * C (4/3) + C (-8) * C 1,
    C (-4) * C 1 + (x + C 7) * C 2 + C (-8) * ((x + C 5) * C (1/4));

    C (-6) * C 0 + C 7 * C 1 + (x - C 7) * C 0,
    C (-6) * C 0 + C 7 * C (4/3) + (x - C 7) * C 1,
    C (-6) * C 1 + C 7 * C 2 + (x - C 7) * ((x + C 5) * C (1/4))
  ] := by
      unfold A Q
      rw [Matrix.mul_fin_three]
  have hAQ' : A x * Q x = AQ x := by
    rw [hAQ]
    unfold AQ
    apply Matrix.ext
    intros i j
    fin_cases i; fin_cases j
    · simp [Matrix.cons_val_zero]
    · simp [Matrix.cons_val_one]
      by_eval
    · simp [Matrix.cons_val_two]
      by_eval
    · simp [Matrix.cons_val_zero]
      ring_nf
      fin_cases j
      · simp [Matrix.cons_val_zero]
      · simp [Matrix.cons_val_one]
        by_eval
      · simp [Matrix.cons_val_two]
        by_eval
    · simp [Matrix.cons_val_two]
      fin_cases j
      simp [Matrix.cons_val_zero]
      · by_eval
      · simp [Matrix.cons_val_two]
        rw [← C_mul]
        rw [← mul_assoc (x - C 7) (x + C 5) (C 4⁻¹)]
        by_eval

[Nick_adfor]

The calculation must be cut now. As the tactic is right but lean cannot work because of maximum!

[Nick_adfor]

Hagb (Junyu Guo) said:

By the way, since the field ℚ used here is infinite, a trick to prove the equality of two polynomials over it is proving the equality of evaluations of them. An evaluation of a polynomial (after rewritten) will be composed of +, -, *, /, and ofNat on the field ℚ, so ring tactic can be used to prove their equality.

macro (name := by_eval) "by_eval" : tactic =>
  `(tactic| (
    apply Polynomial.funext
    intro x
    try simp only [eval_sub, eval_add, eval_X, eval_C, eval_smul, eval_mul, eval_natCast,
        eval_pow, eval_neg, eval_ofNat, eval_one, eval_zero, smul_eq_mul]
    ring) )

example (x : Polynomial ℚ) :
    -(x * C 8 * C (1 / 4)) +
    x * C 2 + C 7 * C 2 + (-(C 8 * C 5 * C (1 / 4)) - C 4) = 0 := by
  by_eval

I want to make by_eval? workable. How to write? It will shorten the code.

[Nick_adfor]

macro "by_eval?" : tactic => `(tactic| (
  apply Polynomial.funext
  intro x
  simp? [eval_sub, eval_add, eval_X, eval_C, eval_smul, eval_mul,
              eval_natCast, eval_pow, eval_neg, eval_ofNat,
              eval_one, eval_zero, smul_eq_mul]
  ring
))

I tried this but failed.

[Hagb (Junyu Guo)]

Nick_adfor said:

May I ask in which piece of code you applied this tactic?

I wrote it when I was exploring ways to verify the identity of polynomials (as elements of polynomial ring), and I applied it mostly for testing.

I want to make by_eval? workable. How to write? It will shorten the code.

On my side, this tactic itself can prove the identity of polynomials. Do you want a tactic (like simp?) giving a "try this" suggestion which can be applied?

[Nick_adfor]

Hagb (Junyu Guo) said:

Nick_adfor said:

May I ask in which piece of code you applied this tactic?

I wrote it when I was exploring ways to verify the identity of polynomials (as elements of polynomial ring), and I applied it mostly for testing.

I want to make by_eval? workable. How to write? It will shorten the code.

On my side, this tactic itself can prove the identity of polynomials. Do you want a tactic (like simp?) giving a "try this" suggestion which can be applied?

Yes, I need a try this suggestion. The proof is failing because it hits the maximum number of heartbeats when by_eval tries to solve it automatically. Using a more restrictive tactic like simp only should reduce the amount of work, preventing it from hitting the limit. (Is this essentially a stack overflow?)

[Hagb (Junyu Guo)]

Nick_adfor said:

Yes, I need a try this suggestion. The proof is failing because it hits the maximum number of heartbeats when by_eval tries to solve it automatically. Using a more restrictive tactic like simp only should reduce the amount of work, preventing it from hitting the limit. (Is this essentially a stack overflow?)

In my understanding, if it happens in a long proof, it might be just because the proof costs too much time. Maybe you can try increasing the maximum number of heartbeats to 2 times of the current one and see whether it works again. (If it keeps hitting the maximum, maybe there is endless loop in a tactic.)

[Nick_adfor]

Hagb (Junyu Guo) said:

Nick_adfor said:

Yes, I need a try this suggestion. The proof is failing because it hits the maximum number of heartbeats when by_eval tries to solve it automatically. Using a more restrictive tactic like simp only should reduce the amount of work, preventing it from hitting the limit. (Is this essentially a stack overflow?)

In my understanding, if it happens in a long proof, it might be just because the proof costs too much time. Maybe you can try increasing the maximum number of heartbeats to 2 times of the current one and see whether it works again. (If it keeps hitting the maximum, maybe there is endless loop in a tactic.)

Surely I'm trying to double the maximum and also I have used some simp? to cut the automatic work. by_eval? is just that I want to try some new tactic. In fact I've never tried to write a tactic before. Just rw, simp or something else. So I'm curious that if by_eval? can be realized.

[Nick_adfor]

And also, I've noticed that ring do not have ring?. Why that?

[Aaron Liu]

what would ring? do?

[Nick_adfor]

Aaron Liu said:

what would ring? do?

I wish it to do similar thing as simp?. It might give me try this.

[Aaron Liu]

The terms ring produces aren't really readable

[Aaron Liu]

and it's not like there's additional configuration options that make it work better or faster

[Aaron Liu]

I guess there's ring!

[Aaron Liu]

import Mathlib.Tactic.Ring

/--
info: Try this: Mathlib.Tactic.Ring.of_eq
  (Mathlib.Tactic.Ring.add_congr
    (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf y)
      (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.atom_pf y) (Mathlib.Tactic.Ring.atom_pf x)
        (Mathlib.Tactic.Ring.add_mul
          (Mathlib.Tactic.Ring.mul_add
            (Mathlib.Tactic.Ring.mul_pf_left y (Nat.rawCast 1)
              (Mathlib.Tactic.Ring.mul_pf_right x (Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))))
            (Mathlib.Tactic.Ring.mul_zero (y ^ Nat.rawCast 1 * Nat.rawCast 1))
            (Mathlib.Tactic.Ring.add_pf_add_zero (y ^ Nat.rawCast 1 * (x ^ Nat.rawCast 1 * Nat.rawCast 1) + 0)))
          (Mathlib.Tactic.Ring.zero_mul (x ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))
          (Mathlib.Tactic.Ring.add_pf_add_zero (y ^ Nat.rawCast 1 * (x ^ Nat.rawCast 1 * Nat.rawCast 1) + 0))))
      (Mathlib.Tactic.Ring.add_pf_add_lt (y ^ Nat.rawCast 1 * Nat.rawCast 1)
        (Mathlib.Tactic.Ring.add_pf_zero_add (y ^ Nat.rawCast 1 * (x ^ Nat.rawCast 1 * Nat.rawCast 1) + 0))))
    (Mathlib.Tactic.Ring.atom_pf x)
    (Mathlib.Tactic.Ring.add_pf_add_lt (y ^ Nat.rawCast 1 * Nat.rawCast 1)
      (Mathlib.Tactic.Ring.add_pf_add_lt (y ^ Nat.rawCast 1 * (x ^ Nat.rawCast 1 * Nat.rawCast 1))
        (Mathlib.Tactic.Ring.add_pf_zero_add (x ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
  (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf x)
    (Mathlib.Tactic.Ring.mul_congr
      (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat R Nat.cast_one))
        (Mathlib.Tactic.Ring.atom_pf x)
        (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1)
          (Mathlib.Tactic.Ring.add_pf_zero_add (x ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
      (Mathlib.Tactic.Ring.atom_pf y)
      (Mathlib.Tactic.Ring.add_mul
        (Mathlib.Tactic.Ring.mul_add
          (Mathlib.Tactic.Ring.mul_pf_right y (Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))
          (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1))
          (Mathlib.Tactic.Ring.add_pf_add_zero (y ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))
        (Mathlib.Tactic.Ring.add_mul
          (Mathlib.Tactic.Ring.mul_add
            (Mathlib.Tactic.Ring.mul_pf_right y (Nat.rawCast 1)
              (Mathlib.Tactic.Ring.mul_pf_left x (Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))))
            (Mathlib.Tactic.Ring.mul_zero (x ^ Nat.rawCast 1 * Nat.rawCast 1))
            (Mathlib.Tactic.Ring.add_pf_add_zero (y ^ Nat.rawCast 1 * (x ^ Nat.rawCast 1 * Nat.rawCast 1) + 0)))
          (Mathlib.Tactic.Ring.zero_mul (y ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))
          (Mathlib.Tactic.Ring.add_pf_add_zero (y ^ Nat.rawCast 1 * (x ^ Nat.rawCast 1 * Nat.rawCast 1) + 0)))
        (Mathlib.Tactic.Ring.add_pf_add_lt (y ^ Nat.rawCast 1 * Nat.rawCast 1)
          (Mathlib.Tactic.Ring.add_pf_zero_add (y ^ Nat.rawCast 1 * (x ^ Nat.rawCast 1 * Nat.rawCast 1) + 0)))))
    (Mathlib.Tactic.Ring.add_pf_add_gt (y ^ Nat.rawCast 1 * Nat.rawCast 1)
      (Mathlib.Tactic.Ring.add_pf_add_gt (y ^ Nat.rawCast 1 * (x ^ Nat.rawCast 1 * Nat.rawCast 1))
        (Mathlib.Tactic.Ring.add_pf_add_zero (x ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
-/
#guard_msgs in
example {R : Type*} [CommSemiring R] (x y : R) : y + y * x + x = x + (1 + x) * y := by?
  ring

[Nick_adfor]

What is by? ring?

[Aaron Liu]

by? will show you the proof that your tactics are producing

[Nick_adfor]

import Mathlib
open Matrix Polynomial
variable (x : Polynomial ℚ)
/--
Custom tactic `by_eval` for proving polynomial equalities:
1. Applies polynomial extensionality (funext)
2. Introduces arbitrary x
3. Simplifies evaluation using specific rules
4. Finishes with ring tactic
Usage: `by_eval` proves equalities like `p = q` for polynomials p,q
-/
macro "by_eval" : tactic => `(tactic| (
  apply Polynomial.funext
  intro x
  simp only [eval_sub, eval_add, eval_X, eval_C, eval_smul, eval_mul, eval_natCast, eval_pow, eval_neg, eval_ofNat, eval_one, eval_zero, smul_eq_mul]
  ring
))
set_option maxHeartbeats 1000000
/--The origin matrix A-/
noncomputable def A : Matrix (Fin 3) (Fin 3) (Polynomial ℚ) :=
  !![
    x - C 1, C 3, C (-4);
    C (-4), x + C 7, C (-8);
    C (-6), C 7, x - C 7
  ]
/-- Transformation matrix Q containing eigenvectors -/
noncomputable def Q : Matrix (Fin 3) (Fin 3) (Polynomial ℚ) :=
  !![
    C 0, C 0, C 1;
    C 1, C (4/3 : ℚ), C 2;
    C 0, C 1, (x + C 5) * C (1/4 : ℚ)
  ]
/-- Product matrix AQ showing transformed structure -/
noncomputable def AQ : Matrix (Fin 3) (Fin 3) (Polynomial ℚ) :=
  !![
    C 3, C 0, C 0;
    x + C 7, C (4/3) * x + C (4/3), C 0;
    C 7, x + C (7/3), C (1/4) * x^2 - C (1/2) * x - C (3/4)
  ]
/-- Transformation matrix P for diagonalization -/
noncomputable def P : Matrix (Fin 3) (Fin 3) (Polynomial ℚ) :=
  !![
    C 4 * x + C 4, C 0, C 0;
    -C (4/3 : ℚ) * x^2 - C (32/3 : ℚ) * x - C (28/3 : ℚ), C 4 * x + C 4, C 0;
    x^2 + C 7, -C 3 * x - C 7, C 4 * x + C 4
  ]
/-- Diagonal matrix D (Smith) -/
noncomputable def D : Matrix (Fin 3) (Fin 3) (Polynomial ℚ) :=
  !![
    C 12 * x + C 12, C 0, C 0;
    C 0, C (16/3 : ℚ) * x^2 + C (32/3 : ℚ) * x + C (16/3 : ℚ), C 0;
    C 0, C 0, x^3 - x^2 - C 5 * x - C 3
  ]
/-- The product of A and Q gives the matrix AQ -/
lemma AQ_AQ :A x * Q x = AQ x := by
  -- Multiply matrix A by matrix Q element by element.
  have hAQ : A x * Q x =
  !![
    (x - C 1) * C 0 + C 3 * C 1 + C (-4) * C 0,
    (x - C 1) * C 0 + C 3 * C (4/3) + C (-4) * C 1,
    (x - C 1) * C 1 + C 3 * C 2 + C (-4) * ((x + C 5) * C (1/4));
    C (-4) * C 0 + (x + C 7) * C 1 + C (-8) * C 0,
    C (-4) * C 0 + (x + C 7) * C (4/3) + C (-8) * C 1,
    C (-4) * C 1 + (x + C 7) * C 2 + C (-8) * ((x + C 5) * C (1/4));
    C (-6) * C 0 + C 7 * C 1 + (x - C 7) * C 0,
    C (-6) * C 0 + C 7 * C (4/3) + (x - C 7) * C 1,
    C (-6) * C 1 + C 7 * C 2 + (x - C 7) * ((x + C 5) * C (1/4))
  ] := by
      unfold A Q
      rw [Matrix.mul_fin_three]
  -- The resulting matrix A * Q is simplified to a specific form.
  have hAQ' : A x * Q x = AQ x := by
    rw [hAQ]
    unfold AQ
    apply Matrix.ext
    intros i j
    fin_cases i; fin_cases j
    · simp only [_root_.map_one, map_zero, mul_zero, mul_one, zero_add, map_neg, add_zero, one_div,
      neg_mul, Fin.zero_eta, Fin.isValue, of_apply, cons_val', cons_val_zero, empty_val',
      cons_val_fin_one]
    · simp only [_root_.map_one, map_zero, mul_zero, mul_one, zero_add, map_neg, add_zero, one_div,
      neg_mul, Fin.zero_eta, Fin.isValue, Fin.mk_one, of_apply, cons_val', cons_val_one, head_cons,
      empty_val', cons_val_fin_one, cons_val_zero]
      rw [← @C_mul]
      ring_nf
    · simp only [_root_.map_one, map_zero, mul_zero, mul_one, zero_add, map_neg, add_zero, one_div,
      neg_mul, Fin.zero_eta, Fin.isValue, Fin.reduceFinMk, of_apply, cons_val', cons_val_two,
      Nat.succ_eq_add_one, Nat.reduceAdd, tail_cons, head_cons, empty_val', cons_val_fin_one,
      cons_val_zero]
      by_eval
    · simp only [_root_.map_one, map_zero, mul_zero, mul_one, zero_add, map_neg, add_zero, one_div,
      neg_mul, Fin.mk_one, Fin.isValue, of_apply, cons_val', empty_val', cons_val_fin_one,
      cons_val_one, head_cons]
      ring_nf
      fin_cases j
      · simp only [one_div, Fin.zero_eta, Fin.isValue, cons_val_zero]
      · simp only [one_div, Fin.mk_one, Fin.isValue, cons_val_one, head_cons, add_right_inj, ← C_mul]
        ring_nf
        rw [← C_sub]
        ring_nf
      · simp only [one_div, Fin.reduceFinMk, cons_val_two, Nat.succ_eq_add_one, Nat.reduceAdd,
        tail_cons, head_cons]
        repeat rw [← C_mul]
        ring_nf
        rw [← C_neg]
        rw [← C_sub]
        ring_nf
        rw [C_neg]
        rw [add_neg_cancel_right]
        rw [neg_add_eq_zero]
        rw [mul_rotate]
        rw [← C_mul]
        ring_nf
    · simp only [_root_.map_one, map_zero, mul_zero, mul_one, zero_add, map_neg, add_zero, one_div,
      neg_mul, Fin.reduceFinMk, of_apply, Fin.isValue, cons_val', empty_val', cons_val_fin_one,
      cons_val_two, Nat.succ_eq_add_one, Nat.reduceAdd, tail_cons, head_fin_const]
      fin_cases j
      simp only [Fin.zero_eta, Fin.isValue, cons_val_zero]
      · simp only [Fin.mk_one, Fin.isValue, cons_val_one, head_cons]
        by_eval
      · simp only [Fin.reduceFinMk, cons_val_two, Nat.succ_eq_add_one, Nat.reduceAdd, tail_cons,
        head_cons]
        rw [← C_mul]
        rw [← mul_assoc (x - C 7) (x + C 5) (C 4⁻¹)]
        by_eval
  rw [hAQ']
/-- The product of P and AQ gives the diagonal matrix D -/
theorem PAQ_eq_D : P x * A x * Q x = D x := by
  rw [Matrix.mul_assoc]
  rw [AQ_AQ]
  -- Multiply matrix P by matrix AQ element by element.
  have hPAQ : P x * AQ x =
  !![
    (C 4 * x + C 4) * C 3 + C 0 * (x + C 7) + C 0 * C 7,
    (C 4 * x + C 4) * C 0 + C 0 * (C (4/3) * x + C (4/3)) + C 0 * (x + C (7/3)),
    (C 4 * x + C 4) * C 0 + C 0 * C 0 + C 0 * (C (1/4) * x^2 - C (1/2) * x - C (3/4));
    (-C (4/3) * x^2 - C (32/3) * x - C (28/3)) * C 3 + (C 4 * x + C 4) * (x + C 7) + C 0 * C 7,
    (-C (4/3) * x^2 - C (32/3) * x - C (28/3)) * C 0 + (C 4 * x + C 4) * (C (4/3) * x + C (4/3)) + C 0 * (x + C (7/3)),
    (-C (4/3) * x^2 - C (32/3) * x - C (28/3)) * C 0 + (C 4 * x + C 4) * C 0 + C 0 * (C (1/4) * x^2 - C (1/2) * x - C (3/4));
    (x^2 + C 7) * C 3 + (-C 3 * x - C 7) * (x + C 7) + (C 4 * x + C 4) * C 7,
    (x^2 + C 7) * C 0 + (-C 3 * x - C 7) * (C (4/3) * x + C (4/3)) + (C 4 * x + C 4) * (x + C (7/3)),
    (x^2 + C 7) * C 0 + (-C 3 * x - C 7) * C 0 + (C 4 * x + C 4) * (C (1/4) * x^2 - C (1/2) * x - C (3/4))
  ]:= by
      unfold P AQ
      rw [Matrix.mul_fin_three]
  -- The resulting matrix P * AQ is simplified to a specific form.
  have hPAQ' : P x * AQ x = D x := by
    rw [hPAQ]
    unfold D
    apply Matrix.ext
    intros i j
    fin_cases i; fin_cases j
    · simp only [_root_.map_one, map_zero, mul_zero, mul_one, zero_add, map_neg, add_zero, one_div,
        neg_mul, Fin.zero_eta, Fin.isValue, of_apply, cons_val', cons_val_zero, empty_val',
        cons_val_fin_one, zero_mul, add_zero]
      by_eval
    · simp only [map_zero, mul_zero, zero_add, add_zero, one_div, neg_mul, Fin.zero_eta,
      Fin.isValue, Fin.mk_one, of_apply, cons_val', cons_val_one, head_cons, empty_val',
      cons_val_fin_one, cons_val_zero]
      simp only [zero_mul, add_zero, eval_zero]
    · simp only [map_zero, mul_zero, zero_add, add_zero, one_div, neg_mul, Fin.zero_eta,
      Fin.isValue, Fin.reduceFinMk, of_apply, cons_val', cons_val_two, Nat.succ_eq_add_one,
      Nat.reduceAdd, tail_cons, head_cons, empty_val', cons_val_fin_one, cons_val_zero]
      ring_nf
    · simp only [map_zero, mul_zero, zero_add, add_zero, one_div, neg_mul, Fin.mk_one, Fin.isValue,
      of_apply, cons_val', empty_val', cons_val_fin_one, cons_val_one, head_cons]
      ring_nf
      fin_cases j
      · simp only [Fin.zero_eta, Fin.isValue, cons_val_zero]
        by_eval
      · simp only [one_div, Fin.mk_one, Fin.isValue, cons_val_one, head_cons, add_right_inj, ← C_mul]
        by_eval
      · simp only [one_div, Fin.reduceFinMk, cons_val_two, Nat.succ_eq_add_one, Nat.reduceAdd,
        tail_cons, head_cons]
    · simp only [add_mul, mul_assoc, map_zero, mul_add, zero_mul, add_zero, mul_zero, one_div,
      sub_eq_add_neg, mul_neg, neg_zero, neg_mul, zero_add, neg_add_rev, Fin.reduceFinMk, of_apply,
      Fin.isValue, cons_val', empty_val', cons_val_fin_one, cons_val_two, Nat.succ_eq_add_one,
      Nat.reduceAdd, tail_cons, head_fin_const]
      fin_cases j
      ring_nf
      · simp only [one_div, Fin.zero_eta, Fin.isValue, cons_val_zero]
        by_eval
      · simp only [← C_mul, Fin.mk_one, Fin.isValue, cons_val_one, head_cons]
        simp only [_root_.map_mul]
        by_eval
      · simp only [Fin.reduceFinMk, cons_val_two, Nat.succ_eq_add_one, Nat.reduceAdd, tail_cons,
        head_cons]
        by_eval
  rw [hPAQ']

[Nick_adfor]

My whole code is here. But as my have is to long to prove, so have hAQ' : A x * Q x = AQ x := by? gives a wrong one. I do really need something like by_eval to print what this tactic produced.

[Nick_adfor]

Aaron Liu said:

example {R : Type*} [CommSemiring R] (x y : R) : y + y * x + x = x + (1 + x) * y := by?
  ring

Will printing out all the proofs generated by tactic increase or decrease the amount of computational power consumed?

[Aaron Liu]

It will decrease the readability and increase the length of your proofs

[Nick_adfor]

Hagb (Junyu Guo) said:

By the way, since the field ℚ used here is infinite, a trick to prove the equality of two polynomials over it is proving the equality of evaluations of them. An evaluation of a polynomial (after rewritten) will be composed of +, -, *, /, and ofNat on the field ℚ, so ring tactic can be used to prove their equality.

macro (name := by_eval) "by_eval" : tactic =>
  `(tactic| (
    apply Polynomial.funext
    intro x
    try simp only [eval_sub, eval_add, eval_X, eval_C, eval_smul, eval_mul, eval_natCast,
        eval_pow, eval_neg, eval_ofNat, eval_one, eval_zero, smul_eq_mul]
    ring) )

example (x : Polynomial ℚ) :
    -(x * C 8 * C (1 / 4)) +
    x * C 2 + C 7 * C 2 + (-(C 8 * C 5 * C (1 / 4)) - C 4) = 0 := by
  by_eval

I may ask if there's a MvPolynomial version

[Nick_adfor]

There's tactic about eval of MvPolynomial needed here.

[Nick_adfor]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Formalize.20paper.20about.20Restricted.20Sums