open import Data.Parity.Base
open import Data.Parity.Properties
open import Data.List using (List)
  renaming (
    _∷_ to _l∷_; [] to l[]; _++_ to _l++_;
    map to lmap
  )
open import Data.Vec
open import Data.Vec.Properties
open import Data.Nat using (ℕ)
  renaming (_<_ to _ℕ<_; _≥_ to _ℕ≥_)
open import Data.Fin using (
    Fin; suc; zero;
    pred;
    fromℕ; fromℕ<;
    inject₁
  )
open import Data.Fin.Properties
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Data.Empty

_Cups : ℕ → Set
n Cups = Vec Parity n

open Parity
initS :  Cups
initS = 0ℙ ∷ 0ℙ ∷ 1ℙ ∷ 1ℙ ∷ 0ℙ ∷ []

target :  Cups
target = 1ℙ ∷ 1ℙ ∷ 1ℙ ∷ 1ℙ ∷ 1ℙ ∷ []

-- To prove it's impossible to start from `initS`, with update two indicies as the only action, get `target`
-- we need to think about two things
-- 1. what's "all" actions on `n Cups`
-- 2. how to reduce the states, for example, the difference between position
--      0ℙ ∷ 0ℙ ∷ 1ℙ ∷ 1ℙ ∷ 0ℙ
--      vs
--      0ℙ ∷ 0ℙ ∷ 1ℙ ∷ 0ℙ ∷ 1ℙ
--    is irrelevant here

-- A middle part for generating all possible actions, but turns out I didn't need these to prove the theorem
-- In fact, though `(i, i)` action is impossible in the real game, but it's not contribute into the proof
module Actions where
  {-# TERMINATING #-}
  half-actions : ∀ {m} → Fin m → Fin m → List (Fin m × Fin m)
  half-actions cnt zero = l[]
  half-actions cnt x = ( cnt , pred x ) l∷ (half-actions cnt (pred x))

  -- 1. `(i, i)` should be skipped
  -- 2. except that we generate `n..0 × n-1..0` to get all possible indicies
  all-actions : ∀ {n} → n Cups → List (Fin n × Fin n)
  all-actions {ℕ.zero} _ = l[]
  all-actions {ℕ.suc n'} (_ ∷ cups') =
    let cnt = fromℕ n'
        as = half-actions cnt cnt
        recur = all-actions cups'
    in as l++ (lmap (λ (a , b) → ( inject₁ a , inject₁ b)) recur)

-- to reduce the states, folding on `Partiy._+_` characterize the `n Cups`
-- the idea is that, whatever an action is, the possible cases are working on
--     (0ℙ, 0ℙ) -> (1ℙ, 1ℙ)
--     (0ℙ, 1ℙ) -> (1ℙ, 0ℙ)
--     (1ℙ, 0ℙ) -> (0ℙ, 1ℙ)
--     (1ℙ, 1ℙ) -> (0ℙ, 0ℙ)
-- 1. middle two are boring, because it's easy to see they're identical to the original Parity result
-- 2. the first case let no `⁻¹` turns to `⁻¹ ∘ ⁻¹`, but that means Parity has no changed
-- 3. the final case let `⁻¹ ∘ ⁻¹` turns to do nothing, and hence still stay at the same place
χ : ∀ {n} → n Cups → Parity
χ [] = 0ℙ
χ (x ∷ cups) = χ cups + x

-- because there have even `1ℙ`
lemma₁ : χ initS ≡ 0ℙ
lemma₁ = refl

lemma₂ : χ target ≡ 1ℙ
lemma₂ = refl

module Lemma where
  helper : ∀ {p} → p ⁻¹ ≡ p + 1ℙ
  helper {0ℙ} = refl
  helper {1ℙ} = refl
  helper₂ : ∀ {p} → p ≡ p + 0ℙ
  helper₂ {0ℙ} = refl
  helper₂ {1ℙ} = refl
  helper₃ : ∀ {p} → p ≡ p ⁻¹ ⁻¹
  helper₃ {0ℙ} = refl
  helper₃ {1ℙ} = refl

  open ≡-Reasoning

  lemma : ∀ {n} → (i : Fin n) → (a : n Cups)
    ----------------------------------------------------------
    → χ (a [ i ]%= _⁻¹) ≡ χ a ⁻¹
  lemma zero (0ℙ ∷ a') =
    begin
      χ a' + 1ℙ ≡⟨ sym helper ⟩
      χ a' ⁻¹ ≡⟨ cong _⁻¹ helper₂ ⟩
      (χ a' + 0ℙ) ⁻¹
    ∎
  lemma zero (1ℙ ∷ a') =
    begin
      χ a' + 0ℙ ≡⟨ sym helper₂ ⟩
      χ a' ≡⟨ helper₃ ⟩
      χ a' ⁻¹ ⁻¹ ≡⟨ cong _⁻¹ helper ⟩
      (χ a' + 1ℙ) ⁻¹
    ∎
  lemma (suc i') (0ℙ ∷ a') =
    begin
      χ (updateAt a' i' _⁻¹) + 0ℙ ≡⟨ sym helper₂ ⟩
      χ (updateAt a' i' _⁻¹) ≡⟨ lemma i' a' ⟩
      χ a' ⁻¹ ≡⟨ cong _⁻¹ helper₂ ⟩
      (χ a' + 0ℙ) ⁻¹
    ∎
  lemma (suc i') (1ℙ ∷ a') =
    begin
      χ (updateAt a' i' _⁻¹) + 1ℙ ≡⟨ sym helper ⟩
      χ (updateAt a' i' _⁻¹) ⁻¹ ≡⟨ cong _⁻¹ (lemma i' a') ⟩
      χ a' ⁻¹ ⁻¹ ≡⟨ sym (cong _⁻¹ (sym helper)) ⟩
      (χ a' + 1ℙ) ⁻¹
    ∎

-- The theorem is showing that, for any `n Cups`,
-- the action works on even cups will not change χ
theorem : ∀ {n} → (i j : Fin n) → (a : n Cups)
  ------------------------------------------------
  → χ ((a [ i ]%= _⁻¹) [ j ]%= _⁻¹) ≡ χ a
theorem i j a =
  begin
    χ (updateAt (updateAt a i _⁻¹) j _⁻¹) ≡⟨ lemma j (a [ i ]%= _⁻¹) ⟩
    χ (updateAt a i _⁻¹)⁻¹ ≡⟨ ⁻¹-selfInverse (sym (lemma i a)) ⟩
    χ a
  ∎ where open ≡-Reasoning
          open Lemma

-- and hence we claim, if χ is different,
-- it's impossible to move to another state
_⇒¬_ : ∀ {n} → n Cups → n Cups → Set
a ⇒¬ b = χ a ≡ χ b → ⊥