Grace/Cumulus/LinearAlgebra/TwoByTwo.g17

Open in Workbench Download source

Imports

Real.Inverse

Declarations

• solutionX def
• solutionY def
• solutionX.real theorem derivation
• solutionY.real theorem derivation
• correct theorem derivation
• unique theorem derivation

Source

1-- Explicit solutions of two real linear equations.2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.LinearAlgebra.TwoByTwo8import Real.Inverse910namespace LinearSystem21112-- These total expressions are solutions only when the determinant is nonzero.13def solutionX (a b c d u v : Real) : Real :=14  realInvValue(a * d - b * c) * (d * u - b * v)1516def solutionY (a b c d u v : Real) : Real :=17  realInvValue(a * d - b * c) * (a * v - c * u)1819theorem solutionX.real (a b c d u v : Real)20  shows Real(solutionX(a, b, c, d, u, v))21proof22  unfold solutionX23  typecheck2425theorem solutionY.real (a b c d u v : Real)26  shows Real(solutionY(a, b, c, d, u, v))27proof28  unfold solutionY29  typecheck3031theorem correct (a b c d u v : Real)32  requires nonsingular : a * d - b * c ≠ 033  shows a * solutionX(a, b, c, d, u, v) + b * solutionY(a, b, c, d, u, v) = u ∧34    c * solutionX(a, b, c, d, u, v) + d * solutionY(a, b, c, d, u, v) = v35proof36  have inverse := realInvValue.mul_left with *37  constructor38  . unfold solutionX39    unfold solutionY40    linear_combination u * inverse41  . unfold solutionX42    unfold solutionY43    linear_combination v * inverse4445-- Uniqueness applies directly to any two solutions, without unfolding Cramer formulas.46theorem unique (a b c d u v x y s t : Real)47  requires nonsingular : a * d - b * c ≠ 048  requires first : a * x + b * y = u49  requires second : c * x + d * y = v50  requires otherFirst : a * s + b * t = u51  requires otherSecond : c * s + d * t = v52  shows x = s ∧ y = t53proof54  have inverse := realInvValue.mul_left with *55  constructor56  . linear_combination (realInvValue(a * d - b * c) * d) * first - (realInvValue(a * d - b * c) * b) * second - (realInvValue(a * d - b * c) * d) * otherFirst + (realInvValue(a * d - b * c) * b) * otherSecond - (x - s) * inverse57  . linear_combination (realInvValue(a * d - b * c) * a) * second - (realInvValue(a * d - b * c) * c) * first - (realInvValue(a * d - b * c) * a) * otherSecond + (realInvValue(a * d - b * c) * c) * otherFirst - (y - t) * inverse5859end LinearSystem260