add LT/LTE for vars

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}

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

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