Use Rekenaar tactics

Given two equavalent terms in `(Nat, 0, +)`, Rekenaar [1] can prove that
the terms are equal. In this proof-of-concept commit, Rekenaar tactics are
applied everywhere they fit.

There was only one location where applying Rekenaar failed. This code is
marked with a `NOTE` comment. However, it's not clear whether this is
due to a bug in Rekenaar or in Idris.

Note that a case can be made that Rekenaar is best suited for solving
more complex tasks. For example, using Rekenaar to replace a single
`plusCommutative` call might be considered overkill by some users.

[1] https://github.com/jdevuyst/rekenaar

data.ipkg

@@ -2,7 +2,7 @@ package data
 
 sourceloc = https://github.com/jdevuyst/idris-data
 
-opts = "--warnreach -p contrib"
+opts = "--warnreach -p contrib -p rekenaar"
 
 sourcedir = src
 modules = Decidable.IntOrder

src/Data/LazyPairingHeap.idr

@@ -1,8 +1,11 @@
 module Data.LazyPairingHeap
 
+import Rekenaar
+
 import Decidable.Order
 
 %default total
+%language ElabReflection
 
 mutual
   public export
@@ -34,14 +37,11 @@ mutual
       -> .{ltePrf : to (findMin h1) (findMin h2)}
       -> (ret : LazyPairingHeap ((S cnt1) + (S cnt2)) constraint ** findMin ret = findMin h1)
   link {cnt1} {cnt2} {ltePrf} h1@(Tree x Empty r) h2
-    = rewrite plusCommutative cnt1 (S cnt2) in
+    = rewrite the (cnt1 + (S cnt2) = (S cnt2) + cnt1) (%runElab natPlusRefl) in
       (Tree (findMin h1) h2 r ** Refl)
   link {constraint} {ltePrf} h1 {cnt2} h2 with (h1)
     | Tree {leftFits} {rightFits} {leftCnt} {rightCnt} x l r
-      = rewrite sym $ plusAssociative leftCnt rightCnt (S cnt2) in
-        rewrite plusCommutative rightCnt (S cnt2) in
-        rewrite plusAssociative leftCnt (S cnt2) rightCnt in
-        rewrite plusCommutative leftCnt (S cnt2) in
+      = rewrite the (plus (plus leftCnt rightCnt) (S cnt2) = S (plus (plus cnt2 leftCnt) rightCnt)) (%runElab natPlusRefl) in
         rewrite sym $ xFindMin in
         let (merged ** fitsPrf) = merge' {lbound = findMin h1}
                                          {fits1 = rewrite xFindMin in ltePrf}
@@ -64,12 +64,13 @@ mutual
         -> .{lbound : ty} -> .{fits1 : Fits lbound h1} -> .{fits2 : Fits lbound h2}
         -> (ret : LazyPairingHeap (cnt1 + cnt2) constraint ** Fits lbound ret)
   merge' {fits2} Empty h = (h ** fits2)
-  merge' {cnt1} {fits1} h Empty = rewrite plusZeroRightNeutral cnt1 in (h ** fits1)
+  merge' {cnt1} {fits1} h Empty = rewrite the (cnt1 + 0 = cnt1) (%runElab natPlusRefl) in (h ** fits1)
   merge' {to} {fits1} {fits2} {cnt1 = S n} {cnt2 = S m} h1 h2 with (order {to} (findMin h1) (findMin h2))
     | Left ltePrf = let (ret ** eqPrf) = assert_total $ link {ltePrf} h1 h2 in
                     (ret ** rewrite eqPrf in fits1)
     | Right ltePrf = rewrite plusCommutative n (S m) in
                      rewrite plusSuccRightSucc m n in
+                     -- NOTE: this failed to compile after refactoring to use Rekenaar
                      let (ret ** eqPrf) = assert_total $ link {ltePrf} h2 h1 in
                      (ret ** rewrite eqPrf in fits2)
 
@@ -79,7 +80,7 @@ merge : .{constraint : Ordered ty to}
      -> {cnt2 : Nat} -> LazyPairingHeap cnt2 constraint
      -> LazyPairingHeap (cnt1 + cnt2) constraint
 merge Empty h = h
-merge {cnt1} h Empty = rewrite plusZeroRightNeutral cnt1 in h
+merge {cnt1} h Empty = rewrite the (cnt1 + 0 = cnt1) (%runElab natPlusRefl) in h
 merge {constraint} {ty} {to} {cnt1 = S n} {cnt2 = S m} h1 h2
   = let (lbound ** (fits1, fits2)) = proofs in
         fst $ merge' {lbound} {fits1} {fits2} h1 h2
@@ -99,8 +100,7 @@ singleton x = Tree x Empty Empty
 
 export
 insert : .{constraint : Ordered ty to} -> {cnt : Nat} -> LazyPairingHeap cnt constraint -> ty -> LazyPairingHeap (S cnt) constraint
-insert {cnt} h x = rewrite sym $ plusZeroRightNeutral cnt in
-                   rewrite plusSuccRightSucc cnt Z in
+insert {cnt} h x = rewrite the (S cnt = cnt + 1) (%runElab natPlusRefl) in
                    merge h (singleton x)
 
 namespace CountedPairingHeap

src/Data/LeftistHeap.idr

@@ -1,8 +1,11 @@
 module Data.LeftistHeap
 
+import Rekenaar
+
 import Decidable.Order
 
 %default total
+%language ElabReflection
 
 mutual
   export
@@ -48,7 +51,7 @@ makeFit : .{constraint : Ordered a rel}
        -> .{auto relPrf : rel fitsValue value}
        -> Subset (Heap constraint (S $ count1 + count2)) (Fits fitsValue)
 makeFit {count1} {count2} {relPrf} fitsValue value h1 h2 with (order {to = LTE} (rank h1) (rank h2))
-  | (Left _) = rewrite plusCommutative count1 count2 in
+  | (Left _) = rewrite the (count1 + count2 = count2 + count1) (%runElab natPlusRefl) in
                Element (Node _ value h2 h1) relPrf
   | (Right _) = Element (Node _ value h1 h2) relPrf
 
@@ -63,18 +66,20 @@ mergeHelper : .{constraint : Ordered a rel}
            -> .{auto fits2 : Fits value h2}
            -> Subset (Heap constraint (count1 + count2)) (Fits value)
 mergeHelper Empty Empty = Element Empty ()
-mergeHelper {fits1} h@(Node {countLeft} {countRight} n _ _ _) Empty = rewrite plusZeroRightNeutral (countLeft + countRight) in Element h fits1
+mergeHelper {fits1} h@(Node {countLeft} {countRight} n _ _ _) Empty = rewrite the ((countLeft + countRight) + 0 = countLeft + countRight) (%runElab natPlusRefl) in Element h fits1
 mergeHelper {fits2} Empty h@(Node {countLeft} {countRight} n _ _ _) = Element h fits2
 mergeHelper {value} {rel}
             (Node {countLeft = countLeft1} {countRight = countRight1} _ value1 left1 right1)
             (Node {countLeft = countLeft2} {countRight = countRight2} _ value2 left2 right2)
   = case order {to = rel} value1 value2 of
-    Left orderPrf => rewrite sym $ plusAssociative countLeft1 countRight1 (S $ countLeft2 + countRight2) in
+    Left orderPrf => rewrite the (S (plus (plus countLeft1 countRight1) (S (plus countLeft2 countRight2)))
+                                 = S (countLeft1 + (countRight1 + S (countLeft2 + countRight2))))
+                             (%runElab natPlusRefl) in
                      let (Element mergedHeap fitsMergedHeap) = mergeHelper {value = value1} right1 (Node _ value2 left2 right2) in
                      makeFit value value1 left1 mergedHeap
-    Right orderPrf => rewrite sym $ plusSuccRightSucc (countLeft1 + countRight1) (countLeft2 + countRight2) in
-                      rewrite plusCommutative countLeft2 countRight2 in
-                      rewrite plusAssociative (countLeft1 + countRight1) countRight2 countLeft2 in
+    Right orderPrf => rewrite the (S (plus (plus countLeft1 countRight1) (S (plus countLeft2 countRight2)))
+                                  = S (S (countLeft1 + countRight1) + countRight2 + countLeft2))
+                              (%runElab natPlusRefl) in
                       let (Element mergedHeap fitsMergedHeap) = mergeHelper {value = value2} (Node _ value1 left1 right1) right2 in
                       makeFit value value2 mergedHeap left2
 
@@ -84,7 +89,7 @@ merge : .{constraint : Ordered a rel}
      -> (h1 : Heap constraint count1) -> (h2 : Heap constraint count2)
      -> Heap constraint (count1 + count2)
 merge Empty Empty = Empty
-merge {count1} h Empty = rewrite plusZeroRightNeutral count1 in h
+merge {count1} h Empty = rewrite the (count1 + 0 = count1) (%runElab natPlusRefl) in h
 merge Empty h = h
 merge h1@(Node _ _ _ _) h2@(Node _ _ _ _)
   = assert_total $ case order {to = rel} (findMin h1) (findMin h2) of

src/Data/MergeList.idr

@@ -1,9 +1,12 @@
 module Data.MergeList
 
+import Rekenaar
+
 import Decidable.Order
 import Data.OrderedVect
 
 %default total
+%language ElabReflection
 
 export
 data MergeList : (rank : Nat) -> (cnt : Nat) -> (constraint : Ordered ty to) -> Type where
@@ -26,12 +29,11 @@ insertVect : {constraint : Ordered ty to}
 insertVect {n} {constraint} {cnt=Z} Nil v
   = rewrite rewriteType in v :: Nil
       where rewriteType : MergeList n n constraint = MergeList n (n + 0) constraint
-            rewriteType = rewrite sym $ plusZeroRightNeutral n in Refl
-insertVect {n} {cnt} (Skip next) v = rewrite plusCommutative cnt n in
+            rewriteType = rewrite the (n = n + 0) (%runElab natPlusRefl) in Refl
+insertVect {n} {cnt} (Skip next) v = rewrite the (cnt + n = n + cnt) (%runElab natPlusRefl) in
                                      v :: next
 insertVect {n} ((::) v next {cnt}) v'
-  = rewrite sym $ plusCommutative cnt n in
-    rewrite sym $ plusAssociative cnt n n in
+  = rewrite the ((n + cnt) + n = cnt + (n + n)) (%runElab natPlusRefl) in
     Skip $ insertVect next (merge n v n v')
 
 export
@@ -68,4 +70,4 @@ namespace CountedMergeList
 
   export
   insert : .{constraint : Ordered ty to} -> CountedMergeList 1 constraint -> ty -> CountedMergeList 1 constraint
-  insert (cnt ** xs) x = (cnt + 1 ** insert xs x)
+  insert (cnt ** xs) x = (cnt + 1 ** insert xs x)

src/Data/OrderedVect.idr

@@ -1,8 +1,11 @@
 module Data.OrderedVect
 
+import Rekenaar
+
 import Decidable.Order
 
 %default total
+%language ElabReflection
 
 mutual
   public export
@@ -42,27 +45,23 @@ mutual
   merge' {to} [x] [y] = case order {to} x y of
                         Left prf => ([x, y] ** Left (reflexive x))
                         Right prf => ([y, x] ** Right (reflexive y))
-  merge' {m} [x] (y :: ys) = rewrite sym $ plusZeroRightNeutral m in
-                             rewrite plusSuccRightSucc m Z in
+  merge' {m} [x] (y :: ys) = rewrite the (S m = m + 1) (%runElab natPlusRefl) in
                              case assert_total $ merge' (y :: ys) [x] of
                              (ref ** Left prf) => (ref ** Right prf)
                              (ref ** Right prf) => (ref ** Left prf)
   merge' {n = S cntX} (x :: xs) [y]
     = case order {to} x y of
       Left prf => case mergeHelper xs [y] x of
                   (zs ** fitsPrf) => (zs ** Left fitsPrf)
-      Right prf => rewrite sym $ plusSuccRightSucc cntX Z in
-                   rewrite plusZeroRightNeutral cntX in
+      Right prf => rewrite the (cntX + 1 = S cntX) (%runElab natPlusRefl) in
                    ((y :: x :: xs) ** Right (reflexive y))
   merge' ((::) {n = S cntX} x (x' :: xs'))
         ((::) {n = S cntY} y (y' :: ys'))
     = case order {to} x y of
       Left prf => case mergeHelper (x' :: xs') (y :: y' :: ys') x of
                   (zs ** fitsPrf) => (zs ** Left fitsPrf)
       Right prf => case mergeHelper (y' :: ys') (x :: x' :: xs') y of
-                   (zs ** fitsPrf) => rewrite plusCommutative cntX (S $ S $ cntY) in
-                                      rewrite plusSuccRightSucc (S $ S cntY) cntX in
-                                      rewrite plusSuccRightSucc (S cntY) (S cntX) in
+                   (zs ** fitsPrf) => rewrite the (cntX + S (S cntY) = cntY + S (S cntX)) (%runElab natPlusRefl) in
                                       (zs ** Right fitsPrf)
   mergeHelper : .{constraint : Ordered ty to}
              -> {n : Nat}
@@ -88,7 +87,7 @@ merge : {constraint : Ordered ty to}
      -> OrderedVect m constraint
      -> OrderedVect (n + m) constraint
 merge Z     [] Z     [] = Nil
-merge n     v1 Z     [] = rewrite plusZeroRightNeutral n in v1
+merge n     v1 Z     [] = rewrite the (n + 0 = n) (%runElab natPlusRefl) in v1
 merge Z     [] _     v2 = v2
 merge (S _) v1 (S _) v2 = fst $ merge' v1 v2
 

src/Data/Queue.idr

@@ -1,10 +1,13 @@
 module Data.Queue
 
+import Rekenaar
+
 import Data.Vect
 import Data.VectRankedElem
 import Decidable.Order
 
 %default total
+%language ElabReflection
 
 export
 data Queue : (size : Nat) -> (ty : Type) -> Type where
@@ -38,7 +41,7 @@ lteAddRightLemma : LTE r c -> LTE r (l + c)
 lteAddRightLemma {l} {r} {c} smaller
   = lteTransitive smaller cLTElc
     where cLTElc : LTE c (l + c)
-          cLTElc = rewrite plusCommutative l c in
+          cLTElc = rewrite the (l + c = c + l) (%runElab natPlusRefl) in
                    lteAddRight {m = l} c
 
 minusPlusEqualsPlusMinus : (l, c, r: Nat) -> LTE r c -> LTE r (l + c) -> (l + c) - r = l + (c - r)
@@ -48,7 +51,7 @@ minusPlusEqualsPlusMinus (S _) (S _) Z _ _ = Refl
 minusPlusEqualsPlusMinus _ Z (S _) _ _ impossible
 minusPlusEqualsPlusMinus l (S c) (S r) smaller _
   = let smaller' = fromLteSucc smaller in
-    rewrite sym $ plusSuccRightSucc l c in
+    rewrite the (l + S c = S (l + c)) (%runElab natPlusRefl) in
     minusPlusEqualsPlusMinus l c r smaller' (lteAddRightLemma smaller')
 
 make_ : {n : Nat}
@@ -62,7 +65,7 @@ make_ {n} f {m} r with (order {to = LTE} m n)
   | Left _ = (MkQueue f r ** (FrontElem, BackElem))
   | Right _ = let (reversed ** rProj) = rev_ r
                   (f' ** (fProj, reversedProj)) = f `concat_` reversed in
-              rewrite sym $ plusZeroRightNeutral (n + m) in
+              rewrite the (n + m = n + m + 0) (%runElab natPlusRefl) in
               (MkQueue f' [] ** (FrontElem . fProj,
                                  rewrite plusZeroRightNeutral (n + m) in
                                  FrontElem . (proj $ reversedProj . rProj)))
@@ -81,7 +84,7 @@ snoc_ : (q : Queue size ty) -> (x : ty)
      -> (ret : Queue (S size) ty
          ** ({x : ty} -> {idx : Nat} -> RankedElem x q idx -> RankedElem x ret idx,
              RankedElem x ret size))
-snoc_ (MkQueue {n} f {m} r) x = rewrite plusSuccRightSucc n m in
+snoc_ (MkQueue {n} f {m} r) x = rewrite the (S (n + m) = n + S m) (%runElab natPlusRefl) in
                                 let (ret ** (fProj, rProj)) = make_ f (x::r) in
                                 (ret ** ((\el => case el of
                                                  (FrontElem el) => fProj el
@@ -93,7 +96,7 @@ snoc_ (MkQueue {n} f {m} r) x = rewrite plusSuccRightSucc n m in
                                 where lemma : (l, c, r : Nat) -> l + S c `minus` S r = l + c `minus` r
                                       lemma Z Z _ = Refl
                                       lemma Z (S _) _ = Refl
-                                      lemma (S l) c r = rewrite plusSuccRightSucc l c in Refl
+                                      lemma (S l) c r = rewrite the (S (l + c) = l + S c) (%runElab natPlusRefl) in Refl
 
 export
 snoc : Queue size ty -> ty -> Queue (S size) ty