Is this a diamond?

Stream: mathlib4

[Jeremy Tan]

I'm trying to prove Theorem 11 in Kozen's 1994 paper, that matrices over Kleene algebras are Kleene algebras. Here is what I have so far:

import Mathlib.Algebra.Order.Kleene
import Mathlib.Data.Matrix.Block

namespace Matrix

variable {α m n : Type*} [Fintype m] [Fintype n]

instance idemSemiring [IdemSemiring α] : IdemSemiring (Matrix n n α) :=
  inferInstanceAs <| IdemSemiring (n → n → α)

open Computability

variable [KleeneAlgebra α] [KleeneAlgebra (Matrix m m α)] [KleeneAlgebra (Matrix n n α)]
  {E X : Matrix (m ⊕ n) (m ⊕ n) α}

/-- The Kleene star operation on block matrices. -/
def kstarBlock (M : Matrix (m ⊕ n) (m ⊕ n) α) : Matrix (m ⊕ n) (m ⊕ n) α :=
  let A := M.toBlocks₁₁
  let B := M.toBlocks₁₂
  let C := M.toBlocks₂₁
  let D := M.toBlocks₂₂
  let F := A + B * D∗ * C
  let B' := F∗ * B * D∗
  let C' := D∗ * C * F∗
  let D' := D∗ + D∗ * C * F∗ * B * D∗
  fromBlocks F∗ B' C' D'

lemma one_add_mul_kstarBlock_le_kstarBlock : E * kstarBlock E ≤ kstarBlock E := by
  rw [← fromBlocks_toBlocks E, kstarBlock]
  set A := E.toBlocks₁₁
  set B := E.toBlocks₁₂
  set C := E.toBlocks₂₁
  set D := E.toBlocks₂₂
  rw [toBlocks_fromBlocks₁₁, toBlocks_fromBlocks₁₂, toBlocks_fromBlocks₂₁, toBlocks_fromBlocks₂₂]
  set F := A + B * D∗ * C
  rw [fromBlocks_multiply]
  rw [← add_eq_right_iff_le]
  ext (i | i) (j | j)
  · simp_rw [fromBlocks_add, fromBlocks_apply₁₁, ← Matrix.mul_assoc, ← add_mul]
    change (F * F∗ + F∗) i j = _
    have : F * F∗ ≤ F∗ := mul_kstar_le_kstar -- here
    sorry
  · sorry
  · sorry
  · sorry

end Matrix

At the -- here I have the following error:

Type mismatch
  mul_kstar_le_kstar
has type
  @HMul.hMul ?m.258 ?m.258 ?m.258 instHMul ?m.260 ?m.260∗ ≤ ?m.260∗
but is expected to have type
  @HMul.hMul (Matrix m m α) (Matrix m m α) (Matrix m m α) instHMulOfFintypeOfMulOfAddCommMonoid F F∗ ≤ F∗

How do I fix this?

[Kevin Buzzard]

This line

instance idemSemiring [IdemSemiring α] : IdemSemiring (Matrix n n α) :=
  inferInstanceAs <| IdemSemiring (n → n → α)

says "put a semiring structure on Matrix n n α where the multiplication is pointwise multiplication on coefficients rather than matrix multiplication". Could this be the problem?

[Jakub Nowak]

You probably want to define KleeneAlgebra on matrices as in the paper, instead of assuming that some arbitrary instance is given. Which boils down to defining order and kstar, and proving some properties of these.

import Mathlib.Algebra.Order.Kleene
import Mathlib.Data.Matrix.Block

namespace Matrix

variable {α m n : Type*} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n]

open Computability

variable [KleeneAlgebra α] {E X : Matrix (m ⊕ n) (m ⊕ n) α}

instance {n} [Fintype n] [DecidableEq n] : KleeneAlgebra (Matrix n n α) where
  le := sorry
  le_refl := sorry
  le_trans := sorry
  le_antisymm := sorry
  le_sup_left := sorry
  le_sup_right := sorry
  sup_le := sorry
  bot_le := sorry
  kstar := sorry
  one_le_kstar := sorry
  mul_kstar_le_kstar := sorry
  kstar_mul_le_kstar := sorry
  mul_kstar_le_self := sorry
  kstar_mul_le_self := sorry

/-- The Kleene star operation on block matrices. -/
def kstarBlock (M : Matrix (m ⊕ n) (m ⊕ n) α) : Matrix (m ⊕ n) (m ⊕ n) α :=
  let A := M.toBlocks₁₁
  let B := M.toBlocks₁₂
  let C := M.toBlocks₂₁
  let D := M.toBlocks₂₂
  let F := A + B * D∗ * C
  let B' := F∗ * B * D∗
  let C' := D∗ * C * F∗
  let D' := D∗ + D∗ * C * F∗ * B * D∗
  fromBlocks F∗ B' C' D'

lemma one_add_mul_kstarBlock_le_kstarBlock : E * kstarBlock E ≤ kstarBlock E := by
  rw [← fromBlocks_toBlocks E, kstarBlock]
  set A := E.toBlocks₁₁
  set B := E.toBlocks₁₂
  set C := E.toBlocks₂₁
  set D := E.toBlocks₂₂
  rw [toBlocks_fromBlocks₁₁, toBlocks_fromBlocks₁₂, toBlocks_fromBlocks₂₁, toBlocks_fromBlocks₂₂]
  set F := A + B * D∗ * C
  rw [fromBlocks_multiply]
  rw [← add_eq_right_iff_le]
  ext (i | i) (j | j)
  · simp_rw [fromBlocks_add, fromBlocks_apply₁₁, ← Matrix.mul_assoc, ← add_mul]
    change (F * F∗ + F∗) i j = _
    have : F * F∗ ≤ F∗ := mul_kstar_le_kstar -- here
    sorry
  · sorry
  · sorry
  · sorry

end Matrix

[Jakub Nowak]

I've also added DecidableEq because it's required by Matrix.semiring.

[Jeremy Tan]

Kevin Buzzard said:

This line

instance idemSemiring [IdemSemiring α] : IdemSemiring (Matrix n n α) :=
  inferInstanceAs <| IdemSemiring (n → n → α)

says "put a semiring structure on Matrix n n α where the multiplication is pointwise multiplication on coefficients rather than matrix multiplication". Could this be the problem?

Yeah, I realised this thinko after some further thinking on the problem

[Jeremy Tan]

Jakub Nowak said:

You probably want to define KleeneAlgebra on matrices as in the paper, instead of assuming that some arbitrary instance is given. Which boils down to defining order and kstar, and proving some properties of these.

It can't work that way; in the paper the Kleene algebra construction for matrices is only defined blockwise, with undefined block size

[Jeremy Tan]

So I could theoretically obtain, say, KleeneAlgebra (Matrix (Fin 7) (Fin 7) α) from KleeneAlgebra (Matrix (Fin 3) (Fin 3) α) and KleeneAlgebra (Matrix (Fin 4) (Fin 4) α) or KleeneAlgebra (Matrix (Fin 2) (Fin 2) α) and KleeneAlgebra (Matrix (Fin 5) (Fin 5) α), and I have to make sure that their LE instances are all elementwise on the matrices

[Jeremy Tan]

Do I have to add hypotheses on the order like this?

instance instKleeneAlgebraSum
    (o₁ : ∀ M₁ M₂ : Matrix m m α, M₁ ≤ M₂ ↔ (M₁ · ·) ≤ (M₂ · ·))
    (o₂ : ∀ M₁ M₂ : Matrix n n α, M₁ ≤ M₂ ↔ (M₁ · ·) ≤ (M₂ · ·)) :
    KleeneAlgebra (Matrix (m ⊕ n) (m ⊕ n) α) where
  le A B := (A · ·) ≤ (B · ·)
  le_refl _ := by rfl
  le_trans _ _ _ h₁ h₂ := h₁.trans h₂
  le_antisymm _ _ h₁ h₂ := by
    ext i j
    exact le_antisymm (h₁ i j) (h₂ i j)
  le_sup_left _ _ _ _ := by simp
  le_sup_right _ _ _ _ := by simp
  sup_le _ _ _ h₁ h₂ i j := by simp [h₁ i j, h₂ i j]
  bot_le _ _ _ := by simp
  kstar M :=
    let A := M.toBlocks₁₁
    let B := M.toBlocks₁₂
    let C := M.toBlocks₂₁
    let D := M.toBlocks₂₂
    let F := A + B * D∗ * C
    let B' := F∗ * B * D∗
    let C' := D∗ * C * F∗
    let D' := D∗ + D∗ * C * F∗ * B * D∗
    fromBlocks F∗ B' C' D'
  one_le_kstar E := by
    extract_lets A B C D F B' C' D'
    rw [← fromBlocks_one]
    rintro (i | i) (j | j)
    · simp only [fromBlocks_apply₁₁]
      sorry
    · simp
    · simp
    · simp only [fromBlocks_apply₂₂]
      sorry
  mul_kstar_le_kstar E := by
    sorry
  kstar_mul_le_kstar E := by
    sorry
  mul_kstar_le_self X E h := by
    sorry
  kstar_mul_le_self X E h := by
    sorry

[Eric Wieser]

I think you want a type alias here

[Eric Wieser]

Also, you're immediately going to run into the fact that KleeneAlgebra doesn't let you work with rectangular matrices anyway, when you get to

In general all the axioms and basic properties of Kleene algebra listed in [...] hold when the primitive letters are interpreted as possibly nonsquare matrices over a Kleene algebra provided that there are no type conflicts in the application of the Kleene algebra operators

[Eric Wieser]

Jeremy Tan said:

It can't work that way; in the paper the Kleene algebra construction for matrices is only defined blockwise, with undefined block size

On the other hand, the paper says

We remark that the inductive definition (53) of $E^{*}$ in Lemma 10 is independent of the partition of E chosen in (52)

which suggests there's some better strategy here

[Eric Wieser]

In particular, it seems you can recurse over Fintype.univ and show under the quotient that the result is the same whatever order you do so in

[Eric Wieser]

It might be easier to define the operator for Fin indices first and then show that it is invariant to permutations, so that you can lift it through truncEquivFin

[Eric Wieser]

So concretely, what I propose is:

1. Define Matrix.kleeneStar using the method I just outlined
2. Prove basic properties of it (in products with rectangular matrices) using (A · ·) ≤ (B · ·) comparisons, such that you cover all the fields of KleeneAlgebra
3. Create a structure KleeneMatrix m n K where ofMatrix :: toMatrix : Matrix m n K that wraps 1 and 2, and then trivially provide the KleeneAlgebra (KleeneMatrix m n K) result