# Zulip Chat Archive

## 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