Tidy up README imports #2280

doc/README/Data/Container/FreeMonad.agda

@@ -16,12 +16,12 @@ open import Data.Unit
 open import Data.Bool.Base using (Bool; true)
 open import Data.Nat
 open import Data.Sum.Base using (inj₁; inj₂)
-open import Data.Product.Base renaming (_×_ to _⟨×⟩_)
+open import Data.Product.Base
 open import Data.Container using (Container; _▷_)
-open import Data.Container.Combinator
-open import Data.Container.FreeMonad as FreeMonad
+open import Data.Container.Combinator hiding (_×_)
+open import Data.Container.FreeMonad
 open import Data.W
-open import Relation.Binary.PropositionalEquality as P
+open import Relation.Binary.PropositionalEquality as ≡
 
 ------------------------------------------------------------------------
 -- Defining the signature of an effect and building trees describing
@@ -51,13 +51,13 @@ prog =
   where
   open RawMonad monad using (_>>_)
 
-runState : {S X : Set} → State S ⋆ X → (S → X ⟨×⟩ S)
+runState : {S X : Set} → State S ⋆ X → (S → X × S)
 runState (pure x)                = λ s → x , s
 runState (impure ((inj₁ _) , k)) = λ s → runState (k s) s
 runState (impure ((inj₂ s) , k)) = λ _ → runState (k _) s
 
 test : runState prog 0 ≡ (true , 1)
-test = P.refl
+test = ≡.refl
 
 -- It should be noted that @State S ⋆ X@ is not the state monad. If we
 -- could quotient @State S ⋆ X@ by the seven axioms of state (see

doc/README/Data/List/Membership.agda

@@ -7,11 +7,11 @@
 module README.Data.List.Membership where
 
 open import Data.Char.Base using (Char; fromℕ)
-open import Data.Char.Properties as CharProp hiding (setoid)
-open import Data.Nat as ℕ using (ℕ; _+_; _<_; s≤s; z≤n; _*_; _∸_; _≤_)
+open import Data.Char.Properties as Char hiding (setoid)
 open import Data.List.Base using (List; []; _∷_; map)
+open import Data.Nat as ℕ using (ℕ)
 open import Relation.Binary.PropositionalEquality
-  using (_≡_; refl; sym; cong; setoid)
+  using (_≡_; refl; cong; setoid)
 
 ------------------------------------------------------------------------
 -- Membership
@@ -66,7 +66,7 @@ import Data.List.Membership.Propositional.Properties as PropProperties
 -- following the first `∈` refers to lists of type `List ℕ` whereas
 -- the second `∈` refers to lists of type `List Char`.
 
-open DecPropMembership CharProp._≟_ renaming (_∈_ to _∈ᶜ_)
+open DecPropMembership Char._≟_ renaming (_∈_ to _∈ᶜ_)
 open SetoidProperties using (∈-map⁺)
 
 lem₂ : {v : ℕ} {xs : List ℕ} → v ∈ xs → fromℕ v ∈ᶜ map fromℕ xs

doc/README/Data/List/Relation/Binary/Equality.agda

@@ -9,10 +9,8 @@
 module README.Data.List.Relation.Binary.Equality where
 
 open import Data.Nat using (ℕ; _+_; _<_; s≤s; z≤n; _*_; _∸_; _≤_)
-open import Data.Nat.Properties as NatProp
+open import Data.Nat.Properties as ℕ
 open import Data.List.Base
-open import Relation.Binary.PropositionalEquality
-  using (_≡_; refl; sym; cong; setoid)
 
 ------------------------------------------------------------------------
 -- Pointwise equality

doc/README/Data/Tree/AVL.agda

@@ -20,7 +20,7 @@ import Data.Tree.AVL
 -- natural numbers as keys and vectors of strings as values.
 
 open import Data.Nat.Properties using (<-strictTotalOrder)
-open import Data.Product.Base as Prod using (_,_; _,′_)
+open import Data.Product.Base as Product using (_,_; _,′_)
 open import Data.String.Base using (String)
 open import Data.Vec.Base using (Vec; _∷_; [])
 open import Relation.Binary.PropositionalEquality
@@ -111,14 +111,14 @@ open import Function.Base using (id)
 v₆ : headTail t₀ ≡ nothing
 v₆ = refl
 
-v₇ : Maybe.map (Prod.map₂ toList) (headTail t₂) ≡
+v₇ : Maybe.map (Product.map₂ toList) (headTail t₂) ≡
      just ((1 , v₁) , ((2 , v₂) ∷ []))
 v₇ = refl
 
 v₈ : initLast t₀ ≡ nothing
 v₈ = refl
 
-v₉ : Maybe.map (Prod.map₁ toList) (initLast t₄) ≡
+v₉ : Maybe.map (Product.map₁ toList) (initLast t₄) ≡
      just (((1 , v₁) ∷ []) ,′ (2 , v₂))
 v₉ = refl
 

doc/README/Data/Trie/NonDependent.agda

@@ -51,15 +51,15 @@ module README.Data.Trie.NonDependent where
 open import Level
 open import Data.Unit
 open import Data.Bool
-open import Data.Char        as Char
-import Data.Char.Properties  as Char
-open import Data.List.Base   as List using (List; []; _∷_)
-open import Data.List.Fresh  as List# using (List#; []; _∷#_)
-open import Data.Maybe       as Maybe
-open import Data.Product.Base as Prod using (_×_; ∃; proj₁; _,_)
-open import Data.String.Base as String using (String)
+open import Data.Char              as Char
+import Data.Char.Properties        as Char
+open import Data.List.Base         as List using (List; []; _∷_)
+open import Data.List.Fresh        as List# using (List#; []; _∷#_)
+open import Data.Maybe             as Maybe
+open import Data.Product.Base      as Product using (_×_; ∃; proj₁; _,_)
+open import Data.String.Base       as String using (String)
 open import Data.String.Properties as String using (_≟_)
-open import Data.These       as These
+open import Data.These             as These
 
 open import Function.Base using (case_of_; _$_; _∘′_; id; _on_)
 open import Relation.Nary
@@ -127,7 +127,7 @@ module _ {t} (L : Lexer t) where
     -- characters one by one
 
     init : Keywords
-    init = fromList $ List.map (Prod.map₁ String.toList) $ proj₁ $ List#.toList keywords
+    init = fromList $ List.map (Product.map₁ String.toList) $ proj₁ $ List#.toList keywords
 
     -- Kickstart the tokeniser with an empty accumulator and the initial
     -- trie.

doc/README/Data/Vec/Relation/Binary/Equality/Cast.agda

@@ -3,22 +3,25 @@
 --
 -- An equational reasoning library for propositional equality over
 -- vectors of different indices using cast.
+--
+-- To see example usages of this library, scroll to the `Combinators`
+-- section.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
 module README.Data.Vec.Relation.Binary.Equality.Cast where
 
 open import Agda.Primitive
-open import Data.List.Base as L using (List)
-import Data.List.Properties as Lₚ
+open import Data.List.Base as List using (List)
+import Data.List.Properties as List
 open import Data.Nat.Base
 open import Data.Nat.Properties
 open import Data.Vec.Base
 open import Data.Vec.Properties
 open import Data.Vec.Relation.Binary.Equality.Cast
 open import Relation.Binary.PropositionalEquality
-  using (_≡_; refl; trans; sym; cong; subst; module ≡-Reasoning)
+  using (_≡_; refl; sym; cong; module ≡-Reasoning)
 
 private variable
   a : Level
@@ -27,10 +30,6 @@ private variable
   xs ys zs ws : Vec A n
 
 
--- To see example usages of this library, scroll to the combinators
--- section.
-
-
 ------------------------------------------------------------------------
 -- Motivation
 --
@@ -60,20 +59,20 @@ private variable
 -- Although `cast` makes it possible to prove vector identities by ind-
 -- uction, the explicit type-casting nature poses a significant barrier
 -- to code reuse in larger proofs. For example, consider the identity
--- ‘fromList (xs L.∷ʳ x) ≡ (fromList xs) ∷ʳ x’ where `L._∷ʳ_` is the
+-- ‘fromList (xs List.∷ʳ x) ≡ (fromList xs) ∷ʳ x’ where `List._∷ʳ_` is the
 -- snoc function of lists. We have
 --
---     fromList (xs L.∷ʳ x)            : Vec A (L.length (xs L.∷ʳ x))
+--     fromList (xs List.∷ʳ x)            : Vec A (List.length (xs List.∷ʳ x))
 --   =   {- by definition -}
---     fromList (xs L.++ L.[ x ])      : Vec A (L.length (xs L.++ L.[ x ]))
+--     fromList (xs List.++ List.[ x ])   : Vec A (List.length (xs List.++ List.[ x ]))
 --   =   {- by fromList-++ -}
---     fromList xs ++ fromList L.[ x ] : Vec A (L.length xs + L.length [ x ])
+--     fromList xs ++ fromList List.[ x ] : Vec A (List.length xs + List.length [ x ])
 --   =   {- by definition -}
---     fromList xs ++ [ x ]            : Vec A (L.length xs + 1)
+--     fromList xs ++ [ x ]               : Vec A (List.length xs + 1)
 --   =   {- by unfold-∷ʳ -}
---     fromList xs ∷ʳ x                : Vec A (suc (L.length xs))
+--     fromList xs ∷ʳ x                   : Vec A (suc (List.length xs))
 -- where
---     fromList-++ : cast _ (fromList (xs L.++ ys)) ≡ fromList xs ++ fromList ys
+--     fromList-++ : cast _ (fromList (xs List.++ ys)) ≡ fromList xs ++ fromList ys
 --     unfold-∷ʳ   : cast _ (xs ∷ʳ x) ≡ xs ++ [ x ]
 --
 -- Although the identity itself is simple, the reasoning process changes
@@ -82,31 +81,42 @@ private variable
 -- rearrange (the Agda version of) the identity into one with two
 -- `cast`s, resulting in lots of boilerplate code as demonstrated by
 -- `example1a-fromList-∷ʳ`.
-example1a-fromList-∷ʳ : ∀ (x : A) xs .(eq : L.length (xs L.∷ʳ x) ≡ suc (L.length xs)) →
-                        cast eq (fromList (xs L.∷ʳ x)) ≡ fromList xs ∷ʳ x
+example1a-fromList-∷ʳ : ∀ (x : A) xs →
+                        .(eq : List.length (xs List.∷ʳ x) ≡ suc (List.length xs)) →
+                        cast eq (fromList (xs List.∷ʳ x)) ≡ fromList xs ∷ʳ x
 example1a-fromList-∷ʳ x xs eq = begin
-  cast eq (fromList (xs L.∷ʳ x))                   ≡⟨⟩
-  cast eq (fromList (xs L.++ L.[ x ]))             ≡⟨ cast-trans eq₁ eq₂ (fromList (xs L.++ L.[ x ])) ⟨
-  cast eq₂ (cast eq₁ (fromList (xs L.++ L.[ x ]))) ≡⟨ cong (cast eq₂) (fromList-++ xs) ⟩
-  cast eq₂ (fromList xs ++ [ x ])                  ≡⟨ ≈-sym (unfold-∷ʳ (sym eq₂) x (fromList xs)) ⟩
-  fromList xs ∷ʳ x                                 ∎
+  cast eq (fromList (xs List.∷ʳ x))
+    ≡⟨⟩
+  cast eq (fromList (xs List.++ List.[ x ]))
+    ≡⟨ cast-trans eq₁ eq₂ (fromList (xs List.++ List.[ x ])) ⟨
+  cast eq₂ (cast eq₁ (fromList (xs List.++ List.[ x ])))
+    ≡⟨ cong (cast eq₂) (fromList-++ xs) ⟩
+  cast eq₂ (fromList xs ++ [ x ])
+    ≡⟨ ≈-sym (unfold-∷ʳ (sym eq₂) x (fromList xs)) ⟩
+  fromList xs ∷ʳ x
+    ∎
   where
   open ≡-Reasoning
-  eq₁ = Lₚ.length-++ xs {L.[ x ]}
-  eq₂ = +-comm (L.length xs) 1
+  eq₁ = List.length-++ xs {List.[ x ]}
+  eq₂ = +-comm (List.length xs) 1
 
 -- The `cast`s are irrelevant to core of the proof. At the same time,
 -- they can be inferred from the lemmas used during the reasoning steps
 -- (e.g. `fromList-++` and `unfold-∷ʳ`). To eliminate the boilerplate,
 -- this library provides a set of equational reasoning combinators for
 -- equality of the form `cast eq xs ≡ ys`.
-example1b-fromList-∷ʳ : ∀ (x : A) xs .(eq : L.length (xs L.∷ʳ x) ≡ suc (L.length xs)) →
-                        cast eq (fromList (xs L.∷ʳ x)) ≡ fromList xs ∷ʳ x
+example1b-fromList-∷ʳ : ∀ (x : A) xs →
+                        .(eq : List.length (xs List.∷ʳ x) ≡ suc (List.length xs)) →
+                        cast eq (fromList (xs List.∷ʳ x)) ≡ fromList xs ∷ʳ x
 example1b-fromList-∷ʳ x xs eq = begin
-  fromList (xs L.∷ʳ x)       ≈⟨⟩
-  fromList (xs L.++ L.[ x ]) ≈⟨ fromList-++ xs ⟩
-  fromList xs ++ [ x ]       ≈⟨ unfold-∷ʳ (+-comm 1 (L.length xs)) x (fromList xs) ⟨
-  fromList xs ∷ʳ x           ∎
+  fromList (xs List.∷ʳ x)
+    ≈⟨⟩
+  fromList (xs List.++ List.[ x ])
+    ≈⟨ fromList-++ xs ⟩
+  fromList xs ++ [ x ]
+    ≈⟨ unfold-∷ʳ (+-comm 1 (List.length xs)) x (fromList xs) ⟨
+  fromList xs ∷ʳ x
+    ∎
   where open CastReasoning
 
 
@@ -149,7 +159,7 @@ example2b eq xs a ys = begin
   (a ∷ xs) ʳ++ ys         ≂⟨ unfold-ʳ++ (a ∷ xs) ys ⟩          -- index: suc m + n
   reverse (a ∷ xs) ++ ys  ≂⟨ cong (_++ ys) (reverse-∷ a xs) ⟩  -- index: suc m + n
   (reverse xs ∷ʳ a) ++ ys ≈⟨ ∷ʳ-++ eq a (reverse xs) ⟩         -- index: suc m + n
-  reverse xs ++ (a ∷ ys)  ≂⟨ unfold-ʳ++ xs (a ∷ ys) ⟨         -- index: m + suc n
+  reverse xs ++ (a ∷ ys)  ≂⟨ unfold-ʳ++ xs (a ∷ ys) ⟨          -- index: m + suc n
   xs ʳ++ (a ∷ ys)         ∎                                    -- index: m + suc n
   where open CastReasoning
 
@@ -169,29 +179,35 @@ example2b eq xs a ys = begin
 -- Note. Technically, `A` and `B` should be vectors of different length
 -- and that `ys`, `zs` are vectors of non-definitionally equal index.
 example3a-fromList-++-++ : {xs ys zs : List A} →
-                           .(eq : L.length (xs L.++ ys L.++ zs) ≡
-                                  L.length xs + (L.length ys + L.length zs)) →
-                           cast eq (fromList (xs L.++ ys L.++ zs)) ≡
+                           .(eq : List.length (xs List.++ ys List.++ zs) ≡
+                                  List.length xs + (List.length ys + List.length zs)) →
+                           cast eq (fromList (xs List.++ ys List.++ zs)) ≡
                                    fromList xs ++ fromList ys ++ fromList zs
 example3a-fromList-++-++ {xs = xs} {ys} {zs} eq = begin
-  fromList (xs L.++ ys L.++ zs)             ≈⟨ fromList-++ xs ⟩
-  fromList xs ++ fromList (ys L.++ zs)      ≈⟨ ≈-cong (fromList xs ++_) (cast-++ʳ (Lₚ.length-++ ys) (fromList xs))
-                                                      (fromList-++ ys) ⟩
-  fromList xs ++ fromList ys ++ fromList zs ∎
+  fromList (xs List.++ ys List.++ zs)
+    ≈⟨ fromList-++ xs ⟩
+  fromList xs ++ fromList (ys List.++ zs)
+    ≈⟨ ≈-cong (fromList xs ++_) (cast-++ʳ (List.length-++ ys) (fromList xs)) (fromList-++ ys) ⟩
+  fromList xs ++ fromList ys ++ fromList zs
+    ∎
   where open CastReasoning
 
 -- As an alternative, one can manually apply `cast-++ʳ` to expose `cast`
 -- in the subterm. However, this unavoidably duplicates the proof term.
 example3b-fromList-++-++′ : {xs ys zs : List A} →
-                            .(eq : L.length (xs L.++ ys L.++ zs) ≡
-                                   L.length xs + (L.length ys + L.length zs)) →
-                            cast eq (fromList (xs L.++ ys L.++ zs)) ≡
+                            .(eq : List.length (xs List.++ ys List.++ zs) ≡
+                                   List.length xs + (List.length ys + List.length zs)) →
+                            cast eq (fromList (xs List.++ ys List.++ zs)) ≡
                                     fromList xs ++ fromList ys ++ fromList zs
 example3b-fromList-++-++′ {xs = xs} {ys} {zs} eq = begin
-  fromList (xs L.++ ys L.++ zs)                 ≈⟨ fromList-++ xs ⟩
-  fromList xs ++ fromList (ys L.++ zs)          ≈⟨ cast-++ʳ (Lₚ.length-++ ys) (fromList xs) ⟩
-  fromList xs ++ cast _ (fromList (ys L.++ zs)) ≂⟨ cong (fromList xs ++_) (fromList-++ ys) ⟩
-  fromList xs ++ fromList ys ++ fromList zs     ∎
+  fromList (xs List.++ ys List.++ zs)
+    ≈⟨ fromList-++ xs ⟩
+  fromList xs ++ fromList (ys List.++ zs)
+    ≈⟨ cast-++ʳ (List.length-++ ys) (fromList xs) ⟩
+  fromList xs ++ cast _ (fromList (ys List.++ zs))
+    ≂⟨ cong (fromList xs ++_) (fromList-++ ys) ⟩
+  fromList xs ++ fromList ys ++ fromList zs
+    ∎
   where open CastReasoning
 
 -- `≈-cong` can be chained together much like how `cong` can be nested.
@@ -201,12 +217,16 @@ example3b-fromList-++-++′ {xs = xs} {ys} {zs} eq = begin
 example4-cong² : ∀ .(eq : (m + 1) + n ≡ n + suc m) a (xs : Vec A m) ys →
           cast eq (reverse ((xs ++ [ a ]) ++ ys)) ≡ ys ʳ++ reverse (xs ∷ʳ a)
 example4-cong² {m = m} {n} eq a xs ys = begin
-  reverse ((xs ++ [ a ]) ++ ys)   ≈⟨ ≈-cong reverse (cast-reverse (cong (_+ n) (+-comm 1 m)) ((xs ∷ʳ a) ++ ys))
+  reverse ((xs ++ [ a ]) ++ ys)
+    ≈⟨ ≈-cong reverse (cast-reverse (cong (_+ n) (+-comm 1 m)) ((xs ∷ʳ a) ++ ys))
                                              (≈-cong (_++ ys) (cast-++ˡ (+-comm 1 m) (xs ∷ʳ a))
                                                      (unfold-∷ʳ _ a xs)) ⟨
-  reverse ((xs ∷ʳ a) ++ ys)       ≈⟨ reverse-++ (+-comm (suc m) n) (xs ∷ʳ a) ys ⟩
-  reverse ys ++ reverse (xs ∷ʳ a) ≂⟨ unfold-ʳ++ ys (reverse (xs ∷ʳ a)) ⟨
-  ys ʳ++ reverse (xs ∷ʳ a)        ∎
+  reverse ((xs ∷ʳ a) ++ ys)
+    ≈⟨ reverse-++ (+-comm (suc m) n) (xs ∷ʳ a) ys ⟩
+  reverse ys ++ reverse (xs ∷ʳ a)
+    ≂⟨ unfold-ʳ++ ys (reverse (xs ∷ʳ a)) ⟨
+  ys ʳ++ reverse (xs ∷ʳ a)
+    ∎
   where open CastReasoning
 
 ------------------------------------------------------------------------
@@ -222,25 +242,33 @@ example4-cong² {m = m} {n} eq a xs ys = begin
 -- reasoning system of `_≈[_]_` and switches back to the reasoning
 -- system of `_≡_`.
 example5-fromList-++-++′ : {xs ys zs : List A} →
-                           .(eq : L.length (xs L.++ ys L.++ zs) ≡
-                                  L.length xs + (L.length ys + L.length zs)) →
-                           cast eq (fromList (xs L.++ ys L.++ zs)) ≡
+                           .(eq : List.length (xs List.++ ys List.++ zs) ≡
+                                  List.length xs + (List.length ys + List.length zs)) →
+                           cast eq (fromList (xs List.++ ys List.++ zs)) ≡
                                    fromList xs ++ fromList ys ++ fromList zs
 example5-fromList-++-++′ {xs = xs} {ys} {zs} eq = begin
-  fromList (xs L.++ ys L.++ zs)                 ≈⟨ fromList-++ xs ⟩
-  fromList xs ++ fromList (ys L.++ zs)          ≃⟨ cast-++ʳ (Lₚ.length-++ ys) (fromList xs) ⟩
-  fromList xs ++ cast _ (fromList (ys L.++ zs)) ≡⟨ cong (fromList xs ++_) (fromList-++ ys) ⟩
-  fromList xs ++ fromList ys ++ fromList zs     ≡-∎
+  fromList (xs List.++ ys List.++ zs)
+    ≈⟨ fromList-++ xs ⟩
+  fromList xs ++ fromList (ys List.++ zs)
+    ≃⟨ cast-++ʳ (List.length-++ ys) (fromList xs) ⟩
+  fromList xs ++ cast _ (fromList (ys List.++ zs))
+    ≡⟨ cong (fromList xs ++_) (fromList-++ ys) ⟩
+  fromList xs ++ fromList ys ++ fromList zs
+    ≡-∎
   where open CastReasoning
 
 -- Of course, it is possible to start with the reasoning system of `_≡_`
 -- and then switch to the reasoning system of `_≈[_]_`.
 example6a-reverse-∷ʳ : ∀ x (xs : Vec A n) → reverse (xs ∷ʳ x) ≡ x ∷ reverse xs
 example6a-reverse-∷ʳ {n = n} x xs = begin-≡
-  reverse (xs ∷ʳ x)     ≡⟨ ≈-reflexive refl ⟨
-  reverse (xs ∷ʳ x)     ≈⟨ ≈-cong reverse (cast-reverse _ _) (unfold-∷ʳ (+-comm 1 n) x xs) ⟩
-  reverse (xs ++ [ x ]) ≈⟨ reverse-++ (+-comm n 1) xs [ x ] ⟩
-  x ∷ reverse xs        ∎
+  reverse (xs ∷ʳ x)
+    ≡⟨ ≈-reflexive refl ⟨
+  reverse (xs ∷ʳ x)
+    ≈⟨ ≈-cong reverse (cast-reverse _ _) (unfold-∷ʳ (+-comm 1 n) x xs) ⟩
+  reverse (xs ++ [ x ])
+    ≈⟨ reverse-++ (+-comm n 1) xs [ x ] ⟩
+  x ∷ reverse xs
+    ∎
   where open CastReasoning
 
 example6b-reverse-∷ʳ-by-induction : ∀ x (xs : Vec A n) → reverse (xs ∷ʳ x) ≡ x ∷ reverse xs