2020-10-06 15:09:02 +03:00
|
|
|
module Syntax.PreorderReasoning.Generic
|
|
|
|
|
2021-07-09 11:06:27 +03:00
|
|
|
import Control.Relation
|
|
|
|
import Control.Order
|
2020-10-06 15:09:02 +03:00
|
|
|
infixl 0 ~~
|
|
|
|
infixl 0 <~
|
|
|
|
prefix 1 |~
|
|
|
|
infix 1 ...
|
|
|
|
|
|
|
|
public export
|
|
|
|
data Step : (leq : a -> a -> Type) -> a -> a -> Type where
|
2020-10-16 00:44:30 +03:00
|
|
|
(...) : (y : a) -> x `leq` y -> Step leq x y
|
2020-10-06 15:09:02 +03:00
|
|
|
|
|
|
|
public export
|
2020-10-16 00:44:30 +03:00
|
|
|
data FastDerivation : (leq : a -> a -> Type) -> (x : a) -> (y : a) -> Type where
|
|
|
|
(|~) : (x : a) -> FastDerivation leq x x
|
|
|
|
(<~) : {x, y : a}
|
|
|
|
-> FastDerivation leq x y -> {z : a} -> (step : Step leq y z)
|
|
|
|
-> FastDerivation leq x z
|
2020-10-06 15:09:02 +03:00
|
|
|
|
2020-10-16 00:44:30 +03:00
|
|
|
public export
|
2021-02-12 18:36:38 +03:00
|
|
|
CalcWith : Preorder dom leq => {0 x : dom} -> {0 y : dom} -> FastDerivation leq x y -> x `leq` y
|
2021-11-22 23:10:08 +03:00
|
|
|
CalcWith (|~ x) = reflexive
|
|
|
|
CalcWith ((<~) der (z ... step)) = transitive (CalcWith der) step
|
2020-10-06 15:09:02 +03:00
|
|
|
|
|
|
|
public export
|
2021-02-12 18:36:38 +03:00
|
|
|
(~~) : {0 x : dom} -> {0 y : dom}
|
2020-10-16 00:44:30 +03:00
|
|
|
-> FastDerivation leq x y -> {z : dom} -> (step : Step Equal y z)
|
|
|
|
-> FastDerivation leq x z
|
2020-10-06 15:09:02 +03:00
|
|
|
(~~) der (z ... Refl) = der
|