Define zippers and prove no cycles exist.

5 files changed, 165 insertions, 0 deletions

diff --git a/src/Data/Fin/Occurs.idr b/src/Data/Fin/Occurs.idr
index 74199d3..899e2a1 100644
--- a/src/Data/Fin/Occurs.idr
+++ b/src/Data/Fin/Occurs.idr
@@ -9,6 +9,7 @@ import Data.Maybe.Properties
 predInjective : {n : Nat} -> pred n = S k -> n = S (S k)
 predInjective {n = S n} prf = cong S prf
 
+public export
 indexIsSuc : Fin n -> Exists (\k => n = S k)
 indexIsSuc FZ = Evidence _ Refl
 indexIsSuc (FS x) = Evidence _ Refl
diff --git a/src/Data/Term.idr b/src/Data/Term.idr
index 95fd9f8..2afc774 100644
--- a/src/Data/Term.idr
+++ b/src/Data/Term.idr
@@ -72,3 +72,16 @@ subComp :
   (r : Fin j -> Fin k) ->
   f . pure r .=. f . r
 subComp f r i = Refl
+
+-- Injectivity -----------------------------------------------------------------
+
+export
+opInjectiveLen : (prf : Op {k} op ts = Op {k = n} op' us) -> k = n
+opInjectiveLen Refl = Refl
+
+export
+opInjectiveTs :
+  {0 ts : Vect k (Term sig n)} ->
+  {0 us : Vect j (Term sig n)} ->
+  (prf : Op op ts = Op op' us) -> ts = (rewrite opInjectiveLen prf in us)
+opInjectiveTs Refl = Refl
diff --git a/src/Data/Term/Zipper.idr b/src/Data/Term/Zipper.idr
new file mode 100644
index 0000000..09ba2c9
--- /dev/null
+++ b/src/Data/Term/Zipper.idr
@@ -0,0 +1,123 @@
+module Data.Term.Zipper
+
+import Data.DPair
+import Data.Fin.Occurs
+import Data.Vect.Properties.Insert
+import Data.Vect.Properties.Map
+import Data.Term
+import Syntax.PreorderReasoning
+
+-- Definition ------------------------------------------------------------------
+
+public export
+data Zipper : Signature -> Nat -> Type where
+  Top : Zipper sig n
+  Op : sig.Operator (S k) -> Fin (S k) -> Vect k (Term sig n) -> Zipper sig n -> Zipper sig n
+
+%name Zipper zip
+
+-- Monoid ----------------------------------------------------------------------
+
+export
+(++) : Zipper sig n -> Zipper sig n -> Zipper sig n
+Top ++ zip2 = zip2
+Op op i ts zip1 ++ zip2 = Op op i ts (zip1 ++ zip2)
+
+-- Properties
+
+export
+leftUnit : (zip : Zipper sig n) -> Top ++ zip = zip
+leftUnit zip = Refl
+
+export
+rightUnit : (zip : Zipper sig n) -> zip ++ Top = zip
+rightUnit Top = Refl
+rightUnit (Op op i ts zip) = cong (Op op i ts) (rightUnit zip)
+
+export
+assoc : (zip1, zip2, zip3 : Zipper sig n) -> (zip1 ++ zip2) ++ zip3 = zip1 ++ (zip2 ++ zip3)
+assoc Top zip2 zip3 = Refl
+assoc (Op op i ts zip1) zip2 zip3 = cong (Op op i ts) (assoc zip1 zip2 zip3)
+
+-- Action ----------------------------------------------------------------------
+
+export
+(+) : Zipper sig n -> Term sig n -> Term sig n
+Top + t = t
+Op op i ts zip + t = Op op (insertAt i (zip + t) ts)
+
+-- Properties
+
+export
+actionAssoc :
+  (zip1, zip2 : Zipper sig n) ->
+  (t : Term sig n) ->
+  (zip1 ++ zip2) + t = zip1 + (zip2 + t)
+actionAssoc Top zip2 t = Refl
+actionAssoc (Op op i ts zip1) zip2 t =
+  cong (\t => Op op (insertAt i t ts)) $ actionAssoc zip1 zip2 t
+
+-- Substitution ----------------------------------------------------------------
+
+export
+(<$>) : (Fin k -> Term sig n) -> Zipper sig k -> Zipper sig n
+f <$> Top = Top
+f <$> Op op i ts zip = Op op i (map (f <$>) ts) (f <$> zip)
+
+-- Properties
+
+export
+actionHomo :
+  (0 f : Fin k -> Term sig n) ->
+  (zip : Zipper sig k) ->
+  (0 t : Term sig k) ->
+  f <$> zip + t = (f <$> zip) + (f <$> t)
+actionHomo f Top t = Refl
+actionHomo f (Op op i ts zip) t = cong (Op op) $ Calc $
+  |~ map (f <$>) (insertAt i (zip + t) ts)
+  ~~ insertAt i (f <$> zip + t) (map (f <$>) ts)           ...(mapInsertAt (f <$>) i (zip + t) ts)
+  ~~ insertAt i ((f <$> zip) + (f <$> t)) (map (f <$>) ts) ...(cong (\t => insertAt i t (map (f <$>) ts)) $ actionHomo f zip t)
+
+-- Cycles ----------------------------------------------------------------------
+
+pivotAt : sig.Operator k -> Fin k -> Vect k (Term sig n) -> Zipper sig n
+pivotAt op i ts =
+  let op' = replace {p = sig.Operator} (snd prf) op in
+  let i' = replace {p = Fin} (snd prf) i in
+  let ts' = replace {p = flip Vect (Term sig n)} (snd prf) ts in
+  Op op' i' (deleteAt i' ts') Top
+  where
+  prf : Exists (\j => k = S j)
+  prf = indexIsSuc i
+
+actionPivotAt :
+  (op : sig.Operator k) ->
+  (i : Fin k) ->
+  (ts : Vect k (Term sig n)) ->
+  pivotAt op i ts + index i ts = Op op ts
+actionPivotAt op i@FZ ts = cong (Op op) $ insertAtIndex i ts
+actionPivotAt op i@(FS _) ts = cong (Op op) $ insertAtIndex i ts
+
+pivotNotTop : (zip : Zipper sig k) -> Not (zip ++ pivotAt op i ts = Top)
+pivotNotTop (Op op' j us zip) prf impossible
+
+export
+noCycles : (zip : Zipper sig k) -> (t : Term sig k) -> zip + t = t -> zip = Top
+noCycles Top t prf = Refl
+noCycles (Op {k} op i ts zip') t@(Op {k = j} op' us) prf =
+  void $ pivotNotTop zip' prf''
+  where
+  I : Fin j
+  I = replace {p = Fin} (opInjectiveLen prf) i
+
+  prf' : ((zip' ++ pivotAt op' I us) + index I us = index I us)
+  prf' = Calc $
+    |~ (zip' ++ pivotAt op' I us) + index I us
+    ~~ zip' + (pivotAt op' I us + index I us)      ...(actionAssoc zip' (pivotAt op' I us) (index I us))
+    ~~ zip' + Op op' us                            ...(cong (zip' +) $ actionPivotAt op' I us)
+    ~~ index i (insertAt i (zip' + Op op' us) ts)  ..<(indexInsertAt i (zip' + Op op' us) ts)
+    ~~ index i (rewrite opInjectiveLen prf in us)  ...(cong (index i) $ opInjectiveTs prf)
+    ~~ index I us                                  ...(rewrite opInjectiveLen prf in Refl)
+
+  prf'' : zip' ++ pivotAt op' I us = Top
+  prf'' = noCycles (zip' ++ pivotAt op' I us) (assert_smaller t (index I us)) prf'
diff --git a/src/Data/Vect/Properties/Insert.idr b/src/Data/Vect/Properties/Insert.idr
new file mode 100644
index 0000000..28393b1
--- /dev/null
+++ b/src/Data/Vect/Properties/Insert.idr
@@ -0,0 +1,26 @@
+module Data.Vect.Properties.Insert
+
+import Data.Vect
+
+export
+mapInsertAt :
+  (0 f : a -> b) ->
+  (i : Fin (S n)) ->
+  (0 x : a) ->
+  (xs : Vect n a) ->
+  map f (insertAt i x xs) = insertAt i (f x) (map f xs)
+mapInsertAt f FZ x xs = Refl
+mapInsertAt f (FS i) x (y :: xs) = cong (f y ::) $ mapInsertAt f i x xs
+
+export
+indexInsertAt : (i : Fin (S n)) -> (0 x : a) -> (xs : Vect n a) -> index i (insertAt i x xs) = x
+indexInsertAt FZ x xs = Refl
+indexInsertAt (FS i) x (y :: xs) = indexInsertAt i x xs
+
+export
+insertAtIndex :
+  (i : Fin (S n)) ->
+  (xs : Vect (S n) a) ->
+  insertAt i (index i xs) (deleteAt i xs) = xs
+insertAtIndex FZ (x :: xs) = Refl
+insertAtIndex (FS i) (x :: xs@(_ :: _)) = cong (x ::) $ insertAtIndex i xs
diff --git a/unify.ipkg b/unify.ipkg
index 7b0e0dd..060368f 100644
--- a/unify.ipkg
+++ b/unify.ipkg
@@ -10,3 +10,5 @@ modules
   = Data.Fin.Occurs
   , Data.Maybe.Properties
   , Data.Term
+  , Data.Term.Zipper
+  , Data.Vect.Properties.Insert