## 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
rw [add_comm m, <-add_assoc],
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) :=
by rw ← nat.succ_add_eq_succ_add; exact append'' (extend 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) :=
cast (by rw nat.succ_add_eq_succ_add) (append'' (extend 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

Last updated: May 08 2021 at 04:14 UTC