Search code examples
lean

Trouble defining a subset of Euclidean space

I am using Lean to try to formalize the notion of a subset of Euclidean space (R^n).

I have tried the following:

import analysis.real

def repeated_prod : ℕ → Type → Type
| 0 s := empty
| 1 s := s
| (n + 1) s := prod s (repeated_prod n s)

structure euclidean_space (n : ℕ) : Type :=
(space : set (repeated_prod n ℝ))

def euclidean_subset (M : Type) := ∃ n : ℕ, (set M) ⊆ (euclidean_space.mk n).space

To try putting in English:

  1. The real numbers (R) are defined in the analysis component of mathlib.
  2. We need to generalize this to k dimensions, so we want the Cartesian product of R with itself any number of times.
  3. repeated_prod allows one to take an arbitrary type and apply the Cartesian product with itself multiple times.
  4. euclidean_space is a specialization to the case of R.
  5. We say that it is a euclidean_subset if there is a some Euclidean space (note: I am trying to avoid the mention of dimension so it is some R^n.) which the set (M) is subset of.

This however gives the error:

euclidean.lean:11:52: error: failed to synthesize type class instance for
M : Type,
n : ℕ
⊢ has_subset Type
euclidean.lean:11:74: error: maximum class-instance resolution depth has been reached (the limit can be increased by setting option 'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option 'trace.class_instances')

Although, I admittedly don't know what the default value for trace.class_instances is, I set it to 10000, it took a bit longer, and the same error message was given, leading to me that it there error message is misleading. Can't seem to find a lot about this language, including the error message I got, any help resolving this error would be appreciated.

Solution

  • You have two compilation errors, although one of them is not visible. Firstly, you can't make a Euclidean space in the way you have tried to, with mk. I suggest changing from a structure to a def for the time being, since your structure only has one field:

    def euclidean_space (n : ℕ) : Type := set (repeated_prod n ℝ)

    Then a euclidean space of dimension n is simply euclidean_space n.

    Secondly, Types are not the same as sets, so that's why Lean can't find an instance for has_subset Type. In the Calculus of Constructions, the type theory that Lean is based on, types can't really be subtypes of other types in the object-oriented programming sense - although you can use "subtype types" and/or coercions to simulate this. So that's what I've changed your code to do - rather than the euclidean_subset predicate trying to check for whether something is a subset, it instead checks that it is a subtype type of a euclidean space n for some n:

    def euclidean_subset (M : Type) := ∃ (n : ℕ) (P : euclidean_space n → Prop), M = subtype P