reverse_reverse definition

Stream: new members

[Ada Weird]

I've reached ch 8 of TPIL after a short break while I dealt with other stuff, and for exercise 2 they're asking me to define reverse and prove reverse (reverse xs) = xs). I've gotten the proof to the following point

def reverse: List α → List α
| [] => []
| x :: xs =>  xs ++ [x]

theorem reverse_reverse: ∀ l : List α, reverse (reverse l) = l := by
  intro l
  cases l
  case nil =>
    rfl
  case cons head tail =>
    unfold reverse
    simp
    sorry

But I'm not sure how to continue. It seems intuitive to me that I can ignore the [] case in the goal because it's being matched on tail ++ [head] which is definitionally not [], and that I can sub head and tail in for x and xs but I'm not sure how to tell that to lean.

[Ada Weird]

Oh and the current goal state

(match tail ++ [head] with
  | [] => []
  | x :: xs => xs ++ [x]) =
  head :: tail

[Ada Weird]

Oh wait no you can't sub in head for x. duh

[Ada Weird]

simp would have just done that for me if it could. I need to eliminate the [] case and then I dunno what

[Aaron Liu]

You might want to try proving reverse_append first

[Ada Weird]

Alright. I don't recognize that name. What's the theorem?

[Aaron Liu]

reverse (a ++ b) = reverse b ++ reverse a

[Ada Weird]

Thank you!

[Ada Weird]

Wait. I modified the definition of reverse to just use ++ instead of List.concat and I forgot to reverse xs. Yeah that'd make things harder.

[Ruben Van de Velde]

It can be difficult to prove things that are false

[Ada Weird]

Generally speaking yes

[Ada Weird]

Okay here is where we are

def reverse: List α → List α
| [] => []
| x :: xs =>  (reverse xs) ++ [x]

theorem reverse_reverse: ∀ l : List α, reverse (reverse l) = l := by
  intro l
  induction l
  case nil =>
    rfl
  case cons head tail hl =>
    unfold reverse
    conv in reverse (head :: tail) => {
      unfold reverse
    }
    sorry

With goal state before the sorry being

1 goal
α : Type u_1
head : α
tail : List α
hl : reverse (reverse tail) = tail
⊢ (match reverse tail ++ [head] with
  | [] => []
  | x :: xs => reverse xs ++ [x]) =
  head :: tail

[Ada Weird]

Again, I know that the [] case is irrelevant but I dunno how to eliminate it

[Ada Weird]

I dunno if that'd actually make things easier

[Ada Weird]

Or am I just barking up the wrong tree?

[Aaron Liu]

Did you prove reverse_append first?

[Ada Weird]

Yes

[Ada Weird]

theorem reverse_append: ∀ a b : List α, reverse (a ++ b) = reverse b ++ reverse a := by
  intro a b
  induction a
  case nil =>
    simp
    rfl
  case cons head_a tail_a ha=>
    simp
    conv =>
      lhs
      unfold reverse
      rw [ha]
    conv =>
      rhs;rhs
      unfold reverse
    simp

[Aaron Liu]

So reverse (reverse tail ++ [head]) = reverse [head] ++ reverse (reverse tail) = [head] ++ tail = head :: tail

[Ada Weird]

Alright lemme parse that out real quick

[Ada Weird]

Oh I see. Yeah I've been going about this wrong

[Ada Weird]

def reverse: List α → List α
| [] => []
| x :: xs =>  (reverse xs) ++ [x]

theorem reverse_len_1_list_eq_id: ∀ x : α, reverse [x] = [x] :=by
  intro x
  rfl

theorem reverse_append: ∀ a b : List α, reverse (a ++ b) = reverse b ++ reverse a := by
  intro a b
  induction a
  case nil =>
    simp
    rfl
  case cons head_a tail_a ha=>
    simp
    conv =>
      lhs
      unfold reverse
      rw [ha]
    conv =>
      rhs;rhs
      unfold reverse
    simp
theorem box_list (a: α) (b: List α): a :: b = [a] ++ b := by
  simp

theorem reverse_reverse: ∀ l : List α, reverse (reverse l) = l := by
  intro l
  induction l
  case nil =>
    rfl
  case cons head tail hl =>
    rw [box_list, reverse_append, reverse_len_1_list_eq_id,
      reverse_append, reverse_len_1_list_eq_id, hl]

[Ada Weird]

Got it!

[Ada Weird]

I assume box_list is a builtin but I didn't feel like finding it and defining it is trivial

[Robin Arnez]

List.singleton_append?

[Ada Weird]

I can't just sub that in the rw like I can with box_list

[Ada Weird]

But I'll look at it

[Ada Weird]

Oh I need to reverse it. Duh