5.2. T1 — What is measured: objects, sorts, and parts🔗

Start at the bottom-left of the square, with the things that bear the properties. The oscillator has two bodies and three springs, so two object types, each a plain inductive with decidable equality:

inductive Body | A | B
deriving DecidableEq, Repr

inductive Spring | kA | kC | kB
deriving DecidableEq, Repr

Each object has a sort, the kind of system it is: a point mass, a linear spring, and, for the pair the bodies and springs make up, a coupled oscillator pair. Two further sorts, springs in parallel and springs in series, are declared now and earn their keep in T6:

def bodyS : SortOfSystem := ⟨"point mass"⟩
def springS : SortOfSystem := ⟨"linear spring"⟩
def pairS : SortOfSystem := ⟨"coupled oscillator pair"⟩
def parallelS : SortOfSystem := ⟨"springs in parallel"⟩
def seriesS : SortOfSystem := ⟨"springs in series"⟩

The left edge of the square, instantiated by, is one instance per object type, declared once and never derived:

/-- Left edge, *instantiated by*: every body is a point mass. Declared once, never derived. -/
instance : Sorted Body := ⟨fun _ => bodyS⟩
/-- Every spring is a linear spring. -/
instance : Sorted Spring := ⟨fun _ => springS⟩

A designation is what lets a quantity name its bearer in words; injectivity is decided:

/-- Designation (so `toIndividualProperty` can name a body); injectivity by `decide`. -/
instance : Designated Body where
  designation
    | .A => ⟨"body A"⟩
    | .B => ⟨"body B"⟩
  designation_inj {x y} h := byx:Bodyy:Bodyh:(match x with
  | Body.A => { id := "body A" }
  | Body.B => { id := "body B" }) =
  match y with
  | Body.A => { id := "body A" }
  | Body.B => { id := "body B" }⊢ x = y
    cases xAy:Bodyh:(match Body.A with
  | Body.A => { id := "body A" }
  | Body.B => { id := "body B" }) =
  match y with
  | Body.A => { id := "body A" }
  | Body.B => { id := "body B" }⊢ Body.A = yBy:Bodyh:(match Body.B with
  | Body.A => { id := "body A" }
  | Body.B => { id := "body B" }) =
  match y with
  | Body.A => { id := "body A" }
  | Body.B => { id := "body B" }⊢ Body.B = y <;>Ay:Bodyh:(match Body.A with
  | Body.A => { id := "body A" }
  | Body.B => { id := "body B" }) =
  match y with
  | Body.A => { id := "body A" }
  | Body.B => { id := "body B" }⊢ Body.A = yBy:Bodyh:(match Body.B with
  | Body.A => { id := "body A" }
  | Body.B => { id := "body B" }) =
  match y with
  | Body.A => { id := "body A" }
  | Body.B => { id := "body B" }⊢ Body.B = y cases yB.Ah:(match Body.B with
  | Body.A => { id := "body A" }
  | Body.B => { id := "body B" }) =
  match Body.A with
  | Body.A => { id := "body A" }
  | Body.B => { id := "body B" }⊢ Body.B = Body.AB.Bh:(match Body.B with
  | Body.A => { id := "body A" }
  | Body.B => { id := "body B" }) =
  match Body.B with
  | Body.A => { id := "body A" }
  | Body.B => { id := "body B" }⊢ Body.B = Body.B <;>A.Ah:(match Body.A with
  | Body.A => { id := "body A" }
  | Body.B => { id := "body B" }) =
  match Body.A with
  | Body.A => { id := "body A" }
  | Body.B => { id := "body B" }⊢ Body.A = Body.AA.Bh:(match Body.A with
  | Body.A => { id := "body A" }
  | Body.B => { id := "body B" }) =
  match Body.B with
  | Body.A => { id := "body A" }
  | Body.B => { id := "body B" }⊢ Body.A = Body.BB.Ah:(match Body.B with
  | Body.A => { id := "body A" }
  | Body.B => { id := "body B" }) =
  match Body.A with
  | Body.A => { id := "body A" }
  | Body.B => { id := "body B" }⊢ Body.B = Body.AB.Bh:(match Body.B with
  | Body.A => { id := "body A" }
  | Body.B => { id := "body B" }) =
  match Body.B with
  | Body.A => { id := "body A" }
  | Body.B => { id := "body B" }⊢ Body.B = Body.B first | rflAll goals completed! 🐙 | exact absurd (System.mk.inj h) (byh:(match Body.B with
  | Body.A => { id := "body A" }
  | Body.B => { id := "body B" }) =
  match Body.A with
  | Body.A => { id := "body A" }
  | Body.B => { id := "body B" }⊢ ¬"body B" = "body A" decideAll goals completed! 🐙)

instance : Designated Spring where
  designation
    | .kA => ⟨"spring A"⟩
    | .kC => ⟨"spring C"⟩
    | .kB => ⟨"spring B"⟩
  designation_inj {x y} h := byx:Springy:Springh:(match x with
  | Spring.kA => { id := "spring A" }
  | Spring.kC => { id := "spring C" }
  | Spring.kB => { id := "spring B" }) =
  match y with
  | Spring.kA => { id := "spring A" }
  | Spring.kC => { id := "spring C" }
  | Spring.kB => { id := "spring B" }⊢ x = y
    cases xkAy:Springh:(match Spring.kA with
  | Spring.kA => { id := "spring A" }
  | Spring.kC => { id := "spring C" }
  | Spring.kB => { id := "spring B" }) =
  match y with
  | Spring.kA => { id := "spring A" }
  | Spring.kC => { id := "spring C" }
  | Spring.kB => { id := "spring B" }⊢ Spring.kA = ykCy:Springh:(match Spring.kC with
  | Spring.kA => { id := "spring A" }
  | Spring.kC => { id := "spring C" }
  | Spring.kB => { id := "spring B" }) =
  match y with
  | Spring.kA => { id := "spring A" }
  | Spring.kC => { id := "spring C" }
  | Spring.kB => { id := "spring B" }⊢ Spring.kC = ykBy:Springh:(match Spring.kB with
  | Spring.kA => { id := "spring A" }
  | Spring.kC => { id := "spring C" }
  | Spring.kB => { id := "spring B" }) =
  match y with
  | Spring.kA => { id := "spring A" }
  | Spring.kC => { id := "spring C" }
  | Spring.kB => { id := "spring B" }⊢ Spring.kB = y <;>kAy:Springh:(match Spring.kA with
  | Spring.kA => { id := "spring A" }
  | Spring.kC => { id := "spring C" }
  | Spring.kB => { id := "spring B" }) =
  match y with
  | Spring.kA => { id := "spring A" }
  | Spring.kC => { id := "spring C" }
  | Spring.kB => { id := "spring B" }⊢ Spring.kA = ykCy:Springh:(match Spring.kC with
  | Spring.kA => { id := "spring A" }
  | Spring.kC => { id := "spring C" }
  | Spring.kB => { id := "spring B" }) =
  match y with
  | Spring.kA => { id := "spring A" }
  | Spring.kC => { id := "spring C" }
  | Spring.kB => { id := "spring B" }⊢ Spring.kC = ykBy:Springh:(match Spring.kB with
  | Spring.kA => { id := "spring A" }
  | Spring.kC => { id := "spring C" }
  | Spring.kB => { id := "spring B" }) =
  match y with
  | Spring.kA => { id := "spring A" }
  | Spring.kC => { id := "spring C" }
  | Spring.kB => { id := "spring B" }⊢ Spring.kB = y cases ykB.kAh:(match Spring.kB with
  | Spring.kA => { id := "spring A" }
  | Spring.kC => { id := "spring C" }
  | Spring.kB => { id := "spring B" }) =
  match Spring.kA with
  | Spring.kA => { id := "spring A" }
  | Spring.kC => { id := "spring C" }
  | Spring.kB => { id := "spring B" }⊢ Spring.kB = Spring.kAkB.kCh:(match Spring.kB with
  | Spring.kA => { id := "spring A" }
  | Spring.kC => { id := "spring C" }
  | Spring.kB => { id := "spring B" }) =
  match Spring.kC with
  | Spring.kA => { id := "spring A" }
  | Spring.kC => { id := "spring C" }
  | Spring.kB => { id := "spring B" }⊢ Spring.kB = Spring.kCkB.kBh:(match Spring.kB with
  | Spring.kA => { id := "spring A" }
  | Spring.kC => { id := "spring C" }
  | Spring.kB => { id := "spring B" }) =
  match Spring.kB with
  | Spring.kA => { id := "spring A" }
  | Spring.kC => { id := "spring C" }
  | Spring.kB => { id := "spring B" }⊢ Spring.kB = Spring.kB <;>kA.kAh:(match Spring.kA with
  | Spring.kA => { id := "spring A" }
  | Spring.kC => { id := "spring C" }
  | Spring.kB => { id := "spring B" }) =
  match Spring.kA with
  | Spring.kA => { id := "spring A" }
  | Spring.kC => { id := "spring C" }
  | Spring.kB => { id := "spring B" }⊢ Spring.kA = Spring.kAkA.kCh:(match Spring.kA with
  | Spring.kA => { id := "spring A" }
  | Spring.kC => { id := "spring C" }
  | Spring.kB => { id := "spring B" }) =
  match Spring.kC with
  | Spring.kA => { id := "spring A" }
  | Spring.kC => { id := "spring C" }
  | Spring.kB => { id := "spring B" }⊢ Spring.kA = Spring.kCkA.kBh:(match Spring.kA with
  | Spring.kA => { id := "spring A" }
  | Spring.kC => { id := "spring C" }
  | Spring.kB => { id := "spring B" }) =
  match Spring.kB with
  | Spring.kA => { id := "spring A" }
  | Spring.kC => { id := "spring C" }
  | Spring.kB => { id := "spring B" }⊢ Spring.kA = Spring.kBkC.kAh:(match Spring.kC with
  | Spring.kA => { id := "spring A" }
  | Spring.kC => { id := "spring C" }
  | Spring.kB => { id := "spring B" }) =
  match Spring.kA with
  | Spring.kA => { id := "spring A" }
  | Spring.kC => { id := "spring C" }
  | Spring.kB => { id := "spring B" }⊢ Spring.kC = Spring.kAkC.kCh:(match Spring.kC with
  | Spring.kA => { id := "spring A" }
  | Spring.kC => { id := "spring C" }
  | Spring.kB => { id := "spring B" }) =
  match Spring.kC with
  | Spring.kA => { id := "spring A" }
  | Spring.kC => { id := "spring C" }
  | Spring.kB => { id := "spring B" }⊢ Spring.kC = Spring.kCkC.kBh:(match Spring.kC with
  | Spring.kA => { id := "spring A" }
  | Spring.kC => { id := "spring C" }
  | Spring.kB => { id := "spring B" }) =
  match Spring.kB with
  | Spring.kA => { id := "spring A" }
  | Spring.kC => { id := "spring C" }
  | Spring.kB => { id := "spring B" }⊢ Spring.kC = Spring.kBkB.kAh:(match Spring.kB with
  | Spring.kA => { id := "spring A" }
  | Spring.kC => { id := "spring C" }
  | Spring.kB => { id := "spring B" }) =
  match Spring.kA with
  | Spring.kA => { id := "spring A" }
  | Spring.kC => { id := "spring C" }
  | Spring.kB => { id := "spring B" }⊢ Spring.kB = Spring.kAkB.kCh:(match Spring.kB with
  | Spring.kA => { id := "spring A" }
  | Spring.kC => { id := "spring C" }
  | Spring.kB => { id := "spring B" }) =
  match Spring.kC with
  | Spring.kA => { id := "spring A" }
  | Spring.kC => { id := "spring C" }
  | Spring.kB => { id := "spring B" }⊢ Spring.kB = Spring.kCkB.kBh:(match Spring.kB with
  | Spring.kA => { id := "spring A" }
  | Spring.kC => { id := "spring C" }
  | Spring.kB => { id := "spring B" }) =
  match Spring.kB with
  | Spring.kA => { id := "spring A" }
  | Spring.kC => { id := "spring C" }
  | Spring.kB => { id := "spring B" }⊢ Spring.kB = Spring.kB first | rflAll goals completed! 🐙 | exact absurd (System.mk.inj h) (byh:(match Spring.kB with
  | Spring.kA => { id := "spring A" }
  | Spring.kC => { id := "spring C" }
  | Spring.kB => { id := "spring B" }) =
  match Spring.kC with
  | Spring.kA => { id := "spring A" }
  | Spring.kC => { id := "spring C" }
  | Spring.kB => { id := "spring B" }⊢ ¬"spring B" = "spring C" decideAll goals completed! 🐙)

The quantities written over the objects are one line each. They are the individual quantities T3 explains, and they are needed now so that the refusals below have something to refuse; the kinds massK and stiffnessK they name are T2's subject:

def mA : IndividualQuantity Body.A massK Int := ⟨3⟩
def mB : IndividualQuantity Body.B massK Int := ⟨5⟩
def kA : IndividualQuantity Spring.kA stiffnessK Int := ⟨6⟩
def kC : IndividualQuantity Spring.kC stiffnessK Int := ⟨2⟩
def kB : IndividualQuantity Spring.kB stiffnessK Int := ⟨3⟩

What this buys is checked by the compiler: every body is a point mass by rfl, the two bodies share a sort, and a quantity reads back its two indices as an individual property that names the kind and the bearer:

/-- Left edge: a substance instantiates its kind (sort). -/
example : Sorted.sortOf Body.A = bodyS := rfl
example : Sorted.sortOf Spring.kC = springS := rfl
theorem bodies_one_sort : Sorted.sortOf Body.A = Sorted.sortOf Body.B := rfl

/-- Bottom + right edges: the two type indices of a mode, read back as an individual
property — the mode characterizes body A and instantiates mass. -/
example : mA.toIndividualProperty = ⟨massK, ⟨"body A"⟩⟩ := rfl

What it refuses is the first value proposition of the object axis. The masses of two bodies do not add, nor the stiffnesses of two springs, and B's mass cannot stand in for A's, each with the error that says why — an error that names the object:

/- Bottom edge: masses of two bodies do not add. -/
/--
error: Application type mismatch: The argument
  mB
has type
  IndividualQuantity Body.B massK Int
but is expected to have type
  IndividualQuantity Body.A massK Int
in the application
  IndividualQuantity.add ⋯ mA mB
-/
#guard_msgs in
example := IndividualQuantity.add DifferenceKind.ofScale mA mB
/- Nor stiffnesses of two springs. -/
/--
error: Application type mismatch: The argument
  kC
has type
  IndividualQuantity Spring.kC stiffnessK Int
but is expected to have type
  IndividualQuantity Spring.kA stiffnessK Int
in the application
  IndividualQuantity.add ⋯ kA kC
-/
#guard_msgs in
example := IndividualQuantity.add DifferenceKind.ofScale kA kC
/- B's mass cannot stand in for A's. -/
/--
error: Type mismatch
  mB
has type
  IndividualQuantity Body.B massK Int
but is expected to have type
  IndividualQuantity Body.A massK Int
-/
#guard_msgs in
example : IndividualQuantity Body.A massK Int := mB

The case study types the same oscillator with nominal objects, a name such as ⟨"oscillator A"⟩ and no sort. One line shows what that costs. dedicatedFor, T2's construct, reaches the catalogue entry dedicated to an object through the object's sort, and an object with no sort has no way up; the first line of the error is the whole story:

/-! The case study's objects are nominal `System`s and know no sort, so they cannot reach
the top edge through `dedicatedFor` at all — the refusal that says why the tutorial needs
an object type with a `Sorted` instance. -/
/--
error: failed to synthesize instance of type class
  Sorted System

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
-/
#guard_msgs in
example := massK.dedicatedFor (⟨"oscillator A"⟩ : Object) whole

A dimension-and-units library has no object axis at all: mA + mB is a sum of two masses and nothing more can be said. Tagging the object into the type by hand recovers the refusal and loses the sum (T0's third row); declaring the object as an index of the quantity keeps both, as T3 shows.

Reference: The object type for Sorted, Designated, and the individual quantity; Foundations for the square this part walks.