Add PreorderReasoning comforts (#2778)

* Add PreorderReasoning comforts

* Drop interface approach in favour of computation

* Update libs/base/Syntax/PreorderReasoning.idr

---------

Co-authored-by: Cristóvão Gomes Ferreira <crisoagf@melo-gibson>
Co-authored-by: Ohad Kammar <ohad.kammar@gmail.com>
Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
CI integration co-authored-by: @stefan-hoeck

libs/base/Data/Nat.idr

@@ -5,6 +5,7 @@ import public Control.Relation
 import public Control.Ord
 import public Control.Order
 import public Control.Function
+import Syntax.PreorderReasoning.Generic
 
 %default total
 
@@ -202,6 +203,23 @@ public export
 isGT : (m, n : Nat) -> Dec (GT m n)
 isGT m n = isLT n m
 
+lteRecallLeft : LTE m n -> (m' : Nat ** m = m')
+lteRecallLeft LTEZero = (0 ** Refl)
+lteRecallLeft (LTESucc x) with (lteRecallLeft x)
+  lteRecallLeft (LTESucc x) | (left ** Refl) = (S left ** Refl)
+
+irrelevantLte : {m : Nat} -> (0 prf : LTE m n) -> LTE m n
+irrelevantLte {m = 0} LTEZero = LTEZero
+irrelevantLte {m = (S k)} (LTESucc x) = LTESucc (irrelevantLte x)
+
+lteRecall : LTE m n -> {p : Nat -> Nat} -> (0 prf : LTE (p m) q) -> LTE (p m) q
+lteRecall {m} x prf with (lteRecallLeft x)
+  lteRecall {m = m} x prf | (m ** Refl) = irrelevantLte prf
+
+ltRecall : LT m n -> {p : Nat -> Nat} -> (0 prf : LT (p m) q) -> LT (p m) q
+ltRecall {m} x prf with (lteRecallLeft x)
+  ltRecall {m = m} x prf | (S m ** Refl) = irrelevantLte prf
+
 export
 lteSuccRight : LTE n m -> LTE n (S m)
 lteSuccRight LTEZero     = LTEZero
@@ -640,8 +658,11 @@ minusLteMonotone {p = S p} (LTESucc lte) = minusLteMonotone lte
 
 export
 minusLtMonotone : m `LT` n -> p `LT` n -> minus m p `LT` minus n p
-minusLtMonotone mltn pltn = case view pltn of
-  LTZero => rewrite minusZeroRight m in mltn
+minusLtMonotone {m} {p} mltn pltn = case view pltn of
+    LTZero => ltRecall {p = (`minus` 0)} mltn $ CalcSmart {leq = LT} $
+      |~ minus m Z
+      ~~ m ...(minusZeroRight m)
+      <~ minus n Z ...(mltn)
     LTSucc pltn => case view mltn of
       LTZero => minusPos pltn
       LTSucc mltn => minusLtMonotone mltn pltn

libs/base/Syntax/PreorderReasoning.idr

@@ -2,7 +2,7 @@
 ||| poor-man's equational reasoning
 module Syntax.PreorderReasoning
 
-infixl 0  ~~
+infixl 0  ~~,~=
 prefix 1  |~
 infix  1  ...,..<,..>,.=.,.=<,.=>
 
@@ -52,3 +52,8 @@ public export
 public export
 (..>) : (0 y : a) -> (0 step : x ~=~ y) -> Step x y
 (..>) = (...)
+
+||| Use a judgemental equality but is not trivial to the reader.
+public export
+(~=) : FastDerivation x y -> (0 z : dom) -> {auto xEqy : y = z} -> FastDerivation x z
+(~=) der y {xEqy = Refl} = der ~~ y ... Refl

libs/base/Syntax/PreorderReasoning/Generic.idr

@@ -2,7 +2,7 @@ module Syntax.PreorderReasoning.Generic
 
 import Control.Relation
 import Control.Order
-infixl 0  ~~
+infixl 0  ~~, ~=
 infixl 0  <~
 prefix 1  |~
 infix  1  ...,..<,..>,.=.,.=<,.=>
@@ -15,19 +15,69 @@ public export
 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 y -> {0 z : a} -> (step : Step leq y z)
          -> FastDerivation leq x z
 
+-- Using a McKinna-McBride view records the depenencies on the type of derivation
+-- the additional benefits for pattern-matching aren't used here
 public export
-CalcWith : Preorder dom leq => {0 x : dom} -> {0 y : dom} -> FastDerivation leq x y -> x `leq` y
-CalcWith (|~ x) = reflexive
-CalcWith ((<~) der (z ... step)) = transitive (CalcWith der) step
+data DerivationType : FastDerivation leq x y -> Type where
+  TrivialDerivation : DerivationType (|~ x)
+  SingleStepDerivation : DerivationType (|~ x <~ step)
+  NonTrivialDerivation : DerivationType (der <~ step1 <~ step2)
+
+public export
+derivationType : (der : FastDerivation leq x y) -> DerivationType der
+derivationType (|~ x) = TrivialDerivation
+derivationType (|~ x <~ step) = SingleStepDerivation
+derivationType ((z <~ w) <~ step) = NonTrivialDerivation
+
+public export
+0 Prerequisite : {0 der : FastDerivation {a = dom} leq x y} -> DerivationType der -> Type
+Prerequisite TrivialDerivation = Reflexive dom leq
+Prerequisite SingleStepDerivation = ()
+Prerequisite NonTrivialDerivation = Transitive dom leq
+
+-- Once we have the prerequisite for transitivity, we have the
+-- prerequisite for its inductive predecessor:
+public export
+inductivePrerequisite : (der : FastDerivation leq x y) ->
+  (0 step1 : Step leq y z) -> (0 step2 : Step leq z w) ->
+  Prerequisite (derivationType (der <~ step1 <~ step2)) ->
+  Prerequisite (derivationType (der <~ step1))
+inductivePrerequisite (  |~ y    ) step1 step2 prerequisite = ()
+inductivePrerequisite (z <~ step0) step1 step2 prerequisite = prerequisite
+
+public export
+preorderPrerequisite : Preorder dom leq => (der : FastDerivation leq x y) -> Prerequisite (derivationType der)
+preorderPrerequisite (|~ x) = %search
+preorderPrerequisite (|~ x <~ step) = ()
+preorderPrerequisite (der <~ step1 <~ step2) = %search
+
+||| The Prerequisite for the derivation:
+||| 0-length derivation: Reflexive dom leq
+||| 1-length derivation: Unit (no prerequisite)
+||| 2 steps of longer: Transitivity
+public export
+CalcSmart : {0 x : dom} -> {0 y : dom} -> (der : FastDerivation leq x y) ->
+  Prerequisite (derivationType der) => x `leq` y
+CalcSmart (|~ x) = reflexive
+CalcSmart (|~ x <~ y ... step) = step
+CalcSmart (der <~ _ ... step1
+               <~ w ... step2) @{prereq} =
+                CalcSmart (der <~ _ ... step1)
+                @{inductivePrerequisite der (_ ... step1) (w ... step2) prereq}
+                  `transitive` step2
+
+public export
+CalcWith : Preorder dom leq => {0 x : dom} -> {0 y : dom} -> (der : FastDerivation leq x y) -> x `leq` y
+CalcWith der = CalcSmart der @{preorderPrerequisite der}
 
 public export
 (~~) : {0 x : dom} -> {0 y : dom}
-         -> FastDerivation leq x y -> {z : dom} -> (step : Step Equal y z)
+         -> FastDerivation leq x y -> {0 z : dom} -> (0 step : Step Equal y z)
          -> FastDerivation leq x z
-(~~) der (z ... Refl) = der
+(~~) der (z ... yEqZ) = replace {p = FastDerivation leq _} yEqZ der
 
 -- Smart constructors
 public export
@@ -52,3 +102,7 @@ public export
 (.=<) : Reflexive a leq  => (y : a) -> {x : a} ->
     y === x -> Step leq x y
 (y .=<(Refl)) = (y ...(reflexive))
+
+public export
+(~=) : FastDerivation leq x y -> (0 z : dom) -> {auto xEqy : y = z} -> FastDerivation leq x z
+(~=) der z {xEqy} = der ~~ z ...(xEqy)