equality of types

Stream: new members

[Greg Price]

I have the feeling that I don't fully understand yet the boundaries of how I can use the fact that two types are equal. Here's a MWE:

universe u

def X : Type u := sorry
def q : X → Prop := sorry
def p : Prop := sorry

def W : Type u := X
lemma W_eq_X : W = X := rfl

lemma exists_X_eq_p : (∃ (x : X), q x) = p := sorry

example : (∃ (x : W), q x) = p :=
begin
  -- This fails:
  /-
    rewrite tactic failed, motive is not type correct
      λ (_a : Type ?), (∃ (x : W), q x) = p = ((∃ (x : _a), q x) = p)
    state:
    ⊢ (∃ (x : W), q x) = p
  -/
  rw W_eq_X,
  exact exists_X_eq_p,
end

example : (∃ (x : W), q x) = p :=
begin
  -- But this works, and does basically the same thing:
  transitivity (∃ (x : X), q x), refl,
  exact exists_X_eq_p,
end

[Greg Price]

Here the types W and X are the same. But if I try to use that equality with rw / rewrite, I get an error.

But then on the other hand I can accomplish exactly the same thing -- that is, make exactly the same change to what the goal is, effectively replacing W with X -- by using transitivity with an appropriate argument, and then refl.

[Greg Price]

One piece of this which I definitely don't understand is the error message: "motive is not type correct". I've seen "motive" mentioned in the documentation, in the context of explaining rec / rec_on for inductive types. So one specific question is: is this "motive" from a rec call that rewrite is using internally?

I don't really have a firm grasp of what it means there either, though, and would be grateful for any explanation of that.

Then: which piece of this is the "motive" that is not type correct? Is it that whole equality on the next line of the message? And what is the _a : Type ? in that equality?

[Greg Price]

Stepping back from the specifics of the error message, I think I have an idea -- thanks to the process of producing this MWE -- of what may be the reason why the rw W_eq_X isn't accepted while the transitivity …, refl is.

I think perhaps the point is something to do with Lean wanting to verify that the types are not just equal, but definitionally equal, before accepting one as a substitute for another when it's being used in the type of some other variable. So the transitivity just introduces a new goal, which is fine, an equality between two expressions of type Prop, which is fine. And then refl asks Lean to look and see that in fact the types tucked inside, along with everything else, are definitionally equal and to discharge that goal.

[Greg Price]

But in rw W_eq_X, I'm asking Lean to use the fact that those types are merely equal, as previously proven, and merely-equal isn't good enough.

[Greg Price]

It happens that indeed that equality is a definitional equality -- in fact it was proven in the first place with just rfl. But the fact which I'm giving rw to try to use is the fact of mere equality.

[Greg Price]

If that's right, then my practical question is: let's imagine that in a real development, W is some definition and X is the details of its construction, and I want to be able to refer to the thing by its name, W, in the statements of theorems, but then in their proofs I want to unpack it into its implementation X in order to get at the details.

I'd like to take the fact that W equals X, and package it up into some simp lemmas: maybe one for W = X itself, or maybe several for things like projections out of it. Or even non-simp lemmas -- but just lemmas that I can refer to by name, so I can pass them to rw or simp to specify what to do with some expression involving W.

And that works great, except that with the tools I've learned how to use so far, this doesn't seem to be possible where W is being used in a type. What are ways that people handle this?

[Yury G. Kudryashov]

If W = X is a rfl, then dsimp should be able to apply it anywhere, incl. inside types.

[Yury G. Kudryashov]

(though we don't use this style in mathlib, so I'm not completely sure that it'll work in all cases)

[Greg Price]

Yury G. Kudryashov said:

If W = X is a rfl, then dsimp should be able to apply it anywhere, incl. inside types.

Oh very interesting, thanks!

[Greg Price]

If this style isn't used in mathlib, what are the alternative idioms that are used instead?

Or perhaps the answer is that it depends a lot on the details -- in that case I can try to expand the example to be concrete enough for an answer.

[Greg Price]

Trying out dsimp in my example, this works great:

example : (∃ (x : W), q x) = p :=
begin
  dsimp only [W_eq_X],
  exact exists_X_eq_p,
end

[Eric Wieser]

I think subst W_eq_X would work too

[Mario Carneiro]

dsimp is fine; also dunfold and delta will do definitional rewriting

[Mario Carneiro]

The "motive is not type correct" error is because rewrite needs to generalize the variable in the position of W/X, and this variable is not defeq to either W or X, meaning that things that depend on it, like Exists in this case, will fail to type check

[Kevin Buzzard]

This is a limitation of Lean's tactics, rather than a limitation of dependent type theory, right?

[Greg Price]

subst fails but for an unrelated reason:

example : (∃ (x : W), q x) = p :=
begin
  /-
  subst tactic failed, given expression is not a local constant
  state:
  ⊢ (∃ (x : W), q x) = p
  -/
  subst W_eq_X,
  exact exists_X_eq_p,
end

[Greg Price]

I think it's saying that it will only work if the thing being replaced, here W, is a local constant i.e. from the local context. I'm pretty sure I've run into this in situations where that applied, too, so that may also come in handy.

[Mario Carneiro]

Right, at least one side of the equality has to be a variable for subst to apply

[Greg Price]

Mario Carneiro said:

dsimp is fine; also dunfold and delta will do definitional rewriting

These also work, thanks! I had not seen those tactics before.

example : (∃ (x : W), q x) = p :=
begin
  dunfold W,
  exact exists_X_eq_p,
end

example : (∃ (x : W), q x) = p :=
begin
  delta W,
  exact exists_X_eq_p,
end

[Mario Carneiro]

you shouldn't use delta under normal circumstances, it's a very low level tactic

[Mario Carneiro]

I'm not actually sure what the difference between dsimp and dunfold is; they have slightly different configuration options but both call in to the same underlying rewriting mechanism

[Mario Carneiro]

(the syntax is a bit different)

[Greg Price]

The docstring for delta says:

Similar to dunfold, but performs a raw delta reduction, rather than using an equation associated with the defined constants.

The term "delta reduction" is new to me. The web tells me it means evaluating a primitive function on given arguments -- a lot like a beta reduction, it seems, but with a primitive rather than an explicit lambda expression.

[Mario Carneiro]

delta reduction is replacing a constant defined with def with the body of the definition, i.e. the original meaning of "true by definition"

[Mario Carneiro]

this is what makes def different from, say, constant

[Greg Price]

Ah interesting, that's a bit different from the definition I'd found (in a non-Lean context), then -- though clearly related

[Greg Price]

What is it that dunfold does, or unfold for that matter? The docstring for dunfold points at unfold, and the latter says it uses "equational lemmas associated with the definition".

[Greg Price]

But I'm not sure what an "equational lemma" is. Is it just a lemma which has an equality as its conclusion?

[Mario Carneiro]

It's a set of automatically generated lemmas created with every definition made using the equation compiler

[Greg Price]

Hmm, I see, and:

/-
W : Type u
W.equations._eqn_1 : W = X
-/
#print prefix W

[Greg Price]

So I guess that's the equational lemma there.

[Mario Carneiro]

def foo := 1

#print foo.equations._eqn_1
-- @[_refl_lemma]
-- theorem ALC.foo.equations._eqn_1 : foo = 1 :=
-- eq.refl foo

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

#print prefix bar.equations
-- bar.equations._eqn_1 : bar 0 = 1
-- bar.equations._eqn_2 : ∀ (n : ℕ), bar (n + 1) = 0

[Mario Carneiro]

yes, that's right

[Mario Carneiro]

The idea is that when "unfolding" bar, you would much rather see those equations than the actual definition:

#print bar._main
-- def bar._main : ℕ → ℕ :=
-- λ (ᾰ : ℕ), ᾰ.cases_on (id_rhs ℕ 1) (λ (ᾰ : ℕ), id_rhs ℕ 0)

Using delta bar will give you this

[Greg Price]

Hmm, yeah, I see.

[Greg Price]

Mario Carneiro said:

The "motive is not type correct" error is because rewrite needs to generalize the variable in the position of W/X, and this variable is not defeq to either W or X, meaning that things that depend on it, like Exists in this case, will fail to type check

Interesting. So rewrite in order to operate needs the thing it's rewriting to be generalizable -- meaning I guess that it can be replaced with anything with the same type, and the expression as a whole would still type-check. So in particular this is unlikely to work with anything that's used in the type of something else.

Whereas dsimp, dunfold, delta, and perhaps subst but I haven't tested it, are able to use the more specific identity of what they're substituting in, and the fact that it's defeq to the thing being replaced.

[Mario Carneiro]

subst isn't in the same category of the others, but change also deserves a place on that list. These tactics all change the goal to something definitionally equal, and they do it by basically doing nothing - the next term you give will simply have the changed type, and the kernel will end up being responsible for checking that any type mismatches that arise are correct up to defeq

[Mario Carneiro]

subst is kind of like rw, except it can't fail (assuming the target equality has a variable on one side) because it essentially comes "pre-generalized": the type-correctness of the typing context itself ensures that the operation of the tactic will go without a hitch. You can think of rw (e : a = b) as doing have h : a = b := e, generalize : a = x, subst h, and the generalize step is the one that can possibly fail if there are reasons why some occurrence of a in the context has to be specifically a and not just any term.

[Greg Price]

Very interesting, thanks!

[Greg Price]

Mario Carneiro said:

and they do it by basically doing nothing - the next term you give will simply have the changed type, and the kernel will end up being responsible for checking that any type mismatches that arise are correct up to defeq

This touches on something else I'd like to understand better: what the interface looks like between the kernel, and the machinery on top of it that we interact with when writing proofs.

Does this example translate to the following? We had a goal, which was the expected type of a proof term to stick into the hole we're currently working to fill in our proof-being-written. And then we change the goal, just meaning that we now decide on a different type we're going to use for the proof term we actually write. So then the kernel will be handed a proof term where when it gets to the subterm we're currently writing, it expects one type, but ends up judging it to have another, and it has to check that those types are defeq.

[Mario Carneiro]

That's right

[Mario Carneiro]

Actually, I lied a bit when I said the tactics do nothing; they could validly do nothing to the term under construction but in practice they instead add an identity function to the term, i.e. if the current partial proof term is (_ : T) and you change U then this changes the proof term to (@id U _ : T). The reason for this so that the precise form of the term U is retained in the proof term, and we ensure that the kernel will actually be faced with a defeq goal of the form T = U and not T = V where V is the actual type of whatever you give next. Since definitional equality in lean is not transitive, this can actually impact the type correctness of some terms, but usually it just impacts performance.

[Greg Price]

Ah interesting

[Greg Price]

Mario Carneiro said:

Since definitional equality in lean is not transitive

I'd seen a brief mention of this fact in the docs somewhere. But it looks like this is a rather more detailed discussion, thanks! I'll have to come back and read more later.