add Injective instances, etc

src/Quox/Syntax/Dim.idr

@@ -4,6 +4,9 @@ import Quox.Syntax.Var
 import Quox.Syntax.Subst
 import Quox.Pretty
 
+import Decidable.Equality
+import Control.Function
+
 %default total
 
 
@@ -70,3 +73,31 @@ export
 CanSubst Dim Dim where
   K e // _  = K e
   B i // th = th !! i
+
+
+export Uninhabited (Zero = One)  where uninhabited _ impossible
+export Uninhabited (One  = Zero) where uninhabited _ impossible
+
+export Uninhabited (B i = K e) where uninhabited _ impossible
+export Uninhabited (K e = B i) where uninhabited _ impossible
+
+public export %inline Injective B where injective Refl = Refl
+public export %inline Injective K where injective Refl = Refl
+
+public export
+DecEq DimConst where
+  decEq Zero Zero = Yes Refl
+  decEq Zero One  = No absurd
+  decEq One  Zero = No absurd
+  decEq One  One  = Yes Refl
+
+public export
+DecEq (Dim d) where
+  decEq (K e) (K f) with (decEq e f)
+    _ | Yes prf    = Yes $ cong K prf
+    _ | No  contra = No  $ contra . injective
+  decEq (K e) (B j) = No absurd
+  decEq (B i) (K f) = No absurd
+  decEq (B i) (B j) with (decEq i j)
+    _ | Yes prf    = Yes $ cong B prf
+    _ | No  contra = No  $ contra . injective

src/Quox/Syntax/Shift.idr

@@ -89,8 +89,11 @@ toNatInj' (SS by) (SS bz) prf = EqSS $ toNatInj' by bz $ injective prf
 toNatInj' (SS by) SZ      Refl impossible
 
 export
-0 toNatInj : (by, bz : Shift from to) -> by.nat = bz.nat -> by = bz
-toNatInj by bz e = fromEqv $ toNatInj' by bz e
+0 toNatInj : {by, bz : Shift from to} -> by.nat = bz.nat -> by = bz
+toNatInj {by, bz} e = fromEqv $ toNatInj' by bz e
+
+export %inline
+Injective Shift.(.nat) where injective eq = irrelevantEq $ toNatInj eq
 
 
 public export

src/Quox/Syntax/Var.idr

@@ -1,11 +1,13 @@
 module Quox.Syntax.Var
 
 import Quox.Name
+import Quox.Pretty
+import Quox.OPE
 
 import Data.Nat
-import Data.Maybe
 import Data.List
-import Quox.Pretty
+import Decidable.Equality
+import Data.Bool.Decidable
 
 %default total
 
@@ -30,6 +32,8 @@ export %inline Eq   (Var n) where i == j = i.nat == j.nat
 export %inline Ord  (Var n) where compare i j = compare i.nat j.nat
 export %inline Show (Var n) where showPrec d i = showCon d "V" $ showArg i.nat
 
+public export %inline Injective VS where injective Refl = Refl
+
 
 parameters {auto _ : Pretty.HasEnv m}
   private
@@ -81,13 +85,14 @@ export
 toNatLT VZ     = LTESucc LTEZero
 toNatLT (VS i) = LTESucc $ toNatLT i
 
-export
-0 toNatInj : {i, j : Var n} -> i.nat = j.nat -> i = j
+public export
+toNatInj : {i, j : Var n} -> i.nat = j.nat -> i = j
 toNatInj {i = VZ}     {j = VZ}     Refl = Refl
 toNatInj {i = VZ}     {j = (VS i)} Refl impossible
 toNatInj {i = (VS i)} {j = VZ}     Refl impossible
-toNatInj {i = (VS i)} {j = (VS j)} prf  =
-  cong VS $ toNatInj $ succInjective _ _ prf
+toNatInj {i = (VS i)} {j = (VS j)} prf  = cong VS $ toNatInj $ injective prf
+
+public export %inline Injective (.nat) where injective = toNatInj
 
 export
 0 fromToNat : (i : Var n) -> (p : i.nat `LT` n) -> fromNatWith i.nat p = i
@@ -223,3 +228,38 @@ splitLTE {j = VS _} LTEZ     = Right LTZ
 splitLTE            (LTES p) with (splitLTE p)
   _ | (Left  eq) = Left $ cong VS eq
   _ | (Right lt) = Right $ LTS lt
+
+
+export Uninhabited (VZ   = VS i) where uninhabited _ impossible
+export Uninhabited (VS i = VZ)   where uninhabited _ impossible
+
+
+public export
+eqReflect : (i, j : Var n) -> (i = j) `Reflects` (i == j)
+eqReflect VZ     VZ     = RTrue  Refl
+eqReflect VZ     (VS i) = RFalse absurd
+eqReflect (VS i) VZ     = RFalse absurd
+eqReflect (VS i) (VS j) with (eqReflect i j)
+  eqReflect (VS i) (VS j) | r with (i == j)
+    eqReflect (VS i) (VS j) | RTrue  yes | True   =  RTrue  $ cong VS yes
+    eqReflect (VS i) (VS j) | 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
+
+-- justified by eqReflect [citation needed]
+private %inline
+decEqFromBool : (i, j : Var n) -> Dec (i = j)
+decEqFromBool i j =
+  if i == j then Yes $ believe_me $ Refl {x = 0}
+            else No  $ id . believe_me
+
+%transform "Var.decEq" varDecEq = decEqFromBool
+
+public export %inline DecEq (Var n) where decEq = varDecEq