diff --git a/CHANGELOG.md b/CHANGELOG.md index 420d85fddc..0d5ca18934 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1174,6 +1174,8 @@ Deprecated names Likewise under issue #1726: the properties `≺⇒<′` and `<′⇒≺` have been deprecated in favour of their proxy counterparts `<⇒<′` and `<′⇒<`. + Additionally, `lower₁-inject₁′` has been deprecated in favour of `inject₁≡⇒lower₁≡`. + * In `Data.Fin.Permutation.Components`: ``` reverse ↦ Data.Fin.Base.opposite @@ -1585,6 +1587,11 @@ New modules Data.Default ``` +* A small library defining a structurally recursive view of `Fin n`: + ``` + Data.Fin.Relation.Unary.Top + ``` + * A small library for a non-empty fresh list: ``` Data.List.Fresh.NonEmpty @@ -2146,6 +2153,8 @@ Additions to existing modules cast-is-id : cast eq k ≡ k subst-is-cast : subst Fin eq k ≡ cast eq k cast-trans : cast eq₂ (cast eq₁ k) ≡ cast (trans eq₁ eq₂) k + + fromℕ≢inject₁ : {i : Fin n} → fromℕ n ≢ inject₁ i ``` * Added new functions in `Data.Integer.Base`: diff --git a/README/Data/Fin/Relation/Unary/Lower.agda b/README/Data/Fin/Relation/Unary/Lower.agda new file mode 100644 index 0000000000..f71b02cfa2 --- /dev/null +++ b/README/Data/Fin/Relation/Unary/Lower.agda @@ -0,0 +1,122 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Example use of the 'top' view of Fin +-- +-- This is an example of a view of (elements of) a datatype, +-- here i : Fin (suc n), which exhibits every such i as +-- * either, i = fromℕ n +-- * or, i = inject₁ j for a unique j : Fin n +-- +-- Using this view, we can redefine certain operations in `Data.Fin.Base`, +-- together with their corresponding properties in `Data.Fin.Properties`. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module README.Data.Fin.Relation.Unary.Lower where + +open import Data.Nat.Base using (ℕ; zero; suc) +open import Data.Fin.Base using (Fin; zero; suc; toℕ; fromℕ; inject₁) +open import Data.Fin.Properties + using (toℕ-fromℕ; toℕ-inject₁; toℕ-inject₁-≢; inject₁-injective) +open import Data.Fin.Relation.Unary.Top + using (view; view≢; ‵fromℕ; ‵inject₁; ‵inj₁) +open import Level using (Level) +open import Relation.Nullary.Negation.Core using (contradiction) +open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; sym; cong) + +private + variable + ℓ : Level + n : ℕ + i j : Fin n + +------------------------------------------------------------------------ +-- Reimplementation of `Data.Fin.Base.lower₁` and its properties, +-- together with the streamlined versions obtained from the view. + +-- definition of lower₁/inject₁⁻¹ + +lower₁ : ∀ (i : Fin (suc n)) → n ≢ toℕ i → Fin n +lower₁ i n≢i with view i +... | ‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i +... | ‵inject₁ j = j + +inject₁⁻¹ : ∀ (i : Fin (suc n)) → (n ≢ toℕ i) → Fin n +inject₁⁻¹ i n≢i with ‵inj₁ j ← view≢ n≢i = j + +------------------------------------------------------------------------ +-- properties of lower₁/inject₁⁻¹ + +toℕ-lower₁ : ∀ i (n≢i : n ≢ toℕ i) → toℕ (lower₁ i n≢i) ≡ toℕ i +toℕ-lower₁ i n≢i with view i +... | ‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i +... | ‵inject₁ j = sym (toℕ-inject₁ j) + +toℕ-inject₁⁻¹ : ∀ i (n≢i : n ≢ toℕ i) → toℕ (inject₁⁻¹ i n≢i) ≡ toℕ i +toℕ-inject₁⁻¹ i n≢i with ‵inj₁ j ← view≢ n≢i = sym (toℕ-inject₁ j) + +lower₁-injective : ∀ {n≢i : n ≢ toℕ i} {n≢j : n ≢ toℕ j} → + lower₁ i n≢i ≡ lower₁ j n≢j → i ≡ j +lower₁-injective {i = i} {j = j} {n≢i} {n≢j} eq with view i +... | ‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i +... | ‵inject₁ _ with view j +... | ‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢j +... | ‵inject₁ _ = cong inject₁ eq + +inject₁⁻¹-injective : ∀ {n≢i : n ≢ toℕ i} {n≢j : n ≢ toℕ j} → + inject₁⁻¹ i n≢i ≡ inject₁⁻¹ j n≢j → i ≡ j +inject₁⁻¹-injective {i = i} {j = j} {n≢i} {n≢j} eq + with ‵inj₁ _ ← view≢ n≢i | ‵inj₁ _ ← view≢ n≢j = cong inject₁ eq + +lower₁-irrelevant : ∀ (i : Fin (suc n)) (n≢i₁ n≢i₂ : n ≢ toℕ i) → + lower₁ i n≢i₁ ≡ lower₁ i n≢i₂ +lower₁-irrelevant i n≢i₁ n≢i₂ with view i +... | ‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i₁ +... | ‵inject₁ _ = refl + +-- here we need/use a helper function, in order to avoid having +-- to appeal to injectivity of inject₁ in the unifier +inject₁⁻¹-irrelevant′ : ∀ {i j : Fin (suc n)} (i≡j : i ≡ j) → + (n≢i : n ≢ toℕ i) (n≢j : n ≢ toℕ j) → + inject₁⁻¹ i n≢i ≡ inject₁⁻¹ j n≢j +inject₁⁻¹-irrelevant′ eq n≢i n≢j + with ‵inj₁ _ ← view≢ n≢i | ‵inj₁ _ ← view≢ n≢j = inject₁-injective eq + +inject₁⁻¹-irrelevant : ∀ (i : Fin (suc n)) (n≢i₁ n≢i₂ : n ≢ toℕ i) → + inject₁⁻¹ i n≢i₁ ≡ inject₁⁻¹ i n≢i₂ +inject₁⁻¹-irrelevant i = inject₁⁻¹-irrelevant′ refl + +------------------------------------------------------------------------ +-- inject₁ and lower₁/inject₁⁻¹ + +inject₁-lower₁ : ∀ (i : Fin (suc n)) (n≢i : n ≢ toℕ i) → + inject₁ (lower₁ i n≢i) ≡ i +inject₁-lower₁ i n≢i with view i +... | ‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i +... | ‵inject₁ _ = refl + +inject₁-inject₁⁻¹ : ∀ (i : Fin (suc n)) (n≢i : n ≢ toℕ i) → + inject₁ (inject₁⁻¹ i n≢i) ≡ i +inject₁-inject₁⁻¹ i n≢i with ‵inj₁ _ ← view≢ n≢i = refl + +inject₁≡⇒lower₁≡ : {i : Fin (ℕ.suc n)} (n≢i : n ≢ toℕ i) → + inject₁ j ≡ i → lower₁ i n≢i ≡ j +inject₁≡⇒lower₁≡ {i = i} n≢i inject₁[j]≡i with view i +... | ‵fromℕ {n} = contradiction (sym (toℕ-fromℕ n)) n≢i +... | ‵inject₁ _ = sym (inject₁-injective inject₁[j]≡i) + +inject₁≡⇒inject₁⁻¹≡ : {i : Fin (ℕ.suc n)} (n≢i : n ≢ toℕ i) → + inject₁ j ≡ i → inject₁⁻¹ i n≢i ≡ j +inject₁≡⇒inject₁⁻¹≡ {i = i} n≢i inject₁[j]≡i with ‵inj₁ _ ← view≢ n≢i + = sym (inject₁-injective inject₁[j]≡i) + +lower₁-inject₁ : ∀ (i : Fin n) → + lower₁ (inject₁ i) (toℕ-inject₁-≢ i) ≡ i +lower₁-inject₁ {n} i = inject₁≡⇒lower₁≡ (toℕ-inject₁-≢ i) refl + +inject₁⁻¹-inject₁ : ∀ (i : Fin n) → + inject₁⁻¹ (inject₁ i) (toℕ-inject₁-≢ i) ≡ i +inject₁⁻¹-inject₁ {n} i = inject₁≡⇒inject₁⁻¹≡ (toℕ-inject₁-≢ i) refl + diff --git a/README/Data/Fin/Relation/Unary/Top.agda b/README/Data/Fin/Relation/Unary/Top.agda new file mode 100644 index 0000000000..e602932827 --- /dev/null +++ b/README/Data/Fin/Relation/Unary/Top.agda @@ -0,0 +1,100 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Example use of the 'top' view of Fin +-- +-- This is an example of a view of (elements of) a datatype, +-- here i : Fin (suc n), which exhibits every such i as +-- * either, i = fromℕ n +-- * or, i = inject₁ j for a unique j : Fin n +-- +-- Using this view, we can redefine certain operations in `Data.Fin.Base`, +-- together with their corresponding properties in `Data.Fin.Properties`. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module README.Data.Fin.Relation.Unary.Top where + +open import Data.Nat.Base using (ℕ; zero; suc; _∸_; _≤_) +open import Data.Nat.Properties using (n∸n≡0; +-∸-assoc; ≤-reflexive) +open import Data.Fin.Base using (Fin; zero; suc; toℕ; fromℕ; inject₁; _>_) +open import Data.Fin.Properties using (toℕ-fromℕ; toℕ-weakInduction) +open import Data.Fin.Relation.Unary.Top +import Induction.WellFounded as WF +open import Level using (Level) +open import Relation.Binary.PropositionalEquality +open import Relation.Unary using (Pred) + +private + variable + ℓ : Level + n : ℕ + +------------------------------------------------------------------------ +-- Reimplementation of `Data.Fin.Base.opposite`, and its properties + +-- Definition + +opposite : Fin n → Fin n +opposite {suc n} i with view i +... | ‵fromℕ = zero +... | ‵inject₁ j = suc (opposite {n} j) + +-- Properties + +opposite-zero≡fromℕ : ∀ n → opposite {suc n} zero ≡ fromℕ n +opposite-zero≡fromℕ zero = refl +opposite-zero≡fromℕ (suc n) = cong suc (opposite-zero≡fromℕ n) + +opposite-fromℕ≡zero : ∀ n → opposite {suc n} (fromℕ n) ≡ zero +opposite-fromℕ≡zero n rewrite view-fromℕ n = refl + +opposite-suc≡inject₁-opposite : (j : Fin n) → + opposite (suc j) ≡ inject₁ (opposite j) +opposite-suc≡inject₁-opposite {suc n} i with view i +... | ‵fromℕ = refl +... | ‵inject₁ j = cong suc (opposite-suc≡inject₁-opposite {n} j) + +opposite-involutive : (j : Fin n) → opposite (opposite j) ≡ j +opposite-involutive {suc n} zero + rewrite opposite-zero≡fromℕ n + | view-fromℕ n = refl +opposite-involutive {suc n} (suc i) + rewrite opposite-suc≡inject₁-opposite i + | view-inject₁ (opposite i) = cong suc (opposite-involutive i) + +opposite-suc : (j : Fin n) → toℕ (opposite (suc j)) ≡ toℕ (opposite j) +opposite-suc j = begin + toℕ (opposite (suc j)) ≡⟨ cong toℕ (opposite-suc≡inject₁-opposite j) ⟩ + toℕ (inject₁ (opposite j)) ≡⟨ toℕ-inject₁ (opposite j) ⟩ + toℕ (opposite j) ∎ where open ≡-Reasoning + +opposite-prop : (j : Fin n) → toℕ (opposite j) ≡ n ∸ suc (toℕ j) +opposite-prop {suc n} i with view i +... | ‵fromℕ rewrite toℕ-fromℕ n | n∸n≡0 n = refl +... | ‵inject₁ j = begin + suc (toℕ (opposite j)) ≡⟨ cong suc (opposite-prop j) ⟩ + suc (n ∸ suc (toℕ j)) ≡˘⟨ +-∸-assoc 1 (toℕ-weakInduction` + +open WF using (Acc; acc) + +>-weakInduction : (P : Pred (Fin (suc n)) ℓ) → + P (fromℕ n) → + (∀ i → P (suc i) → P (inject₁ i)) → + ∀ i → P i +>-weakInduction P Pₙ Pᵢ₊₁⇒Pᵢ i = induct (>-wellFounded i) + where + induct : ∀ {i} → Acc _>_ i → P i + induct {i} (acc rec) with view i + ... | ‵fromℕ = Pₙ + ... | ‵inject₁ j = Pᵢ₊₁⇒Pᵢ j (induct (rec _ inject₁[j]+1≤[j+1])) + where + inject₁[j]+1≤[j+1] : suc (toℕ (inject₁ j)) ≤ toℕ (suc j) + inject₁[j]+1≤[j+1] = ≤-reflexive (toℕ-inject₁ (suc j)) diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 0f520afda5..9c94958033 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -449,6 +449,9 @@ toℕ-inject {i = suc i} (suc j) = cong suc (toℕ-inject j) -- inject₁ ------------------------------------------------------------------------ +fromℕ≢inject₁ : fromℕ n ≢ inject₁ i +fromℕ≢inject₁ {i = suc i} eq = fromℕ≢inject₁ {i = i} (suc-injective eq) + inject₁-injective : inject₁ i ≡ inject₁ j → i ≡ j inject₁-injective {i = zero} {zero} i≡j = refl inject₁-injective {i = suc i} {suc j} i≡j = @@ -494,6 +497,13 @@ lower₁-injective {suc n} {zero} {zero} {_} {_} refl = refl lower₁-injective {suc n} {suc i} {suc j} {n≢i} {n≢j} eq = cong suc (lower₁-injective (suc-injective eq)) +lower₁-irrelevant : ∀ (i : Fin (suc n)) (n≢i₁ n≢i₂ : n ≢ toℕ i) → + lower₁ i n≢i₁ ≡ lower₁ i n≢i₂ +lower₁-irrelevant {zero} zero 0≢0 _ = contradiction refl 0≢0 +lower₁-irrelevant {suc n} zero _ _ = refl +lower₁-irrelevant {suc n} (suc i) _ _ = + cong suc (lower₁-irrelevant i _ _) + ------------------------------------------------------------------------ -- inject₁ and lower₁ @@ -504,26 +514,13 @@ inject₁-lower₁ {suc n} zero _ = refl inject₁-lower₁ {suc n} (suc i) n+1≢i+1 = cong suc (inject₁-lower₁ i (n+1≢i+1 ∘ cong suc)) -lower₁-inject₁′ : ∀ (i : Fin n) (n≢i : n ≢ toℕ (inject₁ i)) → - lower₁ (inject₁ i) n≢i ≡ i -lower₁-inject₁′ zero _ = refl -lower₁-inject₁′ (suc i) n+1≢i+1 = - cong suc (lower₁-inject₁′ i (n+1≢i+1 ∘ cong suc)) +inject₁≡⇒lower₁≡ : ∀ {j : Fin (ℕ.suc n)} (n≢j : n ≢ toℕ j) → + inject₁ i ≡ j → lower₁ j n≢j ≡ i +inject₁≡⇒lower₁≡ n≢j i≡j = inject₁-injective (trans (inject₁-lower₁ _ n≢j) (sym i≡j)) lower₁-inject₁ : ∀ (i : Fin n) → lower₁ (inject₁ i) (toℕ-inject₁-≢ i) ≡ i -lower₁-inject₁ i = lower₁-inject₁′ i (toℕ-inject₁-≢ i) - -lower₁-irrelevant : ∀ (i : Fin (suc n)) (n≢i₁ n≢i₂ : n ≢ toℕ i) → - lower₁ i n≢i₁ ≡ lower₁ i n≢i₂ -lower₁-irrelevant {zero} zero 0≢0 _ = contradiction refl 0≢0 -lower₁-irrelevant {suc n} zero _ _ = refl -lower₁-irrelevant {suc n} (suc i) _ _ = - cong suc (lower₁-irrelevant i _ _) - -inject₁≡⇒lower₁≡ : ∀ {i : Fin n} {j : Fin (ℕ.suc n)} → - (n≢j : n ≢ toℕ j) → inject₁ i ≡ j → lower₁ j n≢j ≡ i -inject₁≡⇒lower₁≡ n≢j i≡j = inject₁-injective (trans (inject₁-lower₁ _ n≢j) (sym i≡j)) +lower₁-inject₁ i = inject₁≡⇒lower₁≡ (toℕ-inject₁-≢ i) refl ------------------------------------------------------------------------ -- inject≤ @@ -1165,3 +1162,12 @@ Please use <⇒<′ instead." "Warning: <′⇒≺ was deprecated in v2.0. Please use <′⇒< instead." #-} + +lower₁-inject₁′ : ∀ (i : Fin n) (n≢i : n ≢ toℕ (inject₁ i)) → + lower₁ (inject₁ i) n≢i ≡ i +lower₁-inject₁′ i n≢i = inject₁≡⇒lower₁≡ n≢i refl +{-# WARNING_ON_USAGE lower₁-inject₁′ +"Warning: lower₁-inject₁′ was deprecated in v2.0. +Please use inject₁≡⇒lower₁≡ instead." +#-} + diff --git a/src/Data/Fin/Relation/Unary/Top.agda b/src/Data/Fin/Relation/Unary/Top.agda new file mode 100644 index 0000000000..a9e425b855 --- /dev/null +++ b/src/Data/Fin/Relation/Unary/Top.agda @@ -0,0 +1,126 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- The 'top' view of Fin. +-- +-- This is an example of a view of (elements of) a datatype, +-- here i : Fin (suc n), which exhibits every such i as +-- * either, i = fromℕ n +-- * or, i = inject₁ j for a unique j : Fin n +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Data.Fin.Relation.Unary.Top where + +open import Data.Nat.Base using (ℕ; zero; suc) +open import Data.Fin.Base as Fin using (Fin; zero; suc; fromℕ; inject₁) +open import Function.Base using (_∘_) +open import Relation.Binary.PropositionalEquality.Core +open import Relation.Nullary.Negation.Core using (contradiction) + +private + variable + n : ℕ + i : Fin n + +------------------------------------------------------------------------ +-- The View, considered as a unary relation on Fin n + +-- NB `Data.Fin.Properties.fromℕ≢inject₁` establishes that the following +-- inductively defined family on `Fin n` has constructors which target +-- *disjoint* instances of the family (moreover at indices `n = suc _`); +-- hence the interpretations of the View constructors will also be disjoint. + +data View : (i : Fin n) → Set where + ‵fromℕ : View (fromℕ n) + ‵inj₁ : View i → View (inject₁ i) + +pattern ‵inject₁ i = ‵inj₁ {i = i} _ + +-- The view covering function, witnessing soundness of the view + +view : (i : Fin n) → View i +view zero = view-zero where + view-zero : View (zero {n}) + view-zero {n = zero} = ‵fromℕ + view-zero {n = suc _} = ‵inj₁ view-zero +view (suc i) with view i +... | ‵fromℕ = ‵fromℕ +... | ‵inject₁ i = ‵inj₁ (view (suc i)) + +-- Interpretation of the view constructors + +⟦_⟧ : {i : Fin n} → View i → Fin n +⟦ ‵fromℕ ⟧ = fromℕ _ +⟦ ‵inject₁ i ⟧ = inject₁ i + +-- Completeness of the view + +view-complete : (v : View i) → ⟦ v ⟧ ≡ i +view-complete ‵fromℕ = refl +view-complete (‵inj₁ _) = refl + +-- 'Computational' behaviour of the covering function + +view-fromℕ : ∀ n → view (fromℕ n) ≡ ‵fromℕ +view-fromℕ zero = refl +view-fromℕ (suc n) rewrite view-fromℕ n = refl + +view-inject₁ : (i : Fin n) → view (inject₁ i) ≡ ‵inj₁ (view i) +view-inject₁ zero = refl +view-inject₁ (suc i) rewrite view-inject₁ i = refl + +-- Uniqueness of the view + +view-unique : (v : View i) → view i ≡ v +view-unique ‵fromℕ = view-fromℕ _ +view-unique (‵inj₁ {i = i} v) = begin + view (inject₁ i) ≡⟨ view-inject₁ i ⟩ + ‵inj₁ (view i) ≡⟨ cong ‵inj₁ (view-unique v) ⟩ + ‵inj₁ v ∎ where open ≡-Reasoning + +-- An important distinguished observer and its properties + +toℕ : {i : Fin n} → View i → ℕ +toℕ (‵fromℕ {n}) = n +toℕ (‵inj₁ v) = toℕ v + +toℕ[view[suc]]≡suc[toℕ[view]] : (i : Fin n) → + toℕ (view (suc i)) ≡ suc (toℕ (view i)) +toℕ[view[suc]]≡suc[toℕ[view]] i with view i +... | ‵fromℕ {n} = refl +... | ‵inj₁ {i = j} v = trans (toℕ[view[suc]]≡suc[toℕ[view]] j) + (cong (suc ∘ toℕ) (view-unique v)) + +toℕ[view]≡Fin[toℕ] : (i : Fin n) → toℕ (view i) ≡ Fin.toℕ i +toℕ[view]≡Fin[toℕ] {n = suc n} zero = toℕ[view[zero]]≡Fin[toℕ[zero]] n + where + toℕ[view[zero]]≡Fin[toℕ[zero]] : ∀ n → toℕ (view (zero {n})) ≡ zero + toℕ[view[zero]]≡Fin[toℕ[zero]] zero = refl + toℕ[view[zero]]≡Fin[toℕ[zero]] (suc n) = toℕ[view[zero]]≡Fin[toℕ[zero]] n +toℕ[view]≡Fin[toℕ] {n = suc n} (suc i) + rewrite toℕ[view[suc]]≡suc[toℕ[view]] i = cong suc (toℕ[view]≡Fin[toℕ] i) + +-- independent reimplementation of Data.Fin.Properties.toℕ-fromℕ +n≡Fin[toℕ[fromℕ]] : ∀ n → n ≡ Fin.toℕ (fromℕ n) +n≡Fin[toℕ[fromℕ]] n = begin -- toℕ[view]≡Fin[toℕ] i + n ≡⟨⟩ + toℕ (‵fromℕ {n}) ≡⟨ sym (cong toℕ (view-fromℕ n)) ⟩ + toℕ (view (fromℕ n)) ≡⟨ toℕ[view]≡Fin[toℕ] (fromℕ n) ⟩ + Fin.toℕ (fromℕ n) ∎ where open ≡-Reasoning + +------------------------------------------------------------------------ +-- Derived induction principle from the Top view, via another view! + +-- The idea being, that in what follows, a call pattern is repeated over +-- and over again, so should be reified as induction over a revised view, +-- `View≢`/`view≢`obtained from `View`/`view` by restricting the domain. + +data View≢ : {i : Fin (suc n)} → n ≢ Fin.toℕ i → Set where + ‵inj₁ : (j : Fin n) {n≢j : n ≢ Fin.toℕ (inject₁ j)} → View≢ n≢j + +view≢ : {i : Fin (suc n)} (n≢i : n ≢ Fin.toℕ i) → View≢ n≢i +view≢ {i = i} n≢ with view i +... | ‵fromℕ {n} = contradiction (n≡Fin[toℕ[fromℕ]] n) n≢ +... | ‵inject₁ j = ‵inj₁ j