-- The cyclic shift on a natural number n: successor on its members, wrapping
-- n − 1 to 0, as a function graph on n; it is a bijection of n.
-- 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.Nat.CyclicShift
import Mod
import Order
import Set.Function

-- The cyclic shift l ↦ l + 1 on n, wrapping n − 1 to 0.
defgraph rotation (n : Set) (l ∈ n) : n := chooseNat(equalNat(succ(l), n), 0, succ(l))
requires nNat : Nat(n)
proof
  have lNat := natural.member at n with member
  have less := Less.of_membership with member
  have alternatives : succ(l) = n ∨ succ(l) ≠ n
    tauto
  cases alternatives with wrap | step
  . have flag := equalNat.true_iff.backward with wrap
    rw flag
    simp [chooseNat]
    have positive : 0 < n by arith
    exact membership.of_Less with positive
  . have flag := equalNat.false_iff.backward with step
    rw flag
    simp [chooseNat]
    have separated : n ≠ succ(l)
      intro same
      apply step
      symm
      exact same
    have below := Less.successor_lower_of_ne with less, separated
    exact membership.of_Less with below

theorem rotation.step (n : Nat) (l : Set)
  requires hl : l ∈ n
  requires hs : succ(l) ∈ n
  shows rotation(n)(l) = succ(l)
proof
  have lNat := natural.member at n with hl
  have different : succ(l) ≠ n
    intro same
    rw same at hs
    exact membership.irreflexive with hs
  have flag := equalNat.false_iff.backward with different
  have value := rotation.value at n, l with *
  rw [value, flag]
  simp [chooseNat]

theorem rotation.wrap (n : Nat) (l : Set)
  requires hl : l ∈ n
  requires top : succ(l) = n
  shows rotation(n)(l) = 0
proof
  have lNat := natural.member at n with hl
  have flag := equalNat.true_iff.backward with top
  have value := rotation.value at n, l with *
  rw [value, flag]
  simp [chooseNat]

theorem rotation.cancel (n : Nat) (x y : Set)
  requires hx : x ∈ n
  requires hy : y ∈ n
  requires same : rotation(n)(x) = rotation(n)(y)
  shows x = y
proof
  have xNat := natural.member at n with hx
  have yNat := natural.member at n with hy
  have xLess := Less.of_membership with hx
  have yLess := Less.of_membership with hy
  have xAlternatives : succ(x) = n ∨ succ(x) ≠ n by tauto
  have yAlternatives : succ(y) = n ∨ succ(y) ≠ n by tauto
  cases xAlternatives with xWrap | xStep
  . have xValue := rotation.wrap with hx, xWrap
    cases yAlternatives with yWrap | yStep
    . have both : succ(x) = succ(y)
        rw [xWrap, yWrap]
        rfl
      have forward : x ≤ y by arith
      have backward : y ≤ x by arith
      exact LessEqual.antisymmetric with forward, backward
    . have ySeparated : n ≠ succ(y)
        intro equal
        apply yStep
        symm
        exact equal
      have yIn := membership.of_Less
        with (Less.successor_lower_of_ne with yLess, ySeparated)
      have yValue := rotation.step with hy, yIn
      rw [xValue, yValue] at same
      arith
  . have xSeparated : n ≠ succ(x)
      intro equal
      apply xStep
      symm
      exact equal
    have xIn := membership.of_Less
      with (Less.successor_lower_of_ne with xLess, xSeparated)
    have xValue := rotation.step with hx, xIn
    cases yAlternatives with yWrap | yStep
    . have yValue := rotation.wrap with hy, yWrap
      rw [xValue, yValue] at same
      arith
    . have ySeparated : n ≠ succ(y)
        intro equal
        apply yStep
        symm
        exact equal
      have yIn := membership.of_Less
        with (Less.successor_lower_of_ne with yLess, ySeparated)
      have yValue := rotation.step with hy, yIn
      rw [xValue, yValue] at same
      have forward : x ≤ y by arith
      have backward : y ≤ x by arith
      exact LessEqual.antisymmetric with forward, backward

theorem rotation.injective (n : Nat)
  shows InjectiveBetween(rotation(n), n, n)
proof
  have function := rotation.function at n with *
  constructor
  . exact function
  . intros x hx y hy z hz hxz hyz
    have xValue := FunctionBetween.apply_value with function, hx, hxz
    have yValue := FunctionBetween.apply_value with function, hy, hyz
    have same : rotation(n)(x) = rotation(n)(y)
      rw [xValue, yValue]
      rfl
    exact rotation.cancel with hx, hy, same

theorem rotation.surjective (n : Nat)
  shows SurjectiveBetween(rotation(n), n, n)
proof
  have function := rotation.function at n with *
  constructor
  . exact function
  . intros y hy
    have yNat := natural.member at n with hy
    have yLess := Less.of_membership with hy
    have shape := natural.zero_or_successor with yNat
    cases shape with zero | successor
    . have nShape := natural.zero_or_successor at n with *
      cases nShape with nZero | nSuccessor
      . exfalso
        rw nZero at yLess
        arith
      . obtain ⟨m, mNat, nEq⟩ := nSuccessor
        have top : succ(m) = n
          symm
          exact nEq
        have mIn : m ∈ n
          rw nEq
          exact bootstrap.succ.self
        have value := rotation.wrap with mIn, top
        have edge := FunctionBetween.relates_apply with function, mIn
        rw value at edge
        witness m
        constructor
        . exact mIn
        . rw zero
          exact edge
    . obtain ⟨k, kNat, yEq⟩ := successor
      have kLess : k < n
        rw yEq at yLess
        arith
      have kIn := membership.of_Less with kLess
      have sIn : succ(k) ∈ n by rwa ← yEq
      have value := rotation.step with kIn, sIn
      have edge := FunctionBetween.relates_apply with function, kIn
      rw value at edge
      witness k
      constructor
      . exact kIn
      . rw yEq
        exact edge

theorem rotation.bijective (n : Nat)
  shows BijectiveBetween(rotation(n), n, n)
proof
  constructor
  . exact rotation.injective at n
  . exact rotation.surjective at n