Merge branch 'master' into list_properties

Author: MatthewDaggitt

CHANGELOG.md

@@ -128,6 +128,19 @@ New modules
   Data.Container.Indexed.Relation.Binary.Equality.Setoid
   ```
 
+* `System.Random` bindings:
+  ```agda
+  System.Random.Primitive
+  System.Random
+  ```
+
+* Show modules:
+  ```agda
+  Data.List.Show
+  Data.Vec.Show
+  Data.Vec.Bounded.Show
+  ```
+
 Additions to existing modules
 -----------------------------
 
@@ -252,6 +265,12 @@ Additions to existing modules
   x \\ y = (x ⁻¹) ∙ y
   ```
 
+* In `Algebra.Structures.IsCancellativeCommutativeSemiring` add the
+  extra property as an exposed definition:
+  ```agda
+    *-cancelʳ-nonZero : AlmostRightCancellative 0# *
+  ```
+
 * In `Data.Container.Indexed.Core`:
   ```agda
   Subtrees o c = (r : Response c) → X (next c r)
@@ -262,6 +281,11 @@ Additions to existing modules
   nonZeroIndex : Fin n → ℕ.NonZero n
   ```
 
+* In `Data.Float.Base`:
+  ```agda
+  _≤_ : Rel Float _
+  ```
+
 * In `Data.Integer.Divisibility`: introduce `divides` as an explicit pattern synonym
   ```agda
   pattern divides k eq = Data.Nat.Divisibility.divides k eq
@@ -276,6 +300,7 @@ Additions to existing modules
 
 * In `Data.List.Properties`:
   ```agda
+  length-catMaybes      : length (catMaybes xs) ≤ length xs
   applyUpTo-∷ʳ          : applyUpTo f n ∷ʳ f n ≡ applyUpTo f (suc n)
   applyDownFrom-∷ʳ      : applyDownFrom (f ∘ suc) n ∷ʳ f 0 ≡ applyDownFrom f (suc n)
   upTo-∷ʳ               : upTo n ∷ʳ n ≡ upTo (suc n)
@@ -409,6 +434,13 @@ Additions to existing modules
 * Added new functions in `Data.String.Base`:
   ```agda
   map : (Char → Char) → String → String
+  between : String → String → String → String
+  ```
+
+* In `Data.Word.Base`:
+  ```agda
+  _≤_ : Rel Word64 zero
+  ```
 
 * Added new definition in `Relation.Binary.Construct.Closure.Transitive`
   ```
@@ -457,5 +489,7 @@ Additions to existing modules
   WeaklyDecidable : Pred A ℓ → Set _
   ```
 
-* `Tactic.Cong` now provides a marker function, `⌞_⌟`, for user-guided
-  anti-unification. See README.Tactic.Cong for details.
+* Enhancements to `Tactic.Cong` - see `README.Tactic.Cong` for details.
+  - Provide a marker function, `⌞_⌟`, for user-guided anti-unification.
+  - Improved support for equalities between terms with instance arguments,
+    such as terms that contain `_/_` or `_%_`.

CHANGELOG/v1.7.3.md

@@ -0,0 +1,18 @@
+Version 1.7.3
+=============
+
+The library has been tested using Agda 2.6.3 & 2.6.4.
+
+* To avoid _large indices_ that are by default no longer allowed in Agda 2.6.4,
+  universe levels have been increased in the following definitions:
+  - `Data.Star.Decoration.DecoratedWith`
+  - `Data.Star.Pointer.Pointer`
+  - `Reflection.AnnotatedAST.Typeₐ`
+  - `Reflection.AnnotatedAST.AnnotationFun`
+
+* The following aliases have been added:
+  - `IO.Primitive.pure` as alias for `IO.Primitive.return`
+  - modules `Effect.*` as aliases for modules `Category.*`
+
+  These allow to address said objects with the new name they will have in v2.0 of the library,
+  to ease the transition from v1.7.3 to v2.0.

GenerateEverything.hs

@@ -76,6 +76,8 @@ unsafeModules = map modToFile
   , "System.FilePath.Posix.Primitive"
   , "System.Process"
   , "System.Process.Primitive"
+  , "System.Random"
+  , "System.Random.Primitive"
   , "Test.Golden"
   , "Text.Pretty.Core"
   , "Text.Pretty"

doc/README/Tactic/Cong.agda

@@ -3,6 +3,7 @@
 module README.Tactic.Cong where
 
 open import Data.Nat
+open import Data.Nat.DivMod
 open import Data.Nat.Properties
 
 open import Relation.Binary.PropositionalEquality
@@ -161,3 +162,35 @@ module EquationalReasoningTests where
     ≤⟨ n≤1+n _ ⟩
       suc (suc (n + n))
     ∎
+
+module MetaTests where
+
+  test₁ : ∀ m n o → .⦃ _ : NonZero o ⦄ → (m + n) / o ≡ (n + m) / o
+  test₁ m n o =
+    let open ≤-Reasoning in
+    begin-equality
+      ⌞ m + n ⌟ / o
+     ≡⟨ cong! (+-comm m n) ⟩
+      (n + m) / o
+    ∎
+
+  test₂ : ∀ m n o p q r → .⦃ _ : NonZero o ⦄ → .⦃ _ : NonZero p ⦄ →
+          .⦃ _ : NonZero q ⦄ → p ≡ q ^ r → (m + n) % o % p ≡ (n + m) % o % p
+  test₂ m n o p q r eq =
+    let
+      open ≤-Reasoning
+      instance q^r≢0 = m^n≢0 q r
+    in
+    begin-equality
+      (m + n) % o % p
+     ≡⟨ %-congʳ eq ⟩
+      ⌞ m + n ⌟ % o % q ^ r
+     ≡⟨ cong! (+-comm m n) ⟩
+      ⌞ n + m ⌟ % o % q ^ r
+     ≡⟨ cong! (+-comm m n) ⟨
+      ⌞ m + n ⌟ % o % q ^ r
+     ≡⟨ cong! (+-comm m n) ⟩
+      (n + m) % o % q ^ r
+     ≡⟨ %-congʳ eq ⟨
+      (n + m) % o % p
+    ∎

src/Algebra/Construct/LexProduct.agda

@@ -6,16 +6,17 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra
-open import Data.Bool using (true; false)
+open import Algebra.Bundles using (Magma)
+open import Algebra.Definitions
+open import Data.Bool.Base using (true; false)
 open import Data.Product.Base using (_×_; _,_)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent using (Pointwise)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Function.Base using (_∘_)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Definitions using (Decidable)
-open import Relation.Nullary using (¬_; does; yes; no)
-open import Relation.Nullary.Negation using (contradiction; contradiction₂)
+open import Relation.Nullary.Decidable.Core using (does; yes; no)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction; contradiction₂)
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
 module Algebra.Construct.LexProduct

src/Algebra/Properties/Monoid/Sum.agda

@@ -7,16 +7,17 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra.Bundles using (Monoid)
+
+module Algebra.Properties.Monoid.Sum {a ℓ} (M : Monoid a ℓ) where
+
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc; NonZero)
-open import Data.Vec.Functional as Vector
+open import Data.Vec.Functional as Vector using (Vector; replicate; init;
+  last; head; tail)
 open import Data.Fin.Base using (zero; suc)
-open import Data.Unit using (tt)
 open import Function.Base using (_∘_)
 open import Relation.Binary.Core using (_Preserves_⟶_)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≗_; _≡_)
 
-module Algebra.Properties.Monoid.Sum {a ℓ} (M : Monoid a ℓ) where
-
 open Monoid M
   renaming
   ( _∙_       to _+_

src/Algebra/Solver/IdempotentCommutativeMonoid.agda

@@ -8,7 +8,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra
+open import Algebra.Bundles using (IdempotentCommutativeMonoid)
 
 open import Data.Bool as Bool using (Bool; true; false; if_then_else_; _∨_)
 open import Data.Fin.Base using (Fin; zero; suc)

src/Algebra/Solver/Monoid.agda

@@ -20,7 +20,7 @@ open import Data.Nat.Base using (ℕ)
 open import Data.Product.Base using (_×_; uncurry)
 open import Data.Vec.Base using (Vec; lookup)
 open import Function.Base using (_∘_; _$_)
-open import Relation.Binary.Definitions using (Decidable)
+open import Relation.Binary.Definitions using (DecidableEquality)
 
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)
 import Relation.Binary.Reflection
@@ -114,7 +114,7 @@ open module R = Relation.Binary.Reflection
 
 infix 5 _≟_
 
-_≟_ : ∀ {n} → Decidable {A = Normal n} _≡_
+_≟_ : ∀ {n} → DecidableEquality (Normal n)
 nf₁ ≟ nf₂ = Dec.map′ ≋⇒≡ ≡⇒≋ (nf₁ ≋? nf₂)
   where open ListEq Fin._≟_
 

src/Algebra/Structures.agda

@@ -573,6 +573,10 @@ record IsCancellativeCommutativeSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a 
 
   open IsCommutativeSemiring isCommutativeSemiring public
 
+  *-cancelʳ-nonZero : AlmostRightCancellative 0# *
+  *-cancelʳ-nonZero = Consequences.comm∧almostCancelˡ⇒almostCancelʳ setoid
+      *-comm *-cancelˡ-nonZero
+
 record IsIdempotentSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
   field
     isSemiring     : IsSemiring + * 0# 1#

src/Axiom/UniquenessOfIdentityProofs.agda

@@ -60,7 +60,7 @@ module Constant⇒UIP
 -- proof produced by the decision procedure.
 
 module Decidable⇒UIP
-  {a} {A : Set a} (_≟_ : Decidable {A = A} _≡_)
+  {a} {A : Set a} (_≟_ : DecidableEquality A)
   where
 
   ≡-normalise : _≡_ {A = A} ⇒ _≡_

src/Codata/Sized/Conat/Literals.agda

@@ -8,9 +8,9 @@
 
 module Codata.Sized.Conat.Literals where
 
-open import Agda.Builtin.FromNat
-open import Data.Unit
-open import Codata.Sized.Conat
+open import Agda.Builtin.FromNat using (Number)
+open import Data.Unit.Base using (⊤)
+open import Codata.Sized.Conat using (Conat; fromℕ)
 
 number : ∀ {i} → Number (Conat i)
 number = record

src/Codata/Sized/Delay/Properties.agda

@@ -10,7 +10,7 @@ module Codata.Sized.Delay.Properties where
 
 open import Size
 import Data.Sum.Base as Sum
-import Data.Nat as ℕ
+import Data.Nat.Base as ℕ
 open import Codata.Sized.Thunk using (Thunk; force)
 open import Codata.Sized.Conat
 open import Codata.Sized.Conat.Bisimilarity as Coℕ using (zero ; suc)

src/Data/Bool/Properties.agda

@@ -25,7 +25,7 @@ open import Relation.Binary.Structures
 open import Relation.Binary.Bundles
   using (Setoid; DecSetoid; Poset; Preorder; TotalOrder; DecTotalOrder; StrictPartialOrder; StrictTotalOrder)
 open import Relation.Binary.Definitions
-  using (Decidable; Reflexive; Transitive; Antisymmetric; Minimum; Maximum; Total; Irrelevant; Irreflexive; Asymmetric; Trans; Trichotomous; tri≈; tri<; tri>; _Respects₂_)
+  using (Decidable; DecidableEquality; Reflexive; Transitive; Antisymmetric; Minimum; Maximum; Total; Irrelevant; Irreflexive; Asymmetric; Trans; Trichotomous; tri≈; tri<; tri>; _Respects₂_)
 open import Relation.Binary.PropositionalEquality.Core
 open import Relation.Binary.PropositionalEquality.Properties
 open import Relation.Nullary.Decidable.Core using (True; yes; no; fromWitness)
@@ -48,7 +48,7 @@ private
 
 infix 4 _≟_
 
-_≟_ : Decidable {A = Bool} _≡_
+_≟_ : DecidableEquality Bool
 true  ≟ true  = yes refl
 false ≟ false = yes refl
 true  ≟ false = no λ()

src/Data/Char/Properties.agda

@@ -23,7 +23,7 @@ open import Relation.Binary.Bundles
 open import Relation.Binary.Structures
   using (IsDecEquivalence; IsStrictPartialOrder; IsStrictTotalOrder; IsPreorder; IsPartialOrder; IsDecPartialOrder; IsEquivalence)
 open import Relation.Binary.Definitions
-  using (Decidable; Trichotomous; Irreflexive; Transitive; Asymmetric; Antisymmetric; Symmetric; Substitutive; Reflexive; tri<; tri≈; tri>)
+  using (Decidable; DecidableEquality; Trichotomous; Irreflexive; Transitive; Asymmetric; Antisymmetric; Symmetric; Substitutive; Reflexive; tri<; tri≈; tri>)
 import Relation.Binary.Construct.On as On
 import Relation.Binary.Construct.Subst.Equality as Subst
 import Relation.Binary.Construct.Closure.Reflexive as Refl
@@ -55,7 +55,7 @@ open import Agda.Builtin.Char.Properties
 -- Properties of _≡_
 
 infix 4 _≟_
-_≟_ : Decidable {A = Char} _≡_
+_≟_ : DecidableEquality Char
 x ≟ y = map′ ≈⇒≡ ≈-reflexive (toℕ x ℕ.≟ toℕ y)
 
 setoid : Setoid _ _

src/Data/Container/Fixpoints/Sized.agda

@@ -8,10 +8,10 @@
 
 module Data.Container.Fixpoints.Sized where
 
-open import Level
-open import Size
-open import Codata.Sized.M
-open import Data.W.Sized
+open import Level using (Level; _⊔_)
+open import Size using (Size)
+open import Codata.Sized.M using (M)
+open import Data.W.Sized using (W)
 open import Data.Container hiding (μ) public
 
 private

src/Data/Container/Indexed/Relation/Binary/Pointwise/Properties.agda

@@ -11,7 +11,7 @@ module Data.Container.Indexed.Relation.Binary.Pointwise.Properties where
 open import Axiom.Extensionality.Propositional
 open import Data.Container.Indexed.Core
 open import Data.Container.Indexed.Relation.Binary.Pointwise
-open import Data.Product using (_,_; Σ-syntax; -,_)
+open import Data.Product.Base using (_,_; Σ-syntax; -,_)
 open import Level using (Level; _⊔_)
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality as P

src/Data/Fin/Permutation.agda

@@ -8,7 +8,7 @@
 
 module Data.Fin.Permutation where
 
-open import Data.Bool using (true; false)
+open import Data.Bool.Base using (true; false)
 open import Data.Empty using (⊥-elim)
 open import Data.Fin.Base
 open import Data.Fin.Patterns

src/Data/Fin/Properties.agda

@@ -22,7 +22,7 @@ open import Data.Nat.Base as ℕ
   using (ℕ; zero; suc; s≤s; z≤n; z<s; s<s; s<s⁻¹; _∸_; _^_)
 import Data.Nat.Properties as ℕ
 open import Data.Nat.Solver
-open import Data.Unit using (⊤; tt)
+open import Data.Unit.Base using (⊤; tt)
 open import Data.Product.Base as Product
   using (∃; ∃₂; _×_; _,_; map; proj₁; proj₂; uncurry; <_,_>)
 open import Data.Product.Properties using (,-injective)

src/Data/Fin/Substitution/Lemmas.agda

@@ -9,19 +9,19 @@
 module Data.Fin.Substitution.Lemmas where
 
 open import Data.Fin.Substitution
-open import Data.Nat hiding (_⊔_; _/_)
+open import Data.Nat.Base using (ℕ; zero; suc; _+_)
 open import Data.Fin.Base using (Fin; zero; suc; lift)
-open import Data.Vec.Base
+open import Data.Vec.Base using (lookup; []; _∷_; map)
 import Data.Vec.Properties as Vec
 open import Function.Base as Fun using (_∘_; _$_; flip)
+open import Level using (Level; _⊔_)
 open import Relation.Binary.PropositionalEquality.Core as ≡
   using (_≡_; refl; sym; cong; cong₂)
 open import Relation.Binary.PropositionalEquality.Properties
   using (module ≡-Reasoning)
 open import Relation.Binary.Construct.Closure.ReflexiveTransitive
   using (Star; ε; _◅_; _▻_)
 open ≡-Reasoning
-open import Level using (Level; _⊔_)
 open import Relation.Unary using (Pred)
 
 private

src/Data/Float/Base.agda

@@ -8,11 +8,12 @@
 
 module Data.Float.Base where
 
-open import Relation.Binary.Core using (Rel)
+open import Data.Bool.Base using (T)
 import Data.Word.Base as Word
 import Data.Maybe.Base as Maybe
 open import Function.Base using (_on_; _∘_)
 open import Agda.Builtin.Equality
+open import Relation.Binary.Core using (Rel)
 
 ------------------------------------------------------------------------
 -- Re-export built-ins publically
@@ -69,3 +70,8 @@ infix 4 _≈_
 
 _≈_ : Rel Float _
 _≈_ = _≡_ on Maybe.map Word.toℕ ∘ toWord
+
+
+infix 4 _≤_
+_≤_ : Rel Float _
+x ≤ y = T (x ≤ᵇ y)

src/Data/Integer.agda

@@ -31,7 +31,7 @@ open import Data.Integer.Properties public
 -- Show
 
 import Data.Nat.Show as ℕ using (show)
-open import Data.Sign as Sign using (Sign)
+open import Data.Sign.Base as Sign using (Sign)
 open import Data.String.Base using (String; _++_)
 
 show : ℤ → String