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

@@ -322,6 +322,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

@@ -5,10 +5,13 @@ open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.GroupoidLaws
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Function
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
 open import Cubical.Foundations.Isomorphism
 
 open import Cubical.Data.Empty as ⊥
 open import Cubical.Data.Nat
+open import Cubical.Data.Maybe
 open import Cubical.Data.Sigma
 open import Cubical.Data.Sum as ⊎ hiding (map)
 open import Cubical.Data.Unit
@@ -194,6 +197,14 @@ length-map : (f : A → B) → (as : List A)
 length-map f [] = refl
 length-map f (a ∷ as) = cong suc (length-map f as)
 
+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
+
 map++ : (f : A → B) → (as bs : List A)
    → map f as ++ map f bs ≡ map f (as ++ bs)
 map++ f [] bs = refl
@@ -302,9 +313,9 @@ split++ (x₁ ∷ xs') ys' (x₂ ∷ xs) ys x =
  in zs , ⊎.map (map-fst (λ q i → p    i  ∷ q i))
                (map-fst (λ q i → p (~ i) ∷ q i)) q
 
-rot : List A → List A
-rot [] = []
-rot (x ∷ xs) = xs ∷ʳ x
+zipWithIndex : List A → List (ℕ × A)
+zipWithIndex [] = []
+zipWithIndex (x ∷ xs) = (zero , x) ∷ map (map-fst suc) (zipWithIndex xs)
 
 take[] : ∀ n → take {A = A} n [] ≡ []
 take[] zero = refl
@@ -319,6 +330,26 @@ lookupAlways a [] _ = a
 lookupAlways _ (x ∷ _) zero = x
 lookupAlways a (x ∷ xs) (suc k) = lookupAlways a xs k
 
+rot : List A → List A
+rot [] = []
+rot (x ∷ xs) = xs ∷ʳ x
+
+rotN : ℕ → List A → List A
+rotN n = iter n rot
+
+module _ {A : Type ℓ} (_≟_ : Discrete A) where
+
+ private
+  fa : ℕ → (xs ys : List A) → Maybe (Σ _ λ k → xs ≡ rotN k ys)
+  fa zero _ _ = nothing
+  fa (suc k) xs ys =
+    decRec (just ∘ ((length xs ∸ k) ,_))
+     (λ _ → fa k xs ys) (discreteList _≟_ xs (rotN (length xs ∸ k) ys) )
+
+ findAligment : (xs ys : List A) → Maybe (Σ _ λ k → xs ≡ rotN k ys)
+ findAligment xs ys = fa (suc (length xs)) xs ys
+
+
 module List₂ where
  open import Cubical.HITs.SetTruncation renaming
    (rec to rec₂ ; map to map₂ ; elim to elim₂ )

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

@@ -51,6 +51,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/Foundations/GroupoidLaws.agda

@@ -78,6 +78,13 @@ rCancel-filler' {x = x} {y} p i j k =
 rCancel' : ∀ {ℓ} {A : Type ℓ} {x y : A} (p : x ≡ y) → p ∙ p ⁻¹ ≡ refl
 rCancel' p j k = rCancel-filler' p i0 j k
 
+midCancel : (p : y ≡ x) (q : z ≡ x) (r : w ≡ x)
+   → (p ∙∙ refl ∙∙ sym q) ∙ (q ∙∙ refl ∙∙ sym r) ≡ (p ∙∙ refl ∙∙ sym r)
+midCancel p q r j =
+     (λ i → p (i ∧ j))
+  ∙∙ doubleCompPath-filler p refl (sym q) (~ j)
+  ∙∙ λ i → hcomp (λ k → λ {(i = i0) → q (~ k ∨ j)  ; (i = i1) → r (~ k) ; (j = i1) → r (~ i ∨ ~ k) }) (r i1)
+
 lCancel : (p : x ≡ y) → p ⁻¹ ∙ p ≡ refl
 lCancel p = rCancel (p ⁻¹)
 

Cubical/Foundations/Path.agda

@@ -438,6 +438,34 @@ Square→compPathΩ² {a = a} sq k i j =
                  ; (k = i1) → cong (λ x → rUnit x r) (flipSquare sq) i j})
         (sq j i)
 
+module 2-cylinder-from-square
+   {a₀₀ a₀₁ a₁₀ a₁₁ a₀₀' a₀₁' a₁₀' a₁₁' : A }
+   {a₀₋  : a₀₀  ≡ a₀₁ } {a₁₋  : a₁₀  ≡ a₁₁ } {a₋₀  : a₀₀  ≡ a₁₀ } {a₋₁  : a₀₁  ≡ a₁₁ }
+   {a₀₋' : a₀₀' ≡ a₀₁'} {a₁₋' : a₁₀' ≡ a₁₁'} {a₋₀' : a₀₀' ≡ a₁₀'} {a₋₁' : a₀₁' ≡ a₁₁'}
+   (aa'₀₀ : a₀₀ ≡ a₀₀')
+ where
+
+ MissingSquare = (a₁₋ ⁻¹ ∙∙ a₋₀ ⁻¹ ∙∙ aa'₀₀ ∙∙ a₋₀' ∙∙ a₁₋')
+               ≡ (a₋₁ ⁻¹ ∙∙ a₀₋ ⁻¹ ∙∙ aa'₀₀ ∙∙ a₀₋' ∙∙ a₋₁')
+
+ cyl : MissingSquare → ∀ i j → I → Partial (i ∨ ~ i ∨ j ∨ ~ j) A
+
+ cyl c i j k = λ where
+  (i = i0) → doubleCompPath-filler (sym a₀₋) aa'₀₀ a₀₋' j k
+  (i = i1) → doubleCompPath-filler (sym a₁₋) (sym a₋₀ ∙∙ aa'₀₀ ∙∙  a₋₀')  a₁₋' j k
+  (j = i0) → doubleCompPath-filler (sym a₋₀) aa'₀₀ a₋₀' i k
+  (j = i1) → compPathR→PathP∙∙ c (~ i) k
+
+ module _ (s : MissingSquare) where
+  IsoSqSq' : Iso (Square a₀₋ a₁₋ a₋₀ a₋₁) (Square a₀₋' a₁₋' a₋₀' a₋₁')
+  Iso.fun IsoSqSq' x i j = hcomp (cyl s i j) (x i j)
+  Iso.inv IsoSqSq' x i j = hcomp (λ k → cyl s i j (~ k)) (x i j)
+  Iso.rightInv IsoSqSq' x l i j  = hcomp-equivFiller (λ k → cyl s i j (~ k)) (inS (x i j)) (~ l)
+  Iso.leftInv IsoSqSq' x l i j = hcomp-equivFiller (cyl s i j) (inS (x i j)) (~ l)
+
+  Sq≃Sq' : (Square a₀₋ a₁₋ a₋₀ a₋₁) ≃ (Square a₀₋' a₁₋' a₋₀' a₋₁')
+  Sq≃Sq' = isoToEquiv IsoSqSq'
+
 pathFiber : {B : Type ℓ} (f : A → B)
   (b : B) {a a' : A} {t : f a ≡ b} {t' : f a' ≡ b} →
   ((a , t) ≡ (a' , t' )) → Σ[ e ∈ a ≡ a' ] (t ≡ cong f e ∙ t')

Cubical/Reflection/Base.agda

@@ -7,6 +7,7 @@ Some basic utilities for reflection
 module Cubical.Reflection.Base where
 
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
 open import Cubical.Data.List.Base
 open import Cubical.Data.Nat.Base
 
@@ -19,6 +20,9 @@ _<|>_ = R.catchTC
 _>>_ : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → R.TC A → R.TC B → R.TC B
 f >> g = f >>= λ _ → g
 
+pure  : ∀ {ℓ} {A : Type ℓ} → A → R.TC A
+pure = R.returnTC
+
 infixl 4 _>>=_ _>>_ _<|>_
 
 liftTC : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → (A → B) → R.TC A → R.TC B
@@ -32,6 +36,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

@@ -63,6 +63,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
 
@@ -139,6 +142,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,84 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Tactics.GroupSolver.Example where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+
+open import Cubical.Algebra.Group
+open import Cubical.Algebra.Group.Morphisms
+open import Cubical.Algebra.Group.MorphismProperties
+
+open import Cubical.Tactics.GroupSolver.Solver
+open import Cubical.Data.List
+
+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)
+
+ 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
+
+
+ module T2 p p' q r s t u where
+
+
+  lhs rhs : fst G
+  lhs = p · (p · inv p) · inv p · (p' · inv p') · (p · p') ·
+            (inv p' · (fst F* (((*.inv q) *.· r) *.· fst F○ (○.inv t) *.·
+              (*.inv (fst F○ ( s ○.· s )) *.· fst F○ u )) ))
+
+  rhs = inv (fst F* q · inv p) · (fst F* r) ·
+          fst (compGroupHom F○ F*) (○.inv (s ○.· s ○.· t) ○.· u )
+
+
+  lhs≡rhs : lhs ≡ rhs
+  lhs≡rhs = solveGroup
+
+module ℤexamples where
+ open import Cubical.Data.Nat using (ℕ)
+ open import Cubical.Algebra.Group.Instances.Int
+
+ open GroupStr (snd ℤGroup)
+
+ module _ k ([_]ᶻ : ℕ → fst ℤGroup) (someℤHom[_] : ℕ → GroupHom ℤGroup ℤGroup) where
+
+
+  open Group-Solver ℓ-zero
+        (quote ℤGroup ∷ [ quote ℤHom ])
+
+
+  lhs rhs : (fst ℤGroup)
+  lhs = fst (ℤHom  k) ([ 1 ]ᶻ · [ 3 ]ᶻ)
+          · fst someℤHom[ 2 ] ([ 4 ]ᶻ · fst (someℤHom[ 1 ]) (inv [ 4 ]ᶻ ·  [ 4 ]ᶻ))
+             · inv (fst someℤHom[ 2 ] ([ 4 ]ᶻ))
+  rhs = fst (ℤHom  k) [ 1 ]ᶻ · fst (ℤHom k) [ 3 ]ᶻ
+
+  lhs≡rhs : lhs ≡ rhs
+  lhs≡rhs = solveGroup[ ℤGroup ]