0 | module Syntax.PreorderReasoning.Generic
  1 |
  2 | import Control.Relation
  3 | import Control.Order
  4 | import public Syntax.PreorderReasoning.Ops
  5 |
  6 | public export
  7 | data Step : (leq : a -> a -> Type) -> a -> a -> Type where
  8 |   (...) : (y : a) -> x `leq` y -> Step leq x y
  9 |
 10 | public export
 11 | data FastDerivation : (leq : a -> a -> Type) -> (x : a) -> (y : a) -> Type where
 12 |   (|~) : (x : a) -> FastDerivation leq x x
 13 |   (<~) : {x, y : a}
 14 |          -> FastDerivation leq x y -> {0 z : a} -> (step : Step leq y z)
 15 |          -> FastDerivation leq x z
 16 |
 17 | -- Using a McKinna-McBride view records the depenencies on the type of derivation
 18 | -- the additional benefits for pattern-matching aren't used here
 19 | public export
 20 | data DerivationType : FastDerivation leq x y -> Type where
 21 |   TrivialDerivation : DerivationType (|~ x)
 22 |   SingleStepDerivation : DerivationType (|~ x <~ step)
 23 |   NonTrivialDerivation : DerivationType (der <~ step1 <~ step2)
 24 |
 25 | public export
 26 | derivationType : (der : FastDerivation leq x y) -> DerivationType der
 27 | derivationType (|~ x) = TrivialDerivation
 28 | derivationType (|~ x <~ step) = SingleStepDerivation
 29 | derivationType ((z <~ w) <~ step) = NonTrivialDerivation
 30 |
 31 | public export
 32 | 0 Prerequisite : {0 der : FastDerivation {a = dom} leq x y} -> DerivationType der -> Type
 33 | Prerequisite TrivialDerivation = Reflexive dom leq
 34 | Prerequisite SingleStepDerivation = ()
 35 | Prerequisite NonTrivialDerivation = Transitive dom leq
 36 |
 37 | -- Once we have the prerequisite for transitivity, we have the
 38 | -- prerequisite for its inductive predecessor:
 39 | public export
 40 | inductivePrerequisite : (der : FastDerivation leq x y) ->
 41 |   (0 step1 : Step leq y z) -> (0 step2 : Step leq z w) ->
 42 |   Prerequisite (derivationType (der <~ step1 <~ step2)) ->
 43 |   Prerequisite (derivationType (der <~ step1))
 44 | inductivePrerequisite (  |~ y    ) step1 step2 prerequisite = ()
 45 | inductivePrerequisite (z <~ step0) step1 step2 prerequisite = prerequisite
 46 |
 47 | public export
 48 | preorderPrerequisite : Preorder dom leq => (der : FastDerivation leq x y) -> Prerequisite (derivationType der)
 49 | preorderPrerequisite (|~ x) = %search
 50 | preorderPrerequisite (|~ x <~ step) = ()
 51 | preorderPrerequisite (der <~ step1 <~ step2) = %search
 52 |
 53 | ||| The Prerequisite for the derivation:
 54 | ||| 0-length derivation: Reflexive dom leq
 55 | ||| 1-length derivation: Unit (no prerequisite)
 56 | ||| 2 steps of longer: Transitivity
 57 | public export
 58 | CalcSmart : {0 x : dom} -> {0 y : dom} -> (der : FastDerivation leq x y) ->
 59 |   Prerequisite (derivationType der) => x `leq` y
 60 | CalcSmart (|~ x) = reflexive
 61 | CalcSmart (|~ x <~ y ... step) = step
 62 | CalcSmart (der <~ _ ... step1
 63 |                <~ w ... step2) @{prereq} =
 64 |                 CalcSmart (der <~ _ ... step1)
 65 |                 @{inductivePrerequisite der (_ ... step1) (w ... step2) prereq}
 66 |                   `transitive` step2
 67 |
 68 | public export
 69 | CalcWith : Preorder dom leq => {0 x : dom} -> {0 y : dom} -> (der : FastDerivation leq x y) -> x `leq` y
 70 | CalcWith der = CalcSmart der @{preorderPrerequisite der}
 71 |
 72 | public export
 73 | (~~) : {0 x : dom} -> {0 y : dom}
 74 |          -> FastDerivation leq x y -> {0 z : dom} -> (0 step : Step Equal y z)
 75 |          -> FastDerivation leq x z
 76 | (~~) der (z ... yEqZ) = replace {p = FastDerivation leq _} yEqZ der
 77 |
 78 | -- Smart constructors
 79 | public export
 80 | (..<) : Symmetric a leq => (y : a) -> {x : a} -> y `leq` x -> Step leq x y
 81 | (y ..<(prf)) {x} = (y ...(symmetric prf))
 82 |
 83 | public export
 84 | (..>) : (y : a) -> x `leq` y -> Step leq x y
 85 | (..>) = (...)
 86 |
 87 | public export
 88 | (.=.) : Reflexive a leq  => (y : a) -> {x : a} ->
 89 |     x === y -> Step leq x y
 90 | (y .=.(Refl)) {x = _} = (y ...(reflexive))
 91 |
 92 | public export
 93 | (.=>) : Reflexive a leq  => (y : a) -> {x : a} ->
 94 |     x === y -> Step leq x y
 95 | (.=>) = (.=.)
 96 |
 97 | public export
 98 | (.=<) : Reflexive a leq  => (y : a) -> {x : a} ->
 99 |     y === x -> Step leq x y
100 | (y .=<(Refl)) = (y ...(reflexive))
101 |
102 | public export
103 | (~=) : FastDerivation leq x y -> (0 z : dom) -> {auto xEqy : y = z} -> FastDerivation leq x z
104 | (~=) der z {xEqy} = der ~~ z ...(xEqy)
105 |