| ← Permutations example | Index | Next: Why bundle proofs with data? → |
Because intGroup is a term of type Group Int, its
fields can be projected out exactly as in Chapter 2:
#eval intGroup.op 3 4 -- 7
#eval intGroup.id -- 0
#eval intGroup.inv 5 -- -5
#check intGroup.assoc -- a proof, for every a b c, of associativity
Mathematical reading. The projections recover the individual components
of the structure: intGroup.op is the multiplication $\cdot$ (so
intGroup.op 3 4 is $3 + 4 = 7$ in $\mathbb{Z}$), intGroup.id is $e = 0$,
and intGroup.inv is $(-)^{-1} = -(-)$. The key point is that
intGroup.assoc projects out a proof: it is the element of $\forall
a,b,c,\ (a\cdot b)\cdot c = a\cdot(b\cdot c)$ that was supplied when building
the group. Data-fields and proof-fields are accessed the same way because,
in the dependent-pair view (a structure is, underneath, exactly this kind
of dependent pair), both are just coordinates of the same tuple.
Mathlib equivalent. There is no intGroup.op 3 4-style field access to
write at all. Once Int is known to be an AddCommGroup, the ordinary
+/0/- notations already resolve to that instance’s operations
directly:
#eval (3 : Int) + 4
#eval (0 : Int)
#eval -(5 : Int)
#check (add_assoc : ∀ a b c : Int, (a + b) + c = a + (b + c))
This is the same contrast as Section 3: the book’s intGroup.op/.id/.inv are
projections out of a bundle built by hand, while Mathlib’s +/0/
- are notation that the typeclass system has already wired to the right
instance. The underlying “which AddCommGroup instance is
this?” bookkeeping remains invisible unless sought out (for example, with #print).
| ← Permutations example | Index | Next: Why bundle proofs with data? → |