-- Reversal of lists: length, interaction with concatenation, involution,
-- and the support
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.List.Reverse
import Algebra.IndexedLists

theorem reverse.length (A : Set) (xs : List(A))
  shows length{A}(reverse(xs)) = length{A}(xs)
proof
  induction xs
  | List.nil =>
    rw reverse
    rfl
  | List.cons(a, tail) using ih =>
    have element : a ∈ A by assumption
    have single : List(A, a :: []) by typecheck
    have reversed : List(A, reverse(tail)) by typecheck
    rw [reverse, length.append, ih, length.cons]
    simp [length, add.succ_right, add.right_unit]

theorem reverse.append (A : Set) (xs ys : List(A))
  shows reverse(append(ys, xs)) = append(reverse(xs), reverse(ys))
proof
  induction xs
  | List.nil =>
    have reversed : List(A, reverse(ys)) by typecheck
    rw [append, reverse, append.right_unit]
    rfl
  | List.cons(a, tail) using ih =>
    have element : a ∈ A by assumption
    have single : List(A, a :: []) by typecheck
    have reversedTail : List(A, reverse(tail)) by typecheck
    have reversedYs : List(A, reverse(ys)) by typecheck
    have appended : List(A, append(ys, tail)) by typecheck
    have reversedAppended : List(A, reverse(append(ys, tail))) by typecheck
    rw [append, reverse, ih, reverse, append.associative]
    rfl

theorem reverse.singleton (A a : Set)
  requires element : a ∈ A
  shows reverse{A}(a :: []) = a :: []
proof
  rw [reverse, reverse, append]
  rfl

theorem reverse.involutive (A : Set) (xs : List(A))
  shows reverse(reverse(xs)) = xs
proof
  induction xs
  | List.nil =>
    rw [reverse, reverse]
    rfl
  | List.cons(a, tail) using ih =>
    have element : a ∈ A by assumption
    have single : List(A, a :: []) by typecheck
    have reversed : List(A, reverse(tail)) by typecheck
    have doubled : List(A, reverse(reverse(tail))) by typecheck
    rw [reverse, reverse.append, ih, reverse.singleton, append, append.left_unit]
    rfl

theorem listSupport.reverse (A : Set) (xs : List(A))
  shows listSupport{A}(reverse(xs)) = listSupport{A}(xs)
proof
  induction xs
  | List.nil =>
    rw reverse
    rfl
  | List.cons(a, tail) using ih =>
    have element : a ∈ A by assumption
    have single : List(A, a :: []) by typecheck
    have reversed : List(A, reverse(tail)) by typecheck
    rw [reverse, listSupport.append, ih, listSupport.cons]
    ext y
    simp [listSupport, insert.membership, union2.membership]