Remove SFin.

Delete unused modules.

Restructure some proofs to reduce the number of lemmas.

1 files changed, 37 insertions, 51 deletions

diff --git a/src/Data/Term/Zipper.idr b/src/Data/Term/Zipper.idr
index ddc0797..05cdfc9 100644
--- a/src/Data/Term/Zipper.idr
+++ b/src/Data/Term/Zipper.idr
@@ -2,44 +2,33 @@ module Data.Term.Zipper
 
 import Data.DPair
 import Data.Fin.Occurs
-import Data.Fin.Strong
 import Data.Vect.Properties.Map
 import Data.Term
 import Syntax.PreorderReasoning
 
 -- Utilities -------------------------------------------------------------------
 
-public export
-insertAt' : SFin k -> a -> Vect (pred k) a -> Vect k a
-insertAt' FZ x xs = x :: xs
-insertAt' (FS i) x (y :: xs) = y :: insertAt' i x xs
-
-public export
-deleteAt' : SFin k -> Vect k a -> Vect (pred k) a
-deleteAt' FZ (x :: xs) = xs
-deleteAt' (FS i) (x :: xs) = x :: deleteAt' i xs
-
 mapInsertAt :
   (0 f : a -> b) ->
-  (i : SFin k) ->
+  (i : Fin (S k)) ->
   (x : a) ->
-  (xs : Vect (pred k) a) ->
-  map f (insertAt' i x xs) = insertAt' i (f x) (map f xs)
+  (xs : Vect k 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
 
 insertAtDeleteAt :
-  (i : SFin k) ->
-  (xs : Vect k a) ->
-  insertAt' i (index (strongToFin i) xs) (deleteAt' i xs) = xs
+  (i : Fin (S k)) ->
+  (xs : Vect (S k) a) ->
+  insertAt i (index i xs) (deleteAt i xs) = xs
 insertAtDeleteAt FZ (x :: xs) = Refl
-insertAtDeleteAt (FS i) (x :: xs) = cong (x ::) $ insertAtDeleteAt i xs
+insertAtDeleteAt (FS i) (x :: xs@(_ :: _)) = cong (x ::) $ insertAtDeleteAt i xs
 
 indexInsertAt :
-  (i : SFin k) ->
+  (i : Fin (S k)) ->
   (x : a) ->
-  (xs : Vect (pred k) a) ->
-  index (strongToFin i) (insertAt' i x xs) = x
+  (xs : Vect k a) ->
+  index i (insertAt i x xs) = x
 indexInsertAt FZ x xs = Refl
 indexInsertAt (FS i) x (y :: xs) = indexInsertAt i x xs
 
@@ -48,7 +37,7 @@ indexInsertAt (FS i) x (y :: xs) = indexInsertAt i x xs
 public export
 data Zipper : Signature -> Nat -> Type where
   Top : Zipper sig n
-  Op : sig.Operator k -> SFin k -> Vect (pred k) (Term sig n) -> Zipper sig n -> 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
 
@@ -81,7 +70,7 @@ assoc (Op op i ts zip1) zip2 zip3 = cong (Op op i ts) (assoc zip1 zip2 zip3)
 public 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)
+Op op i ts zip + t = Op op (insertAt i (zip + t) ts)
 
 -- Properties
 
@@ -92,12 +81,12 @@ actionAssoc :
   (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
+  cong (\t => Op op (insertAt i t ts)) $ actionAssoc zip1 zip2 t
 
 -- Substitution ----------------------------------------------------------------
 
 export
-(<$>) : (SFin k -> Term sig n) -> Zipper sig k -> Zipper sig n
+(<$>) : (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)
 
@@ -105,15 +94,15 @@ f <$> Op op i ts zip = Op op i (map (f <$>) ts) (f <$> zip)
 
 export
 actionHomo :
-  (0 f : SFin k -> Term sig n) ->
+  (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)
+  |~ 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)
 
 export
 invertActionTop : (zip : Zipper sig k) -> (0 _ : f <$> zip = Top) -> zip = Top
@@ -121,14 +110,14 @@ invertActionTop Top prf = Refl
 
 -- Cycles ----------------------------------------------------------------------
 
-pivotAt : sig.Operator k -> SFin k -> Vect k (Term sig n) -> Zipper sig n
-pivotAt op i ts = Op op i (deleteAt' i ts) Top
+pivotAt : sig.Operator (S k) -> Fin (S k) -> Vect (S k) (Term sig n) -> Zipper sig n
+pivotAt op i ts = Op op i (deleteAt i ts) Top
 
 actionPivotAt :
-  (op : sig.Operator k) ->
-  (i : SFin k) ->
-  (ts : Vect k (Term sig n)) ->
-  pivotAt op i ts + index (strongToFin i) ts = Op op ts
+  (op : sig.Operator (S k)) ->
+  (i : Fin (S k)) ->
+  (ts : Vect (S k) (Term sig n)) ->
+  pivotAt op i ts + index i ts = Op op ts
 actionPivotAt op i ts = cong (Op op) $ insertAtDeleteAt i ts
 
 pivotNotTop : (zip : Zipper sig k) -> Not (zip ++ pivotAt op i ts = Top)
@@ -137,26 +126,23 @@ 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 =
+noCycles (Op {k} op i ts zip') t@(Op {k = S j} op' us@(_ :: _)) prf =
   void $ pivotNotTop zip' prf''
   where
-  i' : Fin k
-  i' = strongToFin i
-
-  I : SFin j
-  I = replace {p = SFin} (opInjectiveLen prf) i
+  i' : Fin (S k)
+  i' = i
 
-  I' : Fin j
-  I' = strongToFin I
+  I : Fin (S j)
+  I = replace {p = Fin} (opInjectiveLen prf) i
 
-  prf' : ((zip' ++ pivotAt op' I us) + index I' us = index I' us)
+  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)
+    |~ (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'
+  prf'' = noCycles (zip' ++ pivotAt op' I us) (assert_smaller t (index I us)) prf'