some DimEqs properties

src/Quox/Syntax/DimEq.idr

@@ -8,6 +8,9 @@ import public Quox.Context
 import Data.Maybe
 import Data.Nat
 import Data.DPair
+import Data.Fun.Graph
+import Decidable.Decidable
+import Decidable.Equality
 
 %default total
 
@@ -116,18 +119,6 @@ set (B i) (K e) (C eqs) = setConst i e eqs
 set (B i) (B j) (C eqs) = setVar   i j eqs
 
 
-export
-setSelf : (p : Dim d) -> (eqs : DimEq d) -> set p p eqs = eqs
-setSelf p ZeroIsOne = Refl
-setSelf (K Zero) (C eqs) = Refl
-setSelf (K One)  (C eqs) = Refl
-setSelf (B i)    (C eqs) with (compareP i i)
-  _ | IsLT lt = absurd lt
-  _ | IsEQ    = Refl
-  _ | IsGT gt = absurd gt
-
-
-
 public export %inline
 Split : Nat -> Type
 Split d = (DimEq' d, DSubst (S d) d)
@@ -152,3 +143,33 @@ export %inline
 splits : DimEq d -> List (DSubst d 0)
 splits ZeroIsOne = []
 splits (C eqs)   = splits' eqs
+
+
+private
+0 newGetShift : (d : Nat) -> (i : Var d) -> (by : Shift d d') ->
+                getShift' by (new' d) i = Nothing
+newGetShift (S d) VZ     by = Refl
+newGetShift (S d) (VS i) by = newGetShift d i (drop1 by)
+
+export
+0 newGet' : (d : Nat) -> (i : Var d) -> get' (new' d) i = Nothing
+newGet' d i = newGetShift d i SZ
+
+export
+0 newGet : (d : Nat) -> (p : Dim d) -> get (new' d) p = p
+newGet d (K e) = Refl
+newGet d (B i) = rewrite newGet' d i in Refl
+
+
+export
+0 setSelf : (p : Dim d) -> (eqs : DimEq d) -> set p p eqs = eqs
+setSelf p ZeroIsOne = Refl
+setSelf (K Zero) (C eqs) = Refl
+setSelf (K One)  (C eqs) = Refl
+setSelf (B i)    (C eqs) = rewrite comparePSelf i in Refl
+
+
+-- [todo] "well formed" dimeqs
+-- [todo] operations maintain well-formedness
+-- [todo] if 'Wf eqs' then 'equal eqs' is an equivalence
+-- [todo] 'set' never breaks existing equalities