append and the related theorem for vector type

Stream: new members

[Shanghe Chen]

Hi! I am learning TPIL and in the chapter Inductive Families I am trying to formalize a theorem related to append vector:

inductive Vector (α : Type u) : Nat → Type u where
| nil : Vector α 0
| cons : α → {n : Nat} → Vector α n → Vector α (n+1)

#check Vector.nil
#check Vector.cons 3 Vector.nil

#check Vector.recOn
-- Inductive_Families.Vector.recOn.{u_1, u} {α : Type u} {motive : (a : Nat) → Vector α a → Sort u_1} {a : Nat}
--   (t : Vector α a) (nil : motive 0 Vector.nil)
--   (cons : (a : α) → {n : Nat} → (a_1 : Vector α n) → motive n a_1 → motive (n + 1) (Vector.cons a a_1)) : motive a t

def length {α : Type u} (x : Vector α n) : Nat := n

-- TODO cannot do this now
--      How to prove or state Vector Nat (1+0) = Vector Nat 1?
-- def append {α : Type u} (x : Vector α n) (y : Vector α m) : Vector α (n+m) :=
-- Vector.recOn (motive := fun (a : Nat) (b : Vector α a) => Vector α (a+m)) x
-- (y)
-- sorry

[Shanghe Chen]

How to define the append fun for vector plz? It seems that I stucked at showing something like proving Vector Nat (1+0) = Vector Nat 1

[Bolton Bailey]

You might be looking for docs#cast

[Bolton Bailey]

(Casting things can become very tricky, which I would say is why dependent inductive types like this are generally avoided in mathlib)

[Shanghe Chen]

OK maybe I just stick with the Eq example in TPIL and leave alone the vector type

[Shanghe Chen]

So in fact Vector Nat (1+0), Vector Nat 1 they are not the same type? I suspect they are not?

[Shanghe Chen]

Now I get the def with the following code:

namespace InductiveFamilies

inductive Vector (α : Type u) : Nat → Type u where
| nil : Vector α 0
| cons (a: α) {n : Nat} (b: Vector α n) : Vector α (n+1)

#check Vector.nil
#check Vector.cons 3 Vector.nil

#check Vector.recOn
-- Inductive_Families.Vector.recOn.{u_1, u} {α : Type u} {motive : (a : Nat) → Vector α a → Sort u_1} {a : Nat}
--   (t : Vector α a) (nil : motive 0 Vector.nil)
--   (cons : (a : α) → {n : Nat} → (a_1 : Vector α n) → motive n a_1 → motive (n + 1) (Vector.cons a a_1)) : motive a t

def length {α : Type u} (x : Vector α n) : Nat := n

theorem vector_eq (h : n = m) : Vector α n = Vector α m :=
congrArg (Vector α) h

def append {α : Type u} (x : Vector α n) (y : Vector α m) : Vector α (n+m) :=
Vector.recOn (motive := fun (a : Nat) (b : Vector α a) => Vector α (a+m)) x
(by simp ; exact y)
(by
  intro a' n' x' xy'
  let xy := (Vector.cons a' xy')
  let h: Vector α (n' + m + 1) = Vector α (n' + 1 + m) := by simp [Nat.add_assoc, Nat.add_comm, vector_eq]
  let xy' := cast h xy
  exact xy'
  )

def append₁ {α : Type u} (x : Vector α n) (y : Vector α m) : Vector α (n+m) :=
match x with
| nil => sorry
| cons h t => sorry

end InductiveFamilies

except the error: code generator does not support recursor 'InductiveFamilies.Vector.recOn' yet, consider using 'match ... with' and/or structural recursion and invalid pattern, constructor or constant marked with '[match_pattern]' expected . Why I cannot run recOn on it, and why it's also failed with pattern match?

[Robert Maxton]

Honestly, that seems like a shame. At least in this case, it's not too bad. The syntax is a little weird at first, though

[Shanghe Chen]

If I added noncomputable keyword in the first def, it works but #eval fails. And for the pattern match I get it in Dependent pattern matching in TPIL now :tada:

[Robert Maxton]

The trick is to remember that "proofs" in Lean are just producing a term of a given type anyway, so you can use the := by syntax to produce terms of other types (types that are not in Prop) as well. So you can get started with something like:

  def append {α : Type u} {n m : ℕ} (v : Vector α n) (w : Vector α m) : Vector α (n + m) :=
    match v with
    | .nil => by convert w; simp
    | @Vector.cons _ hd k tl => by ...

.nil is easily done with convert, which in this case successfully realizes that the types Vector α m and Vector α (m+0) would be the same if m = m + 0, which you can then prove with simp. .cons is a bit harder; if you just use convert directly, convert will see that you have a term Vector α (k + 1 + m) and a term Vector α (k + m + 1), and will blindly try and equate atoms, producing the goals 1 = m and m = 1 instead of k + 1 + m = k + m + 1; you'll have to work around that. (I can also just give you the answer -- or at least an answer -- but since you're doing the exercises anyway I thought I'd give you the option at least :p)

[Robert Maxton]

...aaalso somehow I missed your last few posts ^.^;
oops!

[Shanghe Chen]

Yeah. Now I get the def of append in pattern match form with the following snippet:

inductive Vector (α : Type u) : Nat → Type u where
| nil : Vector α 0
| cons (a: α) {n : Nat} (b: Vector α n) : Vector α (n+1)
deriving Repr

#check Vector.nil
#check Vector.cons 3 Vector.nil

#check Vector.recOn
-- Inductive_Families.Vector.recOn.{u_1, u} {α : Type u} {motive : (a : Nat) → Vector α a → Sort u_1} {a : Nat}
--   (t : Vector α a) (nil : motive 0 Vector.nil)
--   (cons : (a : α) → {n : Nat} → (a_1 : Vector α n) → motive n a_1 → motive (n + 1) (Vector.cons a a_1)) : motive a t

def length {α : Type u} (x : Vector α n) : Nat := n

theorem vector_eq (h : n = m) : Vector α n = Vector α m :=
congrArg (Vector α) h

-- the noncomputable keyword is hint from
-- https://leanprover-community.github.io/archive/stream/270676-lean4/topic/code.20generator.20does.20not.20support.20recursor.html
noncomputable def append {α : Type u} (x : Vector α n) (y : Vector α m) : Vector α (n+m) :=
Vector.recOn (motive := fun (a : Nat) (b : Vector α a) => Vector α (a+m)) x
(by simp ; exact y)
(by
  intro a' n' x' xy'
  let xy := (Vector.cons a' xy')
  let h: Vector α (n' + m + 1) = Vector α (n' + 1 + m) := by simp [Nat.add_assoc, Nat.add_comm, vector_eq]
  let xy' := cast h xy
  exact xy'
  )

#check append (Vector.cons 3 Vector.nil) (Vector.cons 4 Vector.nil)
-- cannot eval, still problematic, but the following match version does work
-- TODO why is the recOn version problematic in eval?
-- #eval append (Vector.cons 3 Vector.nil) (Vector.cons 4 Vector.nil)

def append₁ {α : Type u} (x : Vector α n) (y : Vector α m) : Vector α (n+m) :=
match n, x with
| 0, _ => by simp; exact y
-- it must match n, x in the same time, and the first must be n' + 1 for giving implicit
-- argument to the second
| n'+1, Vector.cons a t =>
  by
    let xy := Vector.cons a (append₁ t y)
    let h: Vector α (n' + m + 1) = Vector α (n' + 1 + m) := by simp [Nat.add_assoc, Nat.add_comm, vector_eq]
    let xy' := cast h xy
    exact xy'

#check append₁ (Vector.cons 3 Vector.nil) (Vector.cons 4 Vector.nil)
-- TODO it eval to ⊢ Vector Nat (0 + 1 + (0 + 1))
-- how to make it to Vector Nat 2?
#eval append₁ (Vector.cons 3 Vector.nil) (Vector.cons 4 Vector.nil)

[Shanghe Chen]

It just contains a minor flaws that #eval append (Vector.cons 3 Vector.nil) (Vector.cons 4 Vector.nil) is of type Vector Nat (0 + 1 + (0 + 1)) but not Vector Nat 2

[Robert Maxton]

Nice!

[Robert Maxton]

Coriver Chen said:

It just contains a minor flasw that #eval append (Vector.cons 3 Vector.nil) (Vector.cons 4 Vector.nil) is of type Vector Nat (0 + 1 + (0 + 1)) but not Vector Nat 2

Hmmm... You could probably work around that y doing something like

def append₁ {α : Type u} (x : Vector α n) (y : Vector α m) {r : Nat} {h_r: r = n + m} : Vector α r :=...

but I don't know what that'd do to the usability of the actual function...

[Shanghe Chen]

Yeah it’s just some kind of practice illuminating the strength of the type system I think.