def ISAR.add (A B : Matrix4) : Matrix4

Matrix addition.

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance ISAR.instAddMatrix4 : Add Matrix4

Equations

• ISAR.instAddMatrix4 = { add := ISAR.add }

def ISAR.neg (A : Matrix4) : Matrix4

Matrix negation.

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance ISAR.instNegMatrix4 : Neg Matrix4

Equations

• ISAR.instNegMatrix4 = { neg := ISAR.neg }

def ISAR.sub (A B : Matrix4) : Matrix4

Matrix subtraction.

Equations

• ISAR.sub A B = ISAR.add A (ISAR.neg B)

@[implicit_reducible]

instance ISAR.instSubMatrix4 : Sub Matrix4

Equations

• ISAR.instSubMatrix4 = { sub := ISAR.sub }

def ISAR.toMatrix4 (f : Fin 4 → Fin 4 → Int) : Matrix4

Convert a 4x4 function over Fin 4 to a Matrix4.

Equations

• One or more equations did not get rendered due to their size.

def ISAR.fromMatrix4 (M : Matrix4) (i j : Fin 4) : Int

Convert a Matrix4 back to a 4x4 function over Fin 4.

Equations

• ISAR.fromMatrix4 M ⟨0, isLt⟩ ⟨0, isLt_1⟩ = M.m00
• ISAR.fromMatrix4 M ⟨0, isLt⟩ ⟨1, isLt_1⟩ = M.m01
• ISAR.fromMatrix4 M ⟨0, isLt⟩ ⟨2, isLt_1⟩ = M.m02
• ISAR.fromMatrix4 M ⟨0, isLt⟩ ⟨3, isLt_1⟩ = M.m03
• ISAR.fromMatrix4 M ⟨1, isLt⟩ ⟨0, isLt_1⟩ = M.m10
• ISAR.fromMatrix4 M ⟨1, isLt⟩ ⟨1, isLt_1⟩ = M.m11
• ISAR.fromMatrix4 M ⟨1, isLt⟩ ⟨2, isLt_1⟩ = M.m12
• ISAR.fromMatrix4 M ⟨1, isLt⟩ ⟨3, isLt_1⟩ = M.m13
• ISAR.fromMatrix4 M ⟨2, isLt⟩ ⟨0, isLt_1⟩ = M.m20
• ISAR.fromMatrix4 M ⟨2, isLt⟩ ⟨1, isLt_1⟩ = M.m21
• ISAR.fromMatrix4 M ⟨2, isLt⟩ ⟨2, isLt_1⟩ = M.m22
• ISAR.fromMatrix4 M ⟨2, isLt⟩ ⟨3, isLt_1⟩ = M.m23
• ISAR.fromMatrix4 M ⟨3, isLt⟩ ⟨0, isLt_1⟩ = M.m30
• ISAR.fromMatrix4 M ⟨3, isLt⟩ ⟨1, isLt_1⟩ = M.m31
• ISAR.fromMatrix4 M ⟨3, isLt⟩ ⟨2, isLt_1⟩ = M.m32
• ISAR.fromMatrix4 M ⟨3, isLt⟩ ⟨3, isLt_1⟩ = M.m33

theorem ISAR.toMatrix4_fromMatrix4 (M : Matrix4) : toMatrix4 (fromMatrix4 M) = M

Theorem: converting a matrix to function and back is the identity.

theorem ISAR.fromMatrix4_toMatrix4 (f : Fin 4 → Fin 4 → Int) : fromMatrix4 (toMatrix4 f) = f

Theorem: converting a function to matrix and back is the identity.

def ISAR.K1 : Matrix4

The nilpotent core operator K1 representing konst combinator's matrix.

Equations

• ISAR.K1 = ISAR.I1 * ISAR.R1 * ISAR.A1 * ISAR.S1

inductive ISAR.ISKAlgebra : Matrix4 → Prop

The ISK monoid: what ISK can represent under application (multiplication).

• I : ISKAlgebra I1
• S : ISKAlgebra S1
• K : ISKAlgebra K1
• zero : ISKAlgebra ISAR.zero
• mul (M1 M2 : Matrix4) (h1 : ISKAlgebra M1) (h2 : ISKAlgebra M2) : ISKAlgebra (M1 * M2)

inductive ISAR.BasisAlgebra : Matrix4 → Prop

The full ISAR monoid: what requires R and A (dup and swap).

• I : BasisAlgebra I1
• R : BasisAlgebra R1
• A : BasisAlgebra A1
• S : BasisAlgebra S1
• zero : BasisAlgebra ISAR.zero
• mul (M1 M2 : Matrix4) (h1 : BasisAlgebra M1) (h2 : BasisAlgebra M2) : BasisAlgebra (M1 * M2)

def ISAR.term_signature_val : ITerm → Matrix4

Constructive term signature valuation function mapping ITerm directly to Matrix4.

Equations

• ISAR.term_signature_val (ISAR.ITerm.var a) = ISAR.zero
• ISAR.term_signature_val ISAR.ITerm.norm = ISAR.I1
• ISAR.term_signature_val ISAR.ITerm.sₛ = ISAR.S1
• ISAR.term_signature_val ISAR.ITerm.konst = ISAR.I1 * ISAR.R1 * ISAR.A1 * ISAR.S1
• ISAR.term_signature_val ISAR.ITerm.dup = ISAR.A1
• ISAR.term_signature_val ISAR.ITerm.swap = ISAR.R1
• ISAR.term_signature_val ISAR.ITerm.comp = ISAR.zero
• ISAR.term_signature_val (f · x_1) = ISAR.term_signature_val f * ISAR.term_signature_val x_1

def ISAR.term_signature (t : ISKSubtype) : Fin 4 → Fin 4 → Int

Bijective term signature mapping in the substrate.

Equations

• ISAR.term_signature t = ISAR.fromMatrix4 (ISAR.term_signature_val t.val)

def ISAR.term_matrix (t : ISKSubtype) : Matrix4

The matrix representative of a substrate term.

Equations

• ISAR.term_matrix t = ISAR.toMatrix4 (ISAR.term_signature t)

theorem ISAR.term_matrix_I : term_matrix ⟨ITerm.norm, ISKTerm.norm⟩ = I1

Theorem: The identity term I maps to I1.

theorem ISAR.term_matrix_S : term_matrix ⟨ITerm.sₛ, ISKTerm.sₛ⟩ = S1

Theorem: The combinator S maps to S1.

theorem ISAR.term_matrix_mul (t1 t2 : ISKSubtype) : term_matrix (app_raw t1 t2) = term_matrix t1 * term_matrix t2

Theorem: Application of terms corresponds to matrix multiplication.

theorem ISAR.term_matrix_zero : ∃ (t : ISKSubtype), term_matrix t = zero

Theorem: The zero matrix is constructively representable by applying konst to konst.

def ISAR.Row1OK (M : Matrix4) : Prop

Equations

• ISAR.Row1OK M = (M.m10 = 0 ∧ M.m11 = 0 ∧ M.m12 = 0 ∧ M.m13 = 0 ∨ M.m10 = 0 ∧ M.m11 = 1 ∧ M.m12 = 0 ∧ M.m13 = 0)

def ISAR.Row3OK (M : Matrix4) : Prop

Equations

• ISAR.Row3OK M = (M.m30 = 0 ∧ M.m31 = 0 ∧ M.m32 = 0 ∧ M.m33 = 0 ∨ M.m30 = 0 ∧ M.m31 = 0 ∧ M.m32 = 0 ∧ M.m33 = 1)

theorem ISAR.Row1OK_mul (M1 M2 : Matrix4) (h1 : Row1OK M1) (h2 : Row1OK M2) : Row1OK (M1 * M2)

theorem ISAR.Row3OK_mul (M1 M2 : Matrix4) (h1 : Row3OK M1) (h2 : Row3OK M2) : Row3OK (M1 * M2)

theorem ISAR.Row1OK_term (t : ITerm) (h : ISKTerm t) : Row1OK (term_signature_val t)

theorem ISAR.Row3OK_term (t : ITerm) (h : ISKTerm t) : Row3OK (term_signature_val t)

theorem ISAR.term_matrix_R_unreachable (t : ISKSubtype) : term_matrix t ≠ R1

Theorem: Rotation matrix R1 is unreachable in the pure ISK fragment.

theorem ISAR.term_matrix_A_unreachable (t : ISKSubtype) : term_matrix t ≠ A1

Theorem: Adjacency matrix A1 is unreachable in the pure ISK fragment.

theorem ISAR.isk_expressive_completeness (M : Matrix4) (h : ISKAlgebra M) : ∃ (t : ISKSubtype), term_matrix t = M

Expressive completeness of the pure functional ISK fragment monoid. Any matrix generated in ISKAlgebra is representable by an ISKSubtype term.

theorem ISAR.basis_expressive_completeness (M : Matrix4) (h : BasisAlgebra M) : ∃ (t : ITerm), term_signature_val t = M

Expressive completeness of the full ISAR monoid. Any matrix generated in BasisAlgebra is representable by an ITerm.