4-MAR-2026

0020

Some thoughts before guitar and bed.

I think I need some work around concurrences, which are groups of concurrent lines.

A frequent headache is managing various appelates of the same line. A set of collinear points induces O(n^2) ‘line throughs’ by picking pairs of their points. All of these lines are geometrically identical; but in the prover, they’re a big ol’ pain in the ass. I’ve been thinking about this in the context of more automation for distinct / collinear, but there are a couple properties of these things that are kind of interesting.

  1. Any subset of a distinct/collinear/concurrent set is distinct/collinear/concurrent – follows from the underlying pairwise equality/inequality
  2. for a ‘negative’ property, like distinct, combining two distinct hypotheses is pretty difficult, it requires M * N proofs, where M and N are the numbers of points in the structure.
  3. for positive properties, it’s often possible to satisfy entry much more easily. Collinear points only need to prove they lie on at two induced lines; Concurrent lines only need to prove they’re equal to any of the other lines in the set.
  4. Concurrency and collinearity are related – all those linethroughs are concurrent, and concurrent lines share the same underlying collinear set.

It’s neat how being forced into hyperformality here makes it really clear to see some of the dualities – theorems have very similar proofs despite the type change, and even the underlying plumbing is really just considering the relationships between points and sets of points.

In any case, the aim is to build some more structures, probably divide up the theory section more, I’m not super happy with the way it’s broken by chapter, I think it’s maybe better to try to further divide up things; I believe there should be a way to re-export from the various files; so that I don’t have to import everything by hand; but to be honest the module system (or import system, not really sure which is which) is a mystery.