Providing proof for type equality

Stream: new members

[Yakov Pechersky]

Continuing with TPIL exercises. I couldn't find in the documentation the way to provide proof of add_comm, add_assoc to fix the error I get from my definitions.

equation type mismatch, term
  append (extend xs y) ys
has type
  vector α (n + 1 + m)
but is expected to have type
  vector α (n + (m + 1))

niverse u

inductive vector (α : Type u) : ℕ → Type u
| nil {} : vector 0
| cons   : Π {n}, α → vector n → vector (n+1)

namespace vector
local notation h :: t := cons h t

def extend {α : Type} : Π {n}, vector α n -> α -> vector α (n+1)
| 0     nil        x := x :: nil
| (n+1) (t::ts)    x := t :: (extend ts x)

def append {α : Type} : Π {n m}, vector α n -> vector α m -> vector α (n+m)
| 0     0     nil     nil     := nil
| (n+1) 0     xs      nil     := xs
| n     (m+1) xs      (y::ys) := append (extend xs y) ys

end vector

[Yakov Pechersky]

I guess changing | n (1+m) .... works. Nope, that doesn't.

[Yakov Pechersky]

This works, but I am not sure how to avoid tactic mode for it.

def append {α : Type} : Π {n m}, vector α n -> vector α m -> vector α (n+m)
| 0     0     nil     nil     := nil
| (n+1) 0     xs      nil     := xs
| n     (m+1) xs      (y::ys) :=
begin
rw [add_comm m, <-add_assoc],
exact append (extend xs y) ys
end

[Reid Barton]

Avoid the extra case distinction (the first case is redundant), then induct on whichever list matches the variable that + inducts on.

[Yakov Pechersky]

I'm not sure what you mean by the variable that + inducts on. If I induct on n, then I have to prove that vector (0+m) ~ vector m, and if I induct on m, I have to prove that vector (n + (m + 1)) ~ vector (n + 1 + m)

[Yakov Pechersky]

The TPIL exercise hints that I'll need an auxiliary function to define append, so it seemed to me that extend would be the auxiliary. But I guess I could define append (x::xs) ys = x::(append xs ys), which doesn't use extend. Still needs something to prove the type equality.

[Reid Barton]

Oh, your definition is also backwards (doesn't match +).

[Reid Barton]

Yakov Pechersky said:

But I guess I could define append (x::xs) ys = x::(append xs ys)

Yes, I assumed you were doing this without looking closely.

[Reid Barton]

I might be confused about this, since I never remember how + is defined.

[Johan Commelin]

Well, you just take a apples, and then b apples, and you put them together, and then you have a + b apples.

[Yakov Pechersky]

This works, but now I wonder what the auxiliary function was:

def append {α : Type} : Π {n m}, vector α n -> vector α m -> vector α (m+n)
| 0 m     nil     ys := ys
| (n+1) m (x::xs) ys := x::(@append n m xs ys)

[Yakov Pechersky]

I can see how my original definition was O(n^2).

[Reid Barton]

I guess the point is you end up with m+n this way, not the more obvious n+m. Maybe your original approach was correct. Why do you say you have to prove vector (n + (m + 1)) ~ vector (n + 1 + m)?

[Reid Barton]

it looks like you would have to prove n + (m + 1) = (n + m) + 1, but that one is by definition

[Reid Barton]

Ohhh your definition is still wrong, in another way.

[Reid Barton]

Well, not wrong, but not adapted to the type you want to give it.

[Reid Barton]

If you want to get vector α n -> vector α m -> vector α (n+m), then you should think about the definition of n+m and how you can make a recursive definition that matches it. You do need extend.

[Yakov Pechersky]

The definition of n+m is succ ^ m (n). So I need to extend xs m times.

[Yakov Pechersky]

Reid Barton said:

Well, not wrong, but not adapted to the type you want to give it.

You're talking about the definition of append that uses extend, correct?

[Yakov Pechersky]

I think I am making this more complicated than necessary. Using a combo of reverse and extend lets me keep n -> m -> (n+m)

def extend {α : Type} : Π {n}, vector α n -> α -> vector α (n+1)
| 0     nil        x := x :: nil
| (n+1) (t::ts)    x := t :: (extend ts x)

def reverse {α : Type} : Π {n}, vector α n -> vector α n
| 0     nil     := nil
| (n+1) (t::ts) := extend (reverse ts) t

def append {α : Type} : Π {n m}, vector α n -> vector α m -> vector α (m+n)
| 0 m     nil     ys := ys
| (n+1) m (x::xs) ys := x::(@append n m xs ys)

def append' {α : Type} : Π {n m}, vector α n -> vector α m -> vector α (n+m)
| n 0     xs     nil := xs
| n (m+1) xs     ys  := match reverse ys with (y::ys) := extend (append' xs ys) y end

[Yakov Pechersky]

In any case, let's say I have a wrong definition for append like the following (even though I don't see what's obviously wrong):

def append'' {α : Type} : Π {n m}, vector α n -> vector α m -> vector α (n+m)
| n 0     xs     nil     := xs
| n (m+1) xs     (y::ys) := append'' (extend xs y) ys
-- equation type mismatch, term
--   append'' (extend xs y) ys
-- has type
--   vector α (n + 1 + m)
-- but is expected to have type
--   vector α (n + (m + 1))

Right now I get an error. I can prove the type equality in tactic mode. How would one do this in the equation compiler?

[Mario Carneiro]

the equation compiler itself won't help, but you can use cast to coerce the value across the type equality

[Mario Carneiro]

or \t

[Mario Carneiro]

Usually if you need to do this rw is more reliable though

[Mario Carneiro]

def append'' {α : Type} : Π {n m}, vector α n -> vector α m -> vector α (n+m)
| n 0     xs     nil     := xs
| n (m+1) xs     (y::ys) :=
  by rw ← nat.succ_add_eq_succ_add; exact append'' (extend xs y) ys

[Mario Carneiro]

def append'' {α : Type} : Π {n m}, vector α n -> vector α m -> vector α (n+m)
| n 0     xs     nil     := xs
| n (m+1) xs     (y::ys) :=
  cast (by rw nat.succ_add_eq_succ_add) (append'' (extend xs y) ys)

[Mario Carneiro]

That said, these are the foothills of DTT hell so you should really consider other options that don't involve cast or equivalent mechanisms if you can at all avoid it