-- The list of the first n natural numbers in order: length, entries,
-- support, sortedness, counts, and prefixes
-- 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.Range
import Sorted

def listRange (n : Nat) → Set
  | zero => []
  | succ(k) => append{ℕ}(k :: [], listRange(k))

theorem listRange.zero
  shows listRange(0) = []
proof
  simp [listRange]

theorem listRange.succ (n : Nat)
  shows listRange(succ(n)) = append{ℕ}(n :: [], listRange(n))
proof
  simp [listRange]

theorem listRange.closed (n : Nat)
  shows List(ℕ, listRange(n))
proof
  induction n
  | zero =>
    rw listRange.zero
    typecheck
  | succ(k) using ih =>
    have kIn : k ∈ ℕ := nat.omega.forward with *
    have single : List(ℕ, k :: []) by typecheck
    rw listRange.succ
    typecheck

theorem listRange.length (n : Nat)
  shows length{ℕ}(listRange(n)) = n
proof
  induction n
  | zero =>
    rw [listRange.zero, length.nil]
    rfl
  | succ(k) using ih =>
    have kIn : k ∈ ℕ := nat.omega.forward with *
    have single : List(ℕ, k :: []) by typecheck
    have list := listRange.closed at k with *
    rw [listRange.succ, length.append, ih, length.singleton, add.right_one]
    rfl

theorem listRange.coefficient (n i : Nat)
  requires bound : i < n
  shows listCoefficient{ℕ}(0, listRange(n), i) = i
proof
  induction n
  | zero =>
    intro bound
    exfalso
    arith
  | succ(k) using ih =>
    intro bound
    have kIn : k ∈ ℕ := nat.omega.forward with *
    have list := listRange.closed at k with *
    have length := listRange.length at k with *
    rw listRange.succ
    have alternatives : i < k ∨ ¬(i < k) by tauto
    cases alternatives with below | notBelow
    . have inside : i < length{ℕ}(listRange(k)) by rwa length
      have step := listCoefficient.snoc_below at ℕ, 0, k, listRange(k), i with kIn, inside
      rw step
      exact ih with below
    . have atLeast := LessEqual.of_not_Less at i, k with notBelow
      have same : i = k
        have upper := Less.successor_upper with bound
        exact LessEqual.antisymmetric with upper, atLeast
      have last := listCoefficient.snoc_last at ℕ, 0, k, listRange(k) with kIn
      rw length at last
      rw same
      exact last

theorem listRange.mem_support (n : Nat)
  shows ∀ y, y ∈ listSupport{ℕ}(listRange(n)) ↔ y ∈ n
proof
  induction n
  | zero =>
    intro y
    rw [listRange.zero, listSupport.nil]
    constructor
    . intro member
      exfalso
      exact set.empty with member
    . intro member
      have zero : y ∈ ∅ by rwa ← nat.zero
      exfalso
      exact set.empty with zero
  | succ(k) using ih =>
    intro y
    have kIn : k ∈ ℕ := nat.omega.forward with *
    have single : List(ℕ, k :: []) by typecheck
    have list := listRange.closed at k with *
    have successor := natural.successor_as_insert at k with *
    have inner := ih with y
    rw [listRange.succ, listSupport.append, listSupport.singleton, successor]
    have union := union2.membership at y, listSupport{ℕ}(listRange(k)), {k}
    have insertion := insert.membership at y, k, k
    have singleton := singleton.membership at y, k
    tauto

theorem listRange.support (n : Nat)
  shows listSupport{ℕ}(listRange(n)) = n
proof
  have members := listRange.mem_support at n with *
  ext y
  exact members with y

theorem listRange.mem_support_iff (n : Nat) (y : Set)
  shows y ∈ listSupport{ℕ}(listRange(n)) ↔ (Nat(y) ∧ y < n)
proof
  rw listRange.support
  constructor
  . intro member
    have natural := natural.member at n with *
    have yNat := natural with y, member
    have below := Less.of_membership at y, n with *, member
    exact ⟨yNat, below⟩
  . intro both
    obtain ⟨yNat, below⟩ := both
    exact membership.of_Less at y, n with *, below

theorem listRange.sorted (n : Nat)
  shows ListSorted(listRange(n))
proof
  have list := listRange.closed at n with *
  have length := listRange.length at n with *
  unfold ListSorted
  intros i j iNat jNat below bound
  rw length at bound
  have smaller : i < n by arith
  have left := listRange.coefficient at n, i with smaller
  have right := listRange.coefficient at n, j with bound
  rw [left, right]
  exact Less.implies_LessEqual with below

theorem listRange.count_below (n i : Nat)
  requires bound : i < n
  shows listCount{ℕ}(i, listRange(n)) = 1
proof
  induction n
  | zero =>
    intro bound
    exfalso
    arith
  | succ(k) using ih =>
    intro bound
    have kIn : k ∈ ℕ := nat.omega.forward with *
    have single : List(ℕ, k :: []) by typecheck
    have list := listRange.closed at k with *
    rw [listRange.succ, listCount.append]
    have alternatives : i < k ∨ ¬(i < k) by tauto
    cases alternatives with below | notBelow
    . have inner := ih with below
      have different : i ≠ k
        intro same
        rw same at below
        exact Less.irreflexive with *, below
      have other := listCount.singleton_other at ℕ, i, k with kIn, different
      rw [inner, other, add.right_unit]
      rfl
    . have atLeast := LessEqual.of_not_Less at i, k with notBelow
      have same : i = k
        have upper := Less.successor_upper with bound
        exact LessEqual.antisymmetric with upper, atLeast
      have absent : ¬(i ∈ listSupport{ℕ}(listRange(k)))
        intro member
        have both := listRange.mem_support_iff.forward at k, i with member
        rw same at both
        have strict := both.right
        exact Less.irreflexive at k with *, strict
      have zero := listCount.zero_of_absent with absent
      rw [zero, same, listCount.singleton_self, add.left_unit]
      rfl

theorem listRange.count_above (n i : Nat)
  requires bound : n ≤ i
  shows listCount{ℕ}(i, listRange(n)) = 0
proof
  have list := listRange.closed at n with *
  have absent : ¬(i ∈ listSupport{ℕ}(listRange(n)))
    intro member
    have both := listRange.mem_support_iff.forward at n, i with member
    have below := both.right
    have strict : i < i by arith
    exact Less.irreflexive at i with *, strict
  exact listCount.zero_of_absent with absent

theorem listRange.prefix (m n : Nat)
  requires bound : m ≤ n
  shows ListPrefix(ℕ, listRange(m), listRange(n))
proof
  induction n
  | zero =>
    intro bound
    have zero : m = 0
      have lower : 0 ≤ m by arith
      exact LessEqual.antisymmetric with bound, lower
    rw [zero, listRange.zero]
    have nilList : List(ℕ, []) by typecheck
    exact ListPrefix.reflexive at ℕ, [] with *
  | succ(k) using ih =>
    intro bound
    have kIn : k ∈ ℕ := nat.omega.forward with *
    have single : List(ℕ, k :: []) by typecheck
    have list := listRange.closed at k with *
    have listM := listRange.closed at m with *
    have alternatives : m ≤ k ∨ ¬(m ≤ k) by tauto
    cases alternatives with below | notBelow
    . have inner := ih with below
      have extend := ListPrefix.append at ℕ, listRange(k), k :: [] with *
      rw listRange.succ
      exact ListPrefix.transitive with inner, extend
    . have above := Less.of_not_LessEqual at m, k with notBelow
      have same : m = succ(k)
        have upper : m ≤ succ(k) := bound
        have lower : succ(k) ≤ m by arith
        exact LessEqual.antisymmetric with upper, lower
      rw same
      have listSucc := listRange.closed at succ(k) with *
      exact ListPrefix.reflexive at ℕ, listRange(succ(k)) with *

theorem listRange.take (m n : Nat)
  requires bound : m ≤ n
  shows listTake{ℕ}(m, listRange(n)) = listRange(m)
proof
  have prefix := listRange.prefix with bound
  have listM := listRange.closed at m with *
  have listN := listRange.closed at n with *
  have taken := ListPrefix.eq_take with prefix
  rw listRange.length at taken
  symm
  exact taken