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

to mean something like β€œ through the intermediate step ”. In the syntax, we intersperse the justification for why and We also allow equality steps, so chains like 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

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 _β‰€βˆŽ