Group solver

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-05-06.
Last modified on 2024-02-07.

module reflection.group-solver where
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-functions
open import foundation.coproduct-types
open import foundation.decidable-types
open import foundation.identity-types
open import foundation.universe-levels

open import group-theory.groups

open import linear-algebra.vectors

open import lists.concatenation-lists
open import lists.functoriality-lists
open import lists.lists
open import lists.reversing-lists

Idea

This module simplifies group expressions, such that all items associate the same way and removes units and inverses next to the original.

The main entry-point is solveExpr below

data Inductive-Fin : ℕ → UU lzero where
  zero-Inductive-Fin : {n : ℕ} → Inductive-Fin (succ-ℕ n)
  succ-Inductive-Fin : {n : ℕ} → Inductive-Fin n → Inductive-Fin (succ-ℕ n)

finEq : {n : ℕ} → (a b : Inductive-Fin n) → is-decidable (Id a b)
finEq zero-Inductive-Fin zero-Inductive-Fin = inl refl
finEq zero-Inductive-Fin (succ-Inductive-Fin b) = inr (λ ())
finEq (succ-Inductive-Fin a) zero-Inductive-Fin = inr (λ ())
finEq (succ-Inductive-Fin a) (succ-Inductive-Fin b) with finEq a b
... | inl eq = inl (ap succ-Inductive-Fin eq)
... | inr neq = inr (λ where refl → neq refl)

getVec : {n : ℕ} {l : Level} {A : UU l} → vec A n → Inductive-Fin n → A
getVec (x ∷ v) zero-Inductive-Fin = x
getVec (x ∷ v) (succ-Inductive-Fin k) = getVec v k

data GroupSyntax (n : ℕ) : UU where
  gUnit : GroupSyntax n
  gMul : GroupSyntax n → GroupSyntax n → GroupSyntax n
  gInv : GroupSyntax n → GroupSyntax n
  inner : Inductive-Fin n → GroupSyntax n

data SimpleElem (n : ℕ) : UU where
  inv-SE : Inductive-Fin n → SimpleElem n
  pure-SE : Inductive-Fin n → SimpleElem n

inv-SE' : {n : ℕ} → SimpleElem n → SimpleElem n
inv-SE' (inv-SE k) = pure-SE k
inv-SE' (pure-SE k) = inv-SE k

Simple : (n : ℕ) → UU
Simple n = list (SimpleElem n)

module _ {n : ℕ} where
  unquoteSimpleElem : SimpleElem n → GroupSyntax n
  unquoteSimpleElem (inv-SE x) = gInv (inner x)
  unquoteSimpleElem (pure-SE x) = inner x

  unquoteSimpleNonEmpty : Simple n → GroupSyntax n → GroupSyntax n
  unquoteSimpleNonEmpty nil x = x
  unquoteSimpleNonEmpty (cons y xs) x =
    gMul (unquoteSimpleNonEmpty xs (unquoteSimpleElem y)) x

  unquoteSimple : Simple n → GroupSyntax n
  unquoteSimple nil = gUnit
  unquoteSimple (cons x xs) = unquoteSimpleNonEmpty xs (unquoteSimpleElem x)

  elim-inverses : SimpleElem n → Simple n → Simple n
  elim-inverses x nil = cons x nil
  elim-inverses xi@(inv-SE x) yxs@(cons (inv-SE y) xs) = cons xi yxs
  elim-inverses xi@(inv-SE x) yxs@(cons (pure-SE y) xs) with finEq x y
  ... | inl eq = xs
  ... | inr neq = cons xi yxs
  elim-inverses xi@(pure-SE x) yxs@(cons (inv-SE y) xs) with finEq x y
  ... | inl eq = xs
  ... | inr neq = cons xi yxs
  elim-inverses xi@(pure-SE x) yxs@(cons (pure-SE y) xs) = cons xi yxs

  concat-simplify : Simple n → Simple n → Simple n
  concat-simplify nil b = b
  concat-simplify (cons x a) b = elim-inverses x (concat-simplify a b)

  simplifyGS : GroupSyntax n → Simple n
  simplifyGS gUnit = nil
  simplifyGS (gMul a b) = concat-simplify (simplifyGS b) (simplifyGS a)
  simplifyGS (gInv a) = reverse-list (map-list inv-SE' (simplifyGS a))
  -- simplifyGS (gInv a) = map-list inv-SE' (reverse-list (simplifyGS a))
  simplifyGS (inner n) = cons (pure-SE n) nil

  data GroupEqualityElem : GroupSyntax n → GroupSyntax n → UU where
    -- equivalence relation
    xsym-GE :
      {x y : GroupSyntax n} → GroupEqualityElem x y → GroupEqualityElem y x

    -- Variations on ap
    -- xap-gMul :
    --   {x y z w : GroupSyntax n} →
    --   GroupEqualityElem x y → GroupEqualityElem z w →
    --   GroupEqualityElem (gMul x z) (gMul y w)
    xap-gMul-l :
      {x y z : GroupSyntax n} →
      GroupEqualityElem x y → GroupEqualityElem (gMul x z) (gMul y z)
    xap-gMul-r :
      {x y z : GroupSyntax n} →
      GroupEqualityElem y z → GroupEqualityElem (gMul x y) (gMul x z)
    xap-gInv :
      {x y : GroupSyntax n} →
      GroupEqualityElem x y → GroupEqualityElem (gInv x) (gInv y)

    -- Group laws
    xassoc-GE :
      (x y z : GroupSyntax n) →
      GroupEqualityElem (gMul (gMul x y) z) (gMul x (gMul y z))
    xl-unit :
      (x : GroupSyntax n) → GroupEqualityElem (gMul gUnit x) x
    xr-unit :
      (x : GroupSyntax n) → GroupEqualityElem (gMul x gUnit) x
    xl-inv :
      (x : GroupSyntax n) → GroupEqualityElem (gMul (gInv x) x) gUnit
    xr-inv :
      (x : GroupSyntax n) → GroupEqualityElem (gMul x (gInv x)) gUnit

    -- Theorems that are provable from the others
    xinv-unit-GE :
      GroupEqualityElem (gInv gUnit) gUnit
    xinv-inv-GE :
      (x : GroupSyntax n) → GroupEqualityElem (gInv (gInv x)) x
    xdistr-inv-mul-GE :
      (x y : GroupSyntax n) →
      GroupEqualityElem (gInv (gMul x y)) (gMul (gInv y) (gInv x))

  data GroupEquality : GroupSyntax n → GroupSyntax n → UU where
    refl-GE :
      {x : GroupSyntax n} → GroupEquality x x
    _∷GE_ :
      {x y z : GroupSyntax n} →
      GroupEqualityElem x y → GroupEquality y z → GroupEquality x z

  infixr 10 _∷GE_

  module _ where
    -- equivalence relation
    singleton-GE :
      {x y : GroupSyntax n} → GroupEqualityElem x y → GroupEquality x y
    singleton-GE x = x ∷GE refl-GE

    _∙GE_ :
      {x y z : GroupSyntax n} →
      GroupEquality x y → GroupEquality y z → GroupEquality x z
    refl-GE ∙GE b = b
    (x ∷GE a) ∙GE b = x ∷GE (a ∙GE b)
    infixr 15 _∙GE_

    sym-GE : {x y : GroupSyntax n} → GroupEquality x y → GroupEquality y x
    sym-GE refl-GE = refl-GE
    sym-GE (a ∷GE as) = sym-GE as ∙GE singleton-GE (xsym-GE a)

    -- Variations on ap
    ap-gInv :
      {x y : GroupSyntax n} →
      GroupEquality x y → GroupEquality (gInv x) (gInv y)
    ap-gInv refl-GE = refl-GE
    ap-gInv (a ∷GE as) = xap-gInv a ∷GE ap-gInv as

    ap-gMul-l :
      {x y z : GroupSyntax n} →
      GroupEquality x y → GroupEquality (gMul x z) (gMul y z)
    ap-gMul-l refl-GE = refl-GE
    ap-gMul-l (x ∷GE xs) = xap-gMul-l x ∷GE ap-gMul-l xs

    ap-gMul-r :
      {x y z : GroupSyntax n} →
      GroupEquality y z → GroupEquality (gMul x y) (gMul x z)
    ap-gMul-r refl-GE = refl-GE
    ap-gMul-r (x ∷GE xs) = xap-gMul-r x ∷GE ap-gMul-r xs

    ap-gMul :
      {x y z w : GroupSyntax n} →
      GroupEquality x y → GroupEquality z w →
      GroupEquality (gMul x z) (gMul y w)
    ap-gMul p q = ap-gMul-l p ∙GE ap-gMul-r q

    -- Group laws
    assoc-GE :
      (x y z : GroupSyntax n) →
      GroupEquality (gMul (gMul x y) z) (gMul x (gMul y z))
    assoc-GE x y z = singleton-GE (xassoc-GE x y z)

    l-unit :
      (x : GroupSyntax n) → GroupEquality (gMul gUnit x) x
    l-unit x = singleton-GE (xl-unit x)

    r-unit :
      (x : GroupSyntax n) → GroupEquality (gMul x gUnit) x
    r-unit x = singleton-GE (xr-unit x)

    l-inv :
      (x : GroupSyntax n) → GroupEquality (gMul (gInv x) x) gUnit
    l-inv x = singleton-GE (xl-inv x)

    r-inv :
      (x : GroupSyntax n) → GroupEquality (gMul x (gInv x)) gUnit
    r-inv x = singleton-GE (xr-inv x)

    -- Theorems that are provable from the others
    inv-unit-GE : GroupEquality (gInv gUnit) gUnit
    inv-unit-GE = singleton-GE (xinv-unit-GE)

    inv-inv-GE : (x : GroupSyntax n) → GroupEquality (gInv (gInv x)) x
    inv-inv-GE x = singleton-GE (xinv-inv-GE x)

    distr-inv-mul-GE :
      (x y : GroupSyntax n) →
      GroupEquality (gInv (gMul x y)) (gMul (gInv y) (gInv x))
    distr-inv-mul-GE x y = singleton-GE (xdistr-inv-mul-GE x y)

  assoc-GE' :
    (x y z : GroupSyntax n) →
    GroupEquality (gMul x (gMul y z)) (gMul (gMul x y) z)
  assoc-GE' x y z = sym-GE (assoc-GE x y z)

  elim-inverses-remove-valid :
    (b : list (SimpleElem n)) (w u : GroupSyntax n) →
    GroupEquality (gMul w u) gUnit →
    GroupEquality
      ( gMul (unquoteSimpleNonEmpty b w) u)
      ( unquoteSimple b)
  elim-inverses-remove-valid nil w u eq = eq
  elim-inverses-remove-valid (cons x b) w u eq =
    assoc-GE _ _ _ ∙GE
    ap-gMul-r eq ∙GE
    r-unit _

  elim-inverses-valid :
    (x : SimpleElem n) (b : Simple n) →
    GroupEquality
      ( gMul (unquoteSimple b) (unquoteSimpleElem x))
      ( unquoteSimple (elim-inverses x b))
  elim-inverses-valid x nil = l-unit (unquoteSimpleElem x)
  elim-inverses-valid (inv-SE x) (cons (inv-SE y) b) = refl-GE
  elim-inverses-valid (inv-SE x) (cons (pure-SE y) b) with finEq x y
  ... | inl refl =
    elim-inverses-remove-valid b (inner x) (gInv (inner x)) (r-inv (inner x))
  ... | inr neq = refl-GE
  elim-inverses-valid (pure-SE x) (cons (inv-SE y) b) with finEq x y
  ... | inl refl =
    elim-inverses-remove-valid b (gInv (inner x)) (inner x) (l-inv (inner x))
  ... | inr neq = refl-GE
  elim-inverses-valid (pure-SE x) (cons (pure-SE y) b) = refl-GE

  concat-simplify-nonempty-valid :
    (x : SimpleElem n) (a : list (SimpleElem n)) (b : Simple n) →
    GroupEquality
      ( gMul (unquoteSimple b) (unquoteSimple (cons x a)))
      ( unquoteSimple (concat-simplify (cons x a) b))
  concat-simplify-nonempty-valid x nil b = elim-inverses-valid x b
  concat-simplify-nonempty-valid x (cons y a) b =
    assoc-GE' _ _ _ ∙GE
    ap-gMul-l (concat-simplify-nonempty-valid y a b) ∙GE
    elim-inverses-valid x (elim-inverses y (concat-simplify a b))

  concat-simplify-valid :
    (u w : Simple n) →
    GroupEquality
      ( gMul (unquoteSimple w) (unquoteSimple u))
      ( unquoteSimple (concat-simplify u w))
  concat-simplify-valid nil b = r-unit (unquoteSimple b)
  concat-simplify-valid (cons x a) b = concat-simplify-nonempty-valid x a b

  inv-single-valid :
    (w : SimpleElem n) →
    GroupEquality
      ( gInv (unquoteSimpleElem w))
      ( unquoteSimpleElem (inv-SE' w))
  inv-single-valid (inv-SE x) = inv-inv-GE (inner x)
  inv-single-valid (pure-SE x) = refl-GE

  gMul-concat-nonempty :
    (w : GroupSyntax n) (as b : Simple n) →
    GroupEquality
      ( gMul (unquoteSimple b) (unquoteSimpleNonEmpty as w))
      ( unquoteSimpleNonEmpty (concat-list as b) w)
  gMul-concat-nonempty w nil nil = l-unit w
  gMul-concat-nonempty w nil (cons x b) = refl-GE
  gMul-concat-nonempty w (cons x as) b =
    assoc-GE' _ _ _ ∙GE
    ap-gMul-l (gMul-concat-nonempty (unquoteSimpleElem x) as b)

  gMul-concat' :
    (xs : Simple n) (ys : Simple n) →
    GroupEquality
      ( gMul (unquoteSimple ys) (unquoteSimple xs))
      ( unquoteSimple (concat-list xs ys))
  gMul-concat' nil bs = r-unit _
  gMul-concat' (cons x as) b = gMul-concat-nonempty (unquoteSimpleElem x) as b

  gMul-concat-1 :
    (xs : Simple n) (x : SimpleElem n) →
    GroupEquality
      ( gMul (unquoteSimpleElem x) (unquoteSimple xs))
      ( unquoteSimple (concat-list xs (cons x nil)))
  gMul-concat-1 xs a = gMul-concat' xs (cons a nil)

  -- inv-simplify-valid'-nonempty : (x : SimpleElem n) (xs : list (SimpleElem n)) →
  --                               GroupEquality (gInv (unquoteSimple (cons x xs)))
  --                               (unquoteSimple (reverse-list (map-list inv-SE' (cons x xs))))
  -- inv-simplify-valid'-nonempty x nil = inv-single-valid x
  -- inv-simplify-valid'-nonempty x (cons y xs) =
  --   distr-inv-mul-GE (unquoteSimple (cons y xs)) (unquoteSimpleElem x) ∙GE
  --   ap-gMul (inv-single-valid x) (inv-simplify-valid'-nonempty y xs) ∙GE
  --   gMul-concat-1 (concat-list (reverse-list (map-list inv-SE' xs)) (in-list (inv-SE' y))) (inv-SE' x)

  -- inv-simplify-valid' : (w : list (SimpleElem n)) →
  --                     GroupEquality (gInv (unquoteSimple w))
  --                     (unquoteSimple (reverse-list (map-list inv-SE' w)))
  -- inv-simplify-valid' nil = inv-unit-GE
  -- inv-simplify-valid' (cons x xs) =
  --   inv-simplify-valid'-nonempty x xs

  -- simplifyValid : (g : GroupSyntax n) → GroupEquality g (unquoteSimple (simplifyGS g))
  -- simplifyValid gUnit = refl-GE
  -- simplifyValid (gMul a b) =
  --   (ap-gMul (simplifyValid a) (simplifyValid b)) ∙GE
  --   (concat-simplify-valid (simplifyGS b) (simplifyGS a))
  -- simplifyValid (gInv g) = ap-gInv (simplifyValid g) ∙GE inv-simplify-valid' (simplifyGS g)
  -- simplifyValid (inner _) = refl-GE

  Env : {l : Level} → ℕ → UU l → UU l
  Env n A = vec A n

  module _
    {l : Level} (G : Group l)
    where

    unQuoteGS : {n : ℕ} → GroupSyntax n → Env n (type-Group G) → type-Group G
    unQuoteGS gUnit e = unit-Group G
    unQuoteGS (gMul x y) e = mul-Group G (unQuoteGS x e) (unQuoteGS y e)
    unQuoteGS (gInv x) e = inv-Group G (unQuoteGS x e)
    unQuoteGS (inner x) e = getVec e x

    private
      -- Shorter names to make the proofs less verbose
      _*_ = mul-Group G
      infixl 40 _*_
      _⁻¹ = inv-Group G
      infix 45 _⁻¹
      unit = unit-Group G

    useGroupEqualityElem :
      {x y : GroupSyntax n} (env : Env n (type-Group G)) →
      GroupEqualityElem x y → unQuoteGS x env ＝ unQuoteGS y env
    useGroupEqualityElem env (xsym-GE ge) = inv (useGroupEqualityElem env ge)
    useGroupEqualityElem env (xap-gMul-l {z = z} ge') =
      ap (_* unQuoteGS z env) (useGroupEqualityElem env ge')
    useGroupEqualityElem env (xap-gMul-r {x = x} ge') =
      ap (unQuoteGS x env *_) (useGroupEqualityElem env ge')
    -- useGroupEqualityElem env (xap-gMul {y = y} {z = z} ge ge') =
    --                              ap (_* (unQuoteGS z env)) (useGroupEqualityElem env ge)
    --                              ∙ ap (unQuoteGS y env *_) (useGroupEqualityElem env ge')
    useGroupEqualityElem env (xap-gInv ge) =
      ap (inv-Group G) (useGroupEqualityElem env ge)
    useGroupEqualityElem env (xassoc-GE x y z) = associative-mul-Group G _ _ _
    useGroupEqualityElem env (xl-unit _) = left-unit-law-mul-Group G _
    useGroupEqualityElem env (xr-unit _) = right-unit-law-mul-Group G _
    useGroupEqualityElem env (xl-inv x) = left-inverse-law-mul-Group G _
    useGroupEqualityElem env (xr-inv x) = right-inverse-law-mul-Group G _
    useGroupEqualityElem env xinv-unit-GE = inv-unit-Group G
    useGroupEqualityElem env (xinv-inv-GE x) = inv-inv-Group G (unQuoteGS x env)
    useGroupEqualityElem env (xdistr-inv-mul-GE x y) =
      distributive-inv-mul-Group G

    useGroupEquality :
      {x y : GroupSyntax n} (env : Env n (type-Group G)) →
      GroupEquality x y → unQuoteGS x env ＝ unQuoteGS y env
    useGroupEquality env refl-GE = refl
    useGroupEquality env (x ∷GE refl-GE) = useGroupEqualityElem env x
    useGroupEquality env (x ∷GE xs@(_ ∷GE _)) =
      useGroupEqualityElem env x ∙ useGroupEquality env xs

    -- simplifyExpression :
    --   (g : GroupSyntax n) (env : Env n (type-Group G)) →
    --   unQuoteGS g env ＝ unQuoteGS (unquoteSimple (simplifyGS g)) env
    -- simplifyExpression g env = useGroupEquality env (simplifyValid g)

    -- Variadic functions
    n-args : (n : ℕ) (A B : UU) → UU
    n-args zero-ℕ A B = B
    n-args (succ-ℕ n) A B = A → n-args n A B
    map-n-args :
      {A A' B : UU} (n : ℕ) → (A' → A) → n-args n A B → n-args n A' B
    map-n-args zero-ℕ f v = v
    map-n-args (succ-ℕ n) f v = λ x → map-n-args n f (v (f x))
    apply-n-args-fin : {B : UU} (n : ℕ) → n-args n (Inductive-Fin n) B → B
    apply-n-args-fin zero-ℕ f = f
    apply-n-args-fin (succ-ℕ n) f =
      apply-n-args-fin
        ( n)
        ( map-n-args n succ-Inductive-Fin (f zero-Inductive-Fin))
    apply-n-args : {B : UU} (n : ℕ) → n-args n (GroupSyntax n) B → B
    apply-n-args n f = apply-n-args-fin n (map-n-args n inner f)

    -- A variation of simplifyExpression which takes a function from the free variables to expr
    -- simplifyExpr :
    --   (env : Env n (type-Group G)) (g : n-args n (GroupSyntax n) (GroupSyntax n)) →
    --   unQuoteGS (apply-n-args n g) env ＝ unQuoteGS (unquoteSimple (simplifyGS (apply-n-args n g))) env
    -- simplifyExpr env g = simplifyExpression (apply-n-args n g) env

private
    _*'_ : {n : ℕ} → GroupSyntax n → GroupSyntax n → GroupSyntax n
    _*'_ = gMul
    x : GroupSyntax 2
    x = inner (zero-Inductive-Fin)
    y : GroupSyntax 2
    y = inner (succ-Inductive-Fin zero-Inductive-Fin)

    infixl 40 _*'_
    ex1 : GroupEquality {n = 2} (gInv (x *' y *' gInv x *' gInv y)) (y *' x *' gInv y *' gInv x)
    ex1 = simplifyValid _

    ex2 : ∀ x y → (x * y * x ⁻¹ * y ⁻¹) ⁻¹ ＝ (y * x * y ⁻¹ * x ⁻¹)
    ex2 x' y' = simplifyExpression (gInv (x *' y *' gInv x *' gInv y)) (x' ∷ y' ∷ empty-vec)

    _ : UU
    -- _ = {!simplifyValid (y *' (x *' (gInv y *' (gInv x *' gUnit))))!}
    _ = {!ex1!}

    ex3 : ∀ x y → (x * y) ⁻¹ ＝ (y ⁻¹ * x ⁻¹)
    ex3 x' y' = {!simplifyExpression (gInv (x *' y)) (x' ∷ y' ∷ empty-vec)!}

    _ : GroupEquality {n = 2} (y *' (x *' (gInv y *' (gInv x *' gUnit)))) (y *' (x *' (gInv y *' (gInv x *' gUnit))))
    _ = {!simplifyValid (gInv x *' x *' y)!}
    -- _ = {!simplifyValid (gUnit *' gUnit)!}
    -- _ = {!simplifyValid (x *' gUnit)!}

Recent changes