Skip to content

Commit 5619f17

Browse files
committed
add: lemmas for decidable equality on Fin, plus backport to Nat
1 parent 4b3bb54 commit 5619f17

File tree

3 files changed

+27
-2
lines changed

3 files changed

+27
-2
lines changed

CHANGELOG.md

Lines changed: 12 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -237,13 +237,19 @@ Additions to existing modules
237237
∙-cong-∣ : x ∣ y → a ∣ b → x ∙ a ∣ y ∙ b
238238
```
239239

240+
* In `Data.Fin.Properties`:
241+
```agda
242+
≡-irrelevant : Irrelevant {A = Fin n} _≡_
243+
≟-diag : (eq : i ≡ j) → (i ≟ j) ≡ yes eq
244+
≟-diag-refl : (i : Fin n) → (i ≟ i) ≡ yes refl
245+
```
246+
240247
* In `Data.Fin.Subset`:
241248
```agda
242249
_⊇_ : Subset n → Subset n → Set
243250
_⊉_ : Subset n → Subset n → Set
244251
_⊃_ : Subset n → Subset n → Set
245252
_⊅_ : Subset n → Subset n → Set
246-
247253
```
248254

249255
* In `Data.Fin.Subset.Induction`:
@@ -278,6 +284,11 @@ Additions to existing modules
278284
filter-↭ : ∀ (P? : Pred.Decidable P) → xs ↭ ys → filter P? xs ↭ filter P? ys
279285
```
280286

287+
* In `Data.Nat.Properties`:
288+
```agda
289+
≟-diag-refl : ∀ n → (n ≟ n) ≡ yes refl
290+
```
291+
281292
* In `Data.Product.Function.Dependent.Propositional`:
282293
```agda
283294
Σ-↪ : (I↪J : I ↪ J) → (∀ {j} → A (from I↪J j) ↪ B j) → Σ I A ↪ Σ J B

src/Data/Fin/Properties.agda

Lines changed: 12 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@
1111
module Data.Fin.Properties where
1212

1313
open import Axiom.Extensionality.Propositional
14+
open import Axiom.UniquenessOfIdentityProofs using (module Decidable⇒UIP)
1415
open import Algebra.Definitions using (Involutive)
1516
open import Effect.Applicative using (RawApplicative)
1617
open import Effect.Functor using (RawFunctor)
@@ -44,10 +45,11 @@ open import Relation.Binary.PropositionalEquality.Core as ≡
4445
using (_≡_; _≢_; refl; sym; trans; cong; cong₂; subst; _≗_)
4546
open import Relation.Binary.PropositionalEquality.Properties as ≡
4647
using (module ≡-Reasoning)
48+
open import Relation.Binary.PropositionalEquality using (≡-≟-identity)
4749
open import Relation.Nullary.Decidable as Dec
4850
using (Dec; _because_; yes; no; _×-dec_; _⊎-dec_; map′)
4951
open import Relation.Nullary.Negation.Core using (¬_; contradiction)
50-
open import Relation.Nullary.Reflects using (Reflects; invert)
52+
open import Relation.Nullary.Reflects using (invert)
5153
open import Relation.Unary as U
5254
using (U; Pred; Decidable; _⊆_; Satisfiable; Universal)
5355
open import Relation.Unary.Properties using (U?)
@@ -100,6 +102,15 @@ zero ≟ suc y = no λ()
100102
suc x ≟ zero = no λ()
101103
suc x ≟ suc y = map′ (cong suc) suc-injective (x ≟ y)
102104

105+
≡-irrelevant : Irrelevant {A = Fin n} _≡_
106+
≡-irrelevant = Decidable⇒UIP.≡-irrelevant _≟_
107+
108+
≟-diag : (eq : i ≡ j) (i ≟ j) ≡ yes eq
109+
≟-diag = ≡-≟-identity _≟_
110+
111+
≟-diag-refl : (i : Fin n) (i ≟ i) ≡ yes refl
112+
≟-diag-refl _ = ≟-diag refl
113+
103114
------------------------------------------------------------------------
104115
-- Structures
105116

src/Data/Nat/Properties.agda

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -110,6 +110,9 @@ m ≟ n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n))
110110
≟-diag : (eq : m ≡ n) (m ≟ n) ≡ yes eq
111111
≟-diag = ≡-≟-identity _≟_
112112

113+
≟-diag-refl : n (n ≟ n) ≡ yes refl
114+
≟-diag-refl _ = ≟-diag refl
115+
113116
≡-isDecEquivalence : IsDecEquivalence (_≡_ {A = ℕ})
114117
≡-isDecEquivalence = record
115118
{ isEquivalence = isEquivalence

0 commit comments

Comments
 (0)