From 15f128b2c9092851b8d1cc5cf76a44d8306932c6 Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Tue, 17 Oct 2023 09:26:05 +0900 Subject: [PATCH] =?UTF-8?q?Move=20=E2=89=A1-Reasoning=20from=20Core=20to?= =?UTF-8?q?=20Properties=20and=20implement=20using=20syntax?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- CHANGELOG.md | 6 ++++ src/Codata/Guarded/Stream/Properties.agda | 6 ++-- src/Codata/Musical/Colist/Infinite-merge.agda | 4 ++- src/Codata/Sized/Stream/Properties.agda | 4 ++- src/Data/Fin/Relation/Unary/Top.agda | 2 ++ src/Data/Fin/Substitution/Lemmas.agda | 4 ++- src/Data/List/Countdown.agda | 2 +- .../Example/UniqueBoundVariables.agda | 3 +- .../Ternary/Interleaving/Properties.agda | 4 ++- .../List/Relation/Unary/Any/Properties.agda | 4 ++- src/Data/Nat/Coprimality.agda | 2 +- src/Data/Nat/GCD.agda | 4 ++- src/Data/Nat/LCM.agda | 4 ++- src/Data/String/Unsafe.agda | 5 ++- src/Data/Vec/Bounded/Base.agda | 4 ++- src/Data/Vec/Recursive/Properties.agda | 2 ++ .../Vec/Relation/Binary/Equality/Cast.agda | 4 ++- src/Effect/Applicative/Indexed.agda | 4 ++- src/Function/Related/TypeIsomorphisms.agda | 4 ++- .../Binary/PropositionalEquality/Core.agda | 32 ------------------- .../PropositionalEquality/Properties.agda | 15 +++++++++ src/Relation/Binary/Reasoning/Syntax.agda | 1 - 22 files changed, 70 insertions(+), 50 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 89e22ce60e..2dcdb3d924 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1238,6 +1238,12 @@ Major improvements pre-existing `Reasoning` module in just a couple of lines (e.g. see `∣-Reasoning` in `Data.Nat.Divisibility`) +* One pre-requisite for that is that `≡-Reasoning` has been moved from + `Relation.Binary.PropositionalEquality.Core` (which shouldn't be + imported anyway as it's a `Core` module) to + `Relation.Binary.PropositionalEquality.Properties`. + It is still exported by `Relation.Binary.PropositionalEquality`. + Deprecated modules ------------------ diff --git a/src/Codata/Guarded/Stream/Properties.agda b/src/Codata/Guarded/Stream/Properties.agda index bd41d1967e..3742aab856 100644 --- a/src/Codata/Guarded/Stream/Properties.agda +++ b/src/Codata/Guarded/Stream/Properties.agda @@ -21,6 +21,8 @@ open import Data.Vec.Base as Vec using (Vec; _∷_) open import Function.Base using (const; flip; id; _∘′_; _$′_; _⟨_⟩_; _∘₂′_) open import Level using (Level) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; cong; cong₂) +open import Relation.Binary.PropositionalEquality.Properties + using (module ≡-Reasoning) private variable @@ -218,7 +220,7 @@ lookup-transpose n (as ∷ ass) = begin lookup as n ∷ lookup (transpose ass) n ≡⟨ cong (lookup as n ∷_) (lookup-transpose n ass) ⟩ lookup as n ∷ List.map (flip lookup n) ass ≡⟨⟩ List.map (flip lookup n) (as ∷ ass) ∎ - where open P.≡-Reasoning + where open ≡-Reasoning lookup-transpose⁺ : ∀ n (ass : List⁺ (Stream A)) → lookup (transpose⁺ ass) n ≡ List⁺.map (flip lookup n) ass @@ -228,7 +230,7 @@ lookup-transpose⁺ n (as ∷ ass) = begin lookup as n ∷ lookup (transpose ass) n ≡⟨ cong (lookup as n ∷_) (lookup-transpose n ass) ⟩ lookup as n ∷ List.map (flip lookup n) ass ≡⟨⟩ List⁺.map (flip lookup n) (as ∷ ass) ∎ - where open P.≡-Reasoning + where open ≡-Reasoning lookup-tails : ∀ n (as : Stream A) → lookup (tails as) n ≈ ℕ.iterate tail as n lookup-tails zero as = B.refl diff --git a/src/Codata/Musical/Colist/Infinite-merge.agda b/src/Codata/Musical/Colist/Infinite-merge.agda index cbc142ff5a..584880a768 100644 --- a/src/Codata/Musical/Colist/Infinite-merge.agda +++ b/src/Codata/Musical/Colist/Infinite-merge.agda @@ -26,6 +26,8 @@ open import Level open import Relation.Unary using (Pred) import Induction.WellFounded as WF open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) +open import Relation.Binary.PropositionalEquality.Properties + using (module ≡-Reasoning) import Relation.Binary.Construct.On as On private @@ -132,7 +134,7 @@ merge xss = ⟦ merge′ xss ⟧P Any-merge : ∀ xss → Any P (merge xss) ↔ Any (λ { (x , xs) → P x ⊎ Any P xs }) xss Any-merge {P = P} xss = mk↔ₛ′ (proj₁ ∘ to xss) from to∘from (proj₂ ∘ to xss) where - open P.≡-Reasoning + open ≡-Reasoning -- The from function. diff --git a/src/Codata/Sized/Stream/Properties.agda b/src/Codata/Sized/Stream/Properties.agda index d2cf4e3205..40cb3fc961 100644 --- a/src/Codata/Sized/Stream/Properties.agda +++ b/src/Codata/Sized/Stream/Properties.agda @@ -25,6 +25,8 @@ open import Data.Vec.Base as Vec using (_∷_) open import Function.Base using (id; _$_; _∘′_; const) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; _≢_) +open import Relation.Binary.PropositionalEquality.Properties + using (module ≡-Reasoning) private variable @@ -116,7 +118,7 @@ lookup-iterate-identity (suc n) f a = begin lookup (iterate f (f a)) n ≡⟨ lookup-iterate-identity n f (f a) ⟩ fold (f a) f n ≡⟨ fold-pull a f (const ∘′ f) (f a) P.refl (λ _ → P.refl) n ⟩ f (fold a f n) ≡⟨⟩ - fold a f (suc n) ∎ where open P.≡-Reasoning + fold a f (suc n) ∎ where open ≡-Reasoning ------------------------------------------------------------------------ -- DEPRECATED diff --git a/src/Data/Fin/Relation/Unary/Top.agda b/src/Data/Fin/Relation/Unary/Top.agda index b6a567a9a8..a884a09243 100644 --- a/src/Data/Fin/Relation/Unary/Top.agda +++ b/src/Data/Fin/Relation/Unary/Top.agda @@ -16,6 +16,8 @@ module Data.Fin.Relation.Unary.Top where open import Data.Nat.Base using (ℕ; zero; suc) open import Data.Fin.Base using (Fin; zero; suc; fromℕ; inject₁) open import Relation.Binary.PropositionalEquality.Core +open import Relation.Binary.PropositionalEquality.Properties + using (module ≡-Reasoning) private variable diff --git a/src/Data/Fin/Substitution/Lemmas.agda b/src/Data/Fin/Substitution/Lemmas.agda index ffa26e64fb..8b4d0b176a 100644 --- a/src/Data/Fin/Substitution/Lemmas.agda +++ b/src/Data/Fin/Substitution/Lemmas.agda @@ -16,9 +16,11 @@ import Data.Vec.Properties as VecProp open import Function.Base as Fun using (_∘_; _$_; flip) open import Relation.Binary.PropositionalEquality.Core as PropEq using (_≡_; refl; sym; cong; cong₂) +open import Relation.Binary.PropositionalEquality.Properties + using (module ≡-Reasoning) open import Relation.Binary.Construct.Closure.ReflexiveTransitive using (Star; ε; _◅_; _▻_) -open PropEq.≡-Reasoning +open ≡-Reasoning open import Level using (Level; _⊔_) open import Relation.Unary using (Pred) diff --git a/src/Data/List/Countdown.agda b/src/Data/List/Countdown.agda index 8d6761de27..dbfd75b332 100644 --- a/src/Data/List/Countdown.agda +++ b/src/Data/List/Countdown.agda @@ -31,8 +31,8 @@ open import Relation.Nullary open import Relation.Nullary.Decidable using (dec-true; dec-false) open import Relation.Binary.PropositionalEquality.Core as PropEq using (_≡_; _≢_; refl; cong) -open PropEq.≡-Reasoning import Relation.Binary.PropositionalEquality.Properties as PropEq +open PropEq.≡-Reasoning private open module D = DecSetoid D diff --git a/src/Data/List/Relation/Binary/Sublist/Propositional/Example/UniqueBoundVariables.agda b/src/Data/List/Relation/Binary/Sublist/Propositional/Example/UniqueBoundVariables.agda index 39a6fe65a1..163818b6e8 100644 --- a/src/Data/List/Relation/Binary/Sublist/Propositional/Example/UniqueBoundVariables.agda +++ b/src/Data/List/Relation/Binary/Sublist/Propositional/Example/UniqueBoundVariables.agda @@ -10,7 +10,8 @@ module Data.List.Relation.Binary.Sublist.Propositional.Example.UniqueBoundVariables (Base : Set) where -open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; sym; cong; subst; module ≡-Reasoning) +open import Relation.Binary.PropositionalEquality + using (_≡_; refl; sym; cong; subst; module ≡-Reasoning) open ≡-Reasoning open import Data.List.Base using (List; []; _∷_; [_]) diff --git a/src/Data/List/Relation/Ternary/Interleaving/Properties.agda b/src/Data/List/Relation/Ternary/Interleaving/Properties.agda index dff26bb6b2..5317d5a7c5 100644 --- a/src/Data/List/Relation/Ternary/Interleaving/Properties.agda +++ b/src/Data/List/Relation/Ternary/Interleaving/Properties.agda @@ -16,7 +16,9 @@ open import Data.List.Relation.Ternary.Interleaving hiding (map) open import Function.Base using (_$_) open import Relation.Binary.Core using (REL) open import Relation.Binary.PropositionalEquality.Core - using (_≡_; refl; sym; cong; module ≡-Reasoning) + using (_≡_; refl; sym; cong) +open import Relation.Binary.PropositionalEquality.Properties + using (module ≡-Reasoning) open ≡-Reasoning ------------------------------------------------------------------------ diff --git a/src/Data/List/Relation/Unary/Any/Properties.agda b/src/Data/List/Relation/Unary/Any/Properties.agda index aba1a777ee..b88bdfbe95 100644 --- a/src/Data/List/Relation/Unary/Any/Properties.agda +++ b/src/Data/List/Relation/Unary/Any/Properties.agda @@ -43,6 +43,8 @@ open import Relation.Binary.Core using (Rel; REL) open import Relation.Binary.Definitions as B open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; refl) +open import Relation.Binary.PropositionalEquality.Properties + using (module ≡-Reasoning) open import Relation.Unary as U using (Pred; _⟨×⟩_; _⟨→⟩_) renaming (_⊆_ to _⋐_) open import Relation.Nullary using (¬_; _because_; does; ofʸ; ofⁿ; yes; no) @@ -219,7 +221,7 @@ Any-×⁻ pq with Prod.map₂ (Prod.map₂ find) (find pq) (Any P xs × Any Q ys) ↔ Any (λ x → Any (λ y → P x × Q y) ys) xs ×↔ {P = P} {Q = Q} {xs} {ys} = mk↔ₛ′ Any-×⁺ Any-×⁻ to∘from from∘to where - open P.≡-Reasoning + open ≡-Reasoning from∘to : ∀ pq → Any-×⁻ (Any-×⁺ pq) ≡ pq from∘to (p , q) = diff --git a/src/Data/Nat/Coprimality.agda b/src/Data/Nat/Coprimality.agda index f6f91b44e5..1df320ea96 100644 --- a/src/Data/Nat/Coprimality.agda +++ b/src/Data/Nat/Coprimality.agda @@ -20,7 +20,7 @@ open import Data.Product.Base as Prod open import Function.Base using (_∘_) open import Level using (0ℓ) open import Relation.Binary.PropositionalEquality.Core as P - using (_≡_; _≢_; refl; trans; cong; subst; module ≡-Reasoning) + using (_≡_; _≢_; refl; trans; cong; subst) open import Relation.Nullary as Nullary hiding (recompute) open import Relation.Nullary.Negation using (contradiction) open import Relation.Binary.Core using (Rel) diff --git a/src/Data/Nat/GCD.agda b/src/Data/Nat/GCD.agda index 555a902df6..b88947c707 100644 --- a/src/Data/Nat/GCD.agda +++ b/src/Data/Nat/GCD.agda @@ -24,6 +24,8 @@ open import Induction.Lexicographic using (_⊗_; [_⊗_]) open import Relation.Binary.Definitions using (tri<; tri>; tri≈; Symmetric) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; _≢_; subst; cong) +open import Relation.Binary.PropositionalEquality.Properties + using (module ≡-Reasoning) open import Relation.Nullary.Decidable using (Dec) open import Relation.Nullary.Negation using (contradiction) import Relation.Nullary.Decidable as Dec @@ -190,7 +192,7 @@ c*gcd[m,n]≡gcd[cm,cn] c@(suc _) m n = begin c * gcd m n ≡⟨ cong (c *_) (P.sym (gcd[cm,cn]/c≡gcd[m,n] c m n)) ⟩ c * (gcd (c * m) (c * n) / c) ≡⟨ m*[n/m]≡n (gcd-greatest (m∣m*n m) (m∣m*n n)) ⟩ gcd (c * m) (c * n) ∎ - where open P.≡-Reasoning + where open ≡-Reasoning gcd[m,n]≤n : ∀ m n .{{_ : NonZero n}} → gcd m n ≤ n gcd[m,n]≤n m n = ∣⇒≤ (gcd[m,n]∣n m n) diff --git a/src/Data/Nat/LCM.agda b/src/Data/Nat/LCM.agda index 545870574f..5dff2eb530 100644 --- a/src/Data/Nat/LCM.agda +++ b/src/Data/Nat/LCM.agda @@ -18,7 +18,9 @@ open import Data.Nat.GCD open import Data.Product.Base using (_×_; _,_; uncurry′; ∃) open import Data.Sum.Base using (_⊎_; inj₁; inj₂) open import Relation.Binary.PropositionalEquality.Core as P - using (_≡_; refl; sym; trans; cong; cong₂; module ≡-Reasoning) + using (_≡_; refl; sym; trans; cong; cong₂) +open import Relation.Binary.PropositionalEquality.Properties + using (module ≡-Reasoning) open import Relation.Nullary.Decidable using (False; fromWitnessFalse) private diff --git a/src/Data/String/Unsafe.agda b/src/Data/String/Unsafe.agda index ff1ff28408..35b408f131 100644 --- a/src/Data/String/Unsafe.agda +++ b/src/Data/String/Unsafe.agda @@ -16,8 +16,11 @@ open import Data.Product.Base using (proj₂) open import Data.String.Base open import Function.Base using (_∘′_) -open import Relation.Binary.PropositionalEquality.Core; open ≡-Reasoning +open import Relation.Binary.PropositionalEquality.Core +open import Relation.Binary.PropositionalEquality.Properties + using (module ≡-Reasoning) open import Relation.Binary.PropositionalEquality.TrustMe using (trustMe) +open ≡-Reasoning ------------------------------------------------------------------------ -- Properties of tail diff --git a/src/Data/Vec/Bounded/Base.agda b/src/Data/Vec/Bounded/Base.agda index 63649e940e..c926c9dfb1 100644 --- a/src/Data/Vec/Bounded/Base.agda +++ b/src/Data/Vec/Bounded/Base.agda @@ -22,6 +22,8 @@ open import Function.Base using (_∘_; id; _$_) open import Level using (Level) open import Relation.Nullary.Decidable.Core using (recompute) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; refl) +open import Relation.Binary.PropositionalEquality.Properties + using (module ≡-Reasoning) private variable @@ -66,7 +68,7 @@ private m + (⌈ k /2⌉ + ⌊ k /2⌋) ≡⟨ P.cong (m +_) (ℕₚ.+-comm ⌈ k /2⌉ ⌊ k /2⌋) ⟩ m + (⌊ k /2⌋ + ⌈ k /2⌉) ≡⟨ P.cong (m +_) (ℕₚ.⌊n/2⌋+⌈n/2⌉≡n k) ⟩ m + k ≡⟨ eq ⟩ - n ∎ where open P.≡-Reasoning + n ∎ where open ≡-Reasoning padBoth : ∀ {n} → A → A → Vec≤ A n → Vec A n padBoth aₗ aᵣ as@(vs , m≤n) diff --git a/src/Data/Vec/Recursive/Properties.agda b/src/Data/Vec/Recursive/Properties.agda index b012e59a80..d036134a45 100644 --- a/src/Data/Vec/Recursive/Properties.agda +++ b/src/Data/Vec/Recursive/Properties.agda @@ -15,6 +15,8 @@ open import Data.Vec.Recursive open import Data.Vec.Base using (Vec; _∷_) open import Function.Bundles using (_↔_; mk↔ₛ′) open import Relation.Binary.PropositionalEquality.Core as P +open import Relation.Binary.PropositionalEquality.Properties + using (module ≡-Reasoning) open ≡-Reasoning private diff --git a/src/Data/Vec/Relation/Binary/Equality/Cast.agda b/src/Data/Vec/Relation/Binary/Equality/Cast.agda index adca0a42f2..f65981f7a3 100644 --- a/src/Data/Vec/Relation/Binary/Equality/Cast.agda +++ b/src/Data/Vec/Relation/Binary/Equality/Cast.agda @@ -18,7 +18,9 @@ open import Data.Vec.Base open import Relation.Binary.Core using (REL; _⇒_) open import Relation.Binary.Definitions using (Sym; Trans) open import Relation.Binary.PropositionalEquality.Core - using (_≡_; refl; trans; sym; cong; module ≡-Reasoning) + using (_≡_; refl; trans; sym; cong) +open import Relation.Binary.PropositionalEquality.Properties + using (module ≡-Reasoning) private variable diff --git a/src/Effect/Applicative/Indexed.agda b/src/Effect/Applicative/Indexed.agda index 30e9b632bb..f547e68b27 100644 --- a/src/Effect/Applicative/Indexed.agda +++ b/src/Effect/Applicative/Indexed.agda @@ -16,6 +16,8 @@ open import Data.Product.Base using (_×_; _,_) open import Function.Base open import Level open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) +open import Relation.Binary.PropositionalEquality.Properties + using (module ≡-Reasoning) private variable @@ -111,4 +113,4 @@ record Morphism {I : Set i} {F₁ F₂ : IFun I f} op (A₁._⊛_ (A₁.pure f) x) ≡⟨ op-⊛ _ _ ⟩ A₂._⊛_ (op (A₁.pure f)) (op x) ≡⟨ P.cong₂ A₂._⊛_ (op-pure _) P.refl ⟩ A₂._⊛_ (A₂.pure f) (op x) ∎ - where open P.≡-Reasoning + where open ≡-Reasoning diff --git a/src/Function/Related/TypeIsomorphisms.agda b/src/Function/Related/TypeIsomorphisms.agda index 830bb6f8bb..9fb1fded28 100644 --- a/src/Function/Related/TypeIsomorphisms.agda +++ b/src/Function/Related/TypeIsomorphisms.agda @@ -29,6 +29,8 @@ open import Function.Related.Propositional import Function.Construct.Identity as Identity open import Relation.Binary hiding (_⇔_) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) +open import Relation.Binary.PropositionalEquality.Properties + using (module ≡-Reasoning) open import Relation.Nullary.Reflects using (invert) open import Relation.Nullary using (Dec; ¬_; _because_; ofⁿ) import Relation.Nullary.Indexed as I @@ -284,7 +286,7 @@ private from C↔D (to C↔D (f (from A↔B (to A↔B x)))) ≡⟨ strictlyInverseʳ C↔D _ ⟩ f (from A↔B (to A↔B x)) ≡⟨ P.cong f $ strictlyInverseʳ A↔B x ⟩ f x ∎) - where open Inverse; open P.≡-Reasoning + where open Inverse; open ≡-Reasoning →-cong : Extensionality a c → Extensionality b d → ∀ {k} {A : Set a} {B : Set b} {C : Set c} {D : Set d} → diff --git a/src/Relation/Binary/PropositionalEquality/Core.agda b/src/Relation/Binary/PropositionalEquality/Core.agda index c0c4030b83..848258348b 100644 --- a/src/Relation/Binary/PropositionalEquality/Core.agda +++ b/src/Relation/Binary/PropositionalEquality/Core.agda @@ -91,35 +91,3 @@ resp₂ _∼_ = respʳ _∼_ , respˡ _∼_ ≢-sym : Symmetric {A = A} _≢_ ≢-sym x≢y = x≢y ∘ sym - ------------------------------------------------------------------------- --- Convenient syntax for equational reasoning - --- This is a special instance of `Relation.Binary.Reasoning.Setoid`. --- Rather than instantiating the latter with (setoid A), we reimplement --- equation chains from scratch since then goals are printed much more --- readably. - -module ≡-Reasoning {A : Set a} where - - infix 3 _∎ - infixr 2 _≡⟨⟩_ step-≡ step-≡˘ - infix 1 begin_ - - begin_ : ∀{x y : A} → x ≡ y → x ≡ y - begin_ x≡y = x≡y - - _≡⟨⟩_ : ∀ (x {y} : A) → x ≡ y → x ≡ y - _ ≡⟨⟩ x≡y = x≡y - - step-≡ : ∀ (x {y z} : A) → y ≡ z → x ≡ y → x ≡ z - step-≡ _ y≡z x≡y = trans x≡y y≡z - - step-≡˘ : ∀ (x {y z} : A) → y ≡ z → y ≡ x → x ≡ z - step-≡˘ _ y≡z y≡x = trans (sym y≡x) y≡z - - _∎ : ∀ (x : A) → x ≡ x - _∎ _ = refl - - syntax step-≡ x y≡z x≡y = x ≡⟨ x≡y ⟩ y≡z - syntax step-≡˘ x y≡z y≡x = x ≡˘⟨ y≡x ⟩ y≡z diff --git a/src/Relation/Binary/PropositionalEquality/Properties.agda b/src/Relation/Binary/PropositionalEquality/Properties.agda index 9515b77700..a420e45b64 100644 --- a/src/Relation/Binary/PropositionalEquality/Properties.agda +++ b/src/Relation/Binary/PropositionalEquality/Properties.agda @@ -23,6 +23,8 @@ open import Relation.Binary.Definitions import Relation.Binary.Properties.Setoid as Setoid open import Relation.Binary.PropositionalEquality.Core open import Relation.Unary using (Pred) +open import Relation.Binary.Reasoning.Syntax + private variable @@ -188,3 +190,16 @@ preorder A = Setoid.≈-preorder (setoid A) poset : Set a → Poset _ _ _ poset A = Setoid.≈-poset (setoid A) + +------------------------------------------------------------------------ +-- Reasoning + +-- This is a special instance of `Relation.Binary.Reasoning.Setoid`. +-- Rather than instantiating the latter with (setoid A), we reimplement +-- equation chains from scratch since then goals are printed much more +-- readably. +module ≡-Reasoning {a} {A : Set a} where + + open begin-syntax {A = A} _≡_ id public + open ≡-syntax {A = A} _≡_ trans public + open end-syntax {A = A} _≡_ refl public diff --git a/src/Relation/Binary/Reasoning/Syntax.agda b/src/Relation/Binary/Reasoning/Syntax.agda index 4837fe33f4..e8286bee30 100644 --- a/src/Relation/Binary/Reasoning/Syntax.agda +++ b/src/Relation/Binary/Reasoning/Syntax.agda @@ -22,7 +22,6 @@ open import Relation.Binary.PropositionalEquality.Core as P -- Relation/Binary/HeterogeneousEquality -- Effect/Monad/Partiality -- Effect/Monad/Partiality/All --- Relation/Binary/PropositionalEquality/Core -- Codata/Guarded/Stream/Relation/Binary/Pointwise -- Codata/Sized/Stream/Bisimilarity -- Function/Reasoning