Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

More free groups!

- Use positive (constructive) definitions.
  (Thanks, Dan Licata!)
  • Loading branch information...
commit 31a6e4051aabde98af6eb7ebad85a0fb3fdfa015 1 parent 1f629bd
@favonia authored
Showing with 198 additions and 78 deletions.
  1. +3 −0  Prelude.agda
  2. +195 −78 Space/FreeGroup.agda
View
3  Prelude.agda
@@ -289,6 +289,9 @@ data List {a} (A : Set a) : Set a where
{-# BUILTIN NIL [] #-}
{-# BUILTIN CONS _∷_ #-}
+[_] : {ℓ} {A : Set ℓ} A List A
+[_] a = a ∷ []
+
-- Right fold.
foldr : {a b} {A : Set a} {B : Set b}
View
273 Space/FreeGroup.agda
@@ -24,87 +24,204 @@ data Alphabet (n : ℕ) : Set where
Word : Set
Word n = List (Alphabet n)
-data isUnstable {n : ℕ} : Alphabet n → Alphabet n → Set where
- gen-inv : (x : Fin n) isUnstable (gen x) (inv x)
- inv-gen : (x : Fin n) isUnstable (inv x) (gen x)
-
-isStable : {n} Alphabet n Alphabet n Set
-isStable x y = ¬ isUnstable x y
-
-data isReducible {n} : Word n → Set where
- boom : {x₁ x₂ : Alphabet n} isUnstable x₁ x₂ (xs : Word n) isReducible (x₁ ∷ x₂ ∷ xs)
- skip : (x : Alphabet n) {xs : Word n} isReducible xs isReducible (x ∷ xs)
-
-isNormalized : {n} Word n Set
-isNormalized w = ¬ isReducible w
-
-decideUnstable : {n} (x : Alphabet n) (y : Alphabet n) Dec (isUnstable x y)
-decideUnstable (gen x) (gen y) = inj₂ λ{()}
-decideUnstable (inv x) (inv y) = inj₂ λ{()}
-decideUnstable {n} (gen x) (inv y) with F.decide-≡ x y
-... | inj₁ eq = inj₁ $ subst (isUnstable (gen x)) (cong inv eq) (gen-inv x)
-... | inj₂ neq = inj₂ $ neq ∘ inversion
- where
- inversion : {x y : Fin n} isUnstable (gen x) (inv y) x ≡ y
- inversion (gen-inv _) = refl _
-decideUnstable {n} (inv x) (gen y) with F.decide-≡ x y
-... | inj₁ eq = inj₁ $ subst (isUnstable (inv x)) (cong gen eq) (inv-gen x)
-... | inj₂ neq = inj₂ $ neq ∘ inversion
- where
- inversion : {x y : Fin n} isUnstable (inv x) (gen y) x ≡ y
- inversion (inv-gen _) = refl _
+-- Positive definition (following Dan Licata's advice)
+data Stable {n} : Alphabet n → Alphabet n → Set where
+ gen-gen : {x y} Stable (gen x) (gen y)
+ inv-inv : {x y} Stable (inv x) (inv y)
+ gen-inv : {x y} ¬ x ≡ y Stable (gen x) (inv y)
+ inv-gen : {x y} ¬ x ≡ y Stable (inv x) (gen y)
+
+decideStable : {n} (x y : Alphabet n) Dec (Stable x y)
+decideStable (gen x) (gen y) = inj₁ gen-gen
+decideStable (inv x) (inv y) = inj₁ inv-inv
+decideStable {n} (gen x) (inv y) with F.decide-≡ x y
+... | inj₁ eq = inj₂ λ{(gen-inv neq) neq eq}
+... | inj₂ neq = inj₁ $ gen-inv neq
+decideStable {n} (inv x) (gen y) with F.decide-≡ x y
+... | inj₁ eq = inj₂ λ{(inv-gen neq) neq eq}
+... | inj₂ neq = inj₁ $ inv-gen neq
+
+-- Positive definition (following Dan Licata's advice)
+data Normalized {n} : Word n → Set where
+ empty : Normalized []
+ single : {x} Normalized [ x ]
+ cons : {x₁ x₂} {xs} Stable x₁ x₂
+ Normalized (x₂ ∷ xs)
+ Normalized (x₁ ∷ x₂ ∷ xs)
Free : Set
-Free n = Σ (Word n) isNormalized
+Free n = Σ (Word n) Normalized
private
- cons-stable : {n} {a₁ a₂ : Alphabet n} {w : Word n} isStable a₁ a₂ isNormalized (a₂ ∷ w) isNormalized (a₁ ∷ a₂ ∷ w)
- cons-stable stable norm (skip _ red) = norm red
- cons-stable stable norm (boom u _) = stable u
-
- rev-word-prepend : {n} Word n Free n Free n
- rev-word-prepend [] f = f
- rev-word-prepend (x ∷ xs) ([] , _) = rev-word-prepend xs (x ∷ [] , λ{(skip .x ())})
- rev-word-prepend (x ∷ xs) (y ∷ ys , n) with decideUnstable x y
- ... | inj₁ unstable = rev-word-prepend xs (ys , n ∘ skip y)
- ... | inj₂ stable = rev-word-prepend xs (x ∷ y ∷ ys , λ{(boom u .ys) stable u; (skip .x r) n r})
-
- word-prepend : {n} Word n Free n Free n
- word-prepend w f = rev-word-prepend (rev w) f
-
- free-concat : {n} Free n Free n Free n
- free-concat (w₁ , _) f₂ = word-prepend w₁ f₂
+ ------------------------------------------------------------------------
+ -- rev-append and append
+
+ word-rev-append : {n} Word n Word n Word n
+ word-rev-append [] w = w
+ word-rev-append (x ∷ xs) [] = word-rev-append xs (x ∷ [])
+ word-rev-append (x ∷ xs) (y ∷ ys) with decideStable x y
+ ... | inj₁ stable = word-rev-append xs (x ∷ y ∷ ys)
+ ... | inj₂ unstable = word-rev-append xs ys
+
+ norm-tail : {n} {x} {xs : Word n}
+ Normalized (x ∷ xs) Normalized xs
+ norm-tail single = empty
+ norm-tail (cons _ n) = n
+
+ norm-rev-append : {n} (xs ys : Word n) Normalized ys
+ Normalized (word-rev-append xs ys)
+ norm-rev-append [] ys n = n
+ norm-rev-append (x ∷ xs) [] empty = norm-rev-append xs [ x ] single
+ norm-rev-append (x ∷ xs) (y ∷ ys) n with decideStable x y
+ ... | inj₁ stable = norm-rev-append xs (x ∷ y ∷ ys) (cons stable n)
+ ... | inj₂ unstable = norm-rev-append xs ys (norm-tail n)
+
+ word-rev : {n} Word n Word n
+ word-rev w = word-rev-append w []
+
+ stable-sym : {n} {x y : Alphabet n} Stable x y Stable y x
+ stable-sym gen-gen = gen-gen
+ stable-sym inv-inv = inv-inv
+ stable-sym (gen-inv neq) = inv-gen $ neq ∘ sym
+ stable-sym (inv-gen neq) = gen-inv $ neq ∘ sym
+
+ data HeadStable {n} : Word n → Word n → Set where
+ heads : {x y} {xs ys} Stable x y
+ HeadStable (x ∷ xs) (y ∷ ys)
+ left : {xs} HeadStable xs []
+ right : {xs} HeadStable [] xs
+
+ norm-head : {n} {x} {xs ys : Word n}
+ Normalized (x ∷ xs) HeadStable (x ∷ ys) xs
+ norm-head single = left
+ norm-head (cons s _) = heads s
+
+ head-stable-sym : {n} {xs ys : Word n} HeadStable xs ys HeadStable ys xs
+ head-stable-sym left = right
+ head-stable-sym right = left
+ head-stable-sym (heads s) = heads $ stable-sym s
+
+ word-rev-append-head-stable : {n} x xs (ys : Word n) HeadStable (x ∷ xs) ys
+ word-rev-append (x ∷ xs) ys ≡ word-rev-append xs (x ∷ ys)
+ word-rev-append-head-stable x xs [] _ = refl _
+ word-rev-append-head-stable x xs (y ∷ ys) (heads s) with decideStable x y
+ ... | inj₁ _ = refl _
+ ... | inj₂ u = ⊥-elim $ u s
+
+ word-rev-rev-append : {n} (xs ys : Word n)
+ Normalized xs HeadStable xs ys
+ word-rev (word-rev-append xs ys) ≡ word-rev-append ys xs
+ word-rev-rev-append [] ys _ _ = refl _
+ word-rev-rev-append (x ∷ xs) ys n hs =
+ word-rev (word-rev-append (x ∷ xs) ys)
+ ≡⟨ cong word-rev $ word-rev-append-head-stable x xs ys hs ⟩
+ word-rev (word-rev-append xs (x ∷ ys))
+ ≡⟨ word-rev-rev-append xs (x ∷ ys) (norm-tail n) (head-stable-sym $ norm-head n) ⟩
+ word-rev-append (x ∷ ys) xs
+ ≡⟨ word-rev-append-head-stable x ys xs $ norm-head n ⟩∎
+ word-rev-append ys (x ∷ xs)
+ ∎
+
+ word-rev-rev : {n} (xs : Word n) Normalized xs word-rev (word-rev xs) ≡ xs
+ word-rev-rev xs n = word-rev-rev-append xs [] n left
+
+ word-append : {n} Word n Word n Word n
+ word-append w₁ w₂ = word-rev-append (word-rev w₁) w₂
+
+ norm-append : {n} (xs ys : Word n) Normalized ys
+ Normalized (word-append xs ys)
+ norm-append xs ys n = norm-rev-append (word-rev xs) ys n
+
+ ------------------------------------------------------------------------
+ -- flip
+
+ alphabet-flip : {n} Alphabet n Alphabet n
+ alphabet-flip (gen x) = inv x
+ alphabet-flip (inv x) = gen x
+
+ alphabet-flip-flip : {n} (x : Alphabet n) alphabet-flip (alphabet-flip x) ≡ x
+ alphabet-flip-flip (gen x) = refl _
+ alphabet-flip-flip (inv x) = refl _
+
+ stable-flip : {n} {x₁ x₂ : Alphabet n} Stable x₁ x₂
+ Stable (alphabet-flip x₁) (alphabet-flip x₂)
+ stable-flip gen-gen = inv-inv
+ stable-flip inv-inv = gen-gen
+ stable-flip (gen-inv neq) = inv-gen neq
+ stable-flip (inv-gen neq) = gen-inv neq
+
+ stable-flip-back : {n} {x₁ x₂ : Alphabet n}
+ Stable (alphabet-flip x₁) (alphabet-flip x₂)
+ Stable x₁ x₂
+ stable-flip-back s =
+ subst id (cong₂ Stable (alphabet-flip-flip _) (alphabet-flip-flip _)) $
+ stable-flip s
word-flip : {n} Word n Word n
- word-flip [] = []
- word-flip (gen x ∷ xs) = inv x ∷ word-flip xs
- word-flip (inv x ∷ xs) = gen x ∷ word-flip xs
-
- word-flip-flip : {n} (w : Word n) word-flip (word-flip w) ≡ w
- word-flip-flip [] = refl _
- word-flip-flip (gen x ∷ xs) = cong (λ xs gen x ∷ xs) $ word-flip-flip xs
- word-flip-flip (inv x ∷ xs) = cong (λ xs inv x ∷ xs) $ word-flip-flip xs
-
- -- Q: Is it possible to prove
- -- ∀ {n} (w : Word n) → isNormalized w → isNormalized (word-flip w)
- -- directly? Agda is unhappy when I tried to pattern match against
- -- isNormalized (word-flip w)
- norm-flip′ : {n} (w : Word n) isNormalized (word-flip w) isNormalized w
- norm-flip′ [] n ()
- norm-flip′ (inv x ∷ xs) n (skip .(inv x) rs) = norm-flip′ xs (n ∘ skip (gen x)) rs
- norm-flip′ (gen x ∷ xs) n (skip .(gen x) rs) = norm-flip′ xs (n ∘ skip (inv x)) rs
- norm-flip′ (gen x ∷ inv .x ∷ xs) n (boom (gen-inv .x) .xs) = n $ boom (inv-gen x) (word-flip xs)
- norm-flip′ (inv x ∷ gen .x ∷ xs) n (boom (inv-gen .x) .xs) = n $ boom (gen-inv x) (word-flip xs)
- norm-flip′ (gen _ ∷ gen _ ∷ xs) n (boom () .xs)
- norm-flip′ (inv _ ∷ inv _ ∷ xs) n (boom () .xs)
-
- norm-flip : {n} (w : Word n) isNormalized w isNormalized (word-flip w)
- norm-flip w n = norm-flip′ (word-flip w) $ subst isNormalized (sym $ word-flip-flip w) n
-
- free-flip : {n} Free n Free n
- free-flip (w , n) = (word-flip w , norm-flip w n)
-
- free-rev : {n} Free n Free n
- free-rev (w , n) = rev-word-prepend w ([] , λ{()})
-
- -- TODO correctness of free-rev
+ word-flip [] = []
+ word-flip (x ∷ xs) = alphabet-flip x ∷ word-flip xs
+
+ word-flip-flip : {n} (xs : Word n) word-flip (word-flip xs) ≡ xs
+ word-flip-flip [] = refl _
+ word-flip-flip (x ∷ xs) = cong₂ (λ x xs x ∷ xs) (alphabet-flip-flip x) (word-flip-flip xs)
+
+ norm-flip : {n} {xs : Word n} Normalized xs
+ Normalized (word-flip xs)
+ norm-flip empty = empty
+ norm-flip single = single
+ norm-flip (cons s n) = cons (stable-flip s) $ norm-flip n
+
+ ------------------------------------------------------------------------
+ -- inverse
+
+ word-inverse : {n} Word n Word n
+ word-inverse w = word-rev $ word-flip w
+
+ word-rev-append-flipʳ : {n} (xs : Word n) word-rev-append xs (word-flip xs) ≡ []
+ word-rev-append-flipʳ [] = refl _
+ word-rev-append-flipʳ (gen x ∷ xs) with F.decide-≡ x x
+ ... | inj₁ _ = word-rev-append-flipʳ xs
+ ... | inj₂ neq = ⊥-elim $ neq $ refl _
+ word-rev-append-flipʳ (inv x ∷ xs) with F.decide-≡ x x
+ ... | inj₁ _ = word-rev-append-flipʳ xs
+ ... | inj₂ neq = ⊥-elim $ neq $ refl _
+
+ word-rev-append-flipˡ : {n} (xs : Word n) word-rev-append (word-flip xs) xs ≡ []
+ word-rev-append-flipˡ xs =
+ word-rev-append (word-flip xs) xs
+ ≡⟨ cong (word-rev-append $ word-flip xs) $ sym $ word-flip-flip xs ⟩
+ word-rev-append (word-flip xs) (word-flip $ word-flip xs)
+ ≡⟨ word-rev-append-flipʳ $ word-flip xs ⟩∎
+ []
+ ∎
+
+ word-inverse-append : {n} (xs : Word n) Normalized xs
+ word-append (word-inverse xs) xs ≡ []
+ word-inverse-append xs n =
+ word-append (word-inverse xs) xs
+ ≡⟨ cong (λ xs₁ word-rev-append xs₁ xs) $ word-rev-rev (word-flip xs) (norm-flip n) ⟩
+ word-rev-append (word-flip xs) xs
+ ≡⟨ word-rev-append-flipˡ xs ⟩∎
+ []
+ ∎
+
+ word-flip-rev-append : {n} (xs ys : Word n)
+ word-flip (word-rev-append xs ys) ≡
+ word-rev-append (word-flip xs) (word-flip ys)
+ word-flip-rev-append [] ys = refl _
+ word-flip-rev-append (x ∷ xs) [] = word-flip-rev-append xs [ x ]
+ word-flip-rev-append (x ∷ xs) (y ∷ ys) with decideStable x y | decideStable (alphabet-flip x) (alphabet-flip y)
+ ... | inj₁ _ | inj₁ _ = word-flip-rev-append xs (x ∷ y ∷ ys)
+ ... | inj₂ _ | inj₂ _ = word-flip-rev-append xs ys
+ ... | inj₁ s | inj₂ u = ⊥-elim $ u (stable-flip s)
+ ... | inj₂ u | inj₁ s = ⊥-elim $ u (stable-flip-back s)
+
+ word-append-inverse : {n} (xs : Word n)
+ word-append xs (word-inverse xs) ≡ []
+ word-append-inverse xs =
+ word-append xs (word-rev (word-flip xs))
+ ≡⟨ cong (λ xs₂ word-append xs xs₂) $ sym $ word-flip-rev-append xs [] ⟩
+ word-append xs (word-flip (word-rev xs))
+ ≡⟨ word-rev-append-flipʳ (word-rev xs) ⟩∎
+ []
+ ∎
Please sign in to comment.
Something went wrong with that request. Please try again.