-- Concatenation of lists: how indexing reads through it, cancellation on
-- either side, and mapping over it
-- 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.Append
import Algebra.IndexedLists

-- append(ys, xs) is xs followed by ys. Positions below the length of xs
-- read xs; later positions read ys, shifted by that length.
theorem listCoefficient.append_left (A z : Set) (xs ys : List(A)) (n : Nat)
  requires bound : n < length{A}(xs)
  shows listCoefficient{A}(z, append(ys, xs), n) = listCoefficient{A}(z, xs, n)
proof
  induction xs generalizing n
  | List.nil =>
    intros n nNat bound
    rw length.nil at bound
    arith
  | List.cons(a, tail) using ih =>
    intros n nNat bound
    have element : a ∈ A by assumption
    have appended : List(A, append(ys, tail)) by typecheck
    rw append
    have shape := natural.zero_or_successor with *
    cases shape with zero | successor
    . rw [zero, listCoefficient.zero, listCoefficient.zero]
      rfl
    . obtain ⟨r, rNat, equal⟩ := successor
      rw [equal, length.cons] at bound
      have smaller : r < length{A}(tail) by arith
      rw [equal, listCoefficient.succ, listCoefficient.succ]
      exact ih with r, rNat, smaller

theorem listCoefficient.append_right (A z : Set) (xs ys : List(A)) (n : Nat)
  shows listCoefficient{A}(z, append(ys, xs), n + length{A}(xs)) = listCoefficient{A}(z, ys, n)
proof
  induction xs
  | List.nil =>
    rw [append, length.nil, add.right_unit]
    rfl
  | List.cons(a, tail) using ih =>
    have element : a ∈ A by assumption
    have appended : List(A, append(ys, tail)) by typecheck
    rwa [append, length.cons, add.succ_right, listCoefficient.succ]

-- Cancellation: a common first part, or a common last part, can be dropped.
theorem append.cancel_first (A : Set) (xs ys zs : List(A))
  requires equal : append(ys, xs) = append(zs, xs)
  shows ys = zs
proof
  have lengths : length{A}(append(ys, xs)) = length{A}(append(zs, xs))
    rw equal
    rfl
  rw [length.append, length.append] at lengths
  have sameLength := add.left_cancel with lengths
  apply listCoefficient.ext at A, ∅, ys, zs with sameLength
  intros n nNat bound
  have left := listCoefficient.append_right at A, ∅, xs, ys, n with *
  have right := listCoefficient.append_right at A, ∅, xs, zs, n with *
  rw equal at left
  rwa ← left

theorem append.cancel_last (A : Set) (xs ys zs : List(A))
  requires equal : append(xs, ys) = append(xs, zs)
  shows ys = zs
proof
  have lengths : length{A}(append(xs, ys)) = length{A}(append(xs, zs))
    rw equal
    rfl
  rw [length.append, length.append] at lengths
  have sameLength := add.right_cancel with lengths
  apply listCoefficient.ext at A, ∅, ys, zs with sameLength
  intros n nNat bound
  have boundZs : n < length{A}(zs) by rwa ← sameLength
  have left := listCoefficient.append_left at A, ∅, ys, xs, n with *
  have right := listCoefficient.append_left at A, ∅, zs, xs, n with boundZs, *
  rw equal at left
  rwa ← left

theorem listMap.append (A B f : Set) (xs ys : List(A))
  requires function : f : A → B
  shows listMap{A}(f, append(ys, xs)) = append{B}(listMap{A}(f, ys), listMap{A}(f, xs))
proof
  induction xs
  | List.nil =>
    rw [append, listMap, append]
    rfl
  | List.cons(a, tail) using ih =>
    have element : a ∈ A by assumption
    have image := FunctionBetween.apply_closed with function, element
    rw [append, listMap, listMap, ih, append]
    rfl