From b25e5320d9ad7004165fa420cee4f86964362c67 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Thu, 12 Jan 2023 16:03:09 +0100
Subject: [PATCH] some more properties of var

---
 lib/Quox/Decidable.idr  | 16 ++++++++++++
 lib/Quox/Syntax/Var.idr | 55 +++++++++++++++++++++++++++--------------
 2 files changed, 53 insertions(+), 18 deletions(-)

diff --git a/lib/Quox/Decidable.idr b/lib/Quox/Decidable.idr
index ecd78dd..680b341 100644
--- a/lib/Quox/Decidable.idr
+++ b/lib/Quox/Decidable.idr
@@ -1,5 +1,6 @@
 module Quox.Decidable
 
+import public Data.Bool.Decidable
 import public Decidable.Decidable
 import public Decidable.Equality
 import public Control.Relation
@@ -24,6 +25,15 @@ public export
 Dec2 p = (x : a) -> (y : b) -> Dec (p x y)
 
 
+public export
+0 Reflects1 : Pred a -> (a -> Bool) -> Type
+p `Reflects1` f = (x : a) -> p x `Reflects` f x
+
+public export
+0 Reflects2 : REL a b -> (a -> b -> Bool) -> Type
+p `Reflects2` f = (x : a) -> (y : b) -> p x y `Reflects` f x y
+
+
 public export
 (||) : Dec p -> Dec q -> Dec (Either p q)
 Yes y1 || _      = Yes $ Left y1
@@ -35,3 +45,9 @@ public export
 Yes y1 && Yes y2 = Yes (y1, y2)
 Yes _  && No  n2 = No $ n2 . snd
 No  n1 && _      = No $ n1 . fst
+
+
+public export
+reflectToDec : p `Reflects` b -> Dec p
+reflectToDec (RTrue  y) = Yes y
+reflectToDec (RFalse n) = No  n
diff --git a/lib/Quox/Syntax/Var.idr b/lib/Quox/Syntax/Var.idr
index 4a19a0a..107cbf5 100644
--- a/lib/Quox/Syntax/Var.idr
+++ b/lib/Quox/Syntax/Var.idr
@@ -35,6 +35,11 @@ export %inline Show (Var n) where showPrec d i = showCon d "V" $ showArg i.nat
 
 public export %inline Injective VS where injective Refl = Refl
 
+export Uninhabited (Var 0) where uninhabited _ impossible
+
+export Uninhabited (VZ   = VS i) where uninhabited _ impossible
+export Uninhabited (VS i = VZ)   where uninhabited _ impossible
+
 
 parameters {auto _ : Pretty.HasEnv m}
   private
@@ -161,14 +166,19 @@ Transitive (Var n) LT where
 export Uninhabited (i    `Var.LT` i)  where uninhabited (LTS p) = uninhabited p
 export Uninhabited (VS i `LT`     VZ) where uninhabited _ impossible
 
+
+export
+ltReflect : LT {n} `Reflects2` (<)
+ltReflect VZ     VZ     = RFalse absurd
+ltReflect VZ     (VS j) = RTrue LTZ
+ltReflect (VS i) VZ     = RFalse absurd
+ltReflect (VS i) (VS j) with (ltReflect i j) | (i < j)
+  _ | RTrue  yes | True  = RTrue  $ LTS yes
+  _ | RFalse no  | False = RFalse $ \case LTS p => no p
+
 export
 isLT : Dec2 Var.LT
-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)
+isLT i j = reflectToDec $ ltReflect i j
 
 
 public export
@@ -191,11 +201,18 @@ compareP VZ     (VS j) = IsLT LTZ
 compareP (VS i) VZ     = IsGT LTZ
 compareP (VS i) (VS j) = compareS $ compareP i j
 
+export
+0 compare2 : Compare {n} i j o -> o = compare i j
+compare2 (IsLT LTZ)      = Refl
+compare2 (IsLT (LTS lt)) = compare2 (IsLT lt)
+compare2 IsEQ            = sym $ compareNatDiag i.nat
+compare2 (IsGT LTZ)      = Refl
+compare2 (IsGT (LTS gt)) = compare2 $ IsGT gt
+compare2 _ {n = 0}       = absurd i
+
 export
 0 compareSelf : Compare i i o -> o = EQ
-compareSelf (IsLT lt) = absurd lt
-compareSelf IsEQ      = Refl
-compareSelf (IsGT gt) = absurd gt
+compareSelf p = rewrite compare2 p in compareNatDiag i.nat
 
 export
 0 comparePSelf : (i : Var n) -> Compare i i EQ
@@ -227,12 +244,19 @@ splitLTE : {j : Var n} -> i `LTE` j -> Either (i = j) (i `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
+  _ | Left  eq = Left  $ cong VS eq
+  _ | Right lt = Right $ LTS lt
 
+export Uninhabited (VS i `LTE` VZ) where uninhabited _ impossible
 
-export Uninhabited (VZ   = VS i) where uninhabited _ impossible
-export Uninhabited (VS i = VZ)   where uninhabited _ impossible
+export
+lteReflect : (i, j : Var n) -> (LTE i j) `Reflects` (i <= j)
+lteReflect VZ     VZ     = RTrue LTEZ
+lteReflect VZ     (VS j) = RTrue LTEZ
+lteReflect (VS i) VZ     = RFalse absurd
+lteReflect (VS i) (VS j) with (lteReflect i j) | (i <= j)
+  _ | RTrue  yes | True  = RTrue (LTES yes)
+  _ | RFalse no  | False = RFalse $ \case LTES lte => no lte
 
 
 public export
@@ -244,11 +268,6 @@ eqReflect (VS i) (VS j) with (eqReflect i j) | (i == j)
   _ | RTrue  yes | True  = RTrue  $ cong VS yes
   _ | RFalse no  | False = RFalse $ no . injective
 
-public export
-reflectToDec : p `Reflects` b -> Dec p
-reflectToDec (RTrue  y) = Yes y
-reflectToDec (RFalse n) = No  n
-
 public export %inline
 varDecEq : (i, j : Var n) -> Dec (i = j)
 varDecEq i j = reflectToDec $ eqReflect i j