Basic confusion about type inference in exercise

Stream: new members

[mars0i]

Given this definition:

inductive Vect (α : Type u) : Nat → Type u where
   | nil : Vect α 0
   | cons : α → Vect α n → Vect α (n + 1)
deriving Repr

I should be able to define a reverse function using some version of this algorithm (which works, for example, using List):

def Vect.revHelper (xs : Vect a n) (acc : Vect a m) : Vect a (m + n) :=
  match xs with
  | .nil => acc
  | .cons y ys => revHelper ys (.cons y acc)

def Vect.reverse (xs : Vect a n) : Vect a n :=
    Vect.revHelper xs .nil

def ns :=  Vect.cons 2 (Vect.cons 3 Vect.nil)

The context and error on | .cons y ys => revHelper ys (.cons y acc) is:

▶ expected type (38:19-38:45)
a : Type u_1
n m : Nat
xs : Vect a n
acc : Vect a m
n✝ : Nat
y : a
ys : Vect a n✝
⊢ Vect a (m + (n✝ + 1))

▶ 38:29-38:31: error:
application type mismatch
  revHelper ys
argument
  ys
has type
  Vect a n✝ : Type ?u.2269
but is expected to have type
  Vect a (n✝ + 1) : Type ?u.2269

Why does Lean give ys a new length variable n✝ : Nat? Since xs matched on .cons y ys, I would think that Lean would infer that the type of ys is Vect a (n - 1). Why is ys expected to have type Vect a (n✝ + 1) in revHelper ys (.cons y acc)?

[Kyle Miller]

Lean is automatically including n in the match discriminants, like this

def Vect.revHelper (xs : Vect a n) (acc : Vect a m) : Vect a (m + n) :=
  match n, xs with
  | 0, .nil => acc
  | n' + 1, .cons y ys => revHelper ys (.cons y acc)

[Kyle Miller]

It's necessary because xs depends on n, and the value of n needs to change depending on the constructor.

[Kyle Miller]

The error message is a bit confused, since revHelper is using the expected type when elaborating that case.

This shows the issue more clearly:

def Vect.revHelper (xs : Vect a n) (acc : Vect a m) : Vect a (m + n) :=
  match xs with
  | .nil => acc
  | .cons y ys =>
    let res := revHelper ys (.cons y acc)
    res

[Kyle Miller]

type mismatch
  res
has type
  Vect a (m + 1 + n✝) : Type ?u.7554
but is expected to have type
  Vect a (m + (n✝ + 1)) : Type ?u.7554

[Kyle Miller]

The problem is that m + 1 + n✝ and m + (n✝ + 1) are not definitionally equal.

[Kyle Miller]

It's a classic problem working with dependent types. Here's one possibility for working around the issue:

def Vect.cast {m n : Nat} (h : m = n) (v : Vect α m) : Vect α n :=
  h ▸ v

def Vect.revHelper (xs : Vect a n) (acc : Vect a m) : Vect a (m + n) :=
  match xs with
  | .nil => acc
  | .cons y ys =>
    (revHelper ys (.cons y acc)).cast (by rw [Nat.succ_add]; rfl)

[Kyle Miller]

In practice, I think it's much easier working with a subtype instead of a new inductive type.

structure Vect (α : Type u) (n : Nat) where
  elts : List α
  length_eq : elts.length = n

def Vect.reverse (xs : Vect α n) : Vect α n where
  elts := xs.elts.reverse
  length_eq := (List.length_reverse _).trans xs.length_eq

[mars0i]

Thank you @Kyle Miller for such a thorough explanation! This is very helpful.

There are a couple of points I'm not sure I understand, but I'll do some investigation--your answer will help me learn some things I wanted to learn about--and come back here if I can't figure it out.

[mars0i]

After some study, I figured some things out, but I'm still confused about something. Any insight or tips or readings that anyone can suggest would be very welcome.

The h argument to Vect.cast should be a proposition stating an equality. But instead of passing a proposition we pass the result of two tactics, rw and rfl. I'm confused about this role for by, and about how a rewriting tactic has an effect outside of by. It's likely that quite a bit of what I say here won't make sense--because I am confused. :smile: I kind of understand the simple tactic examples using by that I've studied in FPIL and TPIL, although there are more complex tactic examples that I haven't studied.

rw has to act on something--it has to have something to rewrite--correct? But there is nothing to rewrite until it's passed to cast? I'm confused about the fact that the equality proposition that, I guess, is apparently passed to cast, is generated inside a by context, where there is nothing given to rewrite.

I can see that what the lhs of Nat.succ_add evaluates to would match (m + 1) + n✝ in Vect a (m + 1 + n✝) . Then the rhs of Nat.succ_add, with variable substitutions due to matching , would be (m + n✝) + 1. The latter is definitionally equal to m + (n✝ + 1) because of the way that Nat.add is defined. So at a purely intuitive level, I see that succ_add and rfl provide information that could allow one to substitute m + (n✝ + 1) for (m + 1 + n✝), which is the transformation needed.

What's confusing is that cast expects to be passed an equality, and what is passed to it is (by ...), where the ... consists of a rewrite tactic rw [Nat.succ_add], rewriting by substituting one side of succ_add for the other, followed by an equality proof tactic (rfl). I think I'm confused about about what by and tactics do. Or maybe I'm confused by rw. (I did read the rewrite documentation to which rw refers, but that didn't answer these questions.)

[Henrik Böving]

cast expects a proof of some form x = y and you can use a tactic block with by to do that proof, just like any other proof in the Lean world

[mars0i]

Thanks @Henrik Böving. That's a very helpful clarification. Once you state it, it seems obvious, but it wasn't, for me.

So a by block is in some sense a function--not in the way that it evaluates its arguments--but but it accepts arguments and returns a proof.

I'm still confused though about what is happening inside of (by rw [Nat.succ_add]; rfl).

Is there some way to see what proof (by ...) is returning? When I try to run #check on a by block by itself, or try to assign the value to a variable, the error messages I get suggest to me that a by block is only meaningful within the usual contexts in which it is used.

[mars0i]

I see that I can assign the value of a by block to a local variable. This type checks:

def Vect.revHelper (xs : Vect a n) (acc : Vect a m) : Vect a (m + n) :=
  match xs with
  | .nil => acc
  | .cons y ys =>
     let prf := (by rw [Nat.succ_add]; rfl)
     (revHelper ys (.cons y acc)).cast prf

Or I can use have instead of let. But I don't know how to see the value of prf.

[mars0i]

Oh--I see it now. I can see the value of prf in the Infoview window when the cursor is on the last line. (Yayy!) And what's displayed is different with let and have. I'll experiment.

[mars0i]

I understand now that have shows prf's type--what cast needs; let shows its value as well. (Lean is amazing.)

[Kyle Miller]

mars0i said:

Is there some way to see what proof (by ...) is returning?

(by? ...)

[mars0i]

I didn't know about by?. It doesn't seem to do what I wanted, but it does other things that look useful. Thanks @Kyle Miller as well as @Henrik Böving.

[Kyle Miller]

Could you say what you wanted? The message printed by by? shows exactly what proof the by returns.

[mars0i]

If I use

     have prf := (by rw [Nat.succ_add]; rfl)
     (revHelper ys (.cons y acc)).cast prf

then if I place the cursor on prf I see (among other things)

prf : m + 1 + n✝ = m + (n✝ + 1)

which is the equality needed so that cast can perform the needed substitution.

If I use by? rather than by in your original (extremely helpful) suggestion, this code is

def Vect.revHelper (xs : Vect a n) (acc : Vect a m) : Vect a (m + n) :=
  match xs with
  | .nil => acc
  | .cons y ys =>
    (revHelper ys (.cons y acc)).cast (by? rw [Nat.succ_add]; rfl)

If I place the cursor on by?, the Infoview window shows

a : Type ?u.31378
n m : Nat
xs : Vect a n
acc : Vect a m
n✝ : Nat
y : a
ys : Vect a n✝
⊢ ?m.31630 = m + (n✝ + 1)

▶ 151:49-151:61: error:
tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  ?n.succ + ?m
a : Type ?u.31378
n m : Nat
xs : Vect a n
acc : Vect a m
n✝ : Nat
y : a
ys : Vect a n✝
⊢ ?m.31630 = m + (n✝ + 1)

▶ 151:41-151:44: information:
Try this: sorryAx (?m.31630 = m + (n✝ + 1)) true

▶ suggestions:
sorryAx (?_ = m + (n✝ + 1)) true

The sorryAx lines show ... = m + (n✝ + 1), but the lhs of the expression is just a variable in each case, so I don't learn that (by? ...) is returning an equality proof m + 1 + n✝ = m + (n✝ + 1).

Am I using by? the wrong way, or is there some other place I should put the cursor? Maybe there's a configuration option I need to set. I'm using lean.nvim, so maybe there's something turned on by default in VSCode but not in nvim. I can probably turn it on. Or maybe there's another buffer--not Infoview--that I should be looking at?

[Kyle Miller]

The sorryAx means that things are not working correctly with by?. Notice that switching to by? causes the tactic proof to have errors (this is worth reporting).

[mars0i]

OK--I see. Done: #5625