Beginner question on zip exercise, plus some monoids

Stream: lean4

[DSB]

Hello, friends. Just started learning Lean. I'm going through the Functional Programming book. I was just faced with the following exercise:

Write a function zip that combines two lists into a list of pairs. The resulting list should be as long as the shortest input list. Start the definition with def zip {α β : Type} (xs : List α) (ys : List β) : List (α × β) :=.

I'm having a hard time solving this one. It is not clear to me how to use pattern-matching in both lists at once. Here is my attempt, but it is failing to terminate:

def myzip {α β : Type} (xs : List α) (ys : List β) : List (α × β) :=
  match (xs, ys) with
  | ([], _) => []
  | (_, []) => []
  | (x :: xs', y :: ys') => (x, y) :: myzip xs' ys'

Also, a more advanced question. Is it possible to adapt this zip function to work only on Monoids, such as whenever one gets an empty list, the zip should use the neutral element. For example:

#eval monoidzip [1,2,3] [1,2]

Should return [(1,1),(2,2),(3,0)] where 0 would be the neutral element. Similarly, if instead of Natural numbers I had strings, I could define the monoid with the empty string.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

To your first question: here is a version that Lean can show terminating. Talk about 'spot the difference'!

def myzip {α β : Type} (xs : List α) (ys : List β) : List (α × β) :=
  match xs, ys with
  | [], _ => []
  | _, [] => []
  | x :: xs', y :: ys' => (x, y) :: myzip xs' ys'

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

And for the second one

class Zero.{u} (α : Type u) where -- This is defined in mathlib
  zero : α
open Zero

def myzip {α β : Type} [Zero α] [Zero β] (xs : List α) (ys : List β) : List (α × β) :=
  match xs, ys with
  | [], [] => []
  | [], y :: ys' => (zero, y) :: myzip [] ys'
  | x :: xs', [] => (x, zero) :: myzip xs' []
  | x :: xs', y :: ys' => (x, y) :: myzip xs' ys'

instance : Zero Nat := ⟨0⟩

#eval myzip [1,2,3] [1,2] -- [(1, 1), (2, 2), (3, 0)]

Note that you don't actually need a monoid since nothing is being combined; you just need a neutral element. I chose zero here.

[DSB]

Wojciech Nawrocki said:

And for the second one

class Zero.{u} (α : Type u) where -- This is defined in mathlib
  zero : α
open Zero

def myzip {α β : Type} [Zero α] [Zero β] (xs : List α) (ys : List β) : List (α × β) :=
  match xs, ys with
  | [], [] => []
  | [], y :: ys' => (zero, y) :: myzip [] ys'
  | x :: xs', [] => (x, zero) :: myzip xs' []
  | x :: xs', y :: ys' => (x, y) :: myzip xs' ys'

instance : Zero Nat := ⟨0⟩

#eval myzip [1,2,3] [1,2] -- [(1, 1), (2, 2), (3, 0)]

Note that you don't actually need a monoid since nothing is being combined; you just need a neutral element. I chose zero here.

Thanks! Yeah, I know I don't need a monoid for the example at hand. I was just anticipating, cause I'll be needing monoids in the applications I'm coding.

[Kevin Buzzard]

(In lean the identity element of a Monoid is always 1 not 0)

[James Sully]

There's an open issue for this:
https://github.com/leanprover/fp-lean/issues/118