Dependent hell

Stream: general

[Sebastien Gouezel]

I realize I don't know what to do with dependent types, even the most basic things. Some context: I am building inductively a sequence of more and more complicated metric spaces. In this construction, the metric at each step is constructed from the metric at the previous step, but I am not able to convince Lean of this. I have minimized my problem in the following example:

structure aux : Type 1 :=
(space  : Type)
(metric : metric_space space)

noncomputable def my_def (X : ℕ → Type) [m : ∀n, metric_space (X n)] : ∀n:ℕ, aux
| 0 :=
  { space := X 0,
    metric := by apply_instance }
| (succ n) := by letI : metric_space (my_def n).space := (my_def n).metric; exact
  { space := prod (my_def n).space (X n.succ),
    metric := by apply_instance }

lemma foo (X : ℕ → Type) [m : ∀n, metric_space (X n)] (n : ℕ) : true :=
begin
  letI : ∀k, metric_space (my_def X k).space := λk, (my_def X k).metric,
  have E : prod (my_def X n).space (X n.succ) = (my_def X n.succ).space,
    by simp [my_def],
  have : ∀x y:(my_def X n).space, ∀z:X n.succ,
    dist (prod.mk x z) (prod.mk y z) = dist (cast E (prod.mk x z)) (cast E (prod.mk y z)) :=
  begin
    assume x y z,
    sorry,
  end,
  trivial
end

Here, aux is a structure containing a Type and a metric structure on it, and my_def constructs inductively new metric spaces, by taking the product of the previous one with X n, so that my_def X (n.succ) = prod (my_def X n) (X n.succ), with the same metric. Of course, I only have equality of types, so if I want to express that the distances are the same I need to use a cast. But then I don't know how to prove that the distances are the same, while this is precisely what the definition of my_def does. Probably I miss the good keywords, or a pointer to the relevant chapter in TPIL (or to some part of the library where this game is played). Any idea?

[Chris Hughes]

If you can make my_def X (n.succ) = prod (my_def X n) (X n.succ) definitional, then you won't need cast.

[Reid Barton]

I don't understand how it's not definitional already

[Rob Lewis]

It is actually definitional.

[Reid Barton]

you can prove E by begin dsimp [my_def], refl end but not by rfl

[Rob Lewis]

You can replace the simp [my_def] with unfold my_def.

[Rob Lewis]

And you don't need the cast Es.

[Chris Hughes]

But isn't this space just Π i : fin n, X n?

[Kevin Buzzard]

fin (n+1) but yes

[Sebastien Gouezel]

Yes, of course, it is just Π i : fin n, X n in this simple example, but in my real use-case, it is something much more complicated.

[Kenny Lau]

oh man, inductive-recursive types

[Kenny Lau]

probably just recurse on a sigma type

[Chris Hughes]

I had this problem with splitting fields. The other thing you can do is define the Type and all the definitions you need to prove everything else in one definition

[Chris Hughes]

This is the type of my definition of splitting fields.

Π {n : ℕ} {α : Type u} [discrete_field α] (f : by exactI polynomial α)
  (hf : by exactI nat_degree f = n), by exactI Σ' (β : Type u) [discrete_field β] (i : α → β)
  [by exactI is_field_hom i], (by exactI splits i f)

[Chris Hughes]

Unfortunately this did give me universe issues defining the map from a splitting field, so I still had to make sure the equation lemmas were definitional, and define the map by unfolding the definition.

[Sebastien Gouezel]

Isn't my definition one single definition? I mean, I only define one function my_def. Or does the fact that it is structure-valued mean that I have two intertwined definitions?

[Sebastien Gouezel]

probably just recurse on a sigma type

Could you elaborate a little bit, please?

[Chris Hughes]

I'm saying define the space and every property you need about the space together.

[Chris Hughes]

Or at least enough properties to deduce everything else.

[Chris Hughes]

With a load of nested Sigmas.

[Reid Barton]

It works better if you don't use the equation compiler

noncomputable def my_def (X : ℕ → Type) [m : ∀n, metric_space (X n)] (n:ℕ) : aux :=
nat.rec_on n
  { space := X 0,
    metric := by apply_instance }
(λ n a,
  { space := prod a.space (X n.succ),
    metric := by letI : metric_space a.space := a.metric; apply_instance })

lemma foo (X : ℕ → Type) [m : ∀n, metric_space (X n)] (n : ℕ) : true :=
begin
  letI : ∀k, metric_space (my_def X k).space := λk, (my_def X k).metric,
  have E : prod (my_def X n).space (X n.succ) = (my_def X n.succ).space := rfl,
  have : ∀x y:(my_def X n).space, ∀z:X n.succ,
    dist (prod.mk x z) (prod.mk y z) = dist (cast E (prod.mk x z)) (cast E (prod.mk y z)) :=
  begin
    assume x y z,
    refl,
  end,
  trivial
end

[Reid Barton]

I think I also ran into this here: https://github.com/rwbarton/lean-homotopy-theory/blob/lean-3.4.2/src/homotopy_theory/topological_spaces/disk_sphere.lean#L11

[Reid Barton]

I don't understand why it matters

[Reid Barton]

Apparently the equation compiler uses something called nat.brec_on

[Chris Hughes]

nat.brec_on usually produces definition stuff.

[Sebastien Gouezel]

Amazing. And it also works in my real use case!

[Kevin Buzzard]

def f : ℕ → ℕ
| 0 := 3
| (n+1) := f n + n

example : f 0 = 3 := rfl
example : f 1 = 3 := rfl
example : f 2 = 4 := rfl

#print f._main -- nat.brec_on stuff

Simple use case with equation compiler still giving me rfl proofs.

[Kevin Buzzard]

So what's the difference in Sebastien's case?

[Kevin Buzzard]

But indeed, replacing my_def in Reid's code with

noncomputable def my_def (X : ℕ → Type) [m : ∀n, metric_space (X n)] : ℕ → aux
| 0 :=
  { space := X 0,
    metric := by apply_instance }
| (n + 1) :=
  { space := prod (my_def n).space (X n.succ),
    metric := by letI : metric_space (my_def n).space := (my_def n).metric; apply_instance }

breaks the rfl proof of E

[Kevin Buzzard]

Complete code in case anyone wants to fiddle

import topology.metric_space.basic

structure aux : Type 1 :=
(space  : Type)
(metric : metric_space space)

-- use nat.rec instead and things are better
noncomputable def my_def (X : ℕ → Type) [m : ∀n, metric_space (X n)] : ℕ → aux
| 0 :=
  { space := X 0,
    metric := by apply_instance }
| (n + 1) :=
  { space := prod (my_def n).space (X n.succ),
    metric := by letI : metric_space (my_def n).space := (my_def n).metric; apply_instance }

lemma foo (X : ℕ → Type) [m : ∀n, metric_space (X n)] (n : ℕ) : true :=
begin
  letI : ∀k, metric_space (my_def X k).space := λk, (my_def X k).metric,
  have E : prod (my_def X n).space (X n.succ) = (my_def X n.succ).space := rfl, -- fails
  have : ∀x y:(my_def X n).space, ∀z:X n.succ,
    dist (prod.mk x z) (prod.mk y z) = dist (cast E (prod.mk x z)) (cast E (prod.mk y z)) :=
  begin
    assume x y z,
    refl,
  end,
  trivial
end

[Kevin Buzzard]

import topology.metric_space.basic

structure aux : Type 1 :=
(space  : Type)
(metric : metric_space space)

noncomputable def my_def (X : ℕ → Type) [m : ∀n, metric_space (X n)] (n:ℕ) : aux :=
nat.rec_on n
  { space := X 0,
    metric := by apply_instance }
(λ n a,
  { space := prod a.space (X n.succ),
    metric := by letI : metric_space a.space := a.metric; apply_instance })

lemma foo (X : ℕ → Type) [m : ∀n, metric_space (X n)] (n : ℕ) : true :=
begin
  letI : ∀k, metric_space (my_def X k).space := λk, (my_def X k).metric,
  have E : prod (my_def X n).space (X n.succ) = (my_def X n.succ).space := rfl, -- works
  have : ∀x y:(my_def X n).space, ∀z:X n.succ,
    dist (prod.mk x z) (prod.mk y z) = dist (cast E (prod.mk x z)) (cast E (prod.mk y z)) :=
  begin
    assume x y z,
    refl,
  end,
  trivial
end

[Mario Carneiro]

why is my_def noncomputable?

[Reid Barton]

because the product metric involves doing something with reals

[Mario Carneiro]

I think the noncomputable marker has something to do with why it doesn't compute. Minimized:

noncomputable def my_def (X : ℕ → Type) : ℕ → Type
| 0 := X 0
| (nat.succ n) := prod (my_def n) (X n.succ)

example (X : ℕ → Type) (n : ℕ) :
  my_def X (nat.succ n) = (my_def X n × X (nat.succ n)) := rfl -- fails

[Mario Carneiro]

If you use my_def._main in place of my_def, it works

[Mario Carneiro]

even though these are defined to be the same

[Mario Carneiro]

@Sebastien Gouezel Is it possible to define the type before putting the metric space structure on it?

[Mario Carneiro]

In the case of my_def at least, the space component does not depend on the metric component so they can be defined in that order rather than as a sigma

[Mario Carneiro]

hm, even my_def X n = my_def._main X n := rfl fails

[Mario Carneiro]

Aha, whnf `(my_def X n) returns my_def X n without unfolding anything

[Mario Carneiro]

I think lean thinks my_def is some kind of irreducible

[Sebastien Gouezel]

In my real use case, the definition is noncomputable because it doesn't work without it :) With the equation compiler, I get the complain

equation compiler failed to generate bytecode for 'auxi._main'
nested exception message:
code generation failed, VM does not have code for 'classical.indefinite_description'

So I need to add noncomputable (even though I am already in a noncomputable theory). With the nat.rec_on version, however, I do not need to add it.

[Sebastien Gouezel]

@Sebastien Gouezel Is it possible to define the type before putting the metric space structure on it?

This would solve all my problems, sure, but this is not possible in my real use case: the definition of the type at step n+1 depends on the metric at step n.

[Kenny Lau]

@Sebastien Gouezel what is this mysterious use case?

[Sebastien Gouezel]

There is an optimal way to glue two metric spaces together, to minimize their Hausdorff distance in the coupling. I have a sequence of metric spaces X n, and I want to build a metric space in which each X n is glued to X (n+1) in the optimal way. Start from Y 0 = X 0. Then glue optimally X 1 to X 0, to get Y 1 (with an isometrically embedded copy of X 1). Then glue the optimal coupling of X 1 and X 2 to Y 1 along the space X 1 that they both contain. This gives you a space Y 2 (with an isometrically embedded copy of X 2). Go on like this to get Y 3, Y 4 and so on. Note that each Y n is isometrically embedded in each Y (n+1). Then take the inductive limit of the Y n, and you get the desired space.

All this is useful to show that the space of all nonempty compact metric spaces (a well behaved metric space, called the Gromov Hausdorff space), is complete: the X n will be a Cauchy sequence in the Gromov Hausdorff space, and I am constructing its limit.

[Mario Carneiro]

Is the gluing a disjoint union or a nondisjoint union or something in between?

[Sebastien Gouezel]

Something in between, and non-explicit: an optimal predistance is constructed on the disjoint union to minimize the Hausdorff distance functional, by applying Arzela-Ascoli to show that a minimizer exists. It satisfies all properties of a distance, except that different points can be at zero distance. Then quotient by the natural equivalence relation "being at zero distance" to get the desired metric space. This is highly noncomputable...

[Mario Carneiro]

So the short story is it's a quotient of a disjoint union of X 0 and X 1

[Kenny Lau]

actually I bet you can make it "computable"

[Mario Carneiro]

I'm not sure if this is better, but you could start with the disjoint union, and construct the equivalence relation and the metric space together in your recursion

[Mario Carneiro]

that way the type itself is set up beforehand

[Mario Carneiro]

Alternatively, maybe we should get into pseudometrics?

[Mario Carneiro]

it occurs to me that we have a lot of natural pseudometric spaces

[Sebastien Gouezel]

I could definitely do everything with premetric spaces. By the way, they are already in mathlib, see topology/metric_space/premetric/. But Reid's trick to avoid the equation compiler and use nat.rec_on works perfectly for me, so I am back on track!

[Patrick Massot]

@Sebastien Gouezel I have two pieces of advice for you: first you could go to https://lean-forward.github.io/lean-together/2019/#videos and watch Reid's talk in Amsterdam. But my main advice is you should walk for 30 meters and talk to @Assia Mahboubi about your problem, and then report back here.

[Sebastien Gouezel]

Are you sure Assia is spending her holidays in the same ski resort? :) But I don't have any problem left, thanks to Reid!