Proofs of the Binomial Theorem for (Commutative)Semiring [supersedes #1287]

src/Algebra/Properties/Semiring/Binomial.agda

@@ -18,7 +18,7 @@ open import Data.Fin.Base as Fin
 open import Data.Fin.Patterns using (0F)
 open import Data.Fin.Properties as Fin
   using (toℕ<n; toℕ-inject₁)
-open import Data.Fin.Relation.Unary.TopView
+open import Data.Fin.Relation.Unary.Top
   using (view; top; inj; view-inj; view-top; view-top-toℕ; module Instances)
 open import Function.Base using (_∘_)
 open import Relation.Binary.PropositionalEquality

src/Data/Fin/Relation/Unary/Top.agda

@@ -0,0 +1,141 @@
+------------------------------------------------------------------------
+-- 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.Empty using (⊥; ⊥-elim)
+open import Data.Nat.Base using (ℕ; zero; suc; _<_; _∸_)
+open import Data.Nat.Properties using (n∸n≡0; +-∸-assoc)
+open import Data.Product using (uncurry)
+open import Data.Sum using (inj₁; inj₂)
+open import Data.Fin.Base hiding (_<_)
+open import Data.Fin.Properties as Fin
+  using (suc-injective; toℕ-fromℕ; toℕ<n; toℕ-inject₁; inject₁ℕ<)
+open import Relation.Binary.PropositionalEquality
+
+private
+  variable
+    n : ℕ
+
+------------------------------------------------------------------------
+-- The View, considered as a unary relation on Fin (suc n)
+
+-- First, a lemma not in `Data.Fin.Properties`,
+-- but which establishes disjointness of the
+-- (interpretations of the) constructors of the View
+
+top≢inject₁ : ∀ (j : Fin n) → fromℕ n ≢ inject₁ j
+top≢inject₁ (suc j) eq = top≢inject₁ j (suc-injective eq)
+
+-- The View, itself
+
+data View : (i : Fin (suc n)) → Set where
+
+  top :                View (fromℕ n)
+  inj : (j : Fin n) → View (inject₁ j)
+
+-- The view covering function, witnessing soundness of the view
+
+view : ∀ {n} i → View {n} i
+view {n = zero}  zero = top
+view {n = suc _} zero = inj _
+view {n = suc n} (suc i) with view {n} i
+... | top   = top
+... | inj j = inj (suc j)
+
+-- Interpretation of the view constructors
+
+⟦_⟧ : ∀ {i} → View {n} i → Fin (suc n)
+⟦ top ⟧   = fromℕ _
+⟦ inj j ⟧ = inject₁ j
+
+-- Completeness of the view
+
+view-complete : ∀ {i} (v : View {n} i) → ⟦ v ⟧ ≡ i
+view-complete top     = refl
+view-complete (inj j) = refl
+
+-- 'Computational' behaviour of the covering function
+
+view-top : ∀ n → view {n} (fromℕ n) ≡ top
+view-top zero    = refl
+view-top (suc n) rewrite view-top n = refl
+
+view-inj : ∀ j → view {n} (inject₁ j) ≡ inj j
+view-inj zero       = refl
+view-inj (suc j) rewrite view-inj j = refl
+
+------------------------------------------------------------------------
+-- Experimental
+--
+-- Because we work --without-K, Agda's unifier will complain about
+-- attempts to match `refl` against hypotheses of the form
+--    `view {n] i ≡ v`
+-- or gets stuck trying to solve unification problems of the form
+--    (inferred index ≟ expected index)
+-- even when these problems are *provably* solvable.
+--
+-- So the two predicates on values of the view defined below
+-- are extensionally equivalent to the assertions
+-- `view {n] i ≡ top` and `view {n] i ≡ inj j`
+--
+-- But such assertions can only ever have a unique (irrelevant) proof
+-- so we introduce instances to witness them, themselves given by
+-- the functions `view-top` and `view-inj` defined above
+
+module Instances {n} where
+
+  data IsTop : ∀ {i} → View {n} i → Set where
+
+    top : IsTop top
+
+  instance
+
+    top⁺ : IsTop {i = fromℕ n} (view (fromℕ n))
+    top⁺ rewrite view-top n = top
+
+  data IsInj : ∀ {i} → View {n} i → Set where
+
+    inj : ∀ j → IsInj (inj j)
+
+  instance
+
+    inj⁺ : ∀ {j} → IsInj (view (inject₁ j))
+    inj⁺ {j} rewrite view-inj j = inj j
+
+    inject₁≡⁺ : ∀ {i} {j} {eq : inject₁ i ≡ j} → IsInj (view j)
+    inject₁≡⁺ {eq = refl} = inj⁺
+
+    n≢inject₁⁺ : ∀ {i} {n≢i : n ≢ toℕ (inject₁ i)} → IsInj (view i)
+    n≢inject₁⁺ {i} {n≢i} with view i
+    ... | top   = ⊥-elim (n≢i (begin
+      n                         ≡˘⟨ toℕ-fromℕ n ⟩
+      toℕ (fromℕ n)           ≡˘⟨ toℕ-inject₁ (fromℕ n) ⟩
+      toℕ (inject₁ (fromℕ n)) ∎)) where open ≡-Reasoning
+    ... | inj j = inj j
+
+open Instances
+
+------------------------------------------------------------------------
+-- As a corollary, we obtain two useful properties, which are
+-- witnessed by, but can also serve as proxy replacements for,
+-- the corresponding properties in `Data.Fin.Properties`
+
+module _ {n} where
+
+  view-top-toℕ : ∀ i → .{{IsTop (view i)}} → toℕ i ≡ n
+  view-top-toℕ i with top ← view i = toℕ-fromℕ n
+
+  view-inj-toℕ< : ∀ i → .{{IsInj (view i)}} → toℕ i < n
+  view-inj-toℕ< i with inj j ← view i = inject₁ℕ< j
+