Merge branch 'agda:master' into refactor-fresh

Author: jamesmckinna

CHANGELOG.md

@@ -13,6 +13,9 @@ Bug-fixes
 
 * Fix a typo in `Algebra.Morphism.Construct.DirectProduct`.
 
+* Fix a typo in `Data.Rational.Properties`: `nonPos*nonPos⇒nonPos` erroneously named,
+  corrected to `nonPos*nonPos⇒nonNeg`.
+
 * Fix a typo in `Function.Construct.Constant`.
 
 Non-backwards compatible changes
@@ -21,6 +24,14 @@ Non-backwards compatible changes
 Minor improvements
 ------------------
 
+* The types of `Data.Vec.Base.{truncate|padRight}` have been weakened so
+  that the argument of type `m ≤ n` is marked as irrelevant. This should be
+  backwards compatible, but does change the intensional behaviour of these
+  functions to be more eager, because no longer blocking on pattern matching
+  on that argument. Corresponding changes have been made to the types of their
+  properties (and their proofs). In particular, `truncate-irrelevant` is now
+  deprecated, because definitionally trivial.
+
 * The type of `Relation.Nullary.Negation.Core.contradiction-irr` has been further
   weakened so that the negated hypothesis `¬ A` is marked as irrelevant. This is
   safe to do, in view of `Relation.Nullary.Recomputable.Properties.¬-recompute`.
@@ -68,6 +79,16 @@ Deprecated names
   ¬∀⟶∃¬-          ↦   ¬∀⇒∃¬
   ```
 
+* In `Data.Rational.Properties`:
+  ```agda
+  nonPos*nonPos⇒nonPos  ↦  nonPos*nonPos⇒nonNeg
+  ```
+
+* In `Data.Vec.Properties`:
+  ```agda
+  truncate-irrelevant  ↦  Relation.Binary.PropositionalEquality.Core.refl
+  ```
+
 * In `Relation.Nullary.Decidable.Core`:
   ```agda
   ⊤-dec     ↦   ⊤?
@@ -100,6 +121,8 @@ New modules
 
 * `Algebra.Properties.Semiring`.
 
+* `Data.List.Fresh.Membership.DecSetoid`.
+
 * `Data.List.Relation.Binary.Permutation.Algorithmic{.Properties}` for the Choudhury and Fiore definition of permutation, and its equivalence with `Declarative` below.
 
 * `Data.List.Relation.Binary.Permutation.Declarative{.Properties}` for the least congruence on `List` making `_++_` commutative, and its equivalence with the `Setoid` definition.
@@ -236,46 +259,55 @@ Additions to existing modules
 * In `Data.Vec.Properties`:
   ```agda
   map-removeAt : ∀ (f : A → B) (xs : Vec A (suc n)) (i : Fin (suc n)) →
-               map f (removeAt xs i) ≡ removeAt (map f xs) i
+                 map f (removeAt xs i) ≡ removeAt (map f xs) i
 
   updateAt-take : (xs : Vec A (m + n)) (i : Fin m) (f : A → A) →
                   updateAt (take m xs) i f ≡ take m (updateAt xs (inject≤ i (m≤m+n m n)) f)
 
-  truncate-zipWith : (f : A → B → C) (m≤n : m ≤ n) (xs : Vec A n) (ys : Vec B n) →
-                    truncate m≤n (zipWith f xs ys) ≡ zipWith f (truncate m≤n xs) (truncate m≤n ys)
+  truncate-zipWith : (f : A → B → C) .(m≤n : m ≤ n) (xs : Vec A n) (ys : Vec B n) →
+                     truncate m≤n (zipWith f xs ys) ≡ zipWith f (truncate m≤n xs) (truncate m≤n ys)
 
-  truncate-zipWith-truncate : (f : A → B → C) (m≤n : m ≤ n) (n≤o : n ≤ o) (xs : Vec A o) (ys : Vec B n) →
+  truncate-zipWith-truncate : (f : A → B → C) .(m≤n : m ≤ n) .(n≤o : n ≤ o)
+                              (xs : Vec A o) (ys : Vec B n) →
                               truncate m≤n (zipWith f (truncate n≤o xs) ys) ≡
                               zipWith f (truncate (≤-trans m≤n n≤o) xs) (truncate m≤n ys)
 
-  truncate-updateAt : (m≤n : m ≤ n) (xs : Vec A n) (i : Fin m) (f : A → A) →
+  truncate-updateAt : .(m≤n : m ≤ n) (xs : Vec A n) (i : Fin m) (f : A → A) →
                       updateAt (truncate m≤n xs) i f ≡
                       truncate m≤n (updateAt xs (inject≤ i m≤n) f)
 
   updateAt-truncate : (xs : Vec A (m + n)) (i : Fin m) (f : A → A) →
                       updateAt (truncate (m≤m+n m n) xs) i f ≡
                       truncate (m≤m+n m n) (updateAt xs (inject≤ i (m≤m+n m n)) f)
 
-  map-truncate : (f : A → B) (m≤n : m ≤ n) (xs : Vec A n) →
-                map f (truncate m≤n xs) ≡ truncate m≤n (map f xs)
+  map-truncate : (f : A → B) .(m≤n : m ≤ n) (xs : Vec A n) →
+                 map f (truncate m≤n xs) ≡ truncate m≤n (map f xs)
 
-  padRight-lookup : (m≤n : m ≤ n) (a : A) (xs : Vec A m) (i : Fin m) → lookup (padRight m≤n a xs) (inject≤ i m≤n) ≡ lookup xs i
+  padRight-lookup : .(m≤n : m ≤ n) (a : A) (xs : Vec A m) (i : Fin m) →
+                    lookup (padRight m≤n a xs) (inject≤ i m≤n) ≡ lookup xs i
 
-  padRight-map : (f : A → B) (m≤n : m ≤ n) (a : A) (xs : Vec A m) → map f (padRight m≤n a xs) ≡ padRight m≤n (f a) (map f xs)
+  padRight-map : (f : A → B) .(m≤n : m ≤ n) (a : A) (xs : Vec A m) →
+                 map f (padRight m≤n a xs) ≡ padRight m≤n (f a) (map f xs)
 
-  padRight-zipWith : (f : A → B → C) (m≤n : m ≤ n) (a : A) (b : B) (xs : Vec A m) (ys : Vec B m) →
-                   zipWith f (padRight m≤n a xs) (padRight m≤n b ys) ≡ padRight m≤n (f a b) (zipWith f xs ys)
+  padRight-zipWith : (f : A → B → C) .(m≤n : m ≤ n) (a : A) (b : B)
+                     (xs : Vec A m) (ys : Vec B m) →
+                     zipWith f (padRight m≤n a xs) (padRight m≤n b ys) ≡
+                     padRight m≤n (f a b) (zipWith f xs ys)
 
-  padRight-zipWith₁ : (f : A → B → C) (o≤m : o ≤ m) (m≤n : m ≤ n) (a : A) (b : B) (xs : Vec A m) (ys : Vec B o) →
-                    zipWith f (padRight m≤n a xs) (padRight (≤-trans o≤m m≤n) b ys) ≡
-                    padRight m≤n (f a b) (zipWith f xs (padRight o≤m b ys))
+  padRight-zipWith₁ : (f : A → B → C) .(o≤m : o ≤ m) .(m≤n : m ≤ n) (a : A) (b : B)
+                      (xs : Vec A m) (ys : Vec B o) →
+                      zipWith f (padRight m≤n a xs) (padRight (≤-trans o≤m m≤n) b ys) ≡
+                      padRight m≤n (f a b) (zipWith f xs (padRight o≤m b ys))
 
-  padRight-take : (m≤n : m ≤ n) (a : A) (xs : Vec A m) .(n≡m+o : n ≡ m + o) → take m (cast n≡m+o (padRight m≤n a xs)) ≡ xs
+  padRight-take : .(m≤n : m ≤ n) (a : A) (xs : Vec A m) .(n≡m+o : n ≡ m + o) →
+                  take m (cast n≡m+o (padRight m≤n a xs)) ≡ xs
 
-  padRight-drop : (m≤n : m ≤ n) (a : A) (xs : Vec A m) .(n≡m+o : n ≡ m + o) → drop m (cast n≡m+o (padRight m≤n a xs)) ≡ replicate o a
+  padRight-drop : .(m≤n : m ≤ n) (a : A) (xs : Vec A m) .(n≡m+o : n ≡ m + o) →
+                  drop m (cast n≡m+o (padRight m≤n a xs)) ≡ replicate o a
 
-  padRight-updateAt : (m≤n : m ≤ n) (x : A) (xs : Vec A m) (f : A → A) (i : Fin m) →
-                    updateAt (padRight m≤n x xs) (inject≤ i m≤n) f ≡ padRight m≤n x (updateAt xs i f)
+  padRight-updateAt : .(m≤n : m ≤ n) (x : A) (xs : Vec A m) (f : A → A) (i : Fin m) →
+                      updateAt (padRight m≤n x xs) (inject≤ i m≤n) f ≡
+                      padRight m≤n x (updateAt xs i f)
   ```
 
 * In `Relation.Binary.Construct.Add.Extrema.NonStrict`:

src/Data/List/Fresh/Membership/DecSetoid.agda

@@ -0,0 +1,40 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Decidable setoid membership over fresh lists
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Relation.Binary.Bundles using (DecSetoid)
+
+module Data.List.Fresh.Membership.DecSetoid {a ℓ} (DS : DecSetoid a ℓ) where
+
+open import Level using (Level)
+open import Data.List.Fresh.Relation.Unary.Any using (any?)
+import Data.List.Fresh.Membership.Setoid as MembershipSetoid
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Definitions using (Decidable)
+open import Relation.Nullary.Decidable using (¬?)
+
+open DecSetoid DS using (setoid; _≟_) renaming (Carrier to A)
+
+private
+  variable
+    r : Level
+    R : Rel A r
+
+
+------------------------------------------------------------------------
+-- Re-export contents of Setoid membership
+open MembershipSetoid setoid public
+
+------------------------------------------------------------------------
+-- Other operations
+infix 4 _∈?_ _∉?_
+
+_∈?_ : Decidable (_∈_ {R = R})
+x ∈? xs = any? (x ≟_) xs
+
+_∉?_ : Decidable (_∉_ {R = R})
+x ∉? xs = ¬? (x ∈? xs)

src/Data/Rational/Properties.agda

@@ -1389,8 +1389,8 @@ nonNeg*nonPos⇒nonPos p q = nonPositive $ begin
   0ℚ     ∎
   where open ≤-Reasoning
 
-nonPos*nonPos⇒nonPos : ∀ p .{{_ : NonPositive p}} q .{{_ : NonPositive q}} → NonNegative (p * q)
-nonPos*nonPos⇒nonPos p q = nonNegative $ begin
+nonPos*nonPos⇒nonNeg : ∀ p .{{_ : NonPositive p}} q .{{_ : NonPositive q}} → NonNegative (p * q)
+nonPos*nonPos⇒nonNeg p q = nonNegative $ begin
   0ℚ     ≡⟨ *-zeroʳ p ⟨
   p * 0ℚ ≤⟨ *-monoˡ-≤-nonPos p (nonPositive⁻¹ q) ⟩
   p * q  ∎
@@ -1870,3 +1870,11 @@ Please use neg<pos instead."
 open Data.Rational.Base public
   using (+-rawMagma; +-0-rawGroup; *-rawMagma; +-*-rawNearSemiring; +-*-rawSemiring; +-*-rawRing)
   renaming (+-0-rawMonoid to +-rawMonoid; *-1-rawMonoid to *-rawMonoid)
+
+-- Version 2.4
+
+nonPos*nonPos⇒nonPos = nonPos*nonPos⇒nonNeg
+{-# WARNING_ON_USAGE nonPos*nonPos⇒nonPos
+"Warning: nonPos*nonPos⇒nonPos was deprecated in v2.4.
+Please use nonPos*nonPos⇒nonNeg instead."
+#-}

src/Data/Vec/Base.agda

@@ -289,14 +289,14 @@ uncons (x ∷ xs) = x , xs
 -- Operations involving ≤
 
 -- Take the first 'm' elements of a vector.
-truncate : ∀ {m n} → m ≤ n → Vec A n → Vec A m
-truncate {m = zero} _ _    = []
-truncate (s≤s le) (x ∷ xs) = x ∷ (truncate le xs)
+truncate : .(m ≤ n) → Vec A n → Vec A m
+truncate {m = zero}  _  _        = []
+truncate {m = suc _} le (x ∷ xs) = x ∷ (truncate (s≤s⁻¹ le) xs)
 
 -- Pad out a vector with extra elements.
-padRight : ∀ {m n} → m ≤ n → A → Vec A m → Vec A n
-padRight z≤n      a xs       = replicate _ a
-padRight (s≤s le) a (x ∷ xs) = x ∷ padRight le a xs
+padRight : .(m ≤ n) → A → Vec A m → Vec A n
+padRight {n = n}     _  a []       = replicate n a
+padRight {n = suc _} le a (x ∷ xs) = x ∷ padRight (s≤s⁻¹ le) a xs
 
 ------------------------------------------------------------------------
 -- Operations for converting between lists