[discussion] a view-based analysis of punchOut, punchIn and pinch from Data.Fin

README/Data/Fin/Relation/Ternary/Pinch.agda

@@ -0,0 +1,53 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Example use of the 'Pinch' view of Fin
+--
+-- This is an example of a view of a function defined over a datatype,
+-- such that the recursion and call-pattern(s) of the function are
+-- precisely mirrored in the constructors of the view type
+--
+-- Using this view, we can exhibit the corresponding properties of
+-- the function `punchIn` defined in `Data.Fin.Properties`
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module README.Data.Fin.Relation.Ternary.Pinch where
+
+open import Data.Nat.Base as Nat using (ℕ; suc; ∣_-_∣)
+open import Data.Fin.Base using (Fin; zero; suc; toℕ; _≤_; _<_; pinch)
+open import Data.Fin.Relation.Ternary.Pinch
+open import Data.Product using (_,_; ∃)
+open import Function.Definitions.Core2 using (Surjective)
+open import Relation.Binary.Core
+open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
+
+private
+  variable
+    n : ℕ
+
+
+------------------------------------------------------------------------
+-- Properties of the function, derived from properties of the View
+
+pinch-surjective : ∀ (i : Fin n) → Surjective _≡_ (pinch i)
+pinch-surjective i k
+  with j , v ← view-surjective i k
+  with refl ← view-complete v = j , refl
+
+pinch-injective : ∀ {i : Fin n} {j k : Fin (ℕ.suc n)} →
+                  suc i ≢ j → suc i ≢ k → pinch i j ≡ pinch i k → j ≡ k
+pinch-injective {n = n} {i} {j} {k} = view-injective (view i j) (view i k)
+
+pinch-mono-≤ : ∀ (i : Fin n) → (pinch i) Preserves _≤_ ⟶ _≤_
+pinch-mono-≤ i {j} {k} = view-mono-≤ (view i j) (view i k)
+
+pinch-cancel-< : ∀ (i : Fin (suc n)) {j k} →
+                (pinch i j < pinch i k) → j < k
+pinch-cancel-< i {j} {k} = view-cancel-< (view i j) (view i k)
+
+pinch-≡⇒∣j-k∣≤1 : ∀ (i : Fin n) {j k} →
+                  (pinch i j ≡ pinch i k) → ∣ (toℕ j) - (toℕ k) ∣ Nat.≤ 1
+pinch-≡⇒∣j-k∣≤1 i {j} {k} = view-j≡view-k⇒∣j-k∣≤1 (view i j) (view i k)
+

README/Data/Fin/Relation/Ternary/PunchIn.agda

@@ -0,0 +1,44 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Example use of the 'PunchIn' view of Fin
+--
+-- This is an example of a view of a function defined over a datatype,
+-- such that the recursion and call-pattern(s) of the function are
+-- precisely mirrored in the constructors of the view type
+--
+-- Using this view, we can exhibit the corresponding properties of
+-- the function `punchIn` defined in `Data.Fin.Properties`
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module README.Data.Fin.Relation.Ternary.PunchIn where
+
+open import Data.Nat.Base using (ℕ; suc)
+open import Data.Fin.Base using (Fin; zero; suc; _≤_; punchIn)
+open import Data.Fin.Relation.Ternary.PunchIn
+open import Function.Definitions using (Injective)
+open import Relation.Binary.Core
+open import Relation.Binary.PropositionalEquality using (_≡_; _≢_)
+
+private
+  variable
+    n : ℕ
+
+------------------------------------------------------------------------
+-- Properties of the function, derived from properties of the View
+
+punchInᵢ≢i : ∀ i (j : Fin n) → punchIn i j ≢ i
+punchInᵢ≢i i j = view-codomain (view i j)
+
+punchIn-injective : ∀ (i : Fin (suc n)) → Injective _≡_ _≡_ (punchIn i)
+punchIn-injective i {j} {k} = view-injective (view i j) (view i k)
+
+punchIn-mono-≤ : ∀ (i : Fin (suc n)) → (punchIn i) Preserves _≤_ ⟶ _≤_
+punchIn-mono-≤ i {j} {k} = view-mono-≤ (view i j) (view i k)
+
+punchIn-cancel-≤ : ∀ (i : Fin (suc n)) {j k} →
+                  (punchIn i j ≤ punchIn i k) → j ≤ k
+punchIn-cancel-≤ i {j} {k} = view-cancel-≤ (view i j) (view i k)
+

README/Data/Fin/Relation/Ternary/PunchOut.agda

@@ -0,0 +1,59 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Example use of the 'PunchOut' view of Fin
+--
+-- This is an example of a view of a function defined over a datatype,
+-- such that the recursion and call-pattern(s) of the function are
+-- precisely mirrored in the constructors of the view type
+--
+-- Using this view, we can exhibit the corresponding properties of
+-- the function `punchOut` defined in `Data.Fin.Properties`
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module README.Data.Fin.Relation.Ternary.PunchOut where
+
+open import Data.Nat.Base using (ℕ; suc)
+open import Data.Fin.Base using (Fin; zero; suc; _≤_; punchIn; punchOut)
+open import Data.Fin.Properties using (punchInᵢ≢i)
+open import Data.Fin.Relation.Ternary.PunchIn as PunchIn using ()
+open import Data.Fin.Relation.Ternary.PunchOut
+open import Function.Base using (_∘_)
+open import Relation.Binary.Core
+open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; sym)
+
+private
+  variable
+    n : ℕ
+
+------------------------------------------------------------------------
+-- Properties of the function, derived from properties of the View
+
+punchOut-injective : ∀ {i j k : Fin (suc n)} (i≢j : i ≢ j) (i≢k : i ≢ k) →
+                    punchOut i≢j ≡ punchOut i≢k → j ≡ k
+punchOut-injective i≢j i≢k = view-injective (view i≢j) (view i≢k)
+
+punchOut-cong : ∀ (i : Fin (suc n)) {j k} {i≢j : i ≢ j} {i≢k : i ≢ k} →
+                j ≡ k → punchOut i≢j ≡ punchOut i≢k
+punchOut-cong i {i≢j = i≢j} {i≢k = i≢k} = view-cong (view i≢j) (view i≢k)
+
+punchOut-mono-≤ : ∀ {i j k : Fin (suc n)} (i≢j : i ≢ j) (i≢k : i ≢ k) →
+                j ≤ k → punchOut i≢j ≤ punchOut i≢k
+punchOut-mono-≤ i≢j i≢k = view-mono-≤ (view i≢j) (view i≢k)
+
+punchOut-cancel-≤ : ∀ {i j k : Fin (suc n)} (i≢j : i ≢ j) (i≢k : i ≢ k) →
+                  (punchOut i≢j ≤ punchOut i≢k) → j ≤ k
+punchOut-cancel-≤ i≢j i≢k = view-cancel-≤ (view i≢j) (view i≢k)
+
+-- punchOut and punchIn are mutual inverses,
+-- because their corresponding View s are converses
+
+punchIn-punchOut : ∀ {i j : Fin (suc n)} (i≢j : i ≢ j) →
+                   punchIn i (punchOut i≢j) ≡ j
+punchIn-punchOut = PunchIn.view-complete ∘ view-view⁻¹ ∘ view
+
+punchOut-punchIn : ∀ i {j : Fin n} →
+                   punchOut {i = i} {j = punchIn i j} (punchInᵢ≢i i j ∘ sym) ≡ j
+punchOut-punchIn i {j} = view-complete (view⁻¹-view (PunchIn.view i j))

src/Data/Fin/Relation/Ternary/Pinch.agda

@@ -0,0 +1,119 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- The '`Pinch` view' of the function `pinch` defined on finite sets
+------------------------------------------------------------------------
+--
+-- This is an example of a view of a function defined over a datatype,
+-- such that the recursion and call-pattern(s) of the function are
+-- precisely mirrored in the constructors of the view type,
+-- ie that we 'view the function via its graph relation'
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Fin.Relation.Ternary.Pinch where
+
+open import Data.Fin.Base using (Fin; zero; suc; toℕ; _≤_; _<_; pinch)
+open import Data.Fin.Properties using (suc-injective)
+open import Data.Nat.Base as Nat using (ℕ; zero; suc; z≤n; s≤s; z<s; s<s; ∣_-_∣)
+open import Data.Nat.Properties using (≤-refl; <⇒≤; ∣n-n∣≡0)
+open import Data.Product using (_,_; ∃)
+open import Function.Base using (id; _∘_)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; cong)
+
+private
+  variable
+    n : ℕ
+
+
+------------------------------------------------------------------------
+-- The View, considered as a ternary relation
+
+-- Each constructor corresponds to a particular call-pattern in the original
+-- function definition; recursive calls are represented by inductive premises
+
+data View : ∀ {n} (i : Fin n) (j : Fin (suc n)) (k : Fin n) → Set where
+{-
+
+-- `pinch` is the function f(i,j) such that f(i,j) = if j≤i then j else j-1
+
+pinch : Fin n → Fin (suc n) → Fin n
+pinch {suc n} _       zero    = zero
+pinch {suc n} zero    (suc j) = j
+pinch {suc n} (suc i) (suc j) = suc (pinch i j)
+
+-}
+
+  any-zero : ∀ {n} (i : Fin (suc n))             → View i zero zero
+  zero-suc : ∀ {n} (j : Fin (suc n))             → View zero (suc j) j
+  suc-suc  : ∀ {n} {i} {j} {k} → View {n} i j k → View (suc i) (suc j) (suc k)
+
+-- The View is sound, ie covers all telescopes (satisfying the always-true precondition)
+
+-- The recursion/pattern analysis of the original definition of `pinch`
+-- (which is responsible for showing termination in the first place)
+-- is then exactly replicated in the definition of the covering function `view`;
+-- thus that definitional pattern analysis is encapsulated once and for all
+
+view : ∀ {n} i j → View {n} i j (pinch i j)
+view {suc _} i zero    = any-zero i
+view   zero    (suc j) = zero-suc j
+view   (suc i) (suc j) = suc-suc (view i j)
+
+-- Interpretation of the view: the original function itself
+
+⟦_⟧ : ∀ {i j} {k} .(v : View {n} i j k) → Fin n
+⟦_⟧ {n = n} {i} {j} {k} _ = pinch i j
+
+-- The View is complete
+
+view-complete : ∀ {n} {i j} {k} (v : View {n} i j k) → ⟦ v ⟧ ≡ k
+view-complete (any-zero i) = refl
+view-complete (zero-suc j) = refl
+view-complete (suc-suc v)  = cong suc (view-complete v)
+
+------------------------------------------------------------------------
+-- Properties of the function, derived from properties of the View
+
+view-surjective : ∀ (i k : Fin n) → ∃ λ j → View i j k
+view-surjective zero    k       = suc k , zero-suc k
+view-surjective (suc i) zero    = zero , any-zero (suc i)
+view-surjective (suc i) (suc k) with j , v ← view-surjective i k = suc j , suc-suc v
+
+view-injective : ∀ {i j k} {p q} → View {n} i j p → View {n} i k q →
+                 suc i ≢ j → suc i ≢ k → p ≡ q → j ≡ k
+view-injective v w [i+1]≢j [i+1]≢k refl = aux v w [i+1]≢j [i+1]≢k where
+  aux : ∀ {i j k} {r} → View {n} i j r → View {n} i k r →
+        suc i ≢ j → suc i ≢ k → j ≡ k
+  aux (any-zero _) (any-zero _)     [i+1]≢j [i+1]≢k = refl
+  aux (any-zero _) (zero-suc .zero) [i+1]≢j [i+1]≢k with () ← [i+1]≢k refl
+  aux (zero-suc _) (any-zero .zero) [i+1]≢j [i+1]≢k with () ← [i+1]≢j refl
+  aux (zero-suc _) (zero-suc _)     [i+1]≢j [i+1]≢k = refl
+  aux (suc-suc v)  (suc-suc w)      [i+1]≢j [i+1]≢k
+    = cong suc (aux v w ([i+1]≢j ∘ cong suc) ([i+1]≢k ∘ cong suc))
+
+view-mono-≤ : ∀ {i} {j k} {p q} → View {n} i j p → View {n} i k q →
+              j ≤ k → p ≤ q
+view-mono-≤ (any-zero _) _            _         = z≤n
+view-mono-≤ (zero-suc _) (zero-suc _) (s≤s j≤k) = j≤k
+view-mono-≤ (suc-suc v)  (suc-suc w)  (s≤s j≤k) = s≤s (view-mono-≤ v w j≤k)
+
+view-cancel-< : ∀ {i j k} {p q} → View {n} i j p → View {n} i k q →
+                p < q → j < k
+view-cancel-< (any-zero _) (zero-suc _) _         = z<s
+view-cancel-< (any-zero _) (suc-suc _)  _         = z<s
+view-cancel-< (zero-suc _) (zero-suc _) p<q       = s<s p<q
+view-cancel-< (suc-suc v)  (suc-suc w)  (s<s p<q) = s<s (view-cancel-< v w p<q)
+
+view-j≡view-k⇒∣j-k∣≤1 : ∀ {i j k} {p q} → View {n} i j p → View {n} i k q →
+                        p ≡ q → ∣ (toℕ j) - (toℕ k)∣ Nat.≤ 1
+view-j≡view-k⇒∣j-k∣≤1 v w refl = aux v w
+  where
+    aux : ∀ {n} {i j k} {r} → View {n} i j r → View {n} i k r →
+          ∣ (toℕ j) - (toℕ k) ∣ Nat.≤ 1
+    aux (any-zero _)    (any-zero _)    = z≤n
+    aux (any-zero zero) (zero-suc zero) = ≤-refl
+    aux (zero-suc zero) (any-zero zero) = ≤-refl
+    aux (zero-suc j)    (zero-suc j) rewrite ∣n-n∣≡0 (toℕ j) = z≤n
+    aux (suc-suc v)     (suc-suc w) = aux v w
+

src/Data/Fin/Relation/Ternary/PunchIn.agda

@@ -0,0 +1,102 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- The '`PunchIn` view' of the function `punchIn` defined on finite sets
+------------------------------------------------------------------------
+--
+-- This is an example of a view of a function defined over a datatype,
+-- such that the recursion and call-pattern(s) of the function are
+-- precisely mirrored in the constructors of the view type,
+-- ie that we 'view the function via its graph relation'
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Fin.Relation.Ternary.PunchIn where
+
+open import Data.Fin.Base using (Fin; zero; suc; _≤_; punchIn)
+open import Data.Fin.Properties using (suc-injective)
+open import Data.Nat.Base using (ℕ; zero; suc; z≤n; s≤s)
+open import Function.Base using (id; _∘_)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; cong)
+
+private
+  variable
+    n : ℕ
+
+
+------------------------------------------------------------------------
+-- The View, considered as a ternary relation
+
+-- Each constructor corresponds to a particular call-pattern in the original
+-- function definition; recursive calls are represented by inductive premises
+
+data View : ∀ {n} (i : Fin (suc n)) (j : Fin n) (k : Fin (suc n)) → Set where
+{-
+
+-- `punchIn` is the function f(i,j) = if j≥i then j+1 else j
+
+punchIn : Fin (suc n) → Fin n → Fin (suc n)
+punchIn zero    j       = suc j
+punchIn (suc i) zero    = zero
+punchIn (suc i) (suc j) = suc (punchIn i j)
+
+-}
+  zero-suc : ∀ {n} (j : Fin n)                   → View zero j (suc j)
+  suc-zero : ∀ {n} (i : Fin (suc n))             → View (suc i) zero zero
+  suc-suc  : ∀ {n} {i} {j} {k} → View {n} i j k → View (suc i) (suc j) (suc k)
+
+-- The View enforces the codomain postcondition
+
+Codomain : ∀ (i : Fin (suc n)) (j : Fin n) → Set
+Codomain i j = punchIn i j ≢ i
+
+view-codomain : ∀ {i} {j} {k} → View {n} i j k → Codomain i j
+view-codomain (suc-suc v) = (view-codomain v) ∘ suc-injective
+
+-- The View is sound, ie covers all telescopes (satisfying the always-true precondition)
+
+-- The recursion/pattern analysis of the original definition of `punchIn`
+-- (which is responsible for showing termination in the first place)
+-- is then exactly replicated in the definition of the covering function `view`;
+-- thus that definitional pattern analysis is encapsulated once and for all
+
+view : ∀ i j → View {n} i j (punchIn i j)
+view zero         j  = zero-suc j
+view (suc i) zero    = suc-zero i
+view (suc i) (suc j) = suc-suc (view i j)
+
+-- Interpretation of the view: the original function itself
+
+⟦_⟧ : ∀ {i} {j} {k} .(v : View {n} i j k) → Fin (suc n)
+⟦_⟧ {n = n} {i} {j} {k} _ = punchIn i j
+
+-- The View is complete
+
+view-complete : ∀ {i j} {k} (v : View {n} i j k) → ⟦ v ⟧ ≡ k
+view-complete (zero-suc j) = refl
+view-complete (suc-zero i) = refl
+view-complete (suc-suc v)  = cong suc (view-complete v)
+
+------------------------------------------------------------------------
+-- Properties of the View
+
+view-injective : ∀ {i j k} {p q} →
+                 View {n} i j p → View {n} i k q → p ≡ q → j ≡ k
+view-injective v w refl = aux v w where
+  aux : ∀ {i j k} {r} → View {n} i j r → View {n} i k r → j ≡ k
+  aux (zero-suc _) (zero-suc _) = refl
+  aux (suc-zero i) (suc-zero i) = refl
+  aux (suc-suc v) (suc-suc w)   = cong suc (aux v w)
+
+view-mono-≤ : ∀ {i j k} {p q} → View {n} i j p → View {n} i k q →
+              j ≤ k → p ≤ q
+view-mono-≤ (zero-suc _) (zero-suc _)  j≤k     = s≤s j≤k
+view-mono-≤ (suc-zero i) _             _       = z≤n
+view-mono-≤ (suc-suc v)  (suc-suc w) (s≤s j≤k) = s≤s (view-mono-≤ v w j≤k)
+
+view-cancel-≤ : ∀ {i j k} {p q} → View {n} i j p → View {n} i k q →
+                p ≤ q → j ≤ k
+view-cancel-≤ (zero-suc _) (zero-suc _) (s≤s p≤q) = p≤q
+view-cancel-≤ (suc-zero i) _            _         = z≤n
+view-cancel-≤ (suc-suc v)  (suc-suc w)  (s≤s p≤q) = s≤s (view-cancel-≤ v w p≤q)
+