Skip to content

Instantly share code, notes, and snippets.

@sstucki
Created December 8, 2017 11:10
Show Gist options
  • Save sstucki/2ce758a6dc62883ecbe54e71c0177fd0 to your computer and use it in GitHub Desktop.
Save sstucki/2ce758a6dc62883ecbe54e71c0177fd0 to your computer and use it in GitHub Desktop.
Convenient reasoning about transitive relations
-- In response to https://lists.chalmers.se/pipermail/agda/2017/009872.html
module _ where
open import Data.Product using (proj₁; proj₂)
open import Level using (suc; _⊔_)
open import Relation.Binary
------------------------------------------------------------------------
-- Transitive relations that are not necessarily reflexive
--
-- Following the convention used in the standard library, we define
-- transitive binary relations using a pair of records (see
-- Relation.Binary).
record IsTransRel {a ℓ₁ ℓ₂} {A : Set a}
(_≈_ : Rel A ℓ₁) -- The underlying equality.
(_∼_ : Rel A ℓ₂) -- The relation.
: Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isEquivalence : IsEquivalence _≈_
trans : Transitive _∼_
-- _∼_ respects the underlying equality _≈_.
--
-- (This always true for preorders, but not necessarily for
-- irreflexive relations.)
∼-resp-≈ : _∼_ Respects₂ _≈_
module Eq = IsEquivalence isEquivalence
record TransRel c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 4 _≈_ _∼_
field
Carrier : Set c
_≈_ : Rel Carrier ℓ₁ -- The underlying equality.
_∼_ : Rel Carrier ℓ₂ -- The relation.
isTransRel : IsTransRel _≈_ _∼_
open IsTransRel isTransRel public
-- Sanity check: every pre-order is a transitive relation in the above
-- sense...
preorderIsTransRel : ∀ {c ℓ₁ ℓ₂} → Preorder c ℓ₁ ℓ₂ → TransRel c ℓ₁ ℓ₂
preorderIsTransRel P = record
{ isTransRel = record
{ isEquivalence = isEquivalence
; trans = trans
; ∼-resp-≈ = ∼-resp-≈
}
}
where open IsPreorder (Preorder.isPreorder P)
-- ... and so is every strict partial order.
strictPartialOrderIsTransRel : ∀ {c ℓ₁ ℓ₂} →
StrictPartialOrder c ℓ₁ ℓ₂ → TransRel c ℓ₁ ℓ₂
strictPartialOrderIsTransRel SPO = record
{ isTransRel = record
{ isEquivalence = isEquivalence
; trans = trans
; ∼-resp-≈ = <-resp-≈
}
}
where open IsStrictPartialOrder (StrictPartialOrder.isStrictPartialOrder SPO)
-- A form of relational reasoning for transitive relations.
--
-- The structure of this module is adapted from the
-- Relation.Binary.PreorderReasoning module of the standard library.
-- It differs from the latter in that
--
-- 1. it allows reasoning about relations that are transitive but not
-- reflexive, and
--
-- 2. the _IsRelatedTo_ predicate is extended with an additional
-- index that tracks whether elements of the carrier are actually
-- related in the transitive relation _∼_ or just in the
-- underlying equality _≈_.
--
-- Proofs that elements x, y are related as (x IsRelatedTo y In rel)
-- can be converted back to proofs that x ∼ y using begin_, whereas
-- proofs of (x IsRelatedTo y In eq) are too weak to do so. Since the
-- relation _∼_ is not assumed to be reflexive (i.e. not necessarily a
-- preorder) _∎ can only construct proofs of the weaker form (x ∎ : x
-- IsRelatedTo x In eq). Consequently, at least one use of _∼⟨_⟩_ is
-- necessary to conclude a proof.
module TransRelReasoning {c ℓ₁ ℓ₂} (R : TransRel c ℓ₁ ℓ₂) where
open TransRel R
infix 4 _IsRelatedTo_In_
infix 3 _∎
infixr 2 _∼⟨_⟩_ _≈⟨_⟩_ _≈⟨⟩_
infix 1 begin_
-- Codes for the relation _∼_ and the underlying equality _≈_.
data RelC : Set where
rel eq : RelC
-- A generic relation combining _∼_ and equality.
data _IsRelatedTo_In_ (x y : Carrier) : RelC → Set (ℓ₁ ⊔ ℓ₂) where
relTo : (x∼y : x ∼ y) → x IsRelatedTo y In rel
eqTo : (x≈y : x ≈ y) → x IsRelatedTo y In eq
begin_ : ∀ {x y} → x IsRelatedTo y In rel → x ∼ y
begin (relTo x∼y) = x∼y
_∼⟨_⟩_ : ∀ x {y z c} → x ∼ y → y IsRelatedTo z In c → x IsRelatedTo z In rel
_ ∼⟨ x∼y ⟩ relTo y∼z = relTo (trans x∼y y∼z)
_ ∼⟨ x∼y ⟩ eqTo y≈z = relTo (proj₁ ∼-resp-≈ y≈z x∼y)
_≈⟨_⟩_ : ∀ x {y z c} → x ≈ y → y IsRelatedTo z In c → x IsRelatedTo z In c
x ≈⟨ x≈y ⟩ relTo y∼z = relTo (proj₂ ∼-resp-≈ (Eq.sym x≈y) y∼z)
x ≈⟨ x≈y ⟩ eqTo y≈z = eqTo (Eq.trans x≈y y≈z)
_≈⟨⟩_ : ∀ x {y c} → x IsRelatedTo y In c → x IsRelatedTo y In c
_ ≈⟨⟩ rt-x∼y = rt-x∼y
_∎ : ∀ x → x IsRelatedTo x In eq
_ ∎ = eqTo Eq.refl
-- Example: strict order reasoning.
module StrictOrderReasoning {c ℓ₁ ℓ₂} (SPO : StrictPartialOrder c ℓ₁ ℓ₂) where
open TransRelReasoning (strictPartialOrderIsTransRel SPO) public
renaming (_∼⟨_⟩_ to _<⟨_⟩_)
open import Data.Bin
open import Relation.Binary.PropositionalEquality
postulate
0bs1 0bs'1 bs1 bs'1 2bin : Bin
step-1 : 0bs1 ≡ bs1 * 2bin
step-2 : bs1 * 2bin < bs'1 * 2bin
step-3 : bs'1 * 2bin ≡ bs'1 *2
step-4 : bs'1 *2 ≡ 0# + 0bs'1
open StrictOrderReasoning (StrictTotalOrder.strictPartialOrder strictTotalOrder)
goal : 0bs1 < 0# + 0bs'1
goal =
begin 0bs1 ≈⟨ step-1 ⟩
bs1 * 2bin <⟨ step-2 ⟩
bs'1 * 2bin ≈⟨ step-3 ⟩
bs'1 *2 ≈⟨ step-4 ⟩
0# + 0bs'1
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment