From 7f9db70e158293778609e5306e109707805f6408 Mon Sep 17 00:00:00 2001 From: crisoagf Date: Fri, 17 Feb 2023 17:47:54 +0000 Subject: [PATCH] Add PreorderReasoning comforts (#2778) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * Add PreorderReasoning comforts * Drop interface approach in favour of computation * Update libs/base/Syntax/PreorderReasoning.idr --------- Co-authored-by: Cristóvão Gomes Ferreira Co-authored-by: Ohad Kammar Co-authored-by: Guillaume Allais CI integration co-authored-by: @stefan-hoeck --- libs/base/Data/Nat.idr | 31 +++++++-- libs/base/Syntax/PreorderReasoning.idr | 7 +- .../base/Syntax/PreorderReasoning/Generic.idr | 68 +++++++++++++++++-- 3 files changed, 93 insertions(+), 13 deletions(-) diff --git a/libs/base/Data/Nat.idr b/libs/base/Data/Nat.idr index 3f88de262..16bef9606 100644 --- a/libs/base/Data/Nat.idr +++ b/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,11 +658,14 @@ 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 - LTSucc pltn => case view mltn of - LTZero => minusPos pltn - LTSucc mltn => minusLtMonotone mltn pltn +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 public export minusPlus : (m : Nat) -> minus (plus m n) m === n diff --git a/libs/base/Syntax/PreorderReasoning.idr b/libs/base/Syntax/PreorderReasoning.idr index d0c3d90f9..e2148f8ca 100644 --- a/libs/base/Syntax/PreorderReasoning.idr +++ b/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 diff --git a/libs/base/Syntax/PreorderReasoning/Generic.idr b/libs/base/Syntax/PreorderReasoning/Generic.idr index 777cfbff8..b52f71ba4 100644 --- a/libs/base/Syntax/PreorderReasoning/Generic.idr +++ b/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)