Debug "mutually inductive types compiled to invalid ..."

Stream: new members

[Kevin Sullivan]

In a separate thread I'm discussing the design of an affine space library. That's the context for this question. I need a mutually inductive definition of several types. I'm getting the following error message:

mutually inductive types compiled to invalid basic inductive type
nested exception message:
universe level of type_of(arg #4) of 'apoint._mut_.mk_0' is too big for the corresponding inductive datatypeLean

The question is a basic one: how to debug this problem? It looks like I need to look at the compiled definition. Is that right? In that case, how? Or if it's obvious what's going wrong, I'd be happy simply to know the solution to this blocking problem, at least for right now. I'm not posting the code at this point, hoping for insights without doing that, until the code's in better shape.

[Kenny Lau]

use Type* instead of manually calculating the universe

[Mario Carneiro]

could you show the definition?

[Mario Carneiro]

or at least the inductive itself, MWE not required

[Kevin Sullivan]

or at least the inductive itself, MWE not required

mutual inductive apoint, avector, aframe

with apoint :
    Π (s : space), Type
| mk :                      -- any point
    Π {s : space}
      (d : ℕ) [has_zero (fin d)]
      (K: Type) [discrete_field K]
      (coords : { c : tuple (d+1) K // c.nth 0 = 1 }),
      apoint s
| mk_std :
    Π { s : space }         -- std point, (1, 0, 0, ..., 0)
      (d : ℕ) [has_zero (fin d)]
      (K: Type) [discrete_field K],
      apoint s

with avector :
    Π (s : space), Type
| mk :
    Π {s : space}
      (d : ℕ) [has_zero (fin d)]
      (K: Type) [discrete_field K]
      (coords : { c : tuple (d+1) K // c.nth 0 = 1 }),
      avector s     -- was: aframe s → scalar → avector s
| mk_std :
    Π { s : space }         -- std vector(0, 0, 0, ..., 0)
      (d : ℕ) [has_zero (fin d)]
      (K: Type) [discrete_field K],
      avector s

with aframe :
    Π (s : space), Type
| mk : Π { s : space }, apoint s → avector s → aframe s
| mk_std : Π { s : space }, aframe s -- not yet complete

If I use Type*, I get an error at the end about inductive types having to live in the same universe.

[Kevin Sullivan]

It has a few things that need fixing, but this should give the idea.

[Floris van Doorn]

Change the types of apoint, avector and aframe to space → Type (u+1)(this is the same as Π (s : space), Type (u+1)), and change the types of all Ks to Type u. If you don't like to worry about universe levels, you can set u to 0 (so only use Type - which is Type 0 - and Type 1).

[Floris van Doorn]

Here is a simplified version of your MWE:

universe variable u
constant space : Type

mutual inductive apoint, avector, aframe

with apoint :
    Π (s : space), Type (u+1)
| mk :                      -- any point
    Π {s : space}
      (d : ℕ) [has_zero (fin d)]
      (K: Type u) [discrete_field K],
      apoint s
| mk_std :
    Π { s : space }         -- std point, (1, 0, 0, ..., 0)
      (d : ℕ) [has_zero (fin d)]
      (K: Type u) [discrete_field K],
      apoint s

with avector :
    Π (s : space), Type (u+1)
| mk :
    Π {s : space}
      (d : ℕ) [has_zero (fin d)]
      (K: Type u) [discrete_field K],
      avector s     -- was: aframe s → scalar → avector s
| mk_std :
    Π { s : space }         -- std vector(0, 0, 0, ..., 0)
      (d : ℕ) [has_zero (fin d)]
      (K: Type u) [discrete_field K],
      avector s

with aframe :
    Π (s : space), Type (u+1)
| mk : Π { s : space }, apoint s → avector s → aframe s
| mk_std : Π { s : space }, aframe s -- not yet complete

[Kenny Lau]

here is a simplified simplified version:

universe u

mutual inductive apoint, aframe
with apoint : Type (u+1)
| mk : Type u → apoint
with aframe : Type (u+1)
| mk : Type u → apoint → aframe

[Kevin Sullivan]

I'm coming back to this. I'm having another problem knowing what an error message involving mutually defined types means. The context: I'm defining an affine space abstract data type. An affine space has points, vectors, frames. Points and vectors have coordinates and a frame. A frame has a point (origin) and a set of vectors (basis).

The problem, in the logic below, is that if (as I need to do) I change the type of affine_frame.mk, from taking a point and a single vector to taking a point and a list of vectors (representing a basis), then I get the following error at the top of the inductive definition:

nested occurrence 'list.{1} (affine_vector s)' contains variables that are not parameters

What variables are meant here? What have I done wrong? And how might I fix it? Thank you!

Here's the self-contained code (which I'll be putting in an open GitHub repo once it works).

import algebra.module
import data.vector

-- for testing
import data.real.basic
set_option pp.notation false


-- UNDERLYING REPRESENTATION

--universe u

/-
Background: the "vector" type in the Lean standard library
is a type whose values are really just tuples. We define
a "tuple" type polymorphic as the type of tuples of length
n over values of a type, K.
-/
def tuple
    (n : ℕ)
    (K : Type) :=
        vector K n

-- testing
def aTuple : tuple 3 ℝ := ⟨[2,1,-1], rfl⟩
def aTuple' : tuple 1 ℝ := ⟨[2], rfl⟩

/-
With K a discrete field with zero and one values,
we define a function to return tuples of length n
over K with all elements equal to the field's zero
element.
-/
def mk_zero_tuple :
    ∀ (n : ℕ)
    (K : Type)
    [f : discrete_field K]
    [z : has_zero K],
        vector K n
| 0 K f z := vector.nil
| (nat.succ n') K f z := vector.cons (z.zero) (@mk_zero_tuple n' K f z)

-- testing
def aReal3ZeroTuple : tuple 3 ℝ :=
    subtype.mk [0,0,0] rfl
def aReal4ZeroTuple : tuple 4 ℝ :=
    subtype.mk [0,0,0,0] rfl


structure space : Type 1 :=
mk ::
(name : string)
(dim : ℕ)
(field: Type)
[isField : discrete_field field]
[the_zero : has_zero field]
[the_one : has_one field]

-- testing

def time : space :=         -- non-computable
    space.mk "time" 1 ℝ

def geometry : space :=
    space.mk "geometry" 3 ℝ

/-
We define affine point, vector, and frame types.
The space to which each such object belongs is a
part of its type. The definitions are mutually
recursive, because point and a vector are defined
partly in terms of a frame (in terms of which its
coordinates are interpreted), and a frame in turn
is defined by a point (its origin) and a tuple of
vectors (comprising a basis for its vector space).
-/

mutual inductive affine_point, affine_vector, affine_frame
with affine_point : space → Type 1
    | mk :
        Π { s : space },
        affine_frame s →
        tuple s.dim s.field  → affine_point s
    | mk_std :
        Π { s : space },         -- std point, (1, 0, 0, ..., 0) wrt std_frame
        affine_point s
with affine_vector : space → Type 1
    | mk :
        Π {s : space},
        affine_frame s →
        tuple s.dim s.field →
        affine_vector s
    | mk_std :
        Π { s : space },        -- std vector(0, 0, 0, ..., 0) wrt std_frame
        affine_vector s
with affine_frame : space → Type 1
    | mk : Π { s : space }, affine_point s → list (affine_vector s) → affine_frame s -- stub
    | mk_std : Π { s : space },  affine_frame s  -- std frame

I've tried with a universe variable, u, substituting Type (u+1), and also Type (u+2), for Type 1 where it appears in the mutual definition, to no avail. Thanks, all, for your ongoing help with this stuff.

Kevin

[Kevin Buzzard]

I've done a bunch of maths in Lean and I have never once had to use a mutually inductive type. I know nothing about them and this is why I can't help. Is there any way of just taking things apart and defining some normal inductive types?

[Scott Morrison]

@Ben Leedom and I were faced with a mutual inductive definition when trying to define the product of CW complexes. Lean couldn't cope, so we unrolled it into a single inductive definition of a complicated structure (something like "product of CW complexes along with inclusions of products of the k- and l- skeleta of the factors")

[Chris Hughes]

I've done a bunch of maths in Lean and I have never once had to use a mutually inductive type. I know nothing about them and this is why I can't help. Is there any way of just taking things apart and defining some normal inductive types?

Yes. That is how Lean does it underneath, but it doesn't do it very well. There is a good way of doing it.

[Andrew Ashworth]

This looks difficult to debug, since you are using mutually inductive types with nested inductive types in affine_frame. I am no expert in these things - the only way I would know how to get to the bottom of the error is to unroll the definition into non-mutual/nested inductive types. Someone had a similar problem awhile back, here is the link to the conversation: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Induction/near/160350668.

[Kevin Sullivan]

I've done a bunch of maths in Lean and I have never once had to use a mutually inductive type. I know nothing about them and this is why I can't help. Is there any way of just taking things apart and defining some normal inductive types?

Yes. That is how Lean does it underneath, but it doesn't do it very well. There is a good way of doing it.

I guess my first question is whether my definition violates a fundamental constraint (e.g., positivity), or whether what I'm seeing is the just that Lean isn't yet capable of dealing with such a definition. My second question is, where do I go for a complete definition of the unrolling method?

[Kevin Sullivan]

To help, I've abstracted from the affine space details and have reduced the problem instance to a very short piece of code. I give three versions here of almost the same definition. The first two work; the third is borked and isolates the problem.

(1) Works: Two non-polymorphic mutually inductive types, the second taking a list of the first as an argument.
(2) Works: Two polymorphic mutually inductive types, the second taking only a single instance of the first as an argument.
(3) Borked: Two polymorphic mutually inductive types, the second taking a list of the first as an argument.

-- a type argument
axiom S : Type

-- #1 [WORKS] (Note: s arguments are ignored)
mutual inductive X, Y
with X : Type
    | mk : Π (s : S), Y → X
with Y : Type
    | mk' : Π (s : S), list X  → Y

-- #2 [WORKS]
mutual inductive A, B
with A : S → Type
    | mk : Π (s : S), B s → A s
with B : S → Type
    | mk' : Π (s : S), A s → B s

-- #3 [BORKED]
mutual inductive P, Q
with P : S → Type
    | mk : Π (s : S), Q s → P s
with Q : S → Type
    | mk' : Π (s : S), list (P s) → Q s    -- putting list in front of (P s) breaks it

I should know the answer to this but I don't: Will Lean print out the unrolled definitions of P, Q?

[Kevin Sullivan]

The example that break Lean works in Coq. This suggests that the problem is in Lean, not in definition. Or maybe I don't understand a subtle difference between the logics of Lean and Coq, respectively.

--[BORKED IN LEAN]
mutual inductive P, Q
with P : S → Type
    | mk : Π (s : S), Q s → P s
with Q : S → Type
    | mk' : Π (s : S), list (P s) → Q s    -- putting list in front of (P s) breaks it

(* WORKS IN COQ *)
Axiom S : Set.
Inductive P : S -> Set :=
| mk : forall (s : S), Q s -> P s
with Q : S -> Set :=
| mk' : forall (s : S), list (P s) -> Q s.

[Chris Hughes]

You can see what your inductive type actually is with #print affine_point

[Kevin Sullivan]

I've done a bunch of maths in Lean and I have never once had to use a mutually inductive type.

Kevin B: Thanks. This is a good place for mutual inductive definitions. A point in an affine space can be given coordinates in terms of a frame. A vector can be given coordinates in the same way. A frame, in turn, comprises a point and a set of vectors constituting a basis for the vector space. These points and vectors, being points and vectors, in turn have coordinates in terms of some (possibly other) frame. It all bottoms out with the concept of a standard frame with a standard origin point and standard basis vectors. What this structure naturally supports is the situation where you have chains of changes in basis/coordinate-systems. This kind of situation arises frequently in domains like computer graphics and robotics.

[Kevin Sullivan]

You can see what your inductive type actually is with #print affine_point

Ok, that's easy. Thank you.

[Kevin Sullivan]

You can see what your inductive type actually is with #print affine_point

Ok, that's easy. Thank you.

Except that the definition isn't accepted, so affine_point isn't defined. Any way to see what Lean is trying to reduce the definition to?

[Chris Hughes]

This is mutual and nested, because you have list (affine_vector s) as a constructor. That might be the problem.

[Andrew Ashworth]

this example is given in https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html#mutual-and-nested-inductive-types

[Kevin Sullivan]

This is mutual and nested, because you have list (affine_vector s) as a constructor. That might be the problem.

Example #1 is mutual and nested but not polymorphic, and it works. Example #2 is mutual and polymorphic but not nested, and it works. Example #3 is mutual, polymorphic, and nested. That's where it breaks. Yet it works in Coq.

[Andrew Ashworth]

as a quick fix, you could try to redo it giving the specialization of list explicitly as another type

[Andrew Ashworth]

mutual inductive P, Q, Q_list  (S : Type u) (s : S)
with P : S → Type u
| mk : Q s → P s
with Q : S → Type u
| mk' : list (P s) → Q s
with Q_list : Type u
| nil {} :  Q_list
| cons : Q s → Q_list → Q_list

[Andrew Ashworth]

I have no idea if this translates exactly to the semantics of what you want, though

[Andrew Ashworth]

interesting, your original example doesn't even need that

variable S : Type
mutual inductive P, Q (s : S)
with P : S → Type
| mk : Q s → P s
with Q : S → Type
| mk' : list (P s) → Q s

[Kevin Sullivan]

this example is given in https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html#mutual-and-nested-inductive-types

Andrew, thank you. Your pointer set me off in a direction that seems to be working. The problem appears to be (thus this thread being in the beginners section) that I had the type arguments in the wrong place.

Here are type definitions that at least so far seem good. I have yet to prove that instances are actually affine spaces, formalized as torsors over vector spaces. I might run into problems when I try to do that, but at least I now have a path to try.

Here are type definitions, followed in the second code block by working "test code".

import algebra.module
import data.vector

universe u

/-
Tuples of length n over a type, K
-/
def tuple
    (n : ℕ)
    (K : Type u) : Type u :=
        vector K n

/-
A type, space, values of which we will use to
uniquely identify a given affine space, while
characterizing its key attributes, namely its
dimension and the field over in terms of which
scalars and coordinate tuples are defined. Such
a space has a name, allowing us to distinguish
spaces with the same field and dimensionality.
-/
structure space
(dim : ℕ)
(K: Type)
[isField : discrete_field K]
[theZero : has_zero K]
[theOne : has_one K]
: Type :=
mk :: (name : string)

/-
A mutual inductive definition of affine point,
vector, and frame types. A point in an affine space
is given coordinates in terms of a frame. A vector
can be given coordinates in the same way. A frame,
in turn, has a point, its origin, and a sequence of
vectors, constituting a basis for the vector space.
We are not yet specifying or enforcing the linear
independence of the vectors. The points and vectors
that make up a frame, being points and vectors, in
turn have coordinates expressed in terms of some
(possible other) frame. The recursion bottoms out
with at a standard frame with a standard origin and
standard basis vectors. This structure naturally
supports situation where you have chains of changes
in basis/coordinate-systems. This kind of situation
arises frequently in domains like computer graphics
and robotics.
-/
mutual inductive affine_point, affine_vector, affine_frame
    { d : ℕ }
    { K: Type }
    { f : discrete_field K }
    { z : has_zero K }
    { o : has_one K }
    (s : space d K)
with affine_point : Type 1
| mk_std : affine_point
| mk : affine_frame → tuple d K → affine_point
with affine_vector : Type 1
| mk_std : affine_vector
| mk : affine_frame → tuple d K → affine_vector
with affine_frame : Type 1
| mk_std : affine_frame
| mk : affine_point → (list affine_vector) → affine_frame

Here's code giving the types a little test run.

import .affine_space_new
import data.real.basic


-- Test tuple type
def oneTuple : tuple 1 ℝ := ⟨ [2], rfl ⟩
def aTuple : tuple 3 ℝ := ⟨[2,1,-1], rfl⟩
def aTuple' : tuple 1 ℝ := ⟨[2], rfl⟩
def aReal3ZeroTuple : tuple 3 ℝ :=
    subtype.mk [0,0,0] rfl
def aReal4ZeroTuple : tuple 4 ℝ :=
    ⟨ [0,0,0,0], rfl⟩


-- Test space type
def time : space 1 ℝ :=      -- non-computable
    space.mk 1 ℝ "time"
def geometry : space 3 ℝ :=  -- non-computable
    space.mk 3 ℝ "geometry"
#check time
#check space 1 real


/-
Test affine point, vector, frame types.
Time as an affine space.
-/

-- standard frame
def timeFrame1 : affine_frame time :=
    affine_frame.mk_std time

-- standard point (t = 0)
def timePoint1 : affine_point time :=
    affine_point.mk_std time

-- standard vector (interpret as 1 minute duration)
def timeVector1 : affine_vector time :=
    affine_vector.mk_std time

-- point at 60 min (1 hr) wrt to std frame
def timePoint2 : affine_point time :=
    affine_point.mk timeFrame1 ⟨ [60], rfl ⟩

-- a vector of length 1hr wrt std frame
def timeVector2 : affine_vector time :=
    affine_vector.mk timeFrame1 ⟨ [60], rfl ⟩

-- new frame, origin at 1 hour and unit 1 hr, wrt std frame
def timeFrame2 : affine_frame time :=
    affine_frame.mk timePoint2 [timeVector2]

-- Point @ 24 hours from (t = one hour) wrt std frame
def timePoint3 := affine_point.mk timeFrame2 ⟨ [24], rfl ⟩

/-
Test affine point, vector, frame types.
3D geometry as an affine space.
-/

-- std frame
def geomFrame1 : affine_frame geometry :=
    affine_frame.mk_std geometry

-- std origin
def geomPoint1 : affine_point geometry :=
    affine_point.mk_std geometry

-- std vector [one of them, anyway, need to enhance type]
def geomVector1 : affine_vector geometry :=
    affine_vector.mk_std geometry

-- new point at [1,1,1] wrt std frame
def geomPoint2 : affine_point geometry :=
    affine_point.mk geomFrame1 ⟨ [1,1,1], rfl ⟩

-- new vector at [-1,1,2] wrt std frame
def geomVector2 : affine_vector geometry :=
    affine_vector.mk geomFrame1 ⟨ [-1,1,2], rfl ⟩

-- new frame with new basis vectors (need to add constraints here)
def geomFrame2 : affine_frame geometry :=
    affine_frame.mk geomPoint2 [geomVector1, geomVector2, geomVector1]

[Mario Carneiro]

These work in Coq because the Coq kernel is crazy permissive

[Mario Carneiro]

You can achieve a similar behavior in lean by putting meta in front of the definition

[Scott Morrison]

How close does "crazy permissive" come to "I worry that we'll have another proof of false someday"?

[Mario Carneiro]

There is no paper proof that we can't prove false

[Reid Barton]

I've done a bunch of maths in Lean and I have never once had to use a mutually inductive type.

Kevin B: Thanks. This is a good place for mutual inductive definitions. A point in an affine space can be given coordinates in terms of a frame. A vector can be given coordinates in the same way. A frame, in turn, comprises a point and a set of vectors constituting a basis for the vector space. These points and vectors, being points and vectors, in turn have coordinates in terms of some (possibly other) frame. It all bottoms out with the concept of a standard frame with a standard origin point and standard basis vectors. What this structure naturally supports is the situation where you have chains of changes in basis/coordinate-systems. This kind of situation arises frequently in domains like computer graphics and robotics.

The mathematician's concepts involved here don't need inductive types at all. I'm not sure what exactly you are trying to model. but I suspect you're making things more complicated than they need to be.

[Reid Barton]

The same point of an affine space can be described using coordinates in terms of two different frames. Put differently, points described using two different frames can be equal. But in your inductive types, affine_points involving different frames are certainly not equal.

[Reid Barton]

What you are trying to build looks more like a type of expressions which can be evaluated to yield a point of an affine space, according to certain rules of formation

[Kevin Sullivan]

What you are trying to build looks more like a type of expressions which can be evaluated to yield a point of an affine space, according to certain rules of formation

Reid, Thank you. What I'm trying to build is a library for algebra/geometry: more specifically one that accommodates different representations of the same points and vectors, in coordinates expressed with respect to different frames. The idea will be that, as far as the user is concerned, coordinates are mostly hidden/abstracted behind information hiding interfaces once objects are built, so so the user will be able to write expressions involving these objects independent of the frames in terms of which their underlying coordinate-based representations are expressed. The Lean terms representing a given mathematical point or vector with respect to different frames won't be equal, but they'll be equivalent as witnessed by their equality under change-of-frame operations that render their underlying coordinate-based representations with respect to a "standard frame" for a given space.

It's also important in my application in any case that we distinguish the types of points and vectors that "live in different spaces", even if the dimensions and underlying field(s) are the same. In this way, we'll be able to represent, e.g., time and distance along some line both as 1-d real affine spaces, but the points and vectors in these spaces won't be compatible with respect to affine space operations. E.g., it won't make sense to subtract a point in time from a position in space.

More generally, I'm being driven by a desire to hew as closely as I can to an elegant and traditional mathematical formalization, while also accommodating the demands of my application, which, for now, I can characterize as wanting to model mathematical physics in a type-safe manner.

Kevin

[Reid Barton]

I don't understand why you want to use inductive types for this. It sounds like the standard math approach would be suitable. Have a type that represents a (possibly abstract) affine space, and functions that, given a frame for an affine space, convert between points of the space and their coordinate representations in that frame.

[Reid Barton]

With the inductive type you're basically making the function (frame on an affine space, coordinates in that frame) -> point in affine space into a constructor, but it can just be an ordinary function.

[Reid Barton]

I think the sort of design for affine spaces that was being discussed a while ago would be a lot simpler.

[Kevin Sullivan]

I think the sort of design for affine spaces that was being discussed a while ago would be a lot simpler.

I will think about that. At least in the application I have in mind, I need to be able to capture situations where, say, a point, p1, is represented in terms of a frame f1=(p2,(v_2_i)], where p2 and the vectors are expressed in terms of a frame f2=[p3,(v_3_i)], etc., to arbitrary depths. The mutual inductive type seems a reasonable way to get to that. I'm not controverting what you're saying. I'm listening and will think about it.

Which other conversation did you have in mind?

[Mario Carneiro]

One way to encode this is to say that a frame is an affine isomorphism from k^n to the affine space A (not assumed to have any coordinatization). A coordinatized affine space is one with a designated frame, called the "standard frame"; for example k^n itself is coordinatized. A coordinatized affine space is also a vector space. Given a vector in k^n and an invertible matrix in k^(n x n), we can define an affine automorphism of k^n and so transform one frame to another via precomposition. And of course the frame itself provides functions for getting the point with given coordinates (the forward map) and getting the coordinates of a point (the reverse map).

[Mario Carneiro]

As for distinguishing different types of affine spaces that have the same dimension and field, this is easy to do using a newtype. If you define

structure time := (val : real)
structure space := (val : real)

then time and space are isomorphic to real, but all three types are distinct and you can't confuse one for the other.

[Reid Barton]

I think the sort of design for affine spaces that was being discussed a while ago would be a lot simpler.

I will think about that. At least in the application I have in mind, I need to be able to capture situations where, say, a point, p1, is represented in terms of a frame f1=(p2,(v_2_i)], where p2 and the vectors are expressed in terms of a frame f2=[p3,(v_3_i)], etc., to arbitrary depths. The mutual inductive type seems a reasonable way to get to that. I'm not controverting what you're saying. I'm listening and will think about it.

The Lean expression language itself has this kind of nested structure. You can represent this by a tree of function applications.
Unless you later need access to the particular structure of that tree, you don't need to make those functions be constructors of inductive types.
More likely you want two different such representations of the same point to be equal.

[Kevin Sullivan]

One way to encode this is to say that a frame is an affine isomorphism from k^n to the affine space A (not assumed to have any coordinatization). A coordinatized affine space is one with a designated frame, called the "standard frame"; for example k^n itself is coordinatized.

Yes,:where a frame comprises a point (the origin for that frame) and a basis for the vector space, which along with the origin induces a coordinatization on both the points and vectors of the affine space. I have, at least so far, chosen to represent such isomorphisms by packaging ("hidden") frames and coordinates within each point and vector object. That might change at some point, but for now I'm trying to get at least to a first "working" specification. I think Reid is telling me I don't need to do all this work. I don't yet clearly see a much easier alternative that does everything I want. But I'm still open to a possible v.2 of this still nascent library.

A coordinatized affine space is also a vector space.

I'm formalizing an affine space as a torsor (of "points") over a vector space (of "translations" or "vectors", i.e., differences between points). Speaking in object-oriented terms, I'd say that an affine space "has" a vector space as a component rather than that is "is" a vector space. Not a deep point, but things are represented this way in the emerging library. See the definitions (not yet adequately developed) at the end of the file.

Given a vector in k^n and an invertible matrix in k^(n x n), we can define an affine automorphism of k^n and so transform one frame to another via precomposition.

Yes. I haven't yet specified the concept of an affine transform, but it is necessary and TBD. If you check out the material that I will post to GitHub, you'll see that this concept is missing. It's needed to enable proofs of affine-space properties for the coordinate tuples that I'm using to represent points and vectors. The idea will be that operations such as vector-vector addition will work by changes-of-frames of given arguments to standard frames followed by component-wise addition of coordinates, yielding results expressed in terms of the standard frame.

And of course the frame itself provides functions for getting the point with given coordinates (the forward map) and getting the coordinates of a point (the reverse map).

Yes. I've defined numerous functions to access different elements. More to come.

[Kevin Sullivan]

The code is here. Issues and suggestions are welcome.

https://github.com/kevinsullivan/phys/blob/master/src/algebra/affine_space.lean

[Mario Carneiro]

It is very easy to define an affine map and an affine isomorphism, probably easier than dealing with points and vectors as you are currently doing

[Mario Carneiro]

When I say a coordinatized affine space is a vector space, I mean that because a coordinatized affine space has a designated point (the one with coordinate 0), you can construct a vector space structure on top of the affine space (using differences from the designated point)

[Kevin Sullivan]

It is very easy to define an affine map and an affine isomorphism, probably easier than dealing with points and vectors as you are currently doing

I will put this on the eval-to-do list for a possible refactoring.

[Kevin Sullivan]

When I say a coordinatized affine space is a vector space, I mean that because a coordinatized affine space has a designated point (the one with coordinate 0), you can construct a vector space structure on top of the affine space (using differences from the designated point)

Yes.