From f8e4d049f84a4cd46eae919c5ac0100a6af57d13 Mon Sep 17 00:00:00 2001 From: Guillaume ALLAIS Date: Thu, 11 Feb 2021 23:55:52 +0000 Subject: [PATCH 01/15] [ libs ] some preliminary work --- libs/base/Data/Nat.idr | 47 +++++++++++++++++++++++++++++++++ libs/prelude/Prelude/Basics.idr | 5 ++++ 2 files changed, 52 insertions(+) diff --git a/libs/base/Data/Nat.idr b/libs/base/Data/Nat.idr index ac317db5ed..1e4abded3c 100644 --- a/libs/base/Data/Nat.idr +++ b/libs/base/Data/Nat.idr @@ -80,6 +80,28 @@ public export LT : Nat -> Nat -> Type LT left right = LTE (S left) right +namespace LT + + ||| LT is defined in terms of LTE which makes it annoying to use. + ||| This convenient view of allows us to avoid having to constantly + ||| perform nested matches to obtain another LT subproof instead of + ||| an LTE one. + public export + data View : LT m n -> Type where + LTZero : View (LTESucc LTEZero) + LTSucc : (lt : m `LT` n) -> View (LTESucc lt) + + ||| Deconstruct an LT proof into either a base case or a further *LT* + export + view : (lt : LT m n) -> View lt + view (LTESucc LTEZero) = LTZero + view (LTESucc lt@(LTESucc _)) = LTSucc lt + + ||| A convenient alias for trivial LT proofs + export + ltZero : Z `LT` S m + ltZero = LTESucc LTEZero + public export GT : Nat -> Nat -> Type GT left right = LT right left @@ -482,6 +504,31 @@ minusPlusZero : (n, m : Nat) -> minus n (n + m) = Z minusPlusZero Z _ = Refl minusPlusZero (S n) m = minusPlusZero n m +export +minusPos : m `LT` n -> Z `LT` minus n m +minusPos lt = case view lt of + LTZero => ltZero + LTSucc lt => minusPos lt + +export +minusLteMonotone : {p : Nat} -> m `LTE` n -> minus m p `LTE` minus n p +minusLteMonotone LTEZero = LTEZero +minusLteMonotone {p = Z} prf@(LTESucc _) = prf +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 + +public export +minusPlus : (m : Nat) -> minus (plus m n) m === n +minusPlus Z = irrelevantEq (minusZeroRight n) +minusPlus (S m) = minusPlus m + export plusMinusLte : (n, m : Nat) -> LTE n m -> (minus m n) + n = m plusMinusLte Z m _ = rewrite minusZeroRight m in diff --git a/libs/prelude/Prelude/Basics.idr b/libs/prelude/Prelude/Basics.idr index 1327247e06..535fa0db39 100644 --- a/libs/prelude/Prelude/Basics.idr +++ b/libs/prelude/Prelude/Basics.idr @@ -108,6 +108,11 @@ export cong2 : (0 f : t1 -> t2 -> u) -> (p1 : a = b) -> (p2 : c = d) -> f a c = f b d cong2 f Refl Refl = Refl +||| Irrelevant equalities can always be made relevant +export +irrelevantEq : (0 _ : a === b) -> a === b +irrelevantEq Refl = Refl + -------------- -- BOOLEANS -- -------------- From 571367864b99cdb3cf7ec98df7ec06c02ccb99f1 Mon Sep 17 00:00:00 2001 From: Guillaume ALLAIS Date: Fri, 12 Feb 2021 00:26:30 +0000 Subject: [PATCH 02/15] [ new ] Data.Nat.Exponentiation --- libs/base/Data/Nat/Exponentiation.idr | 50 +++++++++++++++++++++++++++ 1 file changed, 50 insertions(+) create mode 100644 libs/base/Data/Nat/Exponentiation.idr diff --git a/libs/base/Data/Nat/Exponentiation.idr b/libs/base/Data/Nat/Exponentiation.idr new file mode 100644 index 0000000000..04706fc886 --- /dev/null +++ b/libs/base/Data/Nat/Exponentiation.idr @@ -0,0 +1,50 @@ +module Data.Nat.Exponentiation + +import Data.Nat.Views + +%default total + +export +linear : Monoid a => a -> Nat -> a +linear m = go where + + go : Nat -> a + go Z = neutral + go (S k) = m <+> go k + +export +modular : Monoid a => a -> Nat -> a +modular m k = go (halfRec k) where + + go : HalfRec n -> a + go HalfRecZ = neutral + go (HalfRecEven _ acc) = let e = go acc in e <+> e + go (HalfRecOdd _ acc) = let e = go acc in m <+> e <+> e + +-- TODO: proof the two definitions are equivalent for a monoid with laws + +namespace Semigroup + + public export + [ADDITIVE] Num a => Semigroup a + where (<+>) = (+) + public export + [MULTIPLICATIVE] Num a => Semigroup a + where (<+>) = (*) + +namespace Monoid + + public export + [ADDITIVE] Num a => Monoid a + using Semigroup.ADDITIVE + where neutral = 0 + public export + [MULTIPLICATIVE] Num a => Monoid a + using Semigroup.MULTIPLICATIVE + where neutral = 1 + + +infixl 10 ^ +export +(^) : Num a => a -> Nat -> a +(^) = modular @{MULTIPLICATIVE} From 558baf22b4403121fda86e6441b17ab4a5e09577 Mon Sep 17 00:00:00 2001 From: Guillaume ALLAIS Date: Fri, 12 Feb 2021 00:30:52 +0000 Subject: [PATCH 03/15] [ lib ] more preliminary work --- libs/base/Data/Nat.idr | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/libs/base/Data/Nat.idr b/libs/base/Data/Nat.idr index 1e4abded3c..a41880b5f8 100644 --- a/libs/base/Data/Nat.idr +++ b/libs/base/Data/Nat.idr @@ -389,6 +389,14 @@ plusLteMonotoneLeft p q r p_lt_q rewrite plusCommutative p r in plusLteMonotoneRight p q r p_lt_q +export +plusLteMonotone : {m, n, p, q : Nat} -> m `LTE` n -> p `LTE` q -> + (m + p) `LTE` (n + q) +plusLteMonotone left right + = lteTransitive + (plusLteMonotoneLeft m p q right) + (plusLteMonotoneRight q m n left) + zeroPlusLeftZero : (a,b : Nat) -> (0 = a + b) -> a = 0 zeroPlusLeftZero 0 0 Refl = Refl zeroPlusLeftZero (S k) b _ impossible From 0a6511f498df52e0259db9d0bbdaa21369e4de0b Mon Sep 17 00:00:00 2001 From: Guillaume ALLAIS Date: Fri, 12 Feb 2021 11:37:24 +0000 Subject: [PATCH 04/15] [ new ] Data.Tree.Perfect TODO: use the more efficient exponentiation function --- libs/contrib/Data/Nat/Order/Properties.idr | 8 ++ libs/contrib/Data/Tree/Perfect.idr | 106 +++++++++++++++++++++ 2 files changed, 114 insertions(+) create mode 100644 libs/contrib/Data/Tree/Perfect.idr diff --git a/libs/contrib/Data/Nat/Order/Properties.idr b/libs/contrib/Data/Nat/Order/Properties.idr index cf547b0179..301b0dd909 100644 --- a/libs/contrib/Data/Nat/Order/Properties.idr +++ b/libs/contrib/Data/Nat/Order/Properties.idr @@ -34,10 +34,18 @@ export lteIsLTE : (a, b : Nat) -> a `lte` b = True -> a `LTE` b lteIsLTE a b prf = invert (replace {p = Reflects (a `LTE` b)} prf (lteReflection a b)) +export +ltIsLT : (a, b : Nat) -> a `lt` b = True -> a `LT` b +ltIsLT a = lteIsLTE (S a) + export notlteIsNotLTE : (a, b : Nat) -> a `lte` b = False -> Not (a `LTE` b) notlteIsNotLTE a b prf = invert (replace {p = Reflects (a `LTE` b)} prf (lteReflection a b)) +export +notltIsNotLT : (a, b : Nat) -> a `lt` b = False -> Not (a `LT` b) +notltIsNotLT a = notlteIsNotLTE (S a) + export notlteIsLT : (a, b : Nat) -> a `lte` b = False -> b `LT` a diff --git a/libs/contrib/Data/Tree/Perfect.idr b/libs/contrib/Data/Tree/Perfect.idr new file mode 100644 index 0000000000..e3c29fa8e2 --- /dev/null +++ b/libs/contrib/Data/Tree/Perfect.idr @@ -0,0 +1,106 @@ +module Data.Tree.Perfect + +import Decidable.Order +import Decidable.Order.Strict +import Data.Nat +import Data.Nat.Order +import Data.Nat.Order.Strict +import Data.Nat.Order.Properties +import Data.DPair +import Syntax.WithProof + +%default total + +public export +data Tree : Nat -> Type -> Type where + Leaf : a -> Tree Z a + Node : Tree n a -> Tree n a -> Tree (S n) a + +public export +Functor (Tree n) where + map f (Leaf a) = Leaf (f a) + map f (Node l r) = Node (map f l) (map f r) + +public export +data Path : Nat -> Type where + Here : Path Z + Left : Path n -> Path (S n) + Right : Path n -> Path (S n) + +infixl 10 ^ + +public export +(^) : Num a => a -> Nat -> a +m ^ Z = 1 +m ^ S n = let k = m ^ n in k + k + +export +lteExp : {m : Nat} -> LTE 1 (2 ^ m) +lteExp {m = Z} = lteRefl +lteExp {m = S m} = + let ih = lteExp {m} in + transitive {po = LTE} 1 2 (2 ^ S m) (LTESucc LTEZero) (plusLteMonotone ih ih) + +public export +toNat : {n : _} -> Path n -> Nat +toNat Here = Z +toNat (Left p) = toNat p +toNat {n = S n} (Right p) = toNat p + 2 ^ n + +export +toNatBounded : (n : Nat) -> (p : Path n) -> toNat p `LT` 2 ^ n +toNatBounded Z Here = lteRefl +toNatBounded (S n) (Left p) = + let prf = plusLteMonotoneRight (2 ^ n) 1 (2 ^ n) lteExp in + transitive {spo = LT} (toNat p) (2 ^ n) (2 ^ S n) (toNatBounded n p) prf +toNatBounded (S n) (Right p) = + plusLteMonotoneRight (2 ^ n) (S (toNat p)) (2 ^ n) (toNatBounded n p) + +namespace FromNat + + public export + data View : (k, n : Nat) -> Type where + ZZ : View Z Z + SLT : (0 p : k `LT` 2 ^ n) -> View k (S n) + SNLT : (0 p : k `GTE` 2 ^ n) -> + (0 rec : minus k (2 ^ n) `LT` 2 ^ n) -> View k (S n) + + public export + view : (k, n : Nat) -> (0 _ : k `LT` (2 ^ n)) -> View k n + view Z Z p = ZZ + view (S _) Z p = void $ absurd (fromLteSucc p) + view k (S n) p with (@@ lt k (2 ^ n)) + view k (S n) p | (True ** eq) = SLT (ltIsLT k (2 ^ n) eq) + view k (S n) p | (False ** eq) = SNLT gte prf where + + 0 gte : k `GTE` 2 ^ n + gte = notLTImpliesGTE (notltIsNotLT k (2 ^ n) eq) + + 0 bnd : minus k (2 ^ n) `LT` minus (2 ^ (S n)) (2 ^ n) + bnd = minusLtMonotone p (plusLteMonotoneRight (2 ^ n) _ _ lteExp) + + 0 prf : minus k (2 ^ n) `LT` 2 ^ n + prf = replace {p = LTE _} (minusPlus _) bnd + +public export +fromNat : (k, n : Nat) -> (0 _ : k `LT` (2 ^ n)) -> Path n +fromNat k n p with (view k n p) + fromNat Z Z p | ZZ = Here + fromNat k (S n) p | SLT lt = Left (fromNat k n lt) + fromNat k (S n) p | SNLT _ lt = Right (fromNat (minus k (2 ^ n)) n lt) + +export +fromNatCorrect : (k, n : Nat) -> (0 p : k `LT` 2 ^ n) -> + toNat (fromNat k n p) === k +fromNatCorrect k n p with (view k n p) + fromNatCorrect Z Z p | ZZ = Refl + fromNatCorrect k (S n) p | SLT lt = fromNatCorrect k n lt + fromNatCorrect k (S n) p | SNLT gte lt + = rewrite fromNatCorrect (minus k (2 ^ n)) n lt in + irrelevantEq $ plusMinusLte (2 ^ n) k gte + +public export +lookup : Tree n a -> Path n -> a +lookup (Leaf a) Here = a +lookup (Node l _) (Left p) = lookup l p +lookup (Node _ r) (Right p) = lookup r p From c89c81b92190f5b2dcb05a778d03e81b30de51c3 Mon Sep 17 00:00:00 2001 From: Guillaume ALLAIS Date: Fri, 12 Feb 2021 11:41:07 +0000 Subject: [PATCH 05/15] [ doc ] for some of the perfect tree functions --- libs/contrib/Data/Tree/Perfect.idr | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/libs/contrib/Data/Tree/Perfect.idr b/libs/contrib/Data/Tree/Perfect.idr index e3c29fa8e2..6b118a04b5 100644 --- a/libs/contrib/Data/Tree/Perfect.idr +++ b/libs/contrib/Data/Tree/Perfect.idr @@ -58,6 +58,11 @@ toNatBounded (S n) (Right p) = namespace FromNat + ||| This pattern-matching in `fromNat` is annoying: + ||| The `Z (S _)` case is impossible + ||| In the `k (S n)` case we want to branch on whether `k `LT` 2 ^ n` + ||| and get our hands on some proofs. + ||| This view factors out that work. public export data View : (k, n : Nat) -> Type where ZZ : View Z Z @@ -82,6 +87,7 @@ namespace FromNat 0 prf : minus k (2 ^ n) `LT` 2 ^ n prf = replace {p = LTE _} (minusPlus _) bnd +||| Convert a natural number to a path in a perfect binary tree public export fromNat : (k, n : Nat) -> (0 _ : k `LT` (2 ^ n)) -> Path n fromNat k n p with (view k n p) @@ -89,6 +95,7 @@ fromNat k n p with (view k n p) fromNat k (S n) p | SLT lt = Left (fromNat k n lt) fromNat k (S n) p | SNLT _ lt = Right (fromNat (minus k (2 ^ n)) n lt) +||| The `fromNat` conversion is compatible with the semantics `toNat` export fromNatCorrect : (k, n : Nat) -> (0 p : k `LT` 2 ^ n) -> toNat (fromNat k n p) === k From 78c55352807ea610ea027804788539ead7e2f09c Mon Sep 17 00:00:00 2001 From: Guillaume ALLAIS Date: Fri, 12 Feb 2021 16:28:55 +0000 Subject: [PATCH 06/15] [ more ] proofs about exponentiation --- libs/base/Data/Nat/Exponentiation.idr | 50 -------------- libs/contrib/Data/Monoid/Exponentiation.idr | 73 +++++++++++++++++++++ 2 files changed, 73 insertions(+), 50 deletions(-) delete mode 100644 libs/base/Data/Nat/Exponentiation.idr create mode 100644 libs/contrib/Data/Monoid/Exponentiation.idr diff --git a/libs/base/Data/Nat/Exponentiation.idr b/libs/base/Data/Nat/Exponentiation.idr deleted file mode 100644 index 04706fc886..0000000000 --- a/libs/base/Data/Nat/Exponentiation.idr +++ /dev/null @@ -1,50 +0,0 @@ -module Data.Nat.Exponentiation - -import Data.Nat.Views - -%default total - -export -linear : Monoid a => a -> Nat -> a -linear m = go where - - go : Nat -> a - go Z = neutral - go (S k) = m <+> go k - -export -modular : Monoid a => a -> Nat -> a -modular m k = go (halfRec k) where - - go : HalfRec n -> a - go HalfRecZ = neutral - go (HalfRecEven _ acc) = let e = go acc in e <+> e - go (HalfRecOdd _ acc) = let e = go acc in m <+> e <+> e - --- TODO: proof the two definitions are equivalent for a monoid with laws - -namespace Semigroup - - public export - [ADDITIVE] Num a => Semigroup a - where (<+>) = (+) - public export - [MULTIPLICATIVE] Num a => Semigroup a - where (<+>) = (*) - -namespace Monoid - - public export - [ADDITIVE] Num a => Monoid a - using Semigroup.ADDITIVE - where neutral = 0 - public export - [MULTIPLICATIVE] Num a => Monoid a - using Semigroup.MULTIPLICATIVE - where neutral = 1 - - -infixl 10 ^ -export -(^) : Num a => a -> Nat -> a -(^) = modular @{MULTIPLICATIVE} diff --git a/libs/contrib/Data/Monoid/Exponentiation.idr b/libs/contrib/Data/Monoid/Exponentiation.idr new file mode 100644 index 0000000000..fdfbff521f --- /dev/null +++ b/libs/contrib/Data/Monoid/Exponentiation.idr @@ -0,0 +1,73 @@ +module Data.Monoid.Exponentiation + +import Control.Algebra +import Data.Nat.Views +import Data.Num.Implementations +import Syntax.PreorderReasoning + +%default total + +------------------------------------------------------------------------ +-- Implementations + +export +linear : Monoid a => a -> Nat -> a +linear v Z = neutral +linear v (S k) = v <+> linear v k + +export +modularRec : Monoid a => a -> HalfRec n -> a +modularRec v HalfRecZ = neutral +modularRec v (HalfRecEven _ acc) = let e = modularRec v acc in e <+> e +modularRec v (HalfRecOdd _ acc) = let e = modularRec v acc in v <+> e <+> e + +export +modular : Monoid a => a -> Nat -> a +modular v n = modularRec v (halfRec n) + +------------------------------------------------------------------------ +-- Properties + +-- Not using `MonoidV` because it's cursed +export +linearPlusHomo : (mon : Monoid a) => + -- good monoid + (opAssoc : {0 x, y, z : a} -> ((x <+> y) <+> z) === (x <+> (y <+> z))) -> + (neutralL : {0 x : a} -> (neutral @{mon} <+> x) === x) -> + -- result + (v : a) -> {m, n : Nat} -> + (linear v m <+> linear v n) === linear v (m + n) +linearPlusHomo opAssoc neutralL v = go m where + + go : (m : Nat) -> (linear v m <+> linear v n) === linear v (m + n) + go Z = neutralL + go (S m) = Calc $ + |~ (v <+> linear v m) <+> linear v n + ~~ v <+> (linear v m <+> linear v n) ...( opAssoc ) + ~~ v <+> (linear v (m + n)) ...( cong (v <+>) (go m) ) + +export +modularRecCorrect : (mon : Monoid a) => + -- good monoid + (opAssoc : {0 x, y, z : a} -> ((x <+> y) <+> z) === (x <+> (y <+> z))) -> + (neutralL : {0 x : a} -> (neutral @{mon} <+> x) === x) -> + -- result + (v : a) -> {n : Nat} -> (p : HalfRec n) -> + modularRec v p === linear v n +modularRecCorrect opAssoc neutralL v acc = go acc where + + aux : {m, n : Nat} -> (linear v m <+> linear v n) === linear v (m + n) + aux = linearPlusHomo opAssoc neutralL v + + go : {n : Nat} -> (p : HalfRec n) -> modularRec v p === linear v n + go HalfRecZ = Refl + go (HalfRecEven k acc) = rewrite go acc in aux + go (HalfRecOdd k acc) = rewrite go acc in Calc $ + |~ (v <+> linear v k) <+> linear v k + ~~ v <+> (linear v k <+> linear v k) ...( opAssoc ) + ~~ v <+> (linear v (k + k)) ...( cong (v <+>) aux ) + +infixl 10 ^ +export +(^) : Num a => a -> Nat -> a +(^) = modular @{MULTIPLICATIVE} From 327d2e44e015965d3809fc2ad737ba7507607a94 Mon Sep 17 00:00:00 2001 From: Guillaume ALLAIS Date: Fri, 12 Feb 2021 16:31:03 +0000 Subject: [PATCH 07/15] [ fix ] more of Nat's structures --- libs/base/Data/Nat.idr | 36 +++++++++++++++++++++++++------ libs/contrib/Data/Nat/Algebra.idr | 20 ++++++++++------- 2 files changed, 42 insertions(+), 14 deletions(-) diff --git a/libs/base/Data/Nat.idr b/libs/base/Data/Nat.idr index a41880b5f8..e35546fb66 100644 --- a/libs/base/Data/Nat.idr +++ b/libs/base/Data/Nat.idr @@ -697,10 +697,34 @@ sucMinR (S l) = cong S $ sucMinR l -- Algebra ----------------------------- -public export -Semigroup Nat where - (<+>) = plus +namespace Semigroup -public export -Monoid Nat where - neutral = Z + public export + [Additive] Semigroup Nat where + (<+>) = (+) + + public export + [Multiplicative] Semigroup Nat where + (<+>) = (*) + + public export + [Maximum] Semigroup Nat where + (<+>) = max + + public export + [Minimum] Semigroup Nat where + (<+>) = min + +namespace Monoid + + public export + [Additive] Monoid Nat using Semigroup.Additive where + neutral = 0 + + public export + [Multiplicative] Monoid Nat using Semigroup.Multiplicative where + neutral = 1 + + public export + [Maximum] Monoid Nat using Semigroup.Maximum where + neutral = 0 diff --git a/libs/contrib/Data/Nat/Algebra.idr b/libs/contrib/Data/Nat/Algebra.idr index 277fd0251c..3b19e2bbf7 100644 --- a/libs/contrib/Data/Nat/Algebra.idr +++ b/libs/contrib/Data/Nat/Algebra.idr @@ -5,11 +5,15 @@ import Data.Nat %default total -public export -SemigroupV Nat where - semigroupOpIsAssociative = plusAssociative - -public export -MonoidV Nat where - monoidNeutralIsNeutralL = plusZeroRightNeutral - monoidNeutralIsNeutralR = plusZeroLeftNeutral +namespace SemigroupV + + public export + [Additive] SemigroupV Nat using Semigroup.Additive where + semigroupOpIsAssociative = plusAssociative + +namespace MonoidV + + public export + [Additive] MonoidV Nat using Monoid.Additive SemigroupV.Additive where + monoidNeutralIsNeutralL = plusZeroRightNeutral + monoidNeutralIsNeutralR = plusZeroLeftNeutral From 42d79f08608ff0ee532d75b70ae816fa474b933f Mon Sep 17 00:00:00 2001 From: Guillaume ALLAIS Date: Fri, 12 Feb 2021 18:27:30 +0000 Subject: [PATCH 08/15] [ refactor ] using the newly introduced functions and proofs --- libs/contrib/Data/Monoid/Exponentiation.idr | 22 ++++-- libs/contrib/Data/Nat/Exponentiation.idr | 83 +++++++++++++++++++++ libs/contrib/Data/Num/Implementations.idr | 23 ++++++ libs/contrib/Data/Tree/Perfect.idr | 81 ++++++++++---------- 4 files changed, 163 insertions(+), 46 deletions(-) create mode 100644 libs/contrib/Data/Nat/Exponentiation.idr create mode 100644 libs/contrib/Data/Num/Implementations.idr diff --git a/libs/contrib/Data/Monoid/Exponentiation.idr b/libs/contrib/Data/Monoid/Exponentiation.idr index fdfbff521f..abd4363c5b 100644 --- a/libs/contrib/Data/Monoid/Exponentiation.idr +++ b/libs/contrib/Data/Monoid/Exponentiation.idr @@ -10,21 +10,26 @@ import Syntax.PreorderReasoning ------------------------------------------------------------------------ -- Implementations -export +public export linear : Monoid a => a -> Nat -> a linear v Z = neutral linear v (S k) = v <+> linear v k -export +public export modularRec : Monoid a => a -> HalfRec n -> a modularRec v HalfRecZ = neutral modularRec v (HalfRecEven _ acc) = let e = modularRec v acc in e <+> e modularRec v (HalfRecOdd _ acc) = let e = modularRec v acc in v <+> e <+> e -export +public export modular : Monoid a => a -> Nat -> a modular v n = modularRec v (halfRec n) +infixl 10 ^ +public export +(^) : Num a => a -> Nat -> a +(^) = modular @{Multiplicative} + ------------------------------------------------------------------------ -- Properties @@ -67,7 +72,12 @@ modularRecCorrect opAssoc neutralL v acc = go acc where ~~ v <+> (linear v k <+> linear v k) ...( opAssoc ) ~~ v <+> (linear v (k + k)) ...( cong (v <+>) aux ) -infixl 10 ^ export -(^) : Num a => a -> Nat -> a -(^) = modular @{MULTIPLICATIVE} +modularCorrect : (mon : Monoid a) => + -- good monoid + (opAssoc : {0 x, y, z : a} -> ((x <+> y) <+> z) === (x <+> (y <+> z))) -> + (neutralL : {0 x : a} -> (neutral @{mon} <+> x) === x) -> + -- result + (v : a) -> {n : Nat} -> modular v n === linear v n +modularCorrect opAssoc neutralL v + = modularRecCorrect opAssoc neutralL v (halfRec n) diff --git a/libs/contrib/Data/Nat/Exponentiation.idr b/libs/contrib/Data/Nat/Exponentiation.idr new file mode 100644 index 0000000000..1f80b81b58 --- /dev/null +++ b/libs/contrib/Data/Nat/Exponentiation.idr @@ -0,0 +1,83 @@ +module Data.Nat.Exponentiation + +import Data.Nat as Nat +import Data.Monoid.Exponentiation as Mon +import Data.Num.Implementations as Num +import Data.Nat.Views +import Data.Nat.Order +import Decidable.Order +import Syntax.PreorderReasoning +import Syntax.PreorderReasoning.Generic + +%default total + +public export +pow : Nat -> Nat -> Nat +pow = Mon.(^) + +public export +lpow : Nat -> Nat -> Nat +lpow = linear @{Nat.Monoid.Multiplicative} + +public export +pow2 : Nat -> Nat +pow2 = (2 ^) + +public export +lpow2 : Nat -> Nat +lpow2 = lpow 2 + +export +modularCorrect : (v : Nat) -> {n : Nat} -> + pow v n === lpow v n +modularCorrect + = Mon.modularCorrect + @{Nat.Monoid.Multiplicative} + (sym (multAssociative _ _ _)) + (irrelevantEq $ multOneLeftNeutral _) + +export +pow2Correct : {n : Nat} -> pow2 n === lpow2 n +pow2Correct = modularCorrect 2 + +export +unfoldDouble : {0 n : Nat} -> (2 * n) === (n + n) +unfoldDouble = irrelevantEq $ cong (n +) (plusZeroRightNeutral _) + +export +unfoldLpow2 : lpow2 (S n) === (lpow2 n + lpow2 n) +unfoldLpow2 = unfoldDouble + +export +unfoldPow2 : pow2 (S n) === (pow2 n + pow2 n) +unfoldPow2 = irrelevantEq $ Calc $ + let mon : Monoid Nat; mon = Nat.Monoid.Multiplicative + lpow2 : Nat -> Nat; lpow2 = linear @{mon} 2 in + |~ pow2 (S n) + ~~ lpow2 (S n) ...( pow2Correct ) + ~~ lpow2 n + lpow2 n ...( unfoldLpow2 ) + ~~ (pow2 n + pow2 n) ...( cong2 (+) (sym pow2Correct) (sym pow2Correct) ) + +export +lteLpow2 : {m : Nat} -> 1 `LTE` lpow2 m +lteLpow2 {m = Z} = lteRefl +lteLpow2 {m = S m} = CalcWith $ + let ih = lteLpow2 {m} in + |~ 1 + <~ 2 ...( ltZero ) + <~ lpow2 m + lpow2 m ...( plusLteMonotone ih ih ) + ~~ lpow2 (S m) ...( sym (unfoldLpow2) ) + +export +ltePow2 : {m : Nat} -> 1 `LTE` pow2 m +ltePow2 = CalcWith $ + |~ 1 + <~ lpow2 m ...( lteLpow2 ) + ~~ pow2 m ...( sym pow2Correct ) + +export +pow2Increasing : {m : Nat} -> pow2 m `LT` pow2 (S m) +pow2Increasing = CalcWith $ + |~ S (pow2 m) + <~ pow2 m + pow2 m ...( plusLteMonotoneRight (pow2 m) 1 (pow2 m) ltePow2 ) + ~~ pow2 (S m) ...( sym unfoldPow2 ) diff --git a/libs/contrib/Data/Num/Implementations.idr b/libs/contrib/Data/Num/Implementations.idr new file mode 100644 index 0000000000..1af11797ca --- /dev/null +++ b/libs/contrib/Data/Num/Implementations.idr @@ -0,0 +1,23 @@ +module Data.Num.Implementations + +%default total + +namespace Semigroup + + public export + [Additive] Num a => Semigroup a + where (<+>) = (+) + public export + [Multiplicative] Num a => Semigroup a + where (<+>) = (*) + +namespace Monoid + + public export + [Additive] Num a => Monoid a + using Semigroup.Additive + where neutral = 0 + public export + [Multiplicative] Num a => Monoid a + using Semigroup.Multiplicative + where neutral = 1 diff --git a/libs/contrib/Data/Tree/Perfect.idr b/libs/contrib/Data/Tree/Perfect.idr index 6b118a04b5..6f3f4db58d 100644 --- a/libs/contrib/Data/Tree/Perfect.idr +++ b/libs/contrib/Data/Tree/Perfect.idr @@ -1,13 +1,19 @@ module Data.Tree.Perfect +import Control.WellFounded import Decidable.Order import Decidable.Order.Strict +import Data.Monoid.Exponentiation +import Data.Num.Implementations +import Data.Nat.Views import Data.Nat import Data.Nat.Order import Data.Nat.Order.Strict import Data.Nat.Order.Properties +import Data.Nat.Exponentiation import Data.DPair import Syntax.WithProof +import Syntax.PreorderReasoning.Generic %default total @@ -27,84 +33,79 @@ data Path : Nat -> Type where Left : Path n -> Path (S n) Right : Path n -> Path (S n) -infixl 10 ^ - -public export -(^) : Num a => a -> Nat -> a -m ^ Z = 1 -m ^ S n = let k = m ^ n in k + k - -export -lteExp : {m : Nat} -> LTE 1 (2 ^ m) -lteExp {m = Z} = lteRefl -lteExp {m = S m} = - let ih = lteExp {m} in - transitive {po = LTE} 1 2 (2 ^ S m) (LTESucc LTEZero) (plusLteMonotone ih ih) - public export toNat : {n : _} -> Path n -> Nat toNat Here = Z toNat (Left p) = toNat p -toNat {n = S n} (Right p) = toNat p + 2 ^ n +toNat {n = S n} (Right p) = toNat p + pow2 n export -toNatBounded : (n : Nat) -> (p : Path n) -> toNat p `LT` 2 ^ n +toNatBounded : (n : Nat) -> (p : Path n) -> toNat p `LT` pow2 n toNatBounded Z Here = lteRefl -toNatBounded (S n) (Left p) = - let prf = plusLteMonotoneRight (2 ^ n) 1 (2 ^ n) lteExp in - transitive {spo = LT} (toNat p) (2 ^ n) (2 ^ S n) (toNatBounded n p) prf -toNatBounded (S n) (Right p) = - plusLteMonotoneRight (2 ^ n) (S (toNat p)) (2 ^ n) (toNatBounded n p) +toNatBounded (S n) (Left p) = CalcWith $ + |~ S (toNat p) + <~ pow2 n ...( toNatBounded n p ) + <~ pow2 n + pow2 n ...( lteAddRight (pow2 n) ) + ~~ pow2 (S n) ...( sym unfoldPow2 ) +toNatBounded (S n) (Right p) = CalcWith $ + let ih = toNatBounded n p in + |~ S (toNat p) + pow2 n + <~ pow2 n + pow2 n ...( plusLteMonotoneRight _ _ _ ih ) + ~~ pow2 (S n) ...( sym unfoldPow2 ) namespace FromNat ||| This pattern-matching in `fromNat` is annoying: ||| The `Z (S _)` case is impossible - ||| In the `k (S n)` case we want to branch on whether `k `LT` 2 ^ n` + ||| In the `k (S n)` case we want to branch on whether `k `LT` pow2 n` ||| and get our hands on some proofs. ||| This view factors out that work. public export data View : (k, n : Nat) -> Type where ZZ : View Z Z - SLT : (0 p : k `LT` 2 ^ n) -> View k (S n) - SNLT : (0 p : k `GTE` 2 ^ n) -> - (0 rec : minus k (2 ^ n) `LT` 2 ^ n) -> View k (S n) + SLT : (0 p : k `LT` pow2 n) -> View k (S n) + SNLT : (0 p : k `GTE` pow2 n) -> + (0 rec : minus k (pow2 n) `LT` pow2 n) -> View k (S n) public export - view : (k, n : Nat) -> (0 _ : k `LT` (2 ^ n)) -> View k n + view : (k, n : Nat) -> (0 _ : k `LT` (pow2 n)) -> View k n view Z Z p = ZZ view (S _) Z p = void $ absurd (fromLteSucc p) - view k (S n) p with (@@ lt k (2 ^ n)) - view k (S n) p | (True ** eq) = SLT (ltIsLT k (2 ^ n) eq) + view k (S n) p with (@@ lt k (pow2 n)) + view k (S n) p | (True ** eq) = SLT (ltIsLT k (pow2 n) eq) view k (S n) p | (False ** eq) = SNLT gte prf where - 0 gte : k `GTE` 2 ^ n - gte = notLTImpliesGTE (notltIsNotLT k (2 ^ n) eq) - - 0 bnd : minus k (2 ^ n) `LT` minus (2 ^ (S n)) (2 ^ n) - bnd = minusLtMonotone p (plusLteMonotoneRight (2 ^ n) _ _ lteExp) + 0 gte : k `GTE` pow2 n + gte = notLTImpliesGTE (notltIsNotLT k (pow2 n) eq) - 0 prf : minus k (2 ^ n) `LT` 2 ^ n - prf = replace {p = LTE _} (minusPlus _) bnd + 0 prf : minus k (pow2 n) `LT` pow2 n + prf = CalcWith $ + |~ S (minus k (pow2 n)) + <~ minus (pow2 (S n)) (pow2 n) + ...( minusLtMonotone p pow2Increasing ) + ~~ minus (pow2 n + pow2 n) (pow2 n) + ...( cong (\ m => minus m (pow2 n)) unfoldPow2 ) + ~~ pow2 n + ...( minusPlus (pow2 n) ) ||| Convert a natural number to a path in a perfect binary tree public export -fromNat : (k, n : Nat) -> (0 _ : k `LT` (2 ^ n)) -> Path n +fromNat : (k, n : Nat) -> (0 _ : k `LT` pow2 n) -> Path n fromNat k n p with (view k n p) fromNat Z Z p | ZZ = Here fromNat k (S n) p | SLT lt = Left (fromNat k n lt) - fromNat k (S n) p | SNLT _ lt = Right (fromNat (minus k (2 ^ n)) n lt) + fromNat k (S n) p | SNLT _ lt = Right (fromNat (minus k (pow2 n)) n lt) ||| The `fromNat` conversion is compatible with the semantics `toNat` export -fromNatCorrect : (k, n : Nat) -> (0 p : k `LT` 2 ^ n) -> +fromNatCorrect : (k, n : Nat) -> (0 p : k `LT` pow2 n) -> toNat (fromNat k n p) === k fromNatCorrect k n p with (view k n p) fromNatCorrect Z Z p | ZZ = Refl fromNatCorrect k (S n) p | SLT lt = fromNatCorrect k n lt fromNatCorrect k (S n) p | SNLT gte lt - = rewrite fromNatCorrect (minus k (2 ^ n)) n lt in - irrelevantEq $ plusMinusLte (2 ^ n) k gte + = rewrite fromNatCorrect (minus k (pow2 n)) n lt in + irrelevantEq $ plusMinusLte (pow2 n) k gte public export lookup : Tree n a -> Path n -> a From 3d9305cc99f8c1b56c5cdc347e6d84bb7b88fcd4 Mon Sep 17 00:00:00 2001 From: Guillaume ALLAIS Date: Fri, 12 Feb 2021 18:43:18 +0000 Subject: [PATCH 09/15] [ more ] Applicative instance for Tree n --- libs/contrib/Data/Tree/Perfect.idr | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/libs/contrib/Data/Tree/Perfect.idr b/libs/contrib/Data/Tree/Perfect.idr index 6f3f4db58d..a9be4610fc 100644 --- a/libs/contrib/Data/Tree/Perfect.idr +++ b/libs/contrib/Data/Tree/Perfect.idr @@ -27,6 +27,18 @@ Functor (Tree n) where map f (Leaf a) = Leaf (f a) map f (Node l r) = Node (map f l) (map f r) +public export +replicate : (n : Nat) -> a -> Tree n a +replicate Z a = Leaf a +replicate (S n) a = let t = replicate n a in Node t t + +public export +{n : _} -> Applicative (Tree n) where + pure = replicate n + + Leaf f <*> Leaf a = Leaf (f a) + Node fl fr <*> Node xl xr = Node (fl <*> xl) (fr <*> xr) + public export data Path : Nat -> Type where Here : Path Z From 604f0def074645bead0defa77859923ed9b74c28 Mon Sep 17 00:00:00 2001 From: Guillaume ALLAIS Date: Sun, 14 Feb 2021 14:07:41 +0000 Subject: [PATCH 10/15] [ new ] binary numbers Note that the representation is not unique --- libs/base/Data/Nat.idr | 5 +-- libs/contrib/Data/Binary.idr | 42 ++++++++++++++++++++++++ libs/contrib/Data/Binary/Digit.idr | 15 +++++++++ libs/contrib/Data/Nat/Exponentiation.idr | 5 +-- libs/contrib/Data/Nat/Properties.idr | 13 ++++++++ 5 files changed, 74 insertions(+), 6 deletions(-) create mode 100644 libs/contrib/Data/Binary.idr create mode 100644 libs/contrib/Data/Binary/Digit.idr diff --git a/libs/base/Data/Nat.idr b/libs/base/Data/Nat.idr index e35546fb66..8a552c18b6 100644 --- a/libs/base/Data/Nat.idr +++ b/libs/base/Data/Nat.idr @@ -473,8 +473,9 @@ multOneLeftNeutral right = plusZeroRightNeutral right export multOneRightNeutral : (left : Nat) -> left * 1 = left -multOneRightNeutral left = rewrite multCommutative left 1 in multOneLeftNeutral left - +multOneRightNeutral left = + rewrite multCommutative left 1 in + multOneLeftNeutral left -- Proofs on minus diff --git a/libs/contrib/Data/Binary.idr b/libs/contrib/Data/Binary.idr new file mode 100644 index 0000000000..4cc7d0f733 --- /dev/null +++ b/libs/contrib/Data/Binary.idr @@ -0,0 +1,42 @@ +module Data.Binary + +import Data.Nat +import Data.Nat.Properties +import Data.Binary.Digit +import Syntax.PreorderReasoning + +%default total + +||| Bin represents binary numbers right-to-left. +||| For instance `4` can be represented as `OOI`. +||| Note that representations are not unique: one may append arbitrarily +||| many Os to the right of the representation without changing the meaning. +public export +Bin : Type +Bin = List Digit + +||| Conversion from lists of bits to natural number. +public export +toNat : Bin -> Nat +toNat = foldr (\ b, acc => toNat b + 2 * acc) 0 + +||| Successor function on binary numbers. +||| Amortised constant time. +public export +suc : Bin -> Bin +suc [] = [I] +suc (O :: bs) = I :: bs +suc (I :: bs) = O :: (suc bs) + +||| Correctness proof of `suc` with respect to the semantics in terms of Nat +export +sucCorrect : {bs : Bin} -> toNat (suc bs) === S (toNat bs) +sucCorrect {bs = []} = Refl +sucCorrect {bs = O :: bs} = Refl +sucCorrect {bs = I :: bs} = Calc $ + |~ toNat (suc (I :: bs)) + ~~ toNat (O :: suc bs) ...( Refl ) + ~~ 2 * toNat (suc bs) ...( Refl ) + ~~ 2 * S (toNat bs) ...( cong (2 *) sucCorrect ) + ~~ 2 + 2 * toNat bs ...( unfoldDoubleS ) + ~~ S (toNat (I :: bs)) ...( Refl ) diff --git a/libs/contrib/Data/Binary/Digit.idr b/libs/contrib/Data/Binary/Digit.idr new file mode 100644 index 0000000000..20b336fbc5 --- /dev/null +++ b/libs/contrib/Data/Binary/Digit.idr @@ -0,0 +1,15 @@ +module Data.Binary.Digit + +%default total + +||| This is essentially Bool but with names that are easier +||| to understand +public export +data Digit : Type where + O : Digit + I : Digit + +public export +toNat : Digit -> Nat +toNat O = 0 +toNat I = 1 diff --git a/libs/contrib/Data/Nat/Exponentiation.idr b/libs/contrib/Data/Nat/Exponentiation.idr index 1f80b81b58..017943d994 100644 --- a/libs/contrib/Data/Nat/Exponentiation.idr +++ b/libs/contrib/Data/Nat/Exponentiation.idr @@ -1,6 +1,7 @@ module Data.Nat.Exponentiation import Data.Nat as Nat +import Data.Nat.Properties import Data.Monoid.Exponentiation as Mon import Data.Num.Implementations as Num import Data.Nat.Views @@ -40,10 +41,6 @@ export pow2Correct : {n : Nat} -> pow2 n === lpow2 n pow2Correct = modularCorrect 2 -export -unfoldDouble : {0 n : Nat} -> (2 * n) === (n + n) -unfoldDouble = irrelevantEq $ cong (n +) (plusZeroRightNeutral _) - export unfoldLpow2 : lpow2 (S n) === (lpow2 n + lpow2 n) unfoldLpow2 = unfoldDouble diff --git a/libs/contrib/Data/Nat/Properties.idr b/libs/contrib/Data/Nat/Properties.idr index 962410bf82..fa0f98bc70 100644 --- a/libs/contrib/Data/Nat/Properties.idr +++ b/libs/contrib/Data/Nat/Properties.idr @@ -2,9 +2,22 @@ module Data.Nat.Properties import Data.Nat +import Syntax.PreorderReasoning %default total +export +unfoldDouble : {0 n : Nat} -> (2 * n) === (n + n) +unfoldDouble = irrelevantEq $ cong (n +) (plusZeroRightNeutral _) + +export +unfoldDoubleS : {0 n : Nat} -> (2 * S n) === (2 + 2 * n) +unfoldDoubleS = irrelevantEq $ Calc $ + |~ 2 * S n + ~~ S n + S n ...( unfoldDouble {n = S n} ) + ~~ 2 + (n + n) ...( sym (plusSuccRightSucc (S n) n) ) + ~~ 2 + 2 * n ...( cong (2 +) (sym unfoldDouble) ) + export multRightCancel : (a,b,r : Nat) -> Not (r = 0) -> a*r = b*r -> a = b multRightCancel a b 0 r_nz ar_eq_br = void $ r_nz Refl From b8b4792cd477e386809b9c1b9168bab8c3918ec8 Mon Sep 17 00:00:00 2001 From: Guillaume ALLAIS Date: Sun, 14 Feb 2021 14:18:33 +0000 Subject: [PATCH 11/15] [ new ] Data.Vect.Binary --- libs/contrib/Data/Binary/Digit.idr | 6 +++++ libs/contrib/Data/IMaybe.idr | 23 ++++++++++++++++++++ libs/contrib/Data/Vect/Binary.idr | 35 ++++++++++++++++++++++++++++++ libs/contrib/contrib.ipkg | 10 +++++++++ 4 files changed, 74 insertions(+) create mode 100644 libs/contrib/Data/IMaybe.idr create mode 100644 libs/contrib/Data/Vect/Binary.idr diff --git a/libs/contrib/Data/Binary/Digit.idr b/libs/contrib/Data/Binary/Digit.idr index 20b336fbc5..5c31c7cd07 100644 --- a/libs/contrib/Data/Binary/Digit.idr +++ b/libs/contrib/Data/Binary/Digit.idr @@ -9,6 +9,12 @@ data Digit : Type where O : Digit I : Digit +||| Translation to Bool +public export +isI : Digit -> Bool +isI I = True +isI O = False + public export toNat : Digit -> Nat toNat O = 0 diff --git a/libs/contrib/Data/IMaybe.idr b/libs/contrib/Data/IMaybe.idr new file mode 100644 index 0000000000..4870f65d7d --- /dev/null +++ b/libs/contrib/Data/IMaybe.idr @@ -0,0 +1,23 @@ +||| Version of Maybe indexed by an `isJust' boolean +module Data.IMaybe + +%default total + +public export +data IMaybe : Bool -> Type -> Type where + Just : a -> IMaybe True a + Nothing : IMaybe False a + +public export +fromJust : IMaybe True a -> a +fromJust (Just a) = a + +public export +Functor (IMaybe b) where + map f (Just a) = Just (f a) + map f Nothing = Nothing + +public export +Applicative (IMaybe True) where + pure = Just + Just f <*> Just x = Just (f x) diff --git a/libs/contrib/Data/Vect/Binary.idr b/libs/contrib/Data/Vect/Binary.idr new file mode 100644 index 0000000000..94d3a9972e --- /dev/null +++ b/libs/contrib/Data/Vect/Binary.idr @@ -0,0 +1,35 @@ +||| The content of this file is taken from the paper +||| Heterogeneous Binary Random-access lists + +module Data.Vect.Binary + +import Data.Binary.Digit +import Data.Binary +import Data.IMaybe +import Data.Nat +import Data.Nat.Properties +import Data.Tree.Perfect + +%default total + +public export +data BVect : Nat -> Bin -> Type -> Type where + Nil : BVect n [] a + (::) : IMaybe (isI b) (Tree n a) -> BVect (S n) bs a -> BVect n (b :: bs) a + +public export +data Path : Nat -> Bin -> Type where + Here : Path n -> Path n (I :: bs) + There : Path (S n) bs -> Path n (b :: bs) + +public export +lookup : BVect n bs a -> Path n bs -> a +lookup (hd :: _) (Here p) = lookup (fromJust hd) p +lookup (_ :: tl) (There p) = lookup tl p + +public export +cons : {bs : _} -> Tree n a -> BVect n bs a -> BVect n (suc bs) a +cons t [] = [Just t] +cons {bs = b :: _} t (u :: us) = case b of + I => Nothing :: cons (Node t (fromJust u)) us + O => Just t :: us diff --git a/libs/contrib/contrib.ipkg b/libs/contrib/contrib.ipkg index daa6baa78a..e6e0d229e9 100644 --- a/libs/contrib/contrib.ipkg +++ b/libs/contrib/contrib.ipkg @@ -19,6 +19,9 @@ modules = Control.ANSI, Control.Validation, + Data.Binary.Digit, + Data.Binary, + Data.Bool.Algebra, Data.Bool.Decidable, @@ -29,7 +32,10 @@ modules = Control.ANSI, Data.Fun.Extra, Data.Fun.Graph, + Data.IMaybe, + Data.InductionRecursion.DybjerSetzer, + Data.Int.Order, Data.Late, @@ -81,6 +87,10 @@ modules = Control.ANSI, Data.Telescope.SimpleFun, Data.Telescope.Congruence, + Data.Tree.Perfect, + + Data.Vect.Binary, + Data.Vect.Sort, Data.Void, From 2eeb529dd6a089c0fe82b4bdd1796676cf034c7f Mon Sep 17 00:00:00 2001 From: Guillaume ALLAIS Date: Sun, 14 Feb 2021 14:47:50 +0000 Subject: [PATCH 12/15] [ more ] zero-th index --- libs/contrib/Data/Vect/Binary.idr | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/libs/contrib/Data/Vect/Binary.idr b/libs/contrib/Data/Vect/Binary.idr index 94d3a9972e..4481dca53b 100644 --- a/libs/contrib/Data/Vect/Binary.idr +++ b/libs/contrib/Data/Vect/Binary.idr @@ -7,6 +7,7 @@ import Data.Binary.Digit import Data.Binary import Data.IMaybe import Data.Nat +import Data.Nat.Exponentiation import Data.Nat.Properties import Data.Tree.Perfect @@ -22,6 +23,13 @@ data Path : Nat -> Bin -> Type where Here : Path n -> Path n (I :: bs) There : Path (S n) bs -> Path n (b :: bs) +public export +zero : {bs : Bin} -> {n : Nat} -> Path n (suc bs) +zero {bs} = case bs of + [] => Here (fromNat 0 n (ltePow2 {m = n})) + (O :: bs) => Here (fromNat 0 n (ltePow2 {m = n})) + (I :: bs) => There zero + public export lookup : BVect n bs a -> Path n bs -> a lookup (hd :: _) (Here p) = lookup (fromJust hd) p From 6cb2580de24188639abc5eab2e6455381728e1e2 Mon Sep 17 00:00:00 2001 From: Guillaume ALLAIS Date: Sun, 14 Feb 2021 15:02:17 +0000 Subject: [PATCH 13/15] [ more ] weaken Path --- libs/contrib/Data/Vect/Binary.idr | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/libs/contrib/Data/Vect/Binary.idr b/libs/contrib/Data/Vect/Binary.idr index 4481dca53b..aec1e928df 100644 --- a/libs/contrib/Data/Vect/Binary.idr +++ b/libs/contrib/Data/Vect/Binary.idr @@ -30,6 +30,16 @@ zero {bs} = case bs of (O :: bs) => Here (fromNat 0 n (ltePow2 {m = n})) (I :: bs) => There zero +public export +weaken : {bs : _} -> Path n bs -> Path n (suc bs) +weaken {bs = I :: bs} (Here p) = There $ case bs of + [] => Here (Left p) + (I :: bs) => weaken (Here (Left p)) + (O :: bs) => Here (Left p) +weaken {bs = b :: bs} (There p) = case b of + I => There (weaken p) + O => There p + public export lookup : BVect n bs a -> Path n bs -> a lookup (hd :: _) (Here p) = lookup (fromJust hd) p From 01942bf8438d8284cbbc0e9258d985f0720a411d Mon Sep 17 00:00:00 2001 From: Guillaume ALLAIS Date: Thu, 18 Feb 2021 17:46:46 +0000 Subject: [PATCH 14/15] [ fix ] (^) is usually right-associative --- libs/contrib/Data/Monoid/Exponentiation.idr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/libs/contrib/Data/Monoid/Exponentiation.idr b/libs/contrib/Data/Monoid/Exponentiation.idr index abd4363c5b..009d4ab879 100644 --- a/libs/contrib/Data/Monoid/Exponentiation.idr +++ b/libs/contrib/Data/Monoid/Exponentiation.idr @@ -25,7 +25,7 @@ public export modular : Monoid a => a -> Nat -> a modular v n = modularRec v (halfRec n) -infixl 10 ^ +infixr 10 ^ public export (^) : Num a => a -> Nat -> a (^) = modular @{Multiplicative} From 766596290c65faaccddcc66ccd42dfc8564c21e8 Mon Sep 17 00:00:00 2001 From: Guillaume ALLAIS Date: Thu, 18 Feb 2021 17:47:23 +0000 Subject: [PATCH 15/15] Revert "[ more ] weaken Path" This reverts commit 6cb2580de24188639abc5eab2e6455381728e1e2. --- libs/contrib/Data/Vect/Binary.idr | 10 ---------- 1 file changed, 10 deletions(-) diff --git a/libs/contrib/Data/Vect/Binary.idr b/libs/contrib/Data/Vect/Binary.idr index aec1e928df..4481dca53b 100644 --- a/libs/contrib/Data/Vect/Binary.idr +++ b/libs/contrib/Data/Vect/Binary.idr @@ -30,16 +30,6 @@ zero {bs} = case bs of (O :: bs) => Here (fromNat 0 n (ltePow2 {m = n})) (I :: bs) => There zero -public export -weaken : {bs : _} -> Path n bs -> Path n (suc bs) -weaken {bs = I :: bs} (Here p) = There $ case bs of - [] => Here (Left p) - (I :: bs) => weaken (Here (Left p)) - (O :: bs) => Here (Left p) -weaken {bs = b :: bs} (There p) = case b of - I => There (weaken p) - O => There p - public export lookup : BVect n bs a -> Path n bs -> a lookup (hd :: _) (Here p) = lookup (fromJust hd) p