Type unification question

Stream: new members

[Julia Scheaffer]

I am currently working on a formalizing a stack in Lean, but I am having some trouble convincing Lean that my some of the types are in fact the same. Here are some of the relevant definitions:

/-- A typed heterogeneous stack -/
inductive Stack.{u} : List (Type u) -> Type (u + 1) where
  | nil : Stack []
  | cons {α β}: α -> Stack β -> Stack (α :: β)

infixr:67 "; " => Stack.cons

def Stack.append.{u} {α β : List (Type u)} : Stack α -> Stack β -> Stack (α ++ β)
  | nil, b => b | head; tail, b => head; Stack.append tail b

I would like to try proving that {α : List (Type u)} -> (a : Stack α) -> a.append Stack.nil = a but the compiler complains that Stack (α ++ []) does not match Stack α. Is there a way I can tell lean that these two are the same? (I have proven it's equality) Is the fact that these two types are not judgmentally equal stopping it form working?

[Aaron Liu]

I think you should not be trying to prove that a.append Stack.nil = a

[Aaron Liu]

also have you seen docs#List.TProd

[Julia Scheaffer]

I discovered List.TProd after I wrote this code unfortunately. :sweat_smile:

[Julia Scheaffer]

If I were to rewrite my Stack using List.TProd, for the type family α I think I would want to just use id, right?

[Aaron Liu]

What I did is I wrote a get function

Aaron Liu said:

import Mathlib

def List.TProd.get {ι : Type u} {α : ι → Type v} {l : List ι}
    (t : l.TProd α) (n : Nat) (i : ι) (hi : i ∈ l[n]?) : α i :=
  match l, n, hi with
  | _ :: _, 0, rfl => t.1
  | _ :: _, n + 1, hi => List.TProd.get t.2 n i hi

and then I proved get_append_of_lt and get_append_of_ge

[Julia Scheaffer]

I will try to take that approach instead, thanks. I was hoping to get away with my slightly simpler definition, but TProd will probably end up being better in the long run.

[Julia Scheaffer]

Julia Scheaffer said:

I will try to take that approach instead, thanks. I was hoping to get away with my slightly simpler definition, but TProd will probably end up being better in the long run.

I cannot get my code working with List.TProd today. I might try it again another day with some fresh perspective.

[Julia Scheaffer]

Is it impossible to convince lean that Stack (α ++ []) and Stack α are compatible types like in my first message? If not I will have to do something else to state these theorems :/

[pandaman]

You can lift the pattern to an equality proposition. It's a bit cumbersome, but at least it can avoid dependent pattern match failures.

/-- A typed heterogeneous stack -/
inductive Stack.{u} : List (Type u) -> Type (u + 1) where
  | nil : Stack []
  | cons {α β ts} : α -> Stack β → (ts = α :: β) -> Stack ts

-- infixr:67 "; " => Stack.cons

def Stack.append.{u} {α β : List (Type u)} : Stack α -> Stack β -> Stack (α ++ β)
  | nil, b => b
  | cons a b h, b' => .cons a (append b b') (by simp [h])

[pandaman]

Ah sorry, I misunderstood the question. I think we need something like Stack.cast(see #new members > Proofs and casts @ 💬 )

[Julia Scheaffer]

pandaman said:

Ah sorry, I misunderstood the question. I think we need something like Stack.cast(see #new members > Proofs and casts @ 💬 )

Thank you for this advice. I will try that out.

[Julia Scheaffer]

Thank you for the recommendation @pandaman. I got have some proofs about Stack.append working now!
Also thanks to @Kyle Miller for those Vec exercises, they were a huge help for figuring out how to work with cast.