subst

Stream: general

[Sebastien Gouezel]

Consider the following lemma, saying that two equal functions taking two equal arguments give the same result, but in a somewhat dependent setting:

lemma dependent_helper {F G : Σn:ℕ, (fin n → fin n → ℤ)} (h : F = G) {i j: ℕ}
  {iF : i < F.1} {iG : i < G.1} {jF : j < F.1} {jG : j < G.1} :
  F.2 ⟨i, iF⟩ ⟨j, jF⟩ = G.2 ⟨i, iG⟩ ⟨j, jG⟩ :=
by subst h; refl

This works fine. However, exactly in the same situation but in the middle of a more complicated proof (see https://github.com/sgouezel/mathlib/blob/a734bb06a1c4e833cfd1bad117eb0b500f26e929/src/topology/metric_space/gromov_hausdorff.lean#L1287 -- here, hpq is F p = F q), this proof does not work. I proved the above helper lemma separately and applied it, and this solves my problem, but I would like to understand what is going on and why the substitution does not work in the middle of my big proof. I did not find anything about this in TPIL, would you have some pointer?

[Chris Hughes]

subst only works when one side is a local constant. It's a very annoying problem.

[Kevin Buzzard]

Did you try erw?

[Sebastien Gouezel]

erw hpq gives

rewrite tactic failed, motive is not type correct
nested exception message:
check failed, application type mismatch (use 'set_option trace.check true' for additional details)

[Kevin Buzzard]

oh yeah, that's a familiar message.

[Sebastien Gouezel]

The trace is

[check] application type mismatch at
  ⟨i, hip⟩
argument type
  i < N p
expected type
  i < _a.fst

[Kevin Buzzard]

Welcome to dependent type theory.

[Kevin Buzzard]

If it's any consolation, I was singing your praises at a talk in Cambridge last Wednesday.

[Sebastien Gouezel]

Most of the time, I manage to avoid any real use of dependent types, but for this proof this is really the way to go. Anyway, at the end it works!

[Sebastien Gouezel]

It's always a consolation to be praised :)

[Kevin Buzzard]

In front of Larry Paulson no less.

[Sebastien Gouezel]

The proof I am writing is something that is completely impossible in Isabelle. But don't tell that to Larry.

[Kevin Buzzard]

He would just tell you that you were wrong.

[Kevin Buzzard]

He asked one of his post-docs on Wednesday to go away and formalise schemes in Isabelle. My impression from talking to people here was that this was not such a good idea, but I couldn't really tell her this in front of him. But back to your question -- I would be interested to know whether the problem you're now running into are solvable in some sensible way or whether there are genuine issues. I have been banging on here for a while now about how it's really annoying that you can't painlessly rewrite along "canonical isomorphisms", but you have an explicit example where rewriting an equality is painful and it would be interesting to see what the experts have to say about it. My understanding is that this sort of problem does not occur in Isabelle because there are no dependent types, but I really am still a novice in these matters.

[Kevin Buzzard]

I would like to be able to deduce that a topological spaceY is compact, given that X is compact and that X and Y are homeomorphic, using a rewrite; this seems to be genuinely technically difficult though. But you're rewriting an equality so it should be easier. Maybe someone will just come along and tell you how to do it using the tactics we have.

[Sebastien Gouezel]

I completely agree with you that transferring structure is not solved yet in a satisfactory way. For a simple example, assume that a space X is such that, for all e>0, the space X can be covered by finitely many balls or radius e such that any 5 of them have empty intersection. If Y is isometric to X, then the same property holds obviously for Y, but proving this in Lean would be utterly tedious now...

[Kevin Buzzard]

example (GH_space : Type)
(p q : GH_space)
(N : GH_space → ℕ)
(i j : ℕ)
(hip : i < N p)
(hiq : i < N q)
(hjp : j < N p)
(hjq : j < N q)
(P : Π p : GH_space, fin (N p) → fin (N p) → ℤ)
: 2 + 2 = 5 :=
begin

let F : GH_space → (Σ (n : ℕ), fin n → fin n → ℤ) :=
  λ p, (⟨N p, λ a b, P p a b⟩ : (Σ (n : ℕ), fin n → fin n → ℤ)),
have hpq : F p = F q := sorry, -- implies N p = N q
have : (F p).snd ⟨i, hip⟩ ⟨j, hjp⟩ = (F q).snd ⟨i, hiq⟩ ⟨j, hjq⟩,
  sorry, -- this is Sebastien's question.
  sorry -- 2 + 2 isn't 5
end

This is some sort of minimised version of Sebastien's question. The hypothesis that F p = F q implies that N p = N q, so the goal (F p).snd ⟨i, hip⟩ ⟨j, hjp⟩ = (F q).snd ⟨i, hiq⟩ ⟨j, hjq⟩ is a simultaneous rewrite of hpq and its corollaries all in one go. The question is whether there's a slick way to remove that last-but-one sorry. I had to make a random auxiliary goal otherwise there would be lets in the goal.

[Kevin Buzzard]

As for the balls of radius e question, whenever I came up with an example @Mario Carneiro would point out that the rewrite I wanted was a consequence of a stronger statement which I was going to have to prove anyway, so I should stop moaning. I've always been looking for a real-world example which he couldn't counter in this way. Maybe this is one? Just to be clear -- I believe that @Simon Hudon and @Johannes Hölzl talked about this problem in Amsterdam last month and my impression is that there actually _is_ some kind of solution in dependent type theory to problems of this nature, but all I know is that it involves transfer or something. As I'm sure you know, the problem is that it's not true that an arbitrary statement about X is also true for Y, e.g. if P Z := Z = X then P X is true but P Y is not. The point is that any statement about metric spaces which a mathematician finds reasonable will be true for X iff it's true for Y. I have not given up hope that there will one day be a tactic which solves this sort of problem.

[Mario Carneiro]

Here's my solution to that problem in situ:

import tactic.interactive
example (GH_space : Type)
(p q : GH_space)
(N : GH_space → ℕ)
(i j : ℕ)
(hip : i < N p)
(hiq : i < N q)
(hjp : j < N p)
(hjq : j < N q)
(P : Π p : GH_space, fin (N p) → fin (N p) → ℤ)
: 2 + 2 = 5 :=
begin
  let F : GH_space → (Σ (n : ℕ), fin n → fin n → ℤ) :=
    λ p, (⟨N p, λ a b, P p a b⟩ : (Σ (n : ℕ), fin n → fin n → ℤ)),
  have hpq : F p = F q := sorry, -- implies N p = N q
  have : (F p).snd ⟨i, hip⟩ ⟨j, hjp⟩ = (F q).snd ⟨i, hiq⟩ ⟨j, hjq⟩,
  { revert hiq hjq,
    change N q with (F q).1,
    generalize_hyp : F q = f at hpq ⊢, subst f,
    intros, refl },
  sorry -- 2 + 2 isn't 5
end

[Sebastien Gouezel]

Very instructive, thanks. From what I understand, you do what is needed to replace F q by a constant f, then substitute and now it is allowed. Is this limitation of subst, that it can only work with local constants, something that is unavoidable and will stay like that forever, or is there a possibility that it could be improved at some point?

[Mario Carneiro]

it's a fundamental part of how it works. subst can only apply when one side is a variable, but the benefit is that it will never have a "not type correct" error, because it eliminates the variable in the equality completely using eq.rec

[Mario Carneiro]

In this case, we have a combination of generalize_hyp and subst that is essentially what rw does - conceivably with some rearrangement I could also use rw to do this trick

[Mario Carneiro]

ah yes, this also works

  { revert hiq hjq,
    change N q with (F q).1,
    rw ← hpq, intros, refl },

[Sebastien Gouezel]

ah yes, this also works

  { revert hiq hjq,
    change N q with (F q).1,
    rw ← hpq, intros, refl },

This example must be oversimplified, as this does not work in my real-world example. But the previous solution based on subst works fine.