WildCat, Groupoid, Group - Solvers

Cubical/Categories/Category/Base.agda

@@ -161,3 +161,19 @@ isIsoΣPropCat : {C : Category ℓ ℓ'} {P : ℙ (ob C)}
 inv (isIsoΣPropCat p q f isIsoF) = isIsoF .inv
 sec (isIsoΣPropCat p q f isIsoF) = isIsoF .sec
 ret (isIsoΣPropCat p q f isIsoF) = isIsoF .ret
+
+IsGroupoidCat : (C : Category ℓ ℓ') → Type (ℓ-max ℓ ℓ')
+IsGroupoidCat C = ∀ {x} {y} (f : C [ x , y ]) → isIso C f
+
+IsPropIsGroupoidCat : (C : Category ℓ ℓ') → isProp (IsGroupoidCat C)
+IsPropIsGroupoidCat C =
+ isPropImplicitΠ2 λ _ _ → isPropΠ isPropIsIso
+
+record GroupoidCat ℓ ℓ' : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
+ field
+  category : Category ℓ ℓ'
+  isGroupoidCat : IsGroupoidCat category
+
+
+ _⁻¹ : ∀ {x y} → category [ x , y ] → category [ y , x ]
+ f ⁻¹ = isIso.inv (isGroupoidCat f)

Cubical/Data/Bool/Properties.agda

@@ -324,6 +324,10 @@ Dec→DecBool (no ¬p) q = Empty.rec (¬p q)
 DecBool→Dec : {P : Type ℓ} → (dec : Dec P) → Bool→Type (Dec→Bool dec) → P
 DecBool→Dec (yes p) _ = p
 
+Bool→Type-not-⊕ : ∀ {x y} → Bool→Type (not (x ⊕ y)) → Bool→Type x →  Bool→Type y
+Bool→Type-not-⊕ {false} {false} _ ()
+Bool→Type-not-⊕ {true} {true} _ = _
+
 Dec≃DecBool : {P : Type ℓ} → (h : isProp P)(dec : Dec P) → P ≃ Bool→Type (Dec→Bool dec)
 Dec≃DecBool h dec = propBiimpl→Equiv h isPropBool→Type (Dec→DecBool dec) (DecBool→Dec dec)
 

Cubical/Data/List/Properties.agda

@@ -179,3 +179,16 @@ length-map : ∀ {ℓA ℓB} {A : Type ℓA} {B : Type ℓB} → (f : A → B) 
   → length (map f as) ≡ length as
 length-map f [] = refl
 length-map f (a ∷ as) = cong suc (length-map f as)
+
+lookupWithDefault : A → List A → ℕ → A
+lookupWithDefault a [] _ = a
+lookupWithDefault _ (x ∷ _) zero = x
+lookupWithDefault a (x ∷ xs) (suc k) = lookupWithDefault a xs k
+
+intersperse : A → List A → List A
+intersperse _ [] = []
+intersperse a (x ∷ xs) = x ∷ a ∷ intersperse a xs
+
+join : List (List A) → List A
+join [] = []
+join (x ∷ xs) = x ++ join xs

Cubical/Data/Maybe/Base.agda

@@ -28,3 +28,6 @@ rec n j (just a) = j a
 elim : ∀ {A : Type ℓA} (B : Maybe A → Type ℓB) → B nothing → ((x : A) → B (just x)) → (mx : Maybe A) → B mx
 elim B n j nothing = n
 elim B n j (just a) = j a
+
+fromMaybe : A → Maybe A → A
+fromMaybe x = rec x (λ x → x)

Cubical/Data/Maybe/Properties.agda

@@ -179,3 +179,13 @@ congMaybeEquiv e = isoToEquiv isom
   isom .rightInv (just b) = cong just (secEq e b)
   isom .leftInv nothing = refl
   isom .leftInv (just a) = cong just (retEq e a)
+
+bind : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
+          → Maybe A → (A → Maybe B) → Maybe B
+bind nothing _ = nothing
+bind (just x) x₁ = x₁ x
+
+map2-Maybe : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''}
+          → (A → B → C) → Maybe A → Maybe B → Maybe C
+map2-Maybe _ nothing _ = nothing
+map2-Maybe f (just x) = map-Maybe (f x)

Cubical/Data/Sigma/Properties.agda

@@ -52,6 +52,9 @@ map-snd f (a , b) = (a , f b)
 map-× : {B : Type ℓ} {B' : Type ℓ'} → (A → A') → (B → B') → A × B → A' × B'
 map-× f g (a , b) = (f a , g b)
 
+map-both : (A → A') → A × A → A' × A'
+map-both f = map-× f f
+
 ≡-× : {A : Type ℓ} {B : Type ℓ'} {x y : A × B} → fst x ≡ fst y → snd x ≡ snd y → x ≡ y
 ≡-× p q i = (p i) , (q i)
 

Cubical/Reflection/Base.agda

@@ -32,6 +32,8 @@ pattern harg {q = q} t = R.arg (R.arg-info R.hidden (R.modality R.relevant q)) t
 pattern _v∷_ a l = varg a ∷ l
 pattern _h∷_ a l = harg a ∷ l
 
+pattern v[_] a = varg a ∷ []
+
 infixr 5 _v∷_ _h∷_
 
 vlam : String → R.Term → R.Term

Cubical/Relation/Binary/Base.agda

@@ -65,6 +65,9 @@ module BinaryRelation {ℓ ℓ' : Level} {A : Type ℓ} (R : Rel A A ℓ') where
   isSym : Type (ℓ-max ℓ ℓ')
   isSym = (a b : A) → R a b → R b a
 
+  isSym' : Type (ℓ-max ℓ ℓ')
+  isSym' = {a b : A} → R a b → R b a
+
   isAsym : Type (ℓ-max ℓ ℓ')
   isAsym = (a b : A) → R a b → ¬ R b a
 
@@ -141,6 +144,15 @@ module BinaryRelation {ℓ ℓ' : Level} {A : Type ℓ} (R : Rel A A ℓ') where
       symmetric : isSym
       transitive : isTrans
 
+    reflexive' : isRefl'
+    reflexive' = reflexive _
+
+    symmetric' : isSym'
+    symmetric' = symmetric _ _
+
+    transitive' : isTrans'
+    transitive' = transitive _ _ _
+
   isUniversalRel→isEquivRel : HeterogenousRelation.isUniversalRel R → isEquivRel
   isUniversalRel→isEquivRel u .isEquivRel.reflexive a = u a a
   isUniversalRel→isEquivRel u .isEquivRel.symmetric a b _ = u b a

Cubical/Tactics/GroupSolver/Example.agda

@@ -0,0 +1,62 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Tactics.GroupSolver.Example where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Algebra.Group
+open import Cubical.Tactics.GroupSolver.Solver
+open import Cubical.Data.List
+
+open import Cubical.WildCat.Functor
+
+private
+  variable
+    ℓ : Level
+
+module example (G G* G○ : Group ℓ)
+               (F* : GroupHom' G* G)
+               (F○ : GroupHom' G○ G*)
+                where
+
+
+ open Group-Solver ℓ
+
+
+ open GroupStr (snd G)
+
+ open WildFunctor
+
+ module * where
+  open GroupStr (snd G*) public
+
+ module ○ where
+  open GroupStr (snd G○) public
+
+
+
+ module T1 (p p' q r : fst G ) where
+
+
+   pA pB : fst G
+   pA = ((((((1g · p') · q) · (inv q)) · (inv p')) · p) · q) · r
+   pB = ((1g · p) · q) · r
+
+   pA≡pB : pA ≡ pB
+   pA≡pB = solveGroup (G ∷ [])
+
+
+
+ module T2 p p' q r s t u where
+
+
+  lhs rhs : fst G
+  lhs = (p · p') · (inv p' · (F* ⟪ (((*.inv q) *.· r) *.· F○ ⟪ ○.inv t ⟫ *.·
+              (*.inv (F○ ⟪ s ○.· s ⟫) *.· F○ ⟪ u ⟫ )) ⟫ ))
+
+  rhs = inv (F* ⟪ q ⟫ · inv p) · (F* ⟪ r ⟫) ·
+          (comp-WildFunctor F○ F*) ⟪ ○.inv (s ○.· s ○.· t) ○.· u ⟫
+
+
+  lhs≡rhs : lhs ≡ rhs
+  lhs≡rhs = solveGroup (G ∷ G* ∷ G○ ∷ [])

Cubical/Tactics/GroupSolver/Solver.agda

@@ -0,0 +1,82 @@
+{-# OPTIONS --safe  #-}
+
+module Cubical.Tactics.GroupSolver.Solver where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Function
+open import Cubical.Data.Unit
+open import Cubical.Data.List
+open import Cubical.Data.Maybe
+
+open import Cubical.Reflection.Base
+import Agda.Builtin.Reflection as R
+
+open import Cubical.WildCat.Base
+open import Cubical.Tactics.WildCatSolver.Solvers
+
+open import Cubical.WildCat.Functor
+open import Cubical.Algebra.Group
+open import Cubical.Algebra.Group.Morphisms
+open import Cubical.Algebra.Group.MorphismProperties
+
+open import Cubical.Tactics.WildCatSolver.Solvers
+
+
+module _ {ℓ} where
+
+ module _ (G : Group ℓ) where
+  open GroupStr (snd G)
+  Group→WildGroupoid : WildGroupoid ℓ-zero ℓ
+  WildCat.ob (WildGroupoid.wildCat Group→WildGroupoid) = Unit
+  WildCat.Hom[_,_] (WildGroupoid.wildCat Group→WildGroupoid) _ _ = ⟨ G ⟩
+  WildCat.id (WildGroupoid.wildCat Group→WildGroupoid) = 1g
+  WildCat._⋆_ (WildGroupoid.wildCat Group→WildGroupoid) = _·_
+  WildCat.⋆IdL (WildGroupoid.wildCat Group→WildGroupoid) = ·IdL
+  WildCat.⋆IdR (WildGroupoid.wildCat Group→WildGroupoid) = ·IdR
+  WildCat.⋆Assoc (WildGroupoid.wildCat Group→WildGroupoid) _ _ _ = sym (·Assoc _ _ _)
+  wildIsIso.inv' (WildGroupoid.isWildGroupoid Group→WildGroupoid f) = inv f
+  wildIsIso.sect (WildGroupoid.isWildGroupoid Group→WildGroupoid f) = ·InvL f
+  wildIsIso.retr (WildGroupoid.isWildGroupoid Group→WildGroupoid f) = ·InvR f
+
+
+ GroupHom' : (G H : Group ℓ) → Type ℓ
+
+ GroupHom' G H = WildFunctor
+    (WildGroupoid.wildCat (Group→WildGroupoid G))
+    (WildGroupoid.wildCat (Group→WildGroupoid H))
+
+ IsoGroupHom' : ∀ {G H} → Iso (GroupHom' G H) (GroupHom G H)
+ Iso.fun IsoGroupHom' wf = _ , makeIsGroupHom (WildFunctor.F-seq wf)
+ WildFunctor.F-ob (Iso.inv IsoGroupHom' _) = λ _ → tt
+ WildFunctor.F-hom (Iso.inv IsoGroupHom' (f , _)) = f
+ WildFunctor.F-id (Iso.inv IsoGroupHom' (_ , gh)) = IsGroupHom.pres1 gh
+ WildFunctor.F-seq (Iso.inv IsoGroupHom' (_ , gh)) = IsGroupHom.pres· gh
+ Iso.rightInv IsoGroupHom' _ = GroupHom≡ refl
+ WildFunctor.F-ob (Iso.leftInv IsoGroupHom' _ i) = λ _ → tt
+ WildFunctor.F-hom (Iso.leftInv IsoGroupHom' wf i) = WildFunctor.F-hom wf
+ WildFunctor.F-id (Iso.leftInv (IsoGroupHom' {G = G} {H = H}) wf i) =
+   IsGroup.is-set (GroupStr.isGroup (snd H))
+      (WildFunctor.F-hom wf (GroupStr.1g (snd G)))
+      (GroupStr.1g (snd H))
+      (hom1g (G .snd) (WildFunctor.F-hom wf) (H .snd)
+         (WildFunctor.F-seq wf))
+      (WildFunctor.F-id wf) i
+ WildFunctor.F-seq (Iso.leftInv IsoGroupHom' wf i) = λ f g → WildFunctor.F-seq wf f g
+
+
+module Group-Solver ℓ where
+
+ GroupWS : WildCatInstance ℓ-zero ℓ
+ WildCatInstance.wildStr GroupWS = Group ℓ
+ WildCatInstance.toWildCat GroupWS = WildGroupoid.wildCat ∘ Group→WildGroupoid
+ WildCatInstance.mbIsWildGroupoid GroupWS = just (WildGroupoid.isWildGroupoid ∘ Group→WildGroupoid)
+
+ private
+  module GRP-WS = WildCatInstance GroupWS
+
+ macro
+  solveGroup : R.Term → R.Term → R.TC Unit
+  solveGroup = GRP-WS.solveW (R.def (quote GroupWS) ( R.unknown v∷ []))
+

Cubical/Tactics/GroupoidSolver/Example.agda

@@ -0,0 +1,113 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Tactics.GroupoidSolver.Example where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.WildCat.Base
+open import Cubical.Tactics.GroupoidSolver.Solver
+open import Cubical.Data.List
+open import Cubical.Data.Nat
+open import Cubical.Categories.Category
+open import Cubical.WildCat.Functor
+
+private
+  variable
+    ℓ ℓ' : Level
+
+module example (WG WG* : WildGroupoid ℓ ℓ')
+               (F : WildFunctor
+                    (WildGroupoid.wildCat WG*)
+                    (WildGroupoid.wildCat WG))
+                where
+
+ open WildGroupoid-Solver ℓ ℓ'
+
+
+ open WildGroupoid WG
+ open WildCat wildCat
+
+ open WildFunctor
+
+
+ module * where
+  open WildCat (WildGroupoid.wildCat WG*) public
+  open WildGroupoid WG* public
+
+
+ module T1 x y z w
+          (p p' : Hom[ x , y ])
+          (q : Hom[ y , z ])
+          (r : Hom[ z , w ]) where
+
+
+   pA pB : Hom[ x , w ]
+   pA = ((((((id ⋆ p') ⋆ q) ⋆ ((inv q) ⋆ id)) ⋆ (inv p')) ⋆ p) ⋆ q) ⋆ r
+   pB = p ⋆ (q ⋆ r)
+
+   pA≡pB : pA ≡ pB
+   pA≡pB = solveWildGroupoid (WG ∷ WG* ∷ [])
+
+
+
+ module T2 x y z w
+          (p : Hom[ x , F ⟅ y ⟆ ])
+          (p' : Hom[ F ⟅ y ⟆ , x ])
+          (q : *.Hom[ z , y ])
+          (r : *.Hom[ z , w ]) where
+
+
+  lhs rhs : Hom[ x , F ⟅ w ⟆ ]
+  lhs = (p ⋆ p') ⋆ (inv p' ⋆ (F ⟪ (*.inv q) *.⋆ r ⟫))
+  rhs = inv (F ⟪ q ⟫ ⋆ inv p) ⋆ F ⟪ r ⟫
+
+
+  lhs≡rhs : lhs ≡ rhs
+  lhs≡rhs = solveWildGroupoid (WG ∷ WG* ∷ [])
+
+
+ module T3 (obs : ℕ → ob)
+          (homs : ∀ x y → ℕ → Hom[ obs x , obs y ])
+          where
+
+  lhs rhs : Hom[ obs 1 , obs 5 ]
+  lhs = homs _ 2 1 ⋆ (homs _ _ 2 ⋆ (homs 3 5 2 ⋆ (homs _ 6 3 ⋆ inv (homs _ 6 3))))
+  rhs = ((homs _ 2 1 ⋆ homs _ _ 2) ⋆ id) ⋆ homs 3 5 2
+
+
+  lhs≡rhs : lhs ≡ rhs
+  lhs≡rhs = solveWildGroupoid (WG ∷ [])
+
+
+module exampleGpd (G G* : GroupoidCat ℓ ℓ')
+               (F : WildFunctor
+                    (WildGroupoid.wildCat (Groupoid-Solver.Groupoid→WildGroupoid _ _ G*))
+                    (WildGroupoid.wildCat (Groupoid-Solver.Groupoid→WildGroupoid _ _ G)))
+                where
+
+ open Groupoid-Solver ℓ ℓ'
+
+
+
+ module * where
+   open GroupoidCat G* public
+   open Category category public
+
+ open GroupoidCat G
+ open Category category
+
+
+ module T1 x y z w
+          (p : Hom[ x , F ⟅ y ⟆ ])
+          (p' : Hom[ F ⟅ y ⟆ , x ])
+          (q : *.Hom[ z , y ])
+          (r : *.Hom[ z , w ]) where
+
+
+  lhs rhs : Hom[ x , F ⟅ w ⟆ ]
+  lhs = (p ⋆ p') ⋆ (p' ⁻¹ ⋆ (F ⟪ (q *.⁻¹) *.⋆ r ⟫))
+  rhs = (F ⟪ q ⟫ ⋆  p ⁻¹) ⁻¹ ⋆ F ⟪ r ⟫
+
+
+  lhs≡rhs : lhs ≡ rhs
+  lhs≡rhs = solveWildGroupoid (G ∷ G* ∷ [])