open import Cat.Prelude

open import Order.Base

module Order.Reasoning {β„“ β„“'} (P : Poset β„“ β„“') where

Partial order syntaxπŸ”—

This module defines a syntax for reasoning with transitivity in a partial order. Simply speaking, it lets us write chains like

a≀b≀c a \le b \le c

to mean something like β€œa≀ca \le c through the intermediate step bb”. In the syntax, we intersperse the justification for why a≀ba \le b and b≀cb \le c. We also allow equality steps, so chains like a≀b=b′≀ca \le b = b' \le c are supported, too.

open Poset P public

private variable
  a b c d : ⌞ P ⌟

_β‰€βŸ¨_⟩_ : (a : ⌞ P ⌟) β†’ a ≀ b β†’ b ≀ c β†’ a ≀ c
_=⟨_⟩_ : (a : ⌞ P ⌟) β†’ a ≑ b β†’ b ≀ c β†’ a ≀ c
_=˘⟨_⟩_ : (a : ⌞ P ⌟) β†’ b ≑ a β†’ b ≀ c β†’ a ≀ c
_β‰€βˆŽ    : (a : ⌞ P ⌟) β†’ a ≀ a

path→≀ : βˆ€ {x y} β†’ x ≑ y β†’ x ≀ y
path→≀ p = subst (_≀ _) (sym p) ≀-refl

pathβ†’β‰₯ : βˆ€ {x y} β†’ x ≑ y β†’ y ≀ x
pathβ†’β‰₯ p = subst (_≀ _) p ≀-refl

f β‰€βŸ¨ p βŸ©β‰€ q = ≀-trans p q
f =⟨ p ⟩= q = subst (_≀ _) (sym p) q
f =˘⟨ p ⟩=˘ q = subst (_≀ _) p q
f β‰€βˆŽ = ≀-refl

infixr 2 _=⟨_⟩_ _=˘⟨_⟩_ _β‰€βŸ¨_⟩_
infix  3 _β‰€βˆŽ