{-# OPTIONS --safe --cubical --postfix-projections #-}

open import Cubical.Algebra.Group

module Groups.Reasoning {β„“} (𝓖 : Group β„“) where

open import Cubical.Foundations.Prelude
open import Groups.Symmetric.Representable
open import Cubical.Foundations.Structure

private
  variable
    β„“β€² : Level

open GroupStr (RSymGroup 𝓖 .snd) using () renaming (_Β·_ to _∘_; 1g to e; inv to _⁻¹; Β·InvR to Β·InvRβ€²; Β·InvL to Β·InvLβ€²)  public

record Expr : Type β„“ where
  field
    before : ⟨ RSymGroup 𝓖 ⟩
    focus : ⟨ RSymGroup 𝓖 ⟩
    after : ⟨ RSymGroup 𝓖 ⟩

  eval : ⟨ RSymGroup 𝓖 ⟩
  eval = before ∘ focus ∘ after

open Expr

_∼_ : (x : ⟨ RSymGroup 𝓖 ⟩) β†’ (y : Expr) β†’ Type β„“
x ∼ y = x ≑ eval y

infix 6 _∘⌊_βŒ‹βˆ˜_ ⌊_βŒ‹ _∘⌊_βŒ‹ ⌊_βŒ‹βˆ˜_ _βˆ˜βŒŠβŒ‹βˆ˜_ βŒŠβŒ‹ _βˆ˜βŒŠβŒ‹ βŒŠβŒ‹βˆ˜_
infix 3 _βˆŽβ€²

_∘⌊_βŒ‹βˆ˜_ : ⟨ RSymGroup 𝓖 ⟩ β†’ ⟨ RSymGroup 𝓖 ⟩ β†’ ⟨ RSymGroup 𝓖 ⟩ β†’ Expr
(g ∘⌊ f βŒ‹βˆ˜ h) .before = g
(g ∘⌊ f βŒ‹βˆ˜ h) .focus = f
(g ∘⌊ f βŒ‹βˆ˜ h) .after = h

⌊_βŒ‹ : ⟨ RSymGroup 𝓖 ⟩ β†’ Expr
⌊ f βŒ‹ = e ∘⌊ f βŒ‹βˆ˜ e

_∘⌊_βŒ‹ : ⟨ RSymGroup 𝓖 ⟩ β†’ ⟨ RSymGroup 𝓖 ⟩ β†’ Expr
g ∘⌊ f βŒ‹ = g ∘⌊ f βŒ‹βˆ˜ e

⌊_βŒ‹βˆ˜_ : ⟨ RSymGroup 𝓖 ⟩ β†’ ⟨ RSymGroup 𝓖 ⟩ β†’ Expr
⌊ f βŒ‹βˆ˜ g = e ∘⌊ f βŒ‹βˆ˜ g

βŒŠβŒ‹ : Expr
βŒŠβŒ‹ = ⌊ e βŒ‹

_βˆ˜βŒŠβŒ‹ : ⟨ RSymGroup 𝓖 ⟩ β†’ Expr
g βˆ˜βŒŠβŒ‹ = g ∘⌊ e βŒ‹

βŒŠβŒ‹βˆ˜_ : ⟨ RSymGroup 𝓖 ⟩ β†’ Expr
βŒŠβŒ‹βˆ˜ g = ⌊ e βŒ‹βˆ˜ g

_βˆ˜βŒŠβŒ‹βˆ˜_ : ⟨ RSymGroup 𝓖 ⟩ β†’ ⟨ RSymGroup 𝓖 ⟩ β†’ Expr
g βˆ˜βŒŠβŒ‹βˆ˜ h = g ∘⌊ e βŒ‹βˆ˜ h

data _IsRelatedTo_ (x : ⟨ RSymGroup 𝓖 ⟩) (y : Expr) : Type β„“ where
  relTo : x ∼ y β†’ x IsRelatedTo y

infix 1 begin_
begin_ : βˆ€ {x y} β†’ x IsRelatedTo y β†’ x ≑ eval y
begin relTo p = p

step-β‰ˆ : βˆ€ x {y z} β†’ y IsRelatedTo z β†’ x ≑ y β†’ x IsRelatedTo z
step-β‰ˆ _ (relTo y∼z) x∼y = relTo (x∼y βˆ™ y∼z)

step-β‰ˆΛ˜ : βˆ€ x {y z} β†’ y IsRelatedTo z β†’ y ≑ x β†’ x IsRelatedTo z
step-β‰ˆΛ˜ _ p q = step-β‰ˆ _ p (sym q)

_βˆŽβ€² : βˆ€ x β†’ x IsRelatedTo ⌊ x βŒ‹
x βˆŽβ€² = relTo refl

replaceFocus : (x : Expr) β†’ (y : ⟨ RSymGroup 𝓖 ⟩) β†’ Expr
replaceFocus x y .before = x .before
replaceFocus x y .focus = y
replaceFocus x y .after = x .after

congExpr : (x : Expr) β†’ {y : ⟨ RSymGroup 𝓖 ⟩} β†’ focus x ≑ y β†’ eval x ∼ (replaceFocus x y)
congExpr x p = cong (Ξ» a β†’ before x ∘ a ∘ after x) p

step-cong-β‰ˆ : βˆ€ x {y z} β†’ (eval (replaceFocus x y)) IsRelatedTo z β†’ focus x ≑ y β†’ eval x IsRelatedTo z
step-cong-β‰ˆ x (relTo p) q = relTo (congExpr x q βˆ™ p)

step-cong-β‰ˆΛ˜ : βˆ€ x {y z} β†’ (eval (replaceFocus x y)) IsRelatedTo z β†’ y ≑ focus x β†’ eval x IsRelatedTo z
step-cong-β‰ˆΛ˜ x (relTo p) q = relTo (congExpr x (sym q) βˆ™ p)

infixr 2 step-β‰ˆ
syntax step-β‰ˆ x rest p = x β‰ˆβŸ¨ p ⟩ rest

infixr 2 step-β‰ˆΛ˜
syntax step-β‰ˆΛ˜ x rest p = x β‰ˆβŸ¨ p ⟩ rest

infixr 2 step-cong-β‰ˆ
syntax step-cong-β‰ˆ x rest p = x β‰ˆβŒŠ p βŒ‹ rest

infixr 2 step-cong-β‰ˆΛ˜
syntax step-cong-β‰ˆΛ˜ x rest p = x β‰ˆΛ˜βŒŠ p βŒ‹ rest

strictify : (P : Group β„“ β†’ Type β„“β€²) β†’ P (RSymGroup 𝓖) β†’ P 𝓖
strictify P p = transport (sym (cong P (inc≑ 𝓖))) p