module Reassoc where

open import Data.List
open import Data.Product

open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; cong; subst)
open Relation.Binary.PropositionalEquality.≡-Reasoning

-- List lemmas

xs++[]≡xs :  ∀ {a} → {A : Set a}
  → (xs : List A)
  → xs ++ [] ≡ xs
xs++[]≡xs []       = refl
xs++[]≡xs (x ∷ xs) = cong (_∷_ x) (xs++[]≡xs xs)

++-assoc : ∀ {a} → {A : Set a}
  → (xs : List A)
  → (ys : List A)
  → (zs : List A)
  → xs ++ ys ++ zs ≡ (xs ++ ys) ++ zs
++-assoc []       ys zs = refl
++-assoc (x ∷ xs) ys zs = cong (_∷_ x) (++-assoc xs ys zs)

-- Syntax
data L {a} {A : Set a} : List A → Set a where
  nil : L []
  app : (xs : List A) → ∀ {ys zs} → L ys → xs ++ ys ≡ zs → L zs

eval-L : ∀ {a} {A : Set a} {xs : List A} → L xs → Σ (List A) λ xs' → xs' ≡ xs
eval-L nil          = [] , refl
eval-L (app xs l p) with eval-L l
... | ys , q = xs ++ ys , (begin
  xs ++ ys ≡⟨ cong (λ ys' → xs ++ ys') q ⟩
  xs ++ _  ≡⟨ p ⟩
  _ ∎)

l : ∀ {a} → {A : Set a} → (xs : List A) → L xs
l xs = app xs nil (xs++[]≡xs xs)

infixr 5 _<>_
_<>_ : ∀ {a} {A : Set a} {xs ys : List A} → L xs → L ys → L (xs ++ ys)
nil <> zs = zs
_<>_ {ys = ws} (app xs {ys = ys} {zs = zs} ys' p) ws' =
  app xs {ys = ys ++ ws} (ys' <> ws') (begin
     xs ++ ys  ++ ws ≡⟨ ++-assoc xs ys ws ⟩
    (xs ++ ys) ++ ws ≡⟨ cong (λ zs' → zs' ++ ws) p ⟩
    zs ++ ws         ∎)

solve : ∀ {a} {A : Set a} {xs ys : List A}
  → (xs' : L xs)
  → (ys' : L ys)
  → (proj₁ (eval-L xs') ≡ proj₁ (eval-L ys'))
  → xs ≡ ys
solve {xs = xs} {ys = ys} xs' ys' s = begin
  xs                 ≡⟨ sym (proj₂ (eval-L xs')) ⟩
  proj₁ (eval-L xs')  ≡⟨ s ⟩
  proj₁ (eval-L ys')  ≡⟨ proj₂ (eval-L ys') ⟩
  ys                 ∎
  where
    xsp = eval-L xs'

-- DEMOS
--------------

++-assoc-again : ∀ {a} → {A : Set a}
  → (xs : List A)
  → (ys : List A)
  → (zs : List A)
  → xs ++ ys ++ zs ≡ (xs ++ ys) ++ zs
++-assoc-again xs ys zs = solve
  (l xs <> l ys <> l zs)
  ((l xs <> l ys) <> l zs)
  refl

crazier : ∀ {a} → {A : Set a}
  → (xs : List A)
  → (ys : List A)
  → (zs : List A)
  → (ws : List A)
  → xs ++ (ys ++ zs) ++ ws ≡ (xs ++ ys) ++ (zs ++ ws)
crazier xs ys zs ws = solve
  (l xs <> (l ys <> l zs) <> l ws)
  ((l xs <> l ys) <> (l zs <> l ws))
  refl

import Data.List.Properties
module List-solver = Data.List.Properties.List-solver
open List-solver using (_⊕_; _⊜_)

crazier-again : ∀ {a} → {A : Set a}
  → (xs : List A)
  → (ys : List A)
  → (zs : List A)
  → (ws : List A)
  → xs ++ (ys ++ zs) ++ ws ≡ (xs ++ ys) ++ (zs ++ ws)
crazier-again = List-solver.solve 4
  (λ xs ys zs ws → xs ⊕ (ys ⊕ zs) ⊕ ws ⊜ (xs ⊕ ys) ⊕ (zs ⊕ ws))
  refl