Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Normal form of FreeGroup #1099

Merged
merged 16 commits into from
Apr 12, 2024
Merged
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions Cubical/Data/List/Properties.agda
Original file line number Diff line number Diff line change
@@ -315,6 +315,11 @@ drop[] : ∀ n → drop {A = A} n [] ≡ []
drop[] zero = refl
drop[] (suc n) = refl

lookupAlways : A → List A → ℕ → A
lookupAlways a [] _ = a
lookupAlways _ (x ∷ _) zero = x
lookupAlways a (x ∷ xs) (suc k) = lookupAlways a xs k

module List₂ where
open import Cubical.HITs.SetTruncation renaming
(rec to rec₂ ; map to map₂ ; elim to elim₂ )
5 changes: 4 additions & 1 deletion Cubical/Reflection/Base.agda
Original file line number Diff line number Diff line change
@@ -19,7 +19,10 @@ _<|>_ = R.catchTC
_>>_ : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → R.TC A → R.TC B → R.TC B
f >> g = f >>= λ _ → g

infixl 4 _>>=_ _>>_ _<|>_
_<$>_ : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → (A → B) → R.TC A → R.TC B
f <$> x = x >>= λ a → R.returnTC (f a)

infixl 4 _>>=_ _>>_ _<|>_ _<$>_

liftTC : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → (A → B) → R.TC A → R.TC B
liftTC f ta = ta >>= λ a → R.returnTC (f a)
24 changes: 21 additions & 3 deletions Cubical/Tactics/GroupSolver/Examples.agda
Original file line number Diff line number Diff line change
@@ -40,10 +40,28 @@ module TestGeneric (G : Group ℓ) (A : Type ℓ) (f : A → ⟨ G ⟩)
-- x₃ = g1





module TestGroupoidπ1 (A : hGroupoid ℓ) (a : ⟨ A ⟩) (p q r s : a ≡ a) where
open import Cubical.Homotopy.Group.Base

-- for now it does not handle "sym", so it is more MonoidSolver at the moment

test : refl ∙ (p ∙ (refl ∙ refl)) ∙ (q ∙ r) ≡ (p ∙ (q ∙ refl)) ∙ (refl ∙ r) ∙ (refl ∙ refl)
test = solveπ₁ (p ∷ q ∷ r ∷ s ∷ []) (hGroupoidπ₁ A a)
test : ((p ∙∙ refl ∙∙ q) ∙ sym s) ∙ sym r ≡
(p ∙ (q ∙ sym (r ∙ s) ∙ p) ∙∙ refl ∙∙ refl) ∙∙ sym p ∙∙ refl
test = π₁solveGroup ⟨ A ⟩ (snd A) a
felixwellen marked this conversation as resolved.
Show resolved Hide resolved


-- testBad : r ∙ q ∙ refl ∙ q ∙ (p ∙ p ∙ (refl ∙ refl)) ∙ (q ∙ r) ∙ q ≡
-- q ∙ sym (p ∙ (p ∙ q ∙ refl)) ∙ (refl) ∙ (refl ∙ refl) ∙ (sym q) ∙ r ∙ s
-- testBad = π₁solveGroup ⟨ A ⟩ (snd A) a

-- prints error msg :
-- -- LHS ≢ RHS

-- -- LHS: (𝒙₀∙(𝒙₁∙(refl∙(𝒙₁∙((𝒙₂∙(𝒙₂∙(refl∙refl)))∙((𝒙₁∙𝒙₀)∙𝒙₁))))))
-- -- RHS: (𝒙₁∙((((𝒙₁⁻¹∙refl)∙'𝒙₂⁻¹)∙'𝒙₂⁻¹)∙(refl∙((refl∙refl)∙(𝒙₁⁻¹∙(𝒙₀∙𝒙₃))))))
-- -- 𝒙₀ = λ i → r i
-- -- 𝒙₁ = λ i → q i
-- -- 𝒙₂ = λ i → p i
-- -- 𝒙₃ = λ i → s i
149 changes: 115 additions & 34 deletions Cubical/Tactics/GroupSolver/GroupExpression.agda
Original file line number Diff line number Diff line change
@@ -5,6 +5,7 @@ module Cubical.Tactics.GroupSolver.GroupExpression where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Function
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Relation.Nullary
open import Cubical.Data.Nat as ℕ hiding (_·_)
open import Cubical.Data.List as Li
@@ -24,6 +25,8 @@ open import Agda.Builtin.String
open import Agda.Builtin.Char
open import Agda.Builtin.Nat

open import Cubical.Homotopy.Group.Base

infixr 40 _<>_

_<>_ = primStringAppend
@@ -32,8 +35,8 @@ private
variable
ℓ : Level

module GE (A : Type) where
data GroupExpr : Type where
module GE (A : Type) where
data GroupExpr : Type where
η : A → GroupExpr
ε : GroupExpr
inv : GroupExpr → GroupExpr
@@ -58,36 +61,119 @@ module GE (A : Type₀) where
term→FG (inv x) = FG.inv (term→FG x)
term→FG (x · x₁) = term→FG x FG.· term→FG x₁

module _ (G : Group ℓ) where

open GroupStr (snd G)

look : List ⟨ G ⟩ → ℕ → ⟨ G ⟩
look [] _ = 1g
look (x ∷ x₂) zero = x
look (x ∷ x₂) (suc k) = look x₂ k
data π₁GroupExpr : Type ℓ where
atomGE : A → π₁GroupExpr
reflGE : π₁GroupExpr
_··_··_ : π₁GroupExpr → π₁GroupExpr → π₁GroupExpr → π₁GroupExpr

module _ (showA : A → String) where
showπ₁GroupExpr : π₁GroupExpr → String
showπ₁GroupExpr (atomGE x) = showA x
showπ₁GroupExpr reflGE = "refl"
showπ₁GroupExpr (reflGE ·· x₁ ·· x₂) =
"(" <> showπ₁GroupExpr x₁ <> "∙" <> showπ₁GroupExpr x₂ <> ")"
showπ₁GroupExpr (x ·· x₁ ·· reflGE) =
"(" <> showπ₁GroupExpr x <> "∙'" <> showπ₁GroupExpr x₁ <> ")"
showπ₁GroupExpr (x ·· x₁ ·· x₂) =
"(" <> showπ₁GroupExpr x <> "∙∙" <> showπ₁GroupExpr x₁ <> "∙∙" <> showπ₁GroupExpr x₂ <> ")"


module _ (A : Type ℓ) where
open GE

termπ₁→GE : π₁GroupExpr (Bool × A) → GroupExpr A
termπ₁→GE (atomGE (b , a)) = if b then (η a) else inv (η a)
termπ₁→GE reflGE = ε
termπ₁→GE (x ·· x₁ ·· x₂) = (termπ₁→GE x · termπ₁→GE x₁) · termπ₁→GE x₂



module Solver (G : Group ℓ) (gs : List ⟨ G ⟩) where

open GroupStr (snd G)

open import Cubical.HITs.FreeGroup

lk = lookupAlways 1g gs

gh = FG.rec {Group = G} lk

[[_]] : freeGroupGroup ℕ .fst → ⟨ G ⟩
[[_]] = fst gh

Solve : (g h : FreeGroup ℕ) → Dec (g ≡ h) → Type ℓ
Solve g h (yes p) = [[ g ]] ≡ [[ h ]]
Solve g h (no ¬p) = Lift (List R.ErrorPart)

module _ (gs : List ⟨ G ⟩) where
lk = look gs
solve' : ∀ g h w → Solve g h w
solve' _ _ (yes p) = cong [[_]] p
solve' _ _ (no ¬p) = lift [ (R.strErr "L≢R") ]

gh = FG.rec {Group = G} lk
solve : ∀ g h → _
solve g h = solve' (GE.term→FG ℕ g) (GE.term→FG ℕ h) (discreteFreeGroup discreteℕ _ _)

[[_]] : freeGroupGroup ℕ .fst → ⟨ G ⟩
[[_]] = fst gh

Solve : (g h : FreeGroup ℕ) → Dec (g ≡ h) → Type ℓ
Solve g h (yes p) = [[ g ]] ≡ [[ h ]]
Solve g h (no ¬p) = Lift (List R.ErrorPart)

solve' : ∀ g h w → Solve g h w
solve' _ _ (yes p) = cong [[_]] p
solve' _ _ (no ¬p) = lift [ (R.strErr "L≢R") ]
-- module _ (A : Type ℓ) (a : A) where
-- open GE

-- termπ₁→Ω : π₁GroupExpr (Bool × (a ≡ a)) → a ≡ a
-- termπ₁→Ω (atomGE (b , p)) = if b then p else (sym p)
-- termπ₁→Ω reflGE = refl
-- termπ₁→Ω (x ·· x₁ ·· x₂) = termπ₁→Ω x ∙∙ termπ₁→Ω x₁ ∙∙ termπ₁→Ω x₂

-- open import Cubical.Homotopy.Group.Base

-- module _ (isGrpA : isGroupoid A) where

-- fromTermπ≡fromTerm∘[[]] : ∀ x → termπ₁→Ω x ≡
-- fst (FG.rec {Group = hGroupoidπ₁ (A , isGrpA) a} (idfun _)) (term→FG _ (termπ₁→GE _ x))
-- fromTermπ≡fromTerm∘[[]] (atomGE (false , snd₁)) = refl
-- fromTermπ≡fromTerm∘[[]] (atomGE (true , snd₁)) = refl
-- fromTermπ≡fromTerm∘[[]] reflGE = refl
-- fromTermπ≡fromTerm∘[[]] (x ·· x₁ ·· x₂) =
-- λ i → doubleCompPath-elim (fromTermπ≡fromTerm∘[[]] x i)
-- (fromTermπ≡fromTerm∘[[]] x₁ i)
-- (fromTermπ≡fromTerm∘[[]] x₂ i) i


module πSolver (A : Type ℓ) (isGroupoidA : isGroupoid A) (a : A) l where

open Solver (hGroupoidπ₁ (A , isGroupoidA) a) l

open GE

termπ₁→Ω : π₁GroupExpr (Bool × ℕ) → a ≡ a
termπ₁→Ω (atomGE (b , k)) = let p = lk k in if b then p else (sym p)
termπ₁→Ω reflGE = refl
termπ₁→Ω (x ·· x₁ ·· x₂) = termπ₁→Ω x ∙∙ termπ₁→Ω x₁ ∙∙ termπ₁→Ω x₂

fromTermπ≡fromTerm∘[[]] : ∀ x → termπ₁→Ω x ≡ [[ (term→FG _ (termπ₁→GE _ x)) ]]
fromTermπ≡fromTerm∘[[]] (atomGE (false , snd₁)) = refl
fromTermπ≡fromTerm∘[[]] (atomGE (true , snd₁)) = refl
fromTermπ≡fromTerm∘[[]] reflGE = refl
fromTermπ≡fromTerm∘[[]] (x ·· x₁ ·· x₂) =
λ i → doubleCompPath-elim (fromTermπ≡fromTerm∘[[]] x i)
(fromTermπ≡fromTerm∘[[]] x₁ i)
(fromTermπ≡fromTerm∘[[]] x₂ i) i


Solveπ : (g h : π₁GroupExpr (Bool × ℕ)) → Dec (term→FG _ (termπ₁→GE _ g) ≡ term→FG _ (termπ₁→GE _ h)) → Type ℓ
Solveπ g h (yes p) = termπ₁→Ω g ≡ termπ₁→Ω h
Solveπ g h (no ¬p) = Lift (List R.ErrorPart)

solveπ' : ∀ g h w → Solveπ g h w
solveπ' g h (yes p) =
fromTermπ≡fromTerm∘[[]] g
∙∙ cong [[_]] p
∙∙ sym (fromTermπ≡fromTerm∘[[]] h)
solveπ' _ _ (no ¬p) = lift [ (R.strErr "L≢R") ]

solveπ : ∀ g h → _
solveπ g h = solveπ' g h (discreteFreeGroup discreteℕ _ _)

solve : ∀ g h → _
solve g h = solve' (GE.term→FG ℕ g) (GE.term→FG ℕ h) (discreteFreeGroup discreteℕ _ _)


module _ (A : Type) (_≟_ : Discrete A) where
@@ -107,25 +193,21 @@ module _ (A : Type) (_≟_ : Discrete A) where


digitsToSubscripts : Char → Char
digitsToSubscripts '0' = '₀'
digitsToSubscripts '1' = '₁'
digitsToSubscripts '2' = '₂'
digitsToSubscripts '3' = '₃'
digitsToSubscripts '4' = '₄'
digitsToSubscripts '5' = '₅'
digitsToSubscripts '6' = '₆'
digitsToSubscripts '7' = '₇'
digitsToSubscripts '8' = '₈'
digitsToSubscripts '9' = '₉'
digitsToSubscripts x = x
digitsToSubscripts = λ where
'0' → '₀' ; '1' → '₁' ; '2' → '₂' ; '3' → '₃' ; '4' → '₄' ; '5' → '₅'
'6' → '₆' ; '7' → '₇' ; '8' → '₈' ; '9' → '₉' ; x → x

mkNiceVar : ℕ → String
mkNiceVar k = "x" <>
mkNiceVar k = "𝒙" <>
primStringFromList (Li.map digitsToSubscripts $ primStringToList $ primShowNat k)

showGEℕ = GE.showGroupExpr ℕ primShowNat
showNormalizedGEℕ = GE.showGroupExpr ℕ mkNiceVar ∘ normalizeGroupExpr ℕ discreteℕ

showπ₁GEℕ = GE.showπ₁GroupExpr (Bool × ℕ)
λ (b , i) →
let v = mkNiceVar i
in if b then v else (v <> "⁻¹")

travGroupExprTC : {A B : Type₀} → (f : A → R.TC B) →
GE.GroupExpr A → R.TC (GE.GroupExpr B)
@@ -136,4 +218,3 @@ travGroupExprTC f = w
w GE.ε = R.returnTC GE.ε
w (GE.inv x) = w x >>= R.returnTC ∘ GE.inv
w (x GE.· x₁) = do x' ← w x ; x₁' ← w x₁ ; R.returnTC (x' GE.· x₁')

10 changes: 8 additions & 2 deletions Cubical/Tactics/GroupSolver/Reflection.agda
Original file line number Diff line number Diff line change
@@ -87,9 +87,15 @@ match2Vargs (varg t1 ∷ varg t2 ∷ []) = R.returnTC (t1 , t2)
match2Vargs _ = R.typeError []


match3Vargs : List (R.Arg R.Term) → R.TC (R.Term × R.Term × R.Term)
match3Vargs (harg _ ∷ xs) = match3Vargs xs
match3Vargs (varg t1 ∷ varg t2 ∷ varg t3 ∷ []) = R.returnTC (t1 , t2 , t3)
match3Vargs _ = R.typeError []

inferEnds : R.Term → R.Term → R.TC (R.Type × (R.Term × R.Term))
inferEnds tG hole = do


inferEnds : R.Term → R.TC (R.Type × (R.Term × R.Term))
inferEnds hole = do
ty ← R.inferType hole
(eTy , (e0 , e1)) ← pathTypeView ty
blockIfContainsMeta e0
Loading