-- Shared list facts. The sole List datatype and executable operations live in Data.
-- Part of the Grace17 proof assistant for mathematics based on set theory.
-- Copyright (c) 2026 Grant Passmore. Apache License 2.0; see LICENSE.
-- Authors: Grant Passmore

module Grace.Core.List
import Grace.Core.Data
export open Grace.Core.Data

theorem List.cases (A : Set) (xs : List(A))
  shows xs = List.nil ∨ ∃ x ∈ A, ∃ tail, List(A, tail) ∧ xs = x :: tail
proof
  induction xs
  | List.nil =>
    left
    rfl
  | List.cons(x, tail) using ih =>
    right
    refine ⟨x, assumption, tail, assumption, rfl⟩


theorem length.nil (A : Set)
  shows length{A}([]) = 0
proof
  simp [length]

theorem length.cons (A x : Set) (xs : List(A))
  requires element : x ∈ A
  shows length{A}(x :: xs) = succ(length{A}(xs))
proof
  simp [length]

-- append(ys, xs) traverses xs and places ys after it (the existing API).
theorem append.left_unit {A : Set} (ys : List(A))
  shows append(ys, []) = ys
proof
  simp [append]

theorem append.associative {A : Set} (zs ys xs : List(A))
  shows append(zs, append(ys, xs)) = append(append(zs, ys), xs)
proof
  induction xs
  | List.nil => simp [append]
  | List.cons(x, tail) using ih => simp [append, ih]