From 5e11433c9f2a1cd5c6a8269e70ac8a27ac14fe65 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Tue, 15 Nov 2022 15:44:49 +0100
Subject: [PATCH] bit mask OPE stuff

---
 lib/Quox/NatExtra.idr   | 101 +++++---
 lib/Quox/OPE/Comp.idr   | 180 +++++++++-----
 lib/Quox/OPE/Cover.idr  |  86 ++++++-
 lib/Quox/OPE/Length.idr |  10 +
 lib/Quox/OPE/Split.idr  |  26 +-
 lib/Quox/OPE/Sub.idr    | 525 ++++++++++++++++++++++++++--------------
 6 files changed, 638 insertions(+), 290 deletions(-)

diff --git a/lib/Quox/NatExtra.idr b/lib/Quox/NatExtra.idr
index 343fcf3..3e4d4a6 100644
--- a/lib/Quox/NatExtra.idr
+++ b/lib/Quox/NatExtra.idr
@@ -84,58 +84,85 @@ modNatViaIntegerNZ m n _ = assert_total modNatViaInteger m n
 
 
 public export
-data Parity = Even | Odd
-
-public export
-data ViewLsb : Nat -> Parity -> Type where
-  Lsb0 : (n : Nat) -> ViewLsb    (2 * n)  Even
-  Lsb1 : (n : Nat) -> ViewLsb (S (2 * n)) Odd
+data ViewLsb : Nat -> Type where
+  Lsb0 : (n : Nat) -> (0 eq : n' =    2 * n)  -> ViewLsb n'
+  Lsb1 : (n : Nat) -> (0 eq : n' = S (2 * n)) -> ViewLsb n'
 %name ViewLsb p, q
 
-export
-fromLsb0 : ViewLsb n Even -> Subset Nat (\n' => n = 2 * n')
-fromLsb0 (Lsb0 n') = Element n' Refl
+public export data IsLsb0 : ViewLsb n -> Type where ItIsLsb0 : IsLsb0 (Lsb0 n eq)
+public export data IsLsb1 : ViewLsb n -> Type where ItIsLsb1 : IsLsb1 (Lsb1 n eq)
 
 export
-fromLsb1 : ViewLsb n Odd -> Subset Nat (\n' => n = S (2 * n'))
-fromLsb1 (Lsb1 n') = Element n' Refl
-
-
-private
-viewLsb' : (m, d : Nat) -> (0 _ : m `LT` 2) -> Exists $ ViewLsb (m + 2 * d)
-viewLsb' 0 d p = Evidence Even (Lsb0 d)
-viewLsb' 1 d p = Evidence Odd  (Lsb1 d)
-viewLsb' (S (S _)) _ (LTESucc p) = void $ absurd p
-
-export
-viewLsb : (n : Nat) -> Exists $ ViewLsb n
-viewLsb n =
-  let 0 nz = the (NonZero 2) %search in
-  rewrite DivisionTheorem n 2 nz nz in
-  rewrite multCommutative (divNatNZ n 2 nz) 2 in
-  viewLsb' (modNatNZ n 2 nz) (divNatNZ n 2 nz) (boundModNatNZ n 2 nz)
-
-
-export
-0 lsbMutex' : n = (2 * a) -> n = S (2 * b) -> Void
-lsbMutex' ev od {n = 0} impossible
-lsbMutex' ev od {n = 1} {a = S a} {b = 0} =
+0 lsbMutex : n = (2 * a) -> n = S (2 * b) -> Void
+lsbMutex ev od {n = 0} impossible
+lsbMutex ev od {n = 1} {a = S a} {b = 0} =
   let ev = injective ev in
   let s  = sym $ plusSuccRightSucc a (a + 0) in
   absurd $ trans ev s
-lsbMutex' ev od {n = S (S n)} {a = S a} {b = S b} =
+lsbMutex ev od {n = S (S n)} {a = S a} {b = S b} =
   let ev = injective $
            trans (injective ev) (sym $ plusSuccRightSucc a (a + 0)) in
   let od = trans (injective $ injective od)
                  (sym $ plusSuccRightSucc b (b + 0)) in
-  lsbMutex' ev od
+  lsbMutex ev od
+
+public export %hint
+doubleIsLsb0 : (p : ViewLsb (2 * n)) -> IsLsb0 p
+doubleIsLsb0 (Lsb0 k eq) = ItIsLsb0
+doubleIsLsb0 (Lsb1 k eq) = void $ absurd $ lsbMutex Refl eq
+
+public export %hint
+sDoubleIsLsb1 : (p : ViewLsb (S (2 * n))) -> IsLsb1 p
+sDoubleIsLsb1 (Lsb1 k eq) = ItIsLsb1
+sDoubleIsLsb1 (Lsb0 k eq) = void $ absurd $ lsbMutex Refl (sym eq)
+
 
 export
-0 lsbMutex : ViewLsb n Even -> ViewLsb n Odd -> Void
-lsbMutex p q = lsbMutex' (fromLsb0 p).snd (fromLsb1 q).snd
+fromLsb0 : (p : ViewLsb n) -> (0 _ : IsLsb0 p) =>
+           Subset Nat (\n' => n = 2 * n')
+fromLsb0 (Lsb0 n' eq) @{ItIsLsb0} = Element n' eq
 
 export
-doubleInj : {m, n : Nat} -> 2 * m = 2 * n -> m = n
+fromLsb1 : (p : ViewLsb n) -> (0 _ : IsLsb1 p) =>
+           Subset Nat (\n' => n = S (2 * n'))
+fromLsb1 (Lsb1 n' eq) @{ItIsLsb1} = Element n' eq
+
+
+private
+viewLsb' : (m, d : Nat) -> (0 _ : m `LT` 2) -> ViewLsb (m + 2 * d)
+viewLsb' 0 d p = Lsb0 d Refl
+viewLsb' 1 d p = Lsb1 d Refl
+viewLsb' (S (S _)) _ (LTESucc p) = void $ absurd p
+
+export
+viewLsb : (n : Nat) -> ViewLsb n
+viewLsb n =
+  let 0 nz : NonZero 2 = %search in
+  rewrite DivisionTheorem n 2 nz nz in
+  rewrite multCommutative (divNatNZ n 2 nz) 2 in
+  viewLsb' (modNatNZ n 2 nz) (divNatNZ n 2 nz) (boundModNatNZ n 2 nz)
+
+export
+0 doubleInj : {m, n : Nat} -> 2 * m = 2 * n -> m = n
 doubleInj eq =
   multRightCancel m n 2 %search $
     trans (multCommutative m 2) $ trans eq (multCommutative 2 n)
+
+export
+0 sDoubleInj : {m, n : Nat} -> S (2 * m) = S (2 * n) -> m = n
+sDoubleInj eq = doubleInj $ injective eq
+
+
+export
+0 lsbOdd : (n : Nat) -> (eq ** viewLsb (S (2 * n)) = Lsb1 n eq)
+lsbOdd n with (viewLsb (S (2 * n)))
+  _ | Lsb0 _  eq = void $ absurd $ lsbMutex Refl (sym eq)
+  _ | Lsb1 n' eq with (sDoubleInj eq)
+    lsbOdd n | (Lsb1 n eq) | Refl = (eq ** Refl)
+
+export
+0 lsbEven : (n : Nat) -> (eq ** viewLsb (2 * n) = Lsb0 n eq)
+lsbEven n with (viewLsb (2 * n))
+  _ | Lsb1 _  eq = void $ absurd $ lsbMutex Refl eq
+  _ | Lsb0 n' eq with (doubleInj eq)
+    lsbEven n | Lsb0 n eq | Refl = (eq ** Refl)
diff --git a/lib/Quox/OPE/Comp.idr b/lib/Quox/OPE/Comp.idr
index c2e8a74..90e82e4 100644
--- a/lib/Quox/OPE/Comp.idr
+++ b/lib/Quox/OPE/Comp.idr
@@ -5,67 +5,124 @@ import Quox.OPE.Length
 import Quox.OPE.Sub
 import Data.DPair
 
+import Control.Function
+import Data.Nat
+
 %default total
 
 
 public export
-data Comp : ys `Sub` zs -> xs `Sub` ys -> xs `Sub` zs -> Type where
-  CEE : Comp End End End
-  CKK : Comp p q pq -> Comp (Keep p) (Keep q) (Keep pq)
-  CKD : Comp p q pq -> Comp (Keep p) (Drop q) (Drop pq)
-  CD0 : Comp p q pq -> Comp (Drop p) q        (Drop pq)
-
-export
-comp : (p : ys `Sub` zs) -> (q : xs `Sub` ys) -> Comp p q (p . q)
-comp End      End      = CEE
-comp (Keep p) (Keep q) = CKK (comp p q)
-comp (Keep p) (Drop q) = CKD (comp p q)
-comp (Drop p) q        = CD0 (comp p q)
-
-export
-0 compOk : Comp p q r -> r = (p . q)
-compOk CEE     = Refl
-compOk (CKK z) = cong Keep $ compOk z
-compOk (CKD z) = cong Drop $ compOk z
-compOk (CD0 z) = cong Drop $ compOk z
-
-export
-compZero : (sx : Length xs) => (sy : Length ys) =>
-           (p : xs `Sub` ys) -> Comp p (Sub.zero @{sx}) (Sub.zero @{sy})
-compZero {sx = Z,   sy = Z}   End      = CEE
-compZero {sx = S _, sy = S _} (Keep p) = CKD (compZero p)
-compZero           {sy = S _} (Drop p) = CD0 (compZero p)
-
-export
-compIdLeft : (sy : Length ys) =>
-             (p : xs `Sub` ys) -> Comp (Sub.id @{sy}) p p
-compIdLeft {sy = Z}   End      = CEE
-compIdLeft {sy = S _} (Keep p) = CKK (compIdLeft p)
-compIdLeft {sy = S _} (Drop p) = CKD (compIdLeft p)
-
-export
-compIdRight : (sx : Length xs) =>
-              (p : xs `Sub` ys) -> Comp p (Sub.id @{sx}) p
-compIdRight {sx = Z}   End      = CEE
-compIdRight {sx = S _} (Keep p) = CKK (compIdRight p)
-compIdRight            (Drop p) = CD0 (compIdRight p)
-
-
-export
-0 compAssoc : (p : ys `Sub` zs) -> (q : xs `Sub` ys) -> (r : ws `Sub` xs) ->
-              p . (q . r) = (p . q) . r
-compAssoc End      End      End      = Refl
-compAssoc (Keep p) (Keep q) (Keep r) = cong Keep $ compAssoc p q r
-compAssoc (Keep p) (Keep q) (Drop r) = cong Drop $ compAssoc p q r
-compAssoc (Keep p) (Drop q) r        = cong Drop $ compAssoc p q r
-compAssoc (Drop p) q        r        = cong Drop $ compAssoc p q r
-compAssoc End (Drop _) _ impossible
-
+data Comp' : ys `Sub'` zs -> xs `Sub'` ys -> xs `Sub'` zs -> Type where
+  CEE : Comp' End End End
+  CKK : Comp' p q pq -> Comp' (Keep p) (Keep q) (Keep pq)
+  CKD : Comp' p q pq -> Comp' (Keep p) (Drop q) (Drop pq)
+  CD0 : Comp' p q pq -> Comp' (Drop p) q        (Drop pq)
 
 public export
-Subscope : Scope a -> Type
+record Comp {a : Type} {xs, ys, zs : Scope a}
+            (p : ys `Sub` zs) (q : xs `Sub` ys) (pq : xs `Sub` zs) where
+  constructor MkComp
+  0 comp : Comp' p.lte q.lte pq.lte
+
+
+export
+compPrf' : (p : ys `Sub'` zs) -> (q : xs `Sub'` ys) -> Comp' p q (p . q)
+compPrf' End      End      = CEE
+compPrf' (Keep p) (Keep q) = CKK $ compPrf' p q
+compPrf' (Keep p) (Drop q) = CKD $ compPrf' p q
+compPrf' (Drop p) q        = CD0 $ compPrf' p q
+
+export
+0 compOk' : Comp' p q r -> r = (p . q)
+compOk' CEE     = Refl
+compOk' (CKK z) = cong Keep $ compOk' z
+compOk' (CKD z) = cong Drop $ compOk' z
+compOk' (CD0 z) = cong Drop $ compOk' z
+
+
+export %inline
+compPrf : (0 sy : Length ys) => (0 sz : Length zs) =>
+       (p : ys `Sub` zs) -> (q : xs `Sub` ys) ->
+       Comp p q ((p . q) @{sy} @{sz})
+compPrf p q = MkComp $
+  replace {p = Comp' p.lte q.lte} (sym $ compLte p q) $
+    compPrf' p.lte q.lte
+
+
+export
+compZero' : (sx : Length xs) => (sy : Length ys) =>
+            (p : xs `Sub'` ys) -> Comp' p (zero' @{sx}) (zero' @{sy})
+compZero' {sx = Z,   sy = Z}   End      = CEE
+compZero' {sx = S _, sy = S _} (Keep p) = CKD (compZero' p)
+compZero'           {sy = S _} (Drop p) = CD0 (compZero' p)
+
+export %inline
+compZero : (sx : Length xs) => (sy : Length ys) =>
+           (p : xs `Sub` ys) -> Comp p (zero @{sx}) (zero @{sy})
+compZero p = MkComp $
+  rewrite zeroLte {sx} in
+  rewrite zeroLte {sx = sy} in
+  compZero' {}
+
+export
+compIdLeft' : (sy : Length ys) =>
+              (p : xs `Sub'` ys) -> Comp' (refl' @{sy}) p p
+compIdLeft' {sy = Z}   End      = CEE
+compIdLeft' {sy = S _} (Keep p) = CKK (compIdLeft' p)
+compIdLeft' {sy = S _} (Drop p) = CKD (compIdLeft' p)
+
+export %inline
+compIdLeft : (sy : Length ys) =>
+             (p : xs `Sub` ys) -> Comp (refl @{sy}) p p
+compIdLeft {sy} p = MkComp $
+  rewrite reflLte {sx = sy} in compIdLeft' {}
+
+export
+compIdRight' : (sx : Length xs) =>
+               (p : xs `Sub'` ys) -> Comp' p (refl' @{sx}) p
+compIdRight' {sx = Z}   End      = CEE
+compIdRight' {sx = S _} (Keep p) = CKK (compIdRight' p)
+compIdRight'            (Drop p) = CD0 (compIdRight' p)
+
+export %inline
+compIdRight : (sx : Length xs) =>
+              (p : xs `Sub` ys) -> Comp p (refl @{sx}) p
+compIdRight {sx} p = MkComp $ rewrite reflLte {sx} in compIdRight' {}
+
+export
+0 compAssoc' : (p : ys `Sub'` zs) -> (q : xs `Sub'` ys) -> (r : ws `Sub'` xs) ->
+               p . (q . r) = (p . q) . r
+compAssoc' End      End      End      = Refl
+compAssoc' (Keep p) (Keep q) (Keep r) = cong Keep $ compAssoc' p q r
+compAssoc' (Keep p) (Keep q) (Drop r) = cong Drop $ compAssoc' p q r
+compAssoc' (Keep p) (Drop q) r        = cong Drop $ compAssoc' p q r
+compAssoc' (Drop p) q        r        = cong Drop $ compAssoc' p q r
+compAssoc' End (Drop _) _ impossible
+
+export %inline
+0 compAssoc : (sx : Length xs) => (sy : Length ys) => (sz : Length zs) =>
+              (p : ys `Sub` zs) -> (q : xs `Sub` ys) -> (r : ws `Sub` xs) ->
+              comp @{sy} @{sz} p (comp @{sx} @{sy} q r) =
+                comp @{sx} @{sz} (comp @{sy} @{sz} p q) r
+compAssoc p q r = lteEq $
+  trans (transLte {}) $
+  trans (cong (p.lte .) (transLte {})) $
+  sym $
+  trans (transLte {}) $
+  trans (cong (. r.lte) (transLte {})) $
+  sym $ compAssoc' {}
+
+public export
+0 Subscope : Scope a -> Type
 Subscope ys = Exists (`Sub` ys)
 
+public export
+record SubMap' {a : Type} {xs, ys, zs : Scope a}
+               (p : xs `Sub'` zs) (q : ys `Sub'` zs) where
+  constructor SM'
+  thin : xs `Sub'` ys
+  0 comp : Comp' q thin p
+
 public export
 record SubMap {a : Type} {xs, ys, zs : Scope a}
               (p : xs `Sub` zs) (q : ys `Sub` zs) where
@@ -73,10 +130,23 @@ record SubMap {a : Type} {xs, ys, zs : Scope a}
   thin : xs `Sub` ys
   0 comp : Comp q thin p
 
-parameters (p : xs `Sub` ys)
+export
+0 submap' : SubMap p q -> SubMap' p.lte q.lte
+submap' (SM thin comp) = SM' {thin = thin.lte, comp = comp.comp}
+
+parameters (p : xs `Sub'` ys)
+  export
+  subId' : SubMap' p p
+  subId' = SM' refl' (compIdRight' p)
+
+  export
+  subZero' : SubMap' Sub.zero' p
+  subZero' = SM' zero' (compZero' p)
+
+parameters {auto sx : Length xs} (p : xs `Sub` ys)
   export
   subId : SubMap p p
-  subId = SM id (compIdRight p)
+  subId = SM refl (compIdRight p)
 
   export
   subZero : SubMap Sub.zero p
diff --git a/lib/Quox/OPE/Cover.idr b/lib/Quox/OPE/Cover.idr
index 63e5acb..51b660f 100644
--- a/lib/Quox/OPE/Cover.idr
+++ b/lib/Quox/OPE/Cover.idr
@@ -8,17 +8,83 @@ import Quox.OPE.Sub
 
 
 public export
-data Cover_ : (overlap : Bool) -> xs `Sub` zs -> ys `Sub` zs -> Type where
-  CE : Cover_ ov End End
-  CL : Cover_ ov p q -> Cover_ ov   (Keep p) (Drop q)
-  CR : Cover_ ov p q -> Cover_ ov   (Drop p) (Keep q)
-  C2 : Cover_ ov p q -> Cover_ True (Keep p) (Keep q)
+data Cover'_ : (overlap : Bool) -> xs `Sub'` zs -> ys `Sub'` zs -> Type where
+  CE : Cover'_ ov End End
+  CL : Cover'_ ov p q -> Cover'_ ov   (Keep p) (Drop q)
+  CR : Cover'_ ov p q -> Cover'_ ov   (Drop p) (Keep q)
+  C2 : Cover'_ ov p q -> Cover'_ True (Keep p) (Keep q)
+
+parameters (p : xs `Sub'` zs) (q : ys `Sub'` zs)
+  public export
+  0 Cover' : Type
+  Cover' = Cover'_ True p q
+
+  public export
+  0 Partition' : Type
+  Partition' = Cover'_ False p q
+
 
 public export
-Cover : xs `Sub` zs -> ys `Sub` zs -> Type
-Cover = Cover_ True
+record Cover_ {a : Type} {xs, ys, zs : Scope a} (overlap : Bool)
+              (p : xs `Sub` zs) (q : ys `Sub` zs) where
+  constructor MkCover
+  0 cover : Cover'_ overlap p.lte q.lte
 
-public export
-Partition : xs `Sub` zs -> ys `Sub` zs -> Type
-Partition = Cover_ False
+parameters (p : xs `Sub` zs) (q : ys `Sub` zs)
+  public export
+  0 Cover : Type
+  Cover = Cover_ True p q
 
+  public export
+  0 Partition : Type
+  Partition = Cover_ False p q
+
+
+private %inline
+covCast' : {0 p, p' : xs `Sub'` zs} -> {0 q, q' : ys `Sub'` zs} ->
+           (0 pe : p = p') -> (0 qe : q = q') ->
+           Cover'_ overlap p' q' -> Cover'_ overlap p q
+covCast' pe qe c = replace {p = id} (sym $ cong2 (Cover'_ overlap) pe qe) c
+
+
+parameters {0 overlap : Bool} {0 p : xs `Sub` zs} {0 q : ys `Sub` zs}
+  export %inline
+  left : Cover_ overlap p q -> Cover_ overlap (keep p) (drop q)
+  left (MkCover cover) = MkCover $ covCast' (keepLte p) (dropLte q) $ CL cover
+
+  export %inline
+  right : Cover_ overlap p q -> Cover_ overlap (drop p) (keep q)
+  right (MkCover cover) = MkCover $ covCast' (dropLte p) (keepLte q) $ CR cover
+
+  export %inline
+  both : Cover_ overlap p q -> Cover (keep p) (keep q)
+  both (MkCover cover) = MkCover $ covCast' (keepLte p) (keepLte q) $ C2 cover
+
+
+export
+allLeft' : (sx : Length xs) => Partition' (refl' @{sx}) (zero' @{sx})
+allLeft' {sx = Z}   = CE
+allLeft' {sx = S s} = CL allLeft'
+
+export
+allRight' : (sx : Length xs) => Partition' (zero' @{sx}) (refl' @{sx})
+allRight' {sx = Z}   = CE
+allRight' {sx = S s} = CR allRight'
+
+export
+both' : (sx : Length xs) => Cover' (refl' @{sx}) (refl' @{sx})
+both' {sx = Z}   = CE
+both' {sx = S s} = C2 both'
+
+
+export %inline
+allLeft : (sx : Length xs) => Partition (refl @{sx}) (zero @{sx})
+allLeft = MkCover $ rewrite reflLte {sx} in rewrite zeroLte {sx} in allLeft'
+
+export %inline
+allRight : (sx : Length xs) => Partition (zero @{sx}) (refl @{sx})
+allRight = MkCover $ rewrite reflLte {sx} in rewrite zeroLte {sx} in allRight'
+
+export %inline
+allBoth : (sx : Length xs) => Cover (refl @{sx}) (refl @{sx})
+allBoth = MkCover $ rewrite reflLte {sx} in both'
diff --git a/lib/Quox/OPE/Length.idr b/lib/Quox/OPE/Length.idr
index 776cefe..b3da203 100644
--- a/lib/Quox/OPE/Length.idr
+++ b/lib/Quox/OPE/Length.idr
@@ -27,3 +27,13 @@ public export %hint
 toLength : (xs : Scope a) -> Length xs
 toLength [<]       = Z
 toLength (sx :< x) = S (toLength sx)
+
+public export %hint
+lengthApp : Length xs -> Length ys -> Length (xs ++ ys)
+lengthApp sx Z      = sx
+lengthApp sx (S sy) = S (lengthApp sx sy)
+
+public export
+0 lengthIrrel : (sx1, sx2 : Length xs) -> sx1 = sx2
+lengthIrrel Z       Z       = Refl
+lengthIrrel (S sx1) (S sx2) = cong S $ lengthIrrel sx1 sx2
diff --git a/lib/Quox/OPE/Split.idr b/lib/Quox/OPE/Split.idr
index ea8215e..a0647c3 100644
--- a/lib/Quox/OPE/Split.idr
+++ b/lib/Quox/OPE/Split.idr
@@ -17,11 +17,21 @@ record Split {a : Type} (xs, ys, zs : Scope a) (p : xs `Sub` ys ++ zs) where
   0 eqThin : p ~=~ leftThin ++ rightThin
 
 export
-split : (zs : Scope a) -> (p : xs `Sub` ys ++ zs) -> Split xs ys zs p
-split [<] p = MkSplit p zero Refl Refl
-split (zs :< z) (Keep p) with (split zs p)
-  split (zs :< z) (Keep (l ++ r)) | MkSplit l r Refl Refl =
-    MkSplit l (Keep r) Refl Refl
-split (zs :< z) (Drop p) {xs} with (split zs p)
-  split (zs :< z) (Drop (l ++ r)) {xs = _} | MkSplit l r Refl Refl =
-    MkSplit l (Drop r) Refl Refl
+split : Length ys =>
+        (zs : Scope a) -> (p : xs `Sub` ys ++ zs) -> Split xs ys zs p
+split [<] p = MkSplit p zero Refl (endRight p)
+split (zs :< z) p @{ys} with (p.view @{S (lengthApp ys %search)})
+  split (zs :< z) (SubM (S (2 * n)) (Keep p) v0) | (KEEP v Refl) =
+    case split zs (sub v) of
+      MkSplit l r Refl t =>
+        MkSplit l (keep r) Refl $
+          rewrite viewIrrel v0 (KEEP v Refl) in
+          trans (cong keep {a = sub v} t) $
+          sym $ keepAppRight l r
+  split (zs :< z) (SubM (2 * n) (Drop p) v0) | (DROP v Refl) =
+    case split zs (sub v) of
+      MkSplit l r Refl t =>
+        MkSplit l (drop r) Refl $
+          rewrite viewIrrel v0 (DROP v Refl) in
+          trans (cong drop {a = sub v} t) $
+          sym $ dropAppRight l r
diff --git a/lib/Quox/OPE/Sub.idr b/lib/Quox/OPE/Sub.idr
index 233112a..6044626 100644
--- a/lib/Quox/OPE/Sub.idr
+++ b/lib/Quox/OPE/Sub.idr
@@ -9,6 +9,8 @@ import Data.SnocList.Quantifiers
 
 %default total
 
+infix 0 `Sub'`, `Sub`
+
 public export
 data Sub' : Scope a -> Scope a -> Type where
   End  : [<] `Sub'` [<]
@@ -24,7 +26,6 @@ export
 dropInjective : Drop p = Drop q -> p = q
 dropInjective Refl = Refl
 
-
 -- these need to be `public export` so that
 -- `id`, `zero`, and maybe others can reduce
 public export %hint
@@ -67,9 +68,9 @@ lteNilRight End = Refl
 
 
 public export
-id' : Length xs => xs `Sub'` xs
-id' @{Z}   = End
-id' @{S s} = Keep id'
+refl' : Length xs => xs `Sub'` xs
+refl' @{Z}   = End
+refl' @{S s} = Keep refl'
 
 public export
 zero' : Length xs => [<] `Sub'` xs
@@ -82,12 +83,21 @@ single' @{S _} Here      = Keep zero'
 single' @{S _} (There p) = Drop $ single' p
 
 
+namespace Sub
+  public export
+  (.) : ys `Sub'` zs -> xs `Sub'` ys -> xs `Sub'` zs
+  End      . End      = End
+  (Keep p) . (Keep q) = Keep $ p . q
+  (Keep p) . (Drop q) = Drop $ p . q
+  (Drop p) . q        = Drop $ p . q
+
 public export
-trans' : ys `Sub'` zs -> xs `Sub'` ys -> xs `Sub'` zs
-trans' End      End      = End
-trans' (Keep p) (Keep q) = Keep $ trans' p q
-trans' (Keep p) (Drop q) = Drop $ trans' p q
-trans' (Drop p) q        = Drop $ trans' p q
+comp' : ys `Sub'` zs -> xs `Sub'` ys -> xs `Sub'` zs
+comp' = (.)
+
+public export %inline
+trans' : xs `Sub'` ys -> ys `Sub'` zs -> xs `Sub'` zs
+trans' = flip (.)
 
 public export
 app' : xs1 `Sub'` ys1 -> xs2 `Sub'` ys2 -> (xs1 ++ xs2) `Sub'` (ys1 ++ ys2)
@@ -116,11 +126,13 @@ subAny' (Drop q) x         = There (subAny' q x)
 public export
 data SubView : (lte : xs `Sub'` ys) -> (mask : Nat) -> Type where
   [search lte]
-  END  : SubView End 0
+  END  : (0 eq : n = 0) -> SubView End n
   KEEP : {n : Nat} -> {0 p : xs `Sub'` ys} ->
-         (0 v : SubView p n) -> SubView (Keep {z} p) (S (2 * n))
+         (0 v : SubView p n) -> (0 eq : n' = S (2 * n)) ->
+         SubView (Keep {z} p) n'
   DROP : {n : Nat} -> {0 p : xs `Sub'` ys} ->
-         (0 v : SubView p n) -> SubView (Drop {z} p)    (2 * n)
+         (0 v : SubView p n) -> (0 eq : n' = 2 * n) ->
+         SubView (Drop {z} p) n'
 %name SubView v
 
 public export
@@ -129,162 +141,214 @@ record Sub {a : Type} (xs, ys : Scope a) where
   mask : Nat
   0 lte : xs `Sub'` ys
   0 view0 : SubView lte mask
-%name Sub m
+%name Sub sub
+
+public export %inline
+sub : {mask : Nat} -> {0 lte : xs `Sub'` ys} -> (0 view0 : SubView lte mask) ->
+      xs `Sub` ys
+sub v = SubM _ _ v
+
+
+private
+0 uip : (p, q : a = b) -> p = q
+uip Refl Refl = Refl
+
+export
+0 viewIrrel : Length ys =>
+              {m : Nat} -> {lte : xs `Sub'` ys} ->
+              (v1, v2 : SubView lte m) -> v1 === v2
+viewIrrel (END eq1) (END eq2) = rewrite uip eq1 eq2 in Refl
+viewIrrel (KEEP v1 eq1) (KEEP v2 eq2) with (sDoubleInj $ trans (sym eq1) eq2)
+  _ | Refl = rewrite viewIrrel v1 v2 in rewrite uip eq1 eq2 in Refl
+viewIrrel (DROP v1 eq1) (DROP v2 eq2) with (doubleInj $ trans (sym eq1) eq2)
+  _ | Refl = rewrite viewIrrel v1 v2 in rewrite uip eq1 eq2 in Refl
+
+export
+0 viewLteEq : {p, q : xs `Sub'` ys} -> SubView p m -> SubView q m -> p = q
+viewLteEq (END _) (END _) = Refl
+viewLteEq (KEEP {n = m} pv pe) (KEEP {n} qv qe) =
+  let eq = sDoubleInj {m, n} $ trans (sym pe) qe in
+  rewrite viewLteEq pv (rewrite eq in qv) in Refl
+viewLteEq (KEEP pv pe) (DROP qv qe) = absurd $ lsbMutex qe pe
+viewLteEq (DROP pv pe) (KEEP qv qe) = absurd $ lsbMutex pe qe
+viewLteEq (DROP {n = m} pv pe) (DROP {n} qv qe) =
+  let eq = doubleInj {m, n} $ trans (sym pe) qe in
+  rewrite viewLteEq pv (rewrite eq in qv) in Refl
+
+private
+0 lteEq' : (p : xs `Sub'` ys) ->
+           (v1 : SubView p m1) -> (v2 : SubView p m2) ->
+           SubM m1 p v1 = SubM m2 p v2
+lteEq' End (END Refl) (END Refl) = Refl
+lteEq' {m1 = S (2 * n)} {m2 = S (2 * n)} (Keep p) (KEEP v1 Refl) (KEEP v2 Refl) =
+  cong (\v => SubM (S (2 * n)) (Keep p) (KEEP v Refl)) $
+    case lteEq' p v1 v2 of Refl => Refl
+lteEq' {m1 = 2 * n} {m2 = 2 * n} (Drop p) (DROP v1 Refl) (DROP v2 Refl) =
+  cong (\v => SubM (2 * n) (Drop p) (DROP v Refl)) $
+    case lteEq' p v1 v2 of Refl => Refl
+lteEq' {m1 = _} {m2 = S _} _ _ (END _) impossible
+lteEq' {m1 = Z} {m2 = _} _ (KEEP _ _) _ impossible
+lteEq' {m1 = _} {m2 = Z} _ _ (KEEP _ _) impossible
+
+export
+0 lteEq : {p, q : xs `Sub` ys} -> p.lte = q.lte -> p = q
+lteEq {p = SubM pm pl pv} {q = SubM qm ql qv} eq =
+  rewrite eq in lteEq' ql (rewrite sym eq in pv) qv
+
+
+public export %inline
+end : [<] `Sub` [<]
+end = SubM 0 End (END Refl)
+
+public export %inline
+keep : xs `Sub` ys -> xs :< z `Sub` ys :< z
+keep (SubM mask lte view0) = SubM (S (2 * mask)) (Keep lte) (KEEP view0 Refl)
+
+public export %inline
+drop : xs `Sub` ys -> xs `Sub` ys :< z
+drop (SubM mask lte view0) = SubM (2 * mask) (Drop lte) (DROP view0 Refl)
+
+
+export
+0 keepLte : (p : xs `Sub` ys) -> (keep p).lte = Keep p.lte
+keepLte (SubM mask lte view0) = Refl
+
+export
+0 dropLte : (p : xs `Sub` ys) -> (drop p).lte = Drop p.lte
+dropLte (SubM mask lte view0) = Refl
+
+
+public export
+data Eqv : {xs, ys : Scope a} -> (p, q : xs `Sub` ys) -> Type where
+  EQV : {0 p, q : xs `Sub` ys} -> p.mask = q.mask -> p `Eqv` q
+%name Eqv eqv
+
+export
+Reflexive (xs `Sub` ys) Eqv where
+  reflexive = EQV Refl
+
+export
+Symmetric (xs `Sub` ys) Eqv where
+  symmetric (EQV eq) = EQV $ sym eq
+
+export
+Transitive (xs `Sub` ys) Eqv where
+  transitive (EQV eq1) (EQV eq2) = EQV $ trans eq1 eq2
+
+export
+0 eqvToEq : {p, q : xs `Sub` ys} -> p `Eqv` q -> p = q
+eqvToEq {p = SubM _ _ pv} {q = SubM _ _ qv} (EQV Refl) with (viewLteEq pv qv)
+  _ | Refl = rewrite viewIrrel pv qv in Refl
+
+export
+0 eqToEqv : {p, q : xs `Sub` ys} -> p = q -> p `Eqv` q
+eqToEqv Refl = reflexive
 
 
 export
 getMask : SubView lte mask -> Subset Nat (Equal mask)
-
-private
-0 ltemNilLeftZero' : SubView {xs = [<]} lte mask -> mask = 0
-ltemNilLeftZero' END      = Refl
-ltemNilLeftZero' (DROP v) = cong (2 *) $ ltemNilLeftZero' v
-
-export
-ltemNilLeftZero : (0 _ : SubView {xs = [<]} lte mask) -> mask = 0
-ltemNilLeftZero v = irrelevantEq $ ltemNilLeftZero' v
+getMask (END Refl)  = Element 0 Refl
+getMask (KEEP v eq) = Element _ eq
+getMask (DROP v eq) = Element _ eq
 
 
 private
-0 lteNilLeftDrop0 : (p : [<] `Sub'` (xs :< x)) -> (q ** p = Drop q)
-lteNilLeftDrop0 (Drop q) = (q ** Refl)
-
-private
-lteNilLeftDrop : (0 p : [<] `Sub'` (xs :< x)) -> Exists (\q => p = Drop q)
-lteNilLeftDrop q =
-  let 0 res = lteNilLeftDrop0 q in
-  Evidence res.fst (irrelevantEq res.snd)
+splitExEq : {0 f, g : a -> b} ->
+            (0 p : (x : a ** f x = g x)) -> Exists (\x => f x = g x)
+splitExEq p = Evidence p.fst (irr p.snd)
+  where irr : forall a, b. (0 eq : a = b) -> a = b
+        irr Refl = Refl
 
 private
 0 lteNil2End : (p : [<] `Sub'` [<]) -> p = End
 lteNil2End End = Refl
 
 private
-0 ltemEnd' : SubView p n -> p = End -> n = 0
-ltemEnd' END Refl = Refl
+0 ltemEnd : SubView p n -> p = End -> n = 0
+ltemEnd (END eq) Refl = eq
 
 private
-0 ltemEven' : {p : xs `Sub'` (ys :< y)} ->
-              n = 2 * n' -> SubView p n -> (q ** p = Drop q)
-ltemEven' eq (KEEP q) = absurd $ lsbMutex' eq Refl
-ltemEven' eq (DROP q) = (_ ** Refl)
+0 ltemEvenDrop : {p : xs `Sub'` (ys :< y)} ->
+                 n = 2 * n' -> SubView p n -> (q ** p = Drop q)
+ltemEvenDrop eq (KEEP _ eq') = absurd $ lsbMutex eq eq'
+ltemEvenDrop eq (DROP {})    = (_ ** Refl)
 
 private
-ltemEven : {0 p : xs `Sub'` (ys :< y)} ->
-           (0 _ : SubView p (2 * n)) -> Exists (\q => p = Drop q)
-ltemEven q =
-  let 0 res = ltemEven' Refl q in
-  Evidence res.fst (irrelevantEq res.snd)
-
-private
-0 fromDROP' : {lte : xs `Sub'` ys} -> n = 2 * n' ->
-              SubView (Drop lte) n -> SubView lte n'
-fromDROP' eq (DROP {n} p) =
+0 fromDROP : {lte : xs `Sub'` ys :< z} -> n = 2 * n' -> lte = Drop lte' ->
+             SubView lte n -> SubView lte' n'
+fromDROP eq Refl (DROP {n} p Refl) =
   let eq = doubleInj eq {m = n, n = n'} in
   rewrite sym eq in p
 
 private
-0 ltemOdd' : {p : (xs :< x) `Sub'` (ys :< x)} -> {n' : Nat} ->
+0 ltemOddKeep : {p : (xs :< x) `Sub'` (ys :< x)} -> {n' : Nat} ->
                 n = S (2 * n') -> SubView p n -> (q ** p = Keep q)
-ltemOdd' eq (KEEP q) = (_ ** Refl)
-ltemOdd' eq (DROP q) = absurd $ lsbMutex' Refl eq
-ltemOdd' eq END      impossible
+ltemOddKeep eq (KEEP {})    = (_ ** Refl)
+ltemOddKeep eq (DROP _ eq') = absurd $ lsbMutex eq' eq
+ltemOddKeep eq (END _) impossible
 
 private
-ltemOdd : (0 _ : SubView p (S (2 * n))) -> Exists (\q => p = Keep q)
-ltemOdd q =
-  let 0 res = ltemOdd' Refl q in
-  Evidence res.fst (irrelevantEq res.snd)
+0 ltemOddLeft : {0 n, n' : Nat} -> {lte : xs `Sub'` ys :< z} ->
+                n = S (2 * n') -> SubView lte n ->
+                (xs' ** xs = xs' :< z)
+ltemOddLeft eq {lte = Keep p} _ = (_ ** Refl)
+ltemOddLeft eq {lte = Drop p} (DROP n' eq') = void $ lsbMutex eq' eq
 
 private
-0 ltemOddHead' : {p : (xs :< x) `Sub'` (ys :< y)} -> {n' : Nat} ->
-                 n = S (2 * n') -> SubView p n -> x = y
-ltemOddHead' eq (KEEP q) = Refl
-ltemOddHead' eq (DROP q) = absurd $ lsbMutex' Refl eq
-ltemOddHead' eq END      impossible
-
-private
-ltemOddHead : {0 p : (xs :< x) `Sub'` (ys :< y)} ->
-              (0 _ : SubView p (S (2 * n))) -> x = y
-ltemOddHead q = irrelevantEq $ ltemOddHead' Refl q
-
-private
-0 fromKEEP' : {lte : xs `Sub'` ys} -> n = S (2 * n') ->
-              SubView (Keep lte) n -> SubView lte n'
-fromKEEP' eq (KEEP {n} p) =
-  let eq = doubleInj (injective eq) {m = n, n = n'} in
+0 fromKEEP : {lte : xs :< z `Sub'` ys :< z} ->
+             n = S (2 * n') -> lte = Keep lte' ->
+             SubView lte n -> SubView lte' n'
+fromKEEP eq Refl (KEEP {n} p Refl) =
+  let eq = sDoubleInj eq {m = n, n = n'} in
   rewrite sym eq in p
 
-export
-view : Length xs => Length ys =>
-       (m : Sub xs ys) -> SubView m.lte m.mask
-view @{Z} @{Z} (SubM {lte, view0, _}) =
-  rewrite lteNil2End lte in
-  rewrite ltemEnd' view0 (lteNil2End lte) in
-  END
-view @{S _} @{Z} (SubM {lte, _}) = void $ absurd lte
-view @{Z} @{S sy} (SubM mask lte view0) with (ltemNilLeftZero view0)
-  view @{Z} @{S sy} (SubM 0 lte view0)
-      | Refl with (lteNilLeftDrop lte)
-    view @{Z} @{S sy} (SubM 0 (Drop lte) view0)
-        | Refl | Evidence lte Refl =
-            DROP {n = 0} $ let DROP {n = 0} p = view0 in p
-view @{S sx} @{S sy} (SubM mask lte view0) with (viewLsb mask)
-  view @{S sx} @{S sy} (SubM (2 * n) lte view0)
-      | Evidence Even (Lsb0 n) with (ltemEven view0)
-    view @{S sx} @{S sy} (SubM (2 * m) (Drop lte) view0)
-        | Evidence Even (Lsb0 m) | Evidence lte Refl =
-            DROP $ fromDROP' Refl view0
-  view @{S sx} @{S sy} (SubM (S (2 * n)) lte view0)
-      | Evidence Odd (Lsb1 n) with (ltemOddHead view0)
-    view @{S sx} @{S sy} (SubM (S (2 * n)) lte view0)
-        | Evidence Odd (Lsb1 n) | Refl with (ltemOdd view0)
-      view @{S sx} @{S sy} (SubM (S (2 * n)) (Keep lte) view0)
-          | Evidence Odd (Lsb1 n) | Refl | Evidence lte Refl =
-              KEEP $ fromKEEP' Refl view0
 
 export
-(.view) : Length xs => Length ys =>
-          (m : Sub xs ys) -> SubView m.lte m.mask
+view : Length ys => (m : Sub xs ys) -> SubView m.lte m.mask
+view @{Z} (SubM mask lte view0) with 0 (lteNilRight lte)
+  _ | Refl =
+    rewrite lteNil2End lte in
+    rewrite ltemEnd view0 (lteNil2End lte) in
+    END Refl
+view @{S sy} (SubM mask lte view0) {ys = ys :< z} with (viewLsb mask)
+  _ | Lsb0 n eqn with (splitExEq $ ltemEvenDrop eqn view0)
+    _ | Evidence lte' eql =
+      rewrite eqn in rewrite eql in
+      DROP (fromDROP eqn eql view0) Refl
+  _ | Lsb1 n eqn with (splitExEq $ ltemOddLeft eqn view0)
+    _ | Evidence xs' Refl =
+      let Evidence q eqq = splitExEq $ ltemOddKeep eqn view0 in
+      rewrite eqn in rewrite eqq in
+      KEEP (fromKEEP eqn eqq view0) Refl
+
+public export %inline
+(.view) : Length ys => (m : Sub xs ys) -> SubView m.lte m.mask
 (.view) = view
 
+public export %inline
+review : Length ys => {m : Nat} -> {0 lte : xs `Sub'` ys} ->
+         (0 _ : SubView lte m) -> SubView lte m
+review v = view $ sub v
+
+
 
 export
-ltemLen : Length xs => Length ys =>
-          xs `Sub` ys -> length xs `LTE` length ys
-ltemLen @{sx} @{sy} sub@(SubM m l _) with (sub.view)
-  ltemLen @{sx} @{sy} sub@(SubM 0 End _) | END = LTEZero
-  ltemLen @{S sx} @{S sy} sub@(SubM (S (2 * n)) (Keep p) _) | (KEEP q) =
-    LTESucc $ ltemLen $ SubM n p q
-  ltemLen @{sx} @{S sy} sub@(SubM (2 * n) (Drop p) _) | (DROP q) =
-    lteSuccRight $ ltemLen $ SubM n p q
+ltemLen : (sy : Length ys) => xs `Sub` ys -> length xs `LTE` sy.nat
+ltemLen (SubM mask lte view0) {sy} with (review view0)
+  ltemLen (SubM _ _ _)            | END eq    = LTEZero
+  ltemLen (SubM _ _ _) {sy = S _} | KEEP v eq = LTESucc $ ltemLen $ sub v
+  ltemLen (SubM _ _ _) {sy = S _} | DROP v eq = lteSuccRight $ ltemLen $ sub v
 
 export
 ltemNilRight : xs `Sub` [<] -> xs = [<]
 ltemNilRight m = irrelevantEq $ lteNilRight m.lte
 
 
-public export %inline
-end : [<] `Sub` [<]
-end = SubM 0 End END
-
-public export %inline
-keep : xs `Sub` ys -> xs :< z `Sub` ys :< z
-keep (SubM mask lte view0) = SubM (S (2 * mask)) (Keep lte) (KEEP view0)
-
-public export %inline
-drop : xs `Sub` ys -> xs `Sub` ys :< z
-drop (SubM mask lte view0) = SubM (2 * mask) (Drop lte) (DROP view0)
-
-
 export %inline
-dropLast : Length xs => Length ys =>
-           (xs :< x) `Sub` ys -> xs `Sub` ys
-dropLast @{sx} @{sy} sub@(SubM mask lte _) with (sub.view)
-  dropLast sub@(SubM (S (2 * n)) (Keep p) _) | (KEEP v) =
-    SubM (2 * n) (Drop p) (DROP v)
-  dropLast @{_} @{S sy} sub@(SubM (2 * n) (Drop p) _) | DROP v =
-    drop $ dropLast $ SubM n p v
+dropLast : Length ys => (xs :< x) `Sub` ys -> xs `Sub` ys
+dropLast (SubM _ _ view0) @{sy} with (review view0)
+  dropLast (SubM _ _ _)        | KEEP v _ = drop $ sub v
+  dropLast (SubM _ _ _) @{S _} | DROP v _ = drop $ dropLast $ sub v
 
 
 export
@@ -293,11 +357,9 @@ Uninhabited (xs :< x `Sub` [<]) where
 
 export
 Length xs => Uninhabited (xs :< x `Sub` xs) where
-  uninhabited @{sx} sub@(SubM mask lte view0) with (sub.view)
-    uninhabited @{S sx} sub@(SubM (S (2 * n)) (Keep p) _) | KEEP v =
-      uninhabited $ SubM n p v
-    uninhabited @{S sx} sub@(SubM (2 * n) (Drop p) _) | DROP v =
-      uninhabited $ dropLast $ SubM n p v
+  uninhabited (SubM _ _ view0) @{sx} with (review view0)
+    uninhabited (SubM _ _ _) @{S _} | KEEP v _ = uninhabited $ sub v
+    uninhabited (SubM _ _ _) @{S _} | DROP v _ = uninhabited $ dropLast $ sub v
 
 
 export
@@ -305,103 +367,206 @@ refl : Length xs => xs `Sub` xs
 refl @{Z}   = end
 refl @{S s} = keep refl
 
-export Reflexive (Scope a) Sub where reflexive = refl
+export
+0 reflLte : {sx : Length xs} -> (refl @{sx}).lte = refl' @{sx}
+reflLte {sx = Z}   = Refl
+reflLte {sx = S s} = trans (keepLte _) $ cong Keep reflLte
+
+public export %inline
+Reflexive (Scope a) Sub where reflexive = refl
 
 mutual
   private
   antisym_ : Length xs => Length ys =>
              {0 p : xs `Sub'` ys} -> {0 q : ys `Sub'` xs} ->
              SubView p m1 -> SubView q m2 -> xs = ys
-  antisym_ END       END = Refl
-  antisym_ (KEEP v1) (KEEP v2 {z}) @{S sx} @{S sy} =
+  antisym_ (END _)  (END _) = Refl
+  antisym_ (KEEP v1 _) (KEEP v2 _ {z}) @{S sx} @{S sy} =
     cong (:< z) $ antisym (SubM _ _ v1) (SubM _ _ v2)
-  antisym_ (KEEP v1) (DROP v2) {p = Keep p} {q = Drop q} =
+  antisym_ (KEEP {}) (DROP {}) {p = Keep p} {q = Drop q} =
     void $ succNotLTEpred $ lteLen q `transitive` lteLen p
-  antisym_ (DROP v1) (KEEP v2) {p = Drop p} {q = Keep q} =
+  antisym_ (DROP {}) (KEEP {}) {p = Drop p} {q = Keep q} =
     void $ succNotLTEpred $ lteLen p `transitive` lteLen q
-  antisym_ (DROP v1) (DROP v2) {p = Drop p} {q = Drop q} =
+  antisym_ (DROP {}) (DROP {}) {p = Drop p} {q = Drop q} =
     void $ succNotLTEpred $ lteLen p `transitive` lteSuccLeft (lteLen q)
 
   export
   antisym : Length xs => Length ys => xs `Sub` ys -> ys `Sub` xs -> xs = ys
-  antisym p q = antisym_ p.view q.view
+  antisym v1 v2 = antisym_ v1.view v2.view
 
-export
+public export %inline
 Antisymmetric (Scope a) Sub where
   antisymmetric p q = antisym p q
 
 
 mutual
   private
-  trans_ : Length xs => Length ys => Length zs =>
+  trans_ : Length ys => Length zs =>
            {0 p : xs `Sub'` ys} -> {0 q : ys `Sub'` zs} ->
            SubView p m1 -> SubView q m2 -> xs `Sub` zs
-  trans_ END END = end
-  trans_ (KEEP v1) (KEEP v2) @{S sx} @{S sy} @{S sz} =
-    keep $ SubM _ _ v1 `trans` SubM _ _ v2
-  trans_ (DROP v1) (KEEP v2) @{sx} @{S sy} @{S sz} =
-    drop $ SubM _ _ v1 `trans` SubM _ _ v2
-  trans_ v1 (DROP v2) @{sx} @{sy} @{S sz} =
+  trans_ (END _) (END _) = end
+  trans_ (KEEP v1 _) (KEEP v2 _) @{S sy} @{S sz} = keep $ sub v1 `trans` sub v2
+  trans_ (DROP v1 _) (KEEP v2 _) @{S sy} @{S sz} = drop $ sub v1 `trans` sub v2
+  trans_ v1 (DROP v2 _) @{sy} @{S sz} =
     let Element m1' eq = getMask v1 in
-    drop $ SubM m1' _ (rewrite sym eq in v1) `trans` SubM _ _ v2
+    drop $ SubM m1' _ (rewrite sym eq in v1) `trans` sub v2
 
   export
-  trans : Length xs => Length ys => Length zs =>
-          xs `Sub` ys -> ys `Sub` zs -> xs `Sub` zs
+  trans : Length ys => Length zs => xs `Sub` ys -> ys `Sub` zs -> xs `Sub` zs
   trans p q = trans_ p.view q.view
 
-  export
-  (.) : Length xs => Length ys => Length zs =>
-        xs `Sub` ys -> ys `Sub` zs -> xs `Sub` zs
-  (.) = trans
+public export %inline
+(.) : Length ys => Length zs => ys `Sub` zs -> xs `Sub` ys -> xs `Sub` zs
+(.) = flip trans
 
-export
+public export %inline
+comp : Length ys => Length zs => ys `Sub` zs -> xs `Sub` ys -> xs `Sub` zs
+comp = (.)
+
+public export %inline
 Transitive (Scope a) Sub where
-  transitive p q = trans p q
+  transitive p q = q . p
 
 
-export
+public export
 zero : Length xs => [<] `Sub` xs
 zero @{Z}   = end
 zero @{S s} = drop zero
 
 export
+0 zeroLte : {sx : Length xs} -> (zero @{sx}).lte = zero' @{sx}
+zeroLte {sx = Z}   = Refl
+zeroLte {sx = S s} = trans (dropLte zero) $ cong Drop zeroLte
+
+public export
 single : Length xs => x `Elem` xs -> [< x] `Sub` xs
 single @{S sx} Here      = keep zero
 single @{S sx} (There p) = drop $ single p
 
+export
+0 singleLte : {sx : Length xs} -> (p : x `Elem` xs) ->
+              (single p @{sx}).lte = single' p @{sx}
+singleLte {sx = S s} Here      = trans (keepLte zero) $ cong Keep zeroLte
+singleLte {sx = S s} (There p) = trans (dropLte _) $ cong Drop $ singleLte p
+
+
+mutual
+  private
+  app0 : Length ys2 =>
+         (l : xs1 `Sub` ys1) ->
+         {rm : Nat} -> {0 rl : xs2 `Sub'` ys2} -> (rv : SubView rl rm) ->
+         (xs1 ++ xs2) `Sub` (ys1 ++ ys2)
+  app0 l (END eq)              = l
+  app0 l (KEEP v Refl) @{S sy} = keep $ l ++ sub v
+  app0 l (DROP v Refl) @{S sy} = drop $ l ++ sub v
+
+  export
+  app : Length ys2 =>
+        xs1 `Sub` ys1 -> xs2 `Sub` ys2 -> (xs1 ++ xs2) `Sub` (ys1 ++ ys2)
+  app l r = app0 l r.view
+
+  public export %inline
+  (++) : Length ys2 =>
+         xs1 `Sub` ys1 -> xs2 `Sub` ys2 -> (xs1 ++ xs2) `Sub` (ys1 ++ ys2)
+  (++) = app
 
 export
-(++) : Length xs2 => Length ys2 =>
-       xs1 `Sub` ys1 -> xs2 `Sub` ys2 -> (xs1 ++ xs2) `Sub` (ys1 ++ ys2)
-(++) sub1 sub2@(SubM {}) @{sx2} @{sy2} with (sub2.view)
-  (++) sub1 sub2@(SubM {}) | END = sub1
-  (++) sub1 sub2@(SubM {}) @{S sx2} @{S sy2} | KEEP v = keep $ sub1 ++ SubM _ _ v
-  (++) sub1 sub2@(SubM {}) @{sx2} @{S sy2} | DROP v = drop $ sub1 ++ SubM _ _ v
+0 appLte : {sy : Length ys2} ->
+           (l : xs1 `Sub` ys1) -> (r : xs2 `Sub` ys2) ->
+           (app l r @{sy}).lte = app' l.lte r.lte
+appLte l r@(SubM 0 End (END Refl)) =
+  cong (\v => (app0 l v).lte) (viewIrrel (view end) (END Refl))
+appLte l r@(SubM (S (2 * n)) (Keep p) (KEEP v Refl)) {sy = S sy} =
+  trans (cong (\v => (app0 l v @{S sy}).lte) (viewIrrel _ (KEEP v Refl))) $
+  trans (keepLte _) $
+  cong Keep $ appLte l (sub v)
+appLte l r@(SubM 0 (Drop p) (DROP {n = 0} v Refl)) {sy = S sy} =
+  trans (cong (\v => (app0 l v @{S sy}).lte) (viewIrrel _ (DROP v Refl))) $
+  trans (dropLte _) $
+  cong Drop $ appLte l (sub v)
+appLte l r@(SubM (2 * S n) (Drop p) (DROP {n = S n} v Refl)) {sy = S sy} =
+  trans (cong (\v => (app0 l v @{S sy}).lte) (viewIrrel _ (DROP v Refl))) $
+  trans (dropLte _) $
+  cong Drop $ appLte l (sub v)
+appLte {xs2 = _ :< _, ys2 = [<]} _ (SubM _ _ _) impossible
+
+export
+0 keepAppRight : {sy : Length ys2} ->
+                 (l : xs1 `Sub` ys1) -> (r : xs2 `Sub` ys2) ->
+                 (l ++ keep r) @{S sy} = keep ((l ++ r) @{sy})
+keepAppRight l (SubM mask _ _) = rewrite (lsbOdd mask).snd in Refl
+
+export
+0 dropAppRight : (l : xs1 `Sub` ys1) -> (r : xs2 `Sub` ys2) ->
+                 (l ++ drop r) @{S sy} = drop ((l ++ r) @{sy})
+dropAppRight l r = lteEq $
+  trans (appLte l (drop r)) $
+  trans (cong (app' l.lte) (dropLte r)) $
+  trans (cong Drop (sym (appLte l r))) $
+  sym $ dropLte (l ++ r)
+
+
+export
+0 endRight : {xs, ys : Scope a} -> (sub : xs `Sub` ys) -> sub = (sub ++ Sub.end)
+endRight sub = Refl
+
+
+private
+0 transDrop_ : {p : xs `Sub'` ys} -> {q : ys `Sub'` zs} ->
+               (pv : SubView p m1) -> (qv : SubView q m2) ->
+               trans_ pv (DROP qv qe) @{sy} @{S sz} =
+                 drop (trans_ pv qv @{sy} @{sz})
+transDrop_ {sy = Z} {sz = sz} (END Refl) qv =
+  cong (\v => drop $ trans_ {m2, q} (END Refl) v) $ viewIrrel {}
+transDrop_ {sy = S sy} {sz = sz} (KEEP pv Refl) qv {p = Keep p} =
+  cong2 (\x, y => drop (trans_ @{S sy} x y)) (viewIrrel {}) (viewIrrel {})
+transDrop_ {sy = S sy} {sz = S sz} (DROP pv Refl) qv =
+  cong2 (\x, y => drop (trans_ @{S sy} @{S sz} x y))
+    (viewIrrel {}) (viewIrrel {})
+transDrop_ {ys = _ :< _, zs = [<]} _ _ impossible
+
+private
+0 transLte_ : {p : xs `Sub'` ys} -> {q : ys `Sub'` zs} ->
+              (pv : SubView p m1) -> (qv : SubView q m2) ->
+              (trans_ pv qv @{sy} @{sz}).lte = trans' p q
+transLte_ (END _) (END _) = Refl
+transLte_ (KEEP pv pe) (KEEP qv qe) {sy = S _} {sz = S _} =
+  trans (keepLte _) $ cong Keep $ transLte_ {}
+transLte_ (DROP pv pe) (KEEP qv qe) {sy = S _} {sz = S _} =
+  trans (dropLte _) $ cong Drop $ transLte_ {}
+transLte_ pv (DROP qv qe) {sz = S _} =
+  trans (cong lte $ transDrop_ pv qv) $
+  trans (dropLte _) $ cong Drop $ transLte_ pv qv
+transLte_ {ys = _ :< _, zs = [<]} _ _ impossible
+
+export
+0 transLte : {sy : Length ys} -> {sz : Length zs} ->
+             (p : xs `Sub` ys) -> (q : ys `Sub` zs) ->
+             (trans p q @{sy} @{sz}).lte = trans' p.lte q.lte
+transLte p q = transLte_ p.view q.view
+
+public export
+0 compLte : {sy : Length ys} -> {sz : Length zs} ->
+            (q : ys `Sub` zs) -> (p : xs `Sub` ys) ->
+            ((q . p) @{sy} @{sz}).lte = q.lte . p.lte 
+compLte q p = transLte p q
 
 
 ||| if `p` holds for all elements of the main list,
 ||| it holds for all elements of the sublist
 export
-subAll : Length xs => Length ys =>
-         xs `Sub` ys -> All prop ys -> All prop xs
-subAll sub@(SubM {}) ps @{sx} @{sy} with (sub.view)
-  subAll sub@(SubM {}) [<] | END = [<]
-  subAll sub@(SubM {}) (ps :< p) @{S sx} @{S sy} | KEEP v =
-    subAll (SubM _ _ v) ps :< p
-  subAll sub@(SubM {}) (ps :< p) @{sx} @{S sy} | DROP v =
-    subAll (SubM _ _ v) ps
+subAll : Length ys => xs `Sub` ys -> All prop ys -> All prop xs
+subAll (SubM _ _ v) ps @{sy} with (review v)
+  subAll (SubM _ _ _) [<]               | END    _ = [<]
+  subAll (SubM _ _ _) (ps :< p) @{S sy} | KEEP v _ = subAll (sub v) ps :< p
+  subAll (SubM _ _ _) (ps :< p) @{S sy} | DROP v _ = subAll (sub v) ps
 
 
 ||| if `p` holds for one element of the sublist,
 ||| it holds for one element of the main list
 export
-subAny : Length xs => Length ys =>
-         xs `Sub` ys -> Any prop xs -> Any prop ys
-subAny sub@(SubM {}) p @{sx} @{sy} with (sub.view)
-  subAny sub@(SubM {}) p | END impossible
-  subAny sub@(SubM {}) (Here p) | KEEP v = Here p
-  subAny sub@(SubM {}) (There p) @{S sx} @{S sy} | KEEP v =
-    There $ subAny (SubM _ _ v) p
-  subAny sub@(SubM {}) p @{sx} @{S sy} | DROP v =
-    There $ subAny (SubM _ _ v) p
+subAny : Length ys => xs `Sub` ys -> Any prop xs -> Any prop ys
+subAny (SubM _ _ v) p @{sy} with (review v)
+  subAny (SubM _ _ _) (Here  p)         | KEEP v _ = Here p
+  subAny (SubM _ _ _) (There p) @{S sy} | KEEP v _ = There $ subAny (sub v) p
+  subAny (SubM _ _ _) p         @{S sy} | DROP v _ = There $ subAny (sub v) p