module Algebra.Group.Solver where
open import 1Lab.Prelude
open import Data.List hiding (lookup)
open import Data.Fin
open import Data.Nat
open import Data.Dec
open import Algebra.Group.Cat.Base
open import Algebra.Group
open import 1Lab.Reflection
open import 1Lab.Reflection.Solver
open import 1Lab.Reflection.Variables
module _ {ℓ} {A : Type ℓ} (G : Group-on A) where
open Group-on G
data Expr (n : Nat) : Type ℓ where
_‶⋆‶_ : (e1 : Expr n) → (e2 : Expr n) → Expr n
‶unit‶ : Expr n
_‶⁻¹‶ : (e : Expr n) → Expr n
‶_‶ : Fin n → Expr n
private variable
n : Nat
⟦_⟧ₑ : Expr n → Vec A n → A
⟦ e1 ‶⋆‶ e2 ⟧ₑ ρ = ⟦ e1 ⟧ₑ ρ ⋆ ⟦ e2 ⟧ₑ ρ
⟦ ‶unit‶ ⟧ₑ ρ = unit
⟦ e ‶⁻¹‶ ⟧ₑ ρ = ⟦ e ⟧ₑ ρ ⁻¹
⟦ ‶ x ‶ ⟧ₑ ρ = lookup ρ x
data Value (n : Nat) : Type where
vunit : Value n
vmul : Fin n → Value n → Value n
vmul⁻¹ : Fin n → Value n → Value n
⟦_⟧ᵥ : Value n → Vec A n → A
⟦ vunit ⟧ᵥ ρ = unit
⟦ vmul x v ⟧ᵥ ρ = lookup ρ x ⋆ ⟦ v ⟧ᵥ ρ
⟦ vmul⁻¹ x v ⟧ᵥ ρ = lookup ρ x ⁻¹ ⋆ ⟦ v ⟧ᵥ ρ
push : Fin n → Value n → Value n
push n (vmul⁻¹ n' v) with n ≡? n'
... | yes _ = v
... | no _ = vmul n (vmul⁻¹ n' v)
push n v = vmul n v
push-inv : Fin n → Value n → Value n
push-inv n (vmul n' v) with n ≡? n'
... | yes _ = v
... | no _ = vmul⁻¹ n (vmul n' v)
push-inv n v = vmul⁻¹ n v
do-mul : Value n → Value n → Value n
do-mul vunit v2 = v2
do-mul (vmul x v1) v2 = push x (do-mul v1 v2)
do-mul (vmul⁻¹ x v1) v2 = push-inv x (do-mul v1 v2)
do-inv-aux : Value n → Value n → Value n
do-inv-aux vunit acc = acc
do-inv-aux (vmul x v) acc = do-inv-aux v (vmul⁻¹ x acc)
do-inv-aux (vmul⁻¹ x v) acc = do-inv-aux v (vmul x acc)
do-inv : Value n → Value n
do-inv v = do-inv-aux v vunit
eval : Expr n → Value n
eval (e1 ‶⋆‶ e2) = do-mul (eval e1) (eval e2)
eval ‶unit‶ = vunit
eval (e ‶⁻¹‶) = do-inv (eval e)
eval ‶ x ‶ = vmul x vunit
push-sound : ∀ x v → (ρ : Vec A n) → ⟦ push x v ⟧ᵥ ρ ≡ lookup ρ x ⋆ ⟦ v ⟧ᵥ ρ
push-sound x vunit ρ = refl
push-sound x (vmul x' v) ρ = refl
push-sound x (vmul⁻¹ x' v) ρ with x ≡? x'
... | yes x≡x' =
⟦ v ⟧ᵥ ρ ≡˘⟨ idl ⟩
unit ⋆ ⟦ v ⟧ᵥ ρ ≡˘⟨ ap (_⋆ ⟦ v ⟧ᵥ ρ) inverser ⟩
(lookup ρ x ⋆ (lookup ρ x) ⁻¹) ⋆ ⟦ v ⟧ᵥ ρ ≡⟨ ap (λ ϕ → (lookup ρ x ⋆ (lookup ρ ϕ) ⁻¹) ⋆ ⟦ v ⟧ᵥ ρ) x≡x' ⟩
(lookup ρ x ⋆ lookup ρ x' ⁻¹) ⋆ ⟦ v ⟧ᵥ ρ ≡˘⟨ associative ⟩
lookup ρ x ⋆ (lookup ρ x') ⁻¹ ⋆ ⟦ v ⟧ᵥ ρ ∎
... | no _ = refl
push-inv-sound : ∀ x v → (ρ : Vec A n) → ⟦ push-inv x v ⟧ᵥ ρ ≡ lookup ρ x ⁻¹ ⋆ ⟦ v ⟧ᵥ ρ
push-inv-sound x vunit ρ = refl
push-inv-sound x (vmul x' v) ρ with x ≡? x'
... | yes x≡x' =
⟦ v ⟧ᵥ ρ ≡˘⟨ idl ⟩
(unit ⋆ ⟦ v ⟧ᵥ ρ) ≡˘⟨ ap (_⋆ ⟦ v ⟧ᵥ ρ) inversel ⟩
((lookup ρ x) ⁻¹ ⋆ lookup ρ x) ⋆ ⟦ v ⟧ᵥ ρ ≡⟨ ap (λ ϕ → ((lookup ρ x) ⁻¹ ⋆ lookup ρ ϕ) ⋆ ⟦ v ⟧ᵥ ρ) x≡x' ⟩
(lookup ρ x ⁻¹ ⋆ lookup ρ x') ⋆ ⟦ v ⟧ᵥ ρ ≡˘⟨ associative ⟩
(lookup ρ x) ⁻¹ ⋆ lookup ρ x' ⋆ ⟦ v ⟧ᵥ ρ ∎
... | no _ = refl
push-inv-sound x (vmul⁻¹ x' v) ρ = refl
do-mul-sound : ∀ v1 v2 → (ρ : Vec A n) → ⟦ do-mul v1 v2 ⟧ᵥ ρ ≡ ⟦ v1 ⟧ᵥ ρ ⋆ ⟦ v2 ⟧ᵥ ρ
do-mul-sound vunit v2 ρ = sym idl
do-mul-sound (vmul x v1) v2 ρ =
⟦ push x (do-mul v1 v2) ⟧ᵥ ρ ≡⟨ push-sound x (do-mul v1 v2) ρ ⟩
lookup ρ x ⋆ ⟦ do-mul v1 v2 ⟧ᵥ ρ ≡⟨ ap (lookup ρ x ⋆_) (do-mul-sound v1 v2 ρ) ⟩
lookup ρ x ⋆ ⟦ v1 ⟧ᵥ ρ ⋆ ⟦ v2 ⟧ᵥ ρ ≡⟨ associative ⟩
(lookup ρ x ⋆ ⟦ v1 ⟧ᵥ ρ) ⋆ ⟦ v2 ⟧ᵥ ρ ∎
do-mul-sound (vmul⁻¹ x v1) v2 ρ =
⟦ push-inv x (do-mul v1 v2) ⟧ᵥ ρ ≡⟨ push-inv-sound x (do-mul v1 v2) ρ ⟩
lookup ρ x ⁻¹ ⋆ ⟦ do-mul v1 v2 ⟧ᵥ ρ ≡⟨ ap (lookup ρ x ⁻¹ ⋆_) (do-mul-sound v1 v2 ρ) ⟩
lookup ρ x ⁻¹ ⋆ ⟦ v1 ⟧ᵥ ρ ⋆ ⟦ v2 ⟧ᵥ ρ ≡⟨ associative ⟩
(lookup ρ x ⁻¹ ⋆ ⟦ v1 ⟧ᵥ ρ) ⋆ ⟦ v2 ⟧ᵥ ρ ∎
do-inv-aux-mul : ∀ v1 x v2 → (ρ : Vec A n) → ⟦ do-inv-aux v1 (vmul x v2) ⟧ᵥ ρ ≡ ⟦ v1 ⟧ᵥ ρ ⁻¹ ⋆ lookup ρ x ⋆ ⟦ v2 ⟧ᵥ ρ
do-inv-aux-mul⁻¹ : ∀ v1 x v2 → (ρ : Vec A n) → ⟦ do-inv-aux v1 (vmul⁻¹ x v2) ⟧ᵥ ρ ≡ ⟦ v1 ⟧ᵥ ρ ⁻¹ ⋆ lookup ρ x ⁻¹ ⋆ ⟦ v2 ⟧ᵥ ρ
do-inv-aux-mul vunit x v2 ρ =
lookup ρ x ⋆ ⟦ v2 ⟧ᵥ ρ ≡˘⟨ idl ⟩
unit ⋆ lookup ρ x ⋆ ⟦ v2 ⟧ᵥ ρ ≡˘⟨ ap (_⋆ lookup ρ x ⋆ ⟦ v2 ⟧ᵥ ρ) inv-unit ⟩
unit ⁻¹ ⋆ lookup ρ x ⋆ ⟦ v2 ⟧ᵥ ρ ∎
do-inv-aux-mul (vmul x' v1) x v2 ρ =
⟦ do-inv-aux v1 (vmul⁻¹ x' (vmul x v2)) ⟧ᵥ ρ ≡⟨ do-inv-aux-mul⁻¹ v1 x' (vmul x v2) ρ ⟩
(⟦ v1 ⟧ᵥ ρ) ⁻¹ ⋆ (lookup ρ x') ⁻¹ ⋆ lookup ρ x ⋆ ⟦ v2 ⟧ᵥ ρ ≡⟨ associative ⟩
((⟦ v1 ⟧ᵥ ρ) ⁻¹ ⋆ (lookup ρ x') ⁻¹) ⋆ lookup ρ x ⋆ ⟦ v2 ⟧ᵥ ρ ≡˘⟨ ap (_⋆ lookup ρ x ⋆ ⟦ v2 ⟧ᵥ ρ) inv-comm ⟩
(lookup ρ x' ⋆ ⟦ v1 ⟧ᵥ ρ) ⁻¹ ⋆ lookup ρ x ⋆ ⟦ v2 ⟧ᵥ ρ ∎
do-inv-aux-mul (vmul⁻¹ x' v1) x v2 ρ =
⟦ do-inv-aux v1 (vmul x' (vmul x v2)) ⟧ᵥ ρ ≡⟨ do-inv-aux-mul v1 x' (vmul x v2) ρ ⟩
⟦ v1 ⟧ᵥ ρ ⁻¹ ⋆ lookup ρ x' ⋆ lookup ρ x ⋆ ⟦ v2 ⟧ᵥ ρ ≡˘⟨ ap (λ ϕ → ⟦ v1 ⟧ᵥ ρ ⁻¹ ⋆ ϕ ⋆ lookup ρ x ⋆ ⟦ v2 ⟧ᵥ ρ) inv-inv ⟩
⟦ v1 ⟧ᵥ ρ ⁻¹ ⋆ lookup ρ x' ⁻¹ ⁻¹ ⋆ lookup ρ x ⋆ ⟦ v2 ⟧ᵥ ρ ≡⟨ associative ⟩
(⟦ v1 ⟧ᵥ ρ ⁻¹ ⋆ lookup ρ x' ⁻¹ ⁻¹) ⋆ lookup ρ x ⋆ ⟦ v2 ⟧ᵥ ρ ≡˘⟨ ap (_⋆ lookup ρ x ⋆ ⟦ v2 ⟧ᵥ ρ) inv-comm ⟩
(lookup ρ x' ⁻¹ ⋆ ⟦ v1 ⟧ᵥ ρ) ⁻¹ ⋆ lookup ρ x ⋆ ⟦ v2 ⟧ᵥ ρ ∎
do-inv-aux-mul⁻¹ vunit x v2 ρ =
lookup ρ x ⁻¹ ⋆ ⟦ v2 ⟧ᵥ ρ ≡˘⟨ idl ⟩
unit ⋆ lookup ρ x ⁻¹ ⋆ ⟦ v2 ⟧ᵥ ρ ≡˘⟨ ap (_⋆ lookup ρ x ⁻¹ ⋆ ⟦ v2 ⟧ᵥ ρ) inv-unit ⟩
unit ⁻¹ ⋆ lookup ρ x ⁻¹ ⋆ ⟦ v2 ⟧ᵥ ρ ∎
do-inv-aux-mul⁻¹ (vmul x' v1) x v2 ρ =
⟦ do-inv-aux v1 (vmul⁻¹ x' (vmul⁻¹ x v2)) ⟧ᵥ ρ ≡⟨ do-inv-aux-mul⁻¹ v1 x' (vmul⁻¹ x v2) ρ ⟩
⟦ v1 ⟧ᵥ ρ ⁻¹ ⋆ lookup ρ x' ⁻¹ ⋆ lookup ρ x ⁻¹ ⋆ ⟦ v2 ⟧ᵥ ρ ≡⟨ associative ⟩
(⟦ v1 ⟧ᵥ ρ ⁻¹ ⋆ lookup ρ x' ⁻¹) ⋆ lookup ρ x ⁻¹ ⋆ ⟦ v2 ⟧ᵥ ρ ≡˘⟨ ap (_⋆ lookup ρ x ⁻¹ ⋆ ⟦ v2 ⟧ᵥ ρ) inv-comm ⟩
(lookup ρ x' ⋆ ⟦ v1 ⟧ᵥ ρ) ⁻¹ ⋆ lookup ρ x ⁻¹ ⋆ ⟦ v2 ⟧ᵥ ρ ∎
do-inv-aux-mul⁻¹ (vmul⁻¹ x' v1) x v2 ρ =
⟦ do-inv-aux v1 (vmul x' (vmul⁻¹ x v2)) ⟧ᵥ ρ ≡⟨ do-inv-aux-mul v1 x' (vmul⁻¹ x v2) ρ ⟩
⟦ v1 ⟧ᵥ ρ ⁻¹ ⋆ lookup ρ x' ⋆ lookup ρ x ⁻¹ ⋆ ⟦ v2 ⟧ᵥ ρ ≡˘⟨ ap (λ ϕ → ⟦ v1 ⟧ᵥ ρ ⁻¹ ⋆ ϕ ⋆ lookup ρ x ⁻¹ ⋆ ⟦ v2 ⟧ᵥ ρ) inv-inv ⟩
⟦ v1 ⟧ᵥ ρ ⁻¹ ⋆ lookup ρ x' ⁻¹ ⁻¹ ⋆ lookup ρ x ⁻¹ ⋆ ⟦ v2 ⟧ᵥ ρ ≡⟨ associative ⟩
(⟦ v1 ⟧ᵥ ρ ⁻¹ ⋆ lookup ρ x' ⁻¹ ⁻¹) ⋆ lookup ρ x ⁻¹ ⋆ ⟦ v2 ⟧ᵥ ρ ≡˘⟨ ap (_⋆ lookup ρ x ⁻¹ ⋆ ⟦ v2 ⟧ᵥ ρ) inv-comm ⟩
(lookup ρ x' ⁻¹ ⋆ ⟦ v1 ⟧ᵥ ρ) ⁻¹ ⋆ lookup ρ x ⁻¹ ⋆ ⟦ v2 ⟧ᵥ ρ ∎
do-inv-sound : ∀ v → (ρ : Vec A n) → ⟦ do-inv v ⟧ᵥ ρ ≡ ⟦ v ⟧ᵥ ρ ⁻¹
do-inv-sound vunit ρ = sym inv-unit
do-inv-sound (vmul x v) ρ =
⟦ do-inv-aux v (vmul⁻¹ x vunit) ⟧ᵥ ρ ≡⟨ do-inv-aux-mul⁻¹ v x vunit ρ ⟩
⟦ v ⟧ᵥ ρ ⁻¹ ⋆ lookup ρ x ⁻¹ ⋆ unit ≡⟨ ap (⟦ v ⟧ᵥ ρ ⁻¹ ⋆_) idr ⟩
⟦ v ⟧ᵥ ρ ⁻¹ — lookup ρ x ≡˘⟨ inv-comm ⟩
(lookup ρ x ⋆ ⟦ v ⟧ᵥ ρ) ⁻¹ ∎
do-inv-sound (vmul⁻¹ x v) ρ =
⟦ do-inv-aux v (vmul x vunit) ⟧ᵥ ρ ≡⟨ do-inv-aux-mul v x vunit ρ ⟩
⟦ v ⟧ᵥ ρ ⁻¹ ⋆ lookup ρ x ⋆ unit ≡⟨ ap (⟦ v ⟧ᵥ ρ ⁻¹ ⋆_) idr ⟩
⟦ v ⟧ᵥ ρ ⁻¹ ⋆ lookup ρ x ≡˘⟨ ap (⟦ v ⟧ᵥ ρ ⁻¹ ⋆_) inv-inv ⟩
⟦ v ⟧ᵥ ρ ⁻¹ ⋆ (lookup ρ x ⁻¹) ⁻¹ ≡˘⟨ inv-comm ⟩
((lookup ρ x) ⁻¹ ⋆ ⟦ v ⟧ᵥ ρ) ⁻¹ ∎
eval-sound : ∀ e → (ρ : Vec A n) → ⟦ eval e ⟧ᵥ ρ ≡ ⟦ e ⟧ₑ ρ
eval-sound (e1 ‶⋆‶ e2) ρ =
⟦ do-mul (eval e1) (eval e2) ⟧ᵥ ρ ≡⟨ do-mul-sound (eval e1) (eval e2) ρ ⟩
⟦ eval e1 ⟧ᵥ ρ ⋆ ⟦ eval e2 ⟧ᵥ ρ ≡⟨ ap₂ _⋆_ (eval-sound e1 ρ) (eval-sound e2 ρ) ⟩
⟦ e1 ⟧ₑ ρ ⋆ ⟦ e2 ⟧ₑ ρ ∎
eval-sound ‶unit‶ ρ = refl
eval-sound (e ‶⁻¹‶) ρ =
⟦ do-inv (eval e) ⟧ᵥ ρ ≡⟨ do-inv-sound (eval e) ρ ⟩
⟦ eval e ⟧ᵥ ρ ⁻¹ ≡⟨ ap (_⁻¹) (eval-sound e ρ) ⟩
⟦ e ⟧ₑ ρ ⁻¹ ∎
eval-sound ‶ x ‶ ρ = idr
abstract
solve : (e1 e2 : Expr n) → (ρ : Vec A n) → ⟦ eval e1 ⟧ᵥ ρ ≡ ⟦ eval e2 ⟧ᵥ ρ → ⟦ e1 ⟧ₑ ρ ≡ ⟦ e2 ⟧ₑ ρ
solve e1 e2 ρ p = sym (eval-sound e1 ρ) ·· p ·· eval-sound e2 ρ
expand : (e : Expr n) → Vec A n → A
expand e ρ = ⟦ eval e ⟧ᵥ ρ
module Reflection where
pattern is-group-args args = (_ hm∷ _ hm∷ _ hm∷ _ v∷ args)
pattern group-args args = (_ hm∷ _ hm∷ _ v∷ args)
pattern “unit” = def (quote is-group.unit) (is-group-args [])
pattern “⋆” x y = def (quote Group-on._⋆_) (group-args (x v∷ y v∷ []))
pattern “inverse” x = def (quote is-group.inverse) (is-group-args (x v∷ []))
mk-group-args : Term → List (Arg Term) → List (Arg Term)
mk-group-args grp args = unknown h∷ unknown h∷ grp v∷ args
“solve” : Term → Term → Term → Term → Term
“solve” grp lhs rhs env = def (quote solve) (mk-group-args grp $ lhs v∷ rhs v∷ env v∷ def (quote refl) [] v∷ [])
“expand” : Term → Term → Term → Term
“expand” grp e env = def (quote expand) (mk-group-args grp $ e v∷ env v∷ [])
build-expr : ∀ {ℓ} {A : Type ℓ} → Variables A → Term → TC (Term × Variables A)
build-expr vs “unit” =
pure $ con (quote ‶unit‶) [] , vs
build-expr vs (“⋆” t1 t2) = do
e1 , vs ← build-expr vs t1
e2 , vs ← build-expr vs t2
pure $ con (quote _‶⋆‶_) (e1 v∷ e2 v∷ []) , vs
build-expr vs (“inverse” t) = do
e , vs ← build-expr vs t
pure $ con (quote _‶⁻¹‶) (e v∷ []) , vs
build-expr vs tm = do
(v , vs) ← bind-var vs tm
pure $ con (quote ‶_‶) (v v∷ []) , vs
dont-reduce : List Name
dont-reduce = quote is-group.unit ∷ quote Group-on._⋆_ ∷ quote is-group.inverse ∷ []
group-solver : ∀ {ℓ} {A : Type ℓ} → Group-on A → TC (VariableSolver A)
group-solver {A = A} grp = do
grp-tm ← quoteTC grp
pure (var-solver {A = A} dont-reduce build-expr (“solve” grp-tm) (“expand” grp-tm))
repr-macro : ∀ {ℓ} {A : Type ℓ} → Group-on A → Term → Term → TC ⊤
repr-macro {A = A} grp tm hole = do
solver ← group-solver grp
mk-var-repr solver tm
expand-macro : ∀ {ℓ} {A : Type ℓ} → Group-on A → Term → Term → TC ⊤
expand-macro {A = A} grp tm hole = do
solver ← group-solver grp
mk-var-normalise solver tm hole
solve-macro : ∀ {ℓ} {A : Type ℓ} → Group-on A → Term → TC ⊤
solve-macro {A = A} grp hole = do
solver ← group-solver grp
mk-var-solver solver hole
macro
repr-group! : ∀ {ℓ} → Group ℓ → Term → Term → TC ⊤
repr-group! (_ , grp) tm = Reflection.repr-macro grp tm
simpl-group! : ∀ {ℓ} → Group ℓ → Term → Term → TC ⊤
simpl-group! (_ , grp) tm = Reflection.expand-macro grp tm
group-on! : ∀ {ℓ} {A : Type ℓ} → Group-on A → Term → TC ⊤
group-on! grp = Reflection.solve-macro grp
group! : ∀ {ℓ} → Group ℓ → Term → TC ⊤
group! (_ , grp) = Reflection.solve-macro grp
private module TestGroup-on {ℓ} {A : Type ℓ} (grp : Group-on A) where
open Group-on grp
test : ∀ (x y : A) → (x ⋆ inverse y) ⋆ y ⋆ y ≡ x ⋆ (unit ⋆ y)
test x y = group-on! grp
private module TestGroup {ℓ} (grp : Group ℓ) where
A : Type ℓ
A = ⌞ grp ⌟
open Group-on (snd grp)
test : ∀ (x y : A) → (x ⋆ inverse y) ⋆ y ⋆ y ≡ x ⋆ (unit ⋆ y)
test x y = group! grp