Zulip Chat Archive

Stream: new members

Topic: Providing proof for type equality


view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Jun 05 2020 at 17:21):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Reid Barton (Jun 05 2020 at 17:51):

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

view this post on Zulip 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.

view this post on Zulip Reid Barton (Jun 05 2020 at 17:53):

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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Yakov Pechersky (Jun 05 2020 at 17:55):

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

view this post on Zulip 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)?

view this post on Zulip 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

view this post on Zulip Reid Barton (Jun 05 2020 at 17:57):

Ohhh your definition is still wrong, in another way.

view this post on Zulip Reid Barton (Jun 05 2020 at 17:57):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 07 2020 at 02:03):

or \t

view this post on Zulip Mario Carneiro (Jun 07 2020 at 02:04):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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