From a11e4d5ef18a536a4ff1363fa202a28ba8d90f9a Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Thu, 23 Dec 2021 19:01:24 +0100
Subject: [PATCH] add LT/LTE for vars

---
 src/Quox/Context.idr      |  4 +-
 src/Quox/Syntax/Shift.idr |  4 +-
 src/Quox/Syntax/Var.idr   | 79 +++++++++++++++++++++++++++++++++++++++
 3 files changed, 83 insertions(+), 4 deletions(-)

diff --git a/src/Quox/Context.idr b/src/Quox/Context.idr
index 56f2d52..07c2f45 100644
--- a/src/Quox/Context.idr
+++ b/src/Quox/Context.idr
@@ -93,7 +93,7 @@ Triangle' a = Context $ Context (\_ => a)
 
 export
 0 telescopeLTE : Telescope _ from to -> from `LTE` to
-telescopeLTE [<]        = reflexive {rel=LTE}
+telescopeLTE [<]        = reflexive {rel=Nat.LTE}
 telescopeLTE (tel :< _) = lteSuccRight $ telescopeLTE tel
 
 export
@@ -102,7 +102,7 @@ export
 
 export %hint
 0 succGT : S n `GT` n
-succGT = LTESucc $ reflexive {rel=LTE}
+succGT = LTESucc $ reflexive {rel=Nat.LTE}
 
 
 parameters {auto _ : Applicative f}
diff --git a/src/Quox/Syntax/Shift.idr b/src/Quox/Syntax/Shift.idr
index 75b7b7e..7dae475 100644
--- a/src/Quox/Syntax/Shift.idr
+++ b/src/Quox/Syntax/Shift.idr
@@ -59,9 +59,9 @@ export
                by.nat + i.nat `LT` to
 shiftVarLT by i =
   rewrite plusSuccRightSucc by.nat i.nat in
-  transitive {rel=LTE}
+  transitive {rel=Nat.LTE}
     (plusLteMonotoneLeft by.nat (S i.nat) from (toNatLT i))
-    (replace {p=(\n => LTE n to)} (shiftDiff by) $ reflexive {rel=LTE})
+    (replace {p=(`LTE` to)} (shiftDiff by) $ reflexive {rel=Nat.LTE})
 
 
 public export
diff --git a/src/Quox/Syntax/Var.idr b/src/Quox/Syntax/Var.idr
index ca5747b..9f5742a 100644
--- a/src/Quox/Syntax/Var.idr
+++ b/src/Quox/Syntax/Var.idr
@@ -133,3 +133,82 @@ public export
 interface FromVar f where %inline fromVar : Var n -> f n
 
 public export FromVar Var where fromVar = id
+
+
+public export
+data LT : Var n -> Var n -> Type where
+  LTZ : VZ `LT` VS i
+  LTS : i `LT` j -> VS i `LT` VS j
+%builtin Natural Var.LT
+%name Var.LT lt
+
+public export %inline
+GT : Var n -> Var n -> Type
+i `GT` j = j `LT` i
+
+export
+Transitive (Var n) LT where
+  transitive LTZ     (LTS _) = LTZ
+  transitive (LTS p) (LTS q) = LTS $ transitive p q {rel=Var.LT}
+
+export Uninhabited (i    `Var.LT` i)  where uninhabited (LTS p) = uninhabited p
+export Uninhabited (VS i `LT`     VZ) where uninhabited _ impossible
+
+export
+isLT : (i, j : Var n) -> Dec (i `LT` j)
+isLT VZ     VZ     = No uninhabited
+isLT VZ     (VS j) = Yes LTZ
+isLT (VS i) VZ     = No uninhabited
+isLT (VS i) (VS j) with (isLT i j)
+  _ | Yes prf   = Yes (LTS prf)
+  _ | No contra = No  (\case LTS p => contra p)
+
+
+public export
+data Compare : (i, j : Var n) -> Type where
+  IsLT : (lt : i `LT` j) -> Compare i j
+  IsEQ :                    Compare i i
+  IsGT : (gt : i `GT` j) -> Compare i j
+%name Compare cmp
+
+export
+compareS : Compare i j -> Compare (VS i) (VS j)
+compareS (IsLT lt) = IsLT (LTS lt)
+compareS IsEQ      = IsEQ
+compareS (IsGT gt) = IsGT (LTS gt)
+
+export
+compareP : (i, j : Var n) -> Compare i j
+compareP VZ     VZ     = IsEQ
+compareP VZ     (VS j) = IsLT LTZ
+compareP (VS i) VZ     = IsGT LTZ
+compareP (VS i) (VS j) = compareS $ compareP i j
+
+
+public export
+data LTE : Var n -> Var n -> Type where
+  LTEZ : VZ `LTE` j
+  LTES : i  `LTE` j -> VS i `LTE` VS j
+
+export
+Reflexive (Var n) LTE where
+  reflexive {x = VZ}   = LTEZ
+  reflexive {x = VS i} = LTES $ reflexive {x=i}
+
+export
+Transitive (Var n) LTE where
+  transitive LTEZ     q        = LTEZ
+  transitive (LTES p) (LTES q) = LTES $ transitive p q {rel=Var.LTE}
+
+export
+Antisymmetric (Var n) LTE where
+  antisymmetric LTEZ     LTEZ     = Refl
+  antisymmetric (LTES p) (LTES q) = cong VS $ antisymmetric p q {rel=Var.LTE}
+
+export
+splitLTE : {j : Var n} -> i `Var.LTE` j -> Either (i = j) (i `Var.LT` j)
+splitLTE {j = VZ}   LTEZ     = Left Refl
+splitLTE {j = VS _} LTEZ     = Right LTZ
+splitLTE            (LTES p) with (splitLTE p)
+  _ | (Left  eq) = Left $ cong VS eq
+  _ | (Right lt) = Right $ LTS lt