## Stream: new members

### Topic: Providing proof for type equality

#### Yakov Pechersky (Jun 05 2020 at 17:20):

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 (Jun 05 2020 at 17:21):

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

#### Yakov Pechersky (Jun 05 2020 at 17:32):

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
exact append (extend xs y) ys
end


#### Reid Barton (Jun 05 2020 at 17:34):

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

#### Yakov Pechersky (Jun 05 2020 at 17:49):

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 (Jun 05 2020 at 17:51):

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 (Jun 05 2020 at 17:51):

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

#### Reid Barton (Jun 05 2020 at 17:51):

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 (Jun 05 2020 at 17:53):

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

#### Johan Commelin (Jun 05 2020 at 17:54):

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

#### Yakov Pechersky (Jun 05 2020 at 17:54):

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 (Jun 05 2020 at 17:55):

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

#### Reid Barton (Jun 05 2020 at 17:56):

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 (Jun 05 2020 at 17:57):

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

#### Reid Barton (Jun 05 2020 at 17:57):

Ohhh your definition is still wrong, in another way.

#### Reid Barton (Jun 05 2020 at 17:57):

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

#### Reid Barton (Jun 05 2020 at 17:59):

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 (Jun 05 2020 at 19:22):

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

#### Yakov Pechersky (Jun 05 2020 at 19:35):

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 (Jun 05 2020 at 19:41):

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 (Jun 07 2020 at 02:02):

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 (Jun 07 2020 at 02:03):

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

#### Mario Carneiro (Jun 07 2020 at 02:03):

or \t

#### Mario Carneiro (Jun 07 2020 at 02:04):

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

#### Mario Carneiro (Jun 07 2020 at 02:07):

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


#### Mario Carneiro (Jun 07 2020 at 02:07):

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

#### Mario Carneiro (Jun 07 2020 at 02:09):
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