In a previous question I asked about formalizing subsets of Euclidean Spaces I received the following response for how to create n-dimensional Euclidean space:
def euclidean_space (n : ℕ) : Type := set (repeated_prod n ℝ)
And I received the following response for creating a subset of Euclidean space:
def euclidean_subset (M : Type) := ∃ (n : ℕ) (P : euclidean_space n → Prop), M = subtype P
Running through my modified code everything compiled which was great and do believe the answer is (at least, mostly) correct. I wanted to try running some basic checks on the code. In particular, I would expect:
#reduce euclidean_space 2
to give:
ℝ × ℝ
well, it didn't. It timed out. I then proceeded, to try some other sets. I modified euclidean_space to be:
def euclidean_space (n : ℕ) : Type := set (repeated_prod n ℕ)
Although, no longer faithful to it's name, one should expect
#reduce euclidean_space 2
to give:
ℕ × ℕ
well, almost, it gives:
ℕ × ℕ → Prop
Given the result I removed the set call and redefined euclidean_space to be:
def euclidean_space (n : ℕ) : Type := (repeated_prod n ℕ)
which reducing produced the desired result. I then went back and replaced ℕ with ℝ:
def euclidean_space (n : ℕ) : Type := (repeated_prod n ℝ)
euclidean_subset still compiled, however #reduce still gives a timeout using ℝ. Why does ℕ not timeout?
real is a definition, so it will be reduced as well:
def real := @cau_seq.completion.Cauchy ℚ _ _ _ abs _
Actually, it is a complex (no pun intended) definition that probably depends on dozens or hundreds of other definitions. Reducing all of these recursively will take a long time and create some huge and completely unhelpful output.
On the other hand, nat is a parameter-less inductive type. There is nothing to reduce there.