1 files changed, 284 insertions, 1 deletions
diff --git a/src/Total/Term.idr b/src/Total/Term.idr
index 22a9a39..1530981 100644
--- a/src/Total/Term.idr
+++ b/src/Total/Term.idr
@@ -2,6 +2,7 @@ module Total.Term
 
 import public Data.SnocList.Elem
 import public Thinning
+import Syntax.PreorderReasoning
 
 %prefix_record_projections off
 
@@ -25,6 +26,7 @@ data Term : SnocList Ty -> Ty -> Type where
 
 %name Term t, u, v
 
+public export
 wkn : Term ctx ty -> ctx `Thins` ctx' -> Term ctx' ty
 wkn (Var i) thin = Var (index thin i)
 wkn (Abs t) thin = Abs (wkn t $ keep thin)
@@ -40,16 +42,18 @@ data Terms : SnocList Ty -> SnocList Ty -> Type where
 
 %name Terms sub
 
+public export
 index : Terms ctx' ctx -> Elem ty ctx -> Term ctx' ty
 index (Base thin) i = Var (index thin i)
 index (sub :< t) Here = t
 index (sub :< t) (There i) = index sub i
 
+public export
 wknAll : Terms ctx' ctx -> ctx' `Thins` ctx'' -> Terms ctx'' ctx
 wknAll (Base thin') thin = Base (thin . thin')
 wknAll (sub :< t) thin = wknAll sub thin :< wkn t thin
 
-export
+public export
 subst : Term ctx ty -> Terms ctx' ctx -> Term ctx' ty
 subst (Var i) sub = index sub i
 subst (Abs t) sub = Abs (subst t $ wknAll sub (Drop Id) :< Var Here)
@@ -58,12 +62,291 @@ subst Zero sub = Zero
 subst (Suc t) sub = Suc (subst t sub)
 subst (Rec t u v) sub = Rec (subst t sub) (subst u sub) (subst v sub)
 
+public export
 restrict : Terms ctx'' ctx' -> ctx `Thins` ctx' -> Terms ctx'' ctx
 restrict (Base thin') thin = Base (thin' . thin)
 restrict (sub :< t) Id = sub :< t
 restrict (sub :< t) (Drop thin) = restrict sub thin
 restrict (sub :< t) (Keep thin) = restrict sub thin :< t
 
+public export
 (.) : Terms ctx'' ctx' -> Terms ctx' ctx -> Terms ctx'' ctx
 sub2 . (Base thin) = restrict sub2 thin
 sub2 . (sub1 :< t) = sub2 . sub1 :< subst t sub2
+
+-- Properties ------------------------------------------------------------------
+
+-- Utilities
+
+cong3 : (0 f : a -> b -> c -> d) -> x1 = x2 -> y1 = y2 -> z1 = z2 -> f x1 y1 z1 = f x2 y2 z2
+cong3 f Refl Refl Refl = Refl
+
+-- Weakening
+
+export
+wknHomo :
+  (t : Term ctx ty) ->
+  (thin1 : ctx `Thins` ctx') ->
+  (thin2 : ctx' `Thins` ctx'') ->
+  wkn (wkn t thin1) thin2 = wkn t (thin2 . thin1)
+wknHomo (Var i) thin1 thin2 =
+  cong Var (indexHomo thin2 thin1 i)
+wknHomo (Abs t) thin1 thin2 =
+  cong Abs $ trans (wknHomo t (keep thin1) (keep thin2)) (cong (wkn t) $ keepHomo thin2 thin1)
+wknHomo (App t u) thin1 thin2 =
+  cong2 App (wknHomo t thin1 thin2) (wknHomo u thin1 thin2)
+wknHomo Zero thin1 thin2 =
+  Refl
+wknHomo (Suc t) thin1 thin2 =
+  cong Suc (wknHomo t thin1 thin2)
+wknHomo (Rec t u v) thin1 thin2 =
+  cong3 Rec (wknHomo t thin1 thin2) (wknHomo u thin1 thin2) (wknHomo v thin1 thin2)
+
+export
+wknId : (t : Term ctx ty) -> wkn t Id = t
+wknId (Var i) = Refl
+wknId (Abs t) = cong Abs (wknId t)
+wknId (App t u) = cong2 App (wknId t) (wknId u)
+wknId Zero = Refl
+wknId (Suc t) = cong Suc (wknId t)
+wknId (Rec t u v) = cong3 Rec (wknId t) (wknId u) (wknId v)
+
+indexWknAll :
+  (sub : Terms ctx' ctx) ->
+  (thin : ctx' `Thins` ctx'') ->
+  (i : Elem ty ctx) ->
+  index (wknAll sub thin) i = wkn (index sub i) thin
+indexWknAll (Base thin') thin i = sym $ cong Var $ indexHomo thin thin' i
+indexWknAll (sub :< t) thin Here = Refl
+indexWknAll (sub :< t) thin (There i) = indexWknAll sub thin i
+
+wknAllHomo :
+  (sub : Terms ctx ctx''') ->
+  (thin1 : ctx `Thins` ctx') ->
+  (thin2 : ctx' `Thins` ctx'') ->
+  wknAll (wknAll sub thin1) thin2 = wknAll sub (thin2 . thin1)
+wknAllHomo (Base thin) thin1 thin2 = cong Base (assoc thin2 thin1 thin)
+wknAllHomo (sub :< t) thin1 thin2 = cong2 (:<) (wknAllHomo sub thin1 thin2) (wknHomo t thin1 thin2)
+
+-- Restrict
+
+indexRestrict :
+  (thin : ctx `Thins` ctx') ->
+  (sub : Terms ctx'' ctx') ->
+  (i : Elem ty ctx) ->
+  index (restrict sub thin) i = index sub (index thin i)
+indexRestrict thin (Base thin') i = sym $ cong Var $ indexHomo thin' thin i
+indexRestrict Id (sub :< t) i = Refl
+indexRestrict (Drop thin) (sub :< t) i = indexRestrict thin sub i
+indexRestrict (Keep thin) (sub :< t) Here = Refl
+indexRestrict (Keep thin) (sub :< t) (There i) = indexRestrict thin sub i
+
+restrictId : (sub : Terms ctx' ctx) -> restrict sub Id = sub
+restrictId (Base thin) = cong Base (identityRight thin)
+restrictId (sub :< t) = Refl
+
+export
+restrictKeep :
+  (sub : Terms ctx'' ctx) ->
+  (t : Term ctx'' ty) ->
+  (thin : ctx' `Thins` ctx) ->
+  restrict (sub :< t) (keep thin) = restrict sub thin :< t
+restrictKeep sub t Id = sym $ cong (:< t) $ restrictId sub
+restrictKeep sub t (Drop thin) = Refl
+restrictKeep sub t (Keep thin) = Refl
+
+restrictHomo :
+  (sub : Terms ctx ctx''') ->
+  (thin1 : ctx'' `Thins` ctx''') ->
+  (thin2 : ctx' `Thins` ctx'') ->
+  restrict sub (thin1 . thin2) = restrict (restrict sub thin1) thin2
+restrictHomo (Base thin) thin1 thin2 = cong Base (assoc thin thin1 thin2)
+restrictHomo (sub :< t) Id thin2 = Refl
+restrictHomo (sub :< t) (Drop thin1) thin2 = restrictHomo sub thin1 thin2
+restrictHomo (sub :< t) (Keep thin1) Id = Refl
+restrictHomo (sub :< t) (Keep thin1) (Drop thin2) = restrictHomo sub thin1 thin2
+restrictHomo (sub :< t) (Keep thin1) (Keep thin2) = cong (:< t) $ restrictHomo sub thin1 thin2
+
+wknAllRestrict :
+  (thin1 : ctx `Thins` ctx') ->
+  (sub : Terms ctx'' ctx') ->
+  (thin2 : ctx'' `Thins` ctx''') ->
+  restrict (wknAll sub thin2) thin1 = wknAll (restrict sub thin1) thin2
+wknAllRestrict thin1 (Base thin) thin2 = sym $ cong Base $ assoc thin2 thin thin1
+wknAllRestrict Id (sub :< t) thin2 = Refl
+wknAllRestrict (Drop thin) (sub :< t) thin2 = wknAllRestrict thin sub thin2
+wknAllRestrict (Keep thin) (sub :< t) thin2 = cong (:< wkn t thin2) (wknAllRestrict thin sub thin2)
+
+-- Substitution & Weakening
+
+export
+wknSubst :
+  (t : Term ctx ty) ->
+  (sub : Terms ctx' ctx) ->
+  (thin : ctx' `Thins` ctx'') ->
+  wkn (subst t sub) thin = subst t (wknAll sub thin)
+wknSubst (Var i) sub thin =
+  sym (indexWknAll sub thin i)
+wknSubst (Abs t) sub thin =
+  cong Abs $ Calc $
+    |~ wkn (subst t (wknAll sub (Drop Id) :< Var Here)) (keep thin)
+    ~~ subst t (wknAll (wknAll sub (Drop Id)) (keep thin) :< Var (index (keep thin) Here))
+      ...(wknSubst t (wknAll sub (Drop Id) :< Var Here) (keep thin))
+    ~~ subst t (wknAll sub (keep thin . Drop Id) :< Var Here)
+      ...(cong2 (\sub, i => subst t (sub :< Var i)) (wknAllHomo sub (Drop Id) (keep thin)) (indexKeepHere thin))
+    ~~ subst t (wknAll sub (Drop Id . thin) :< Var Here)
+      ...(cong (subst t . (:< Var Here) . wknAll sub) $ trans (keepDrop thin Id) (cong Drop $ identityRight thin))
+    ~~ subst t (wknAll (wknAll sub thin) (Drop Id) :< Var Here)
+      ...(sym $ cong (subst t . (:< Var Here)) $ wknAllHomo sub thin (Drop Id))
+wknSubst (App t u) sub thin =
+  cong2 App (wknSubst t sub thin) (wknSubst u sub thin)
+wknSubst Zero sub thin =
+  Refl
+wknSubst (Suc t) sub thin =
+  cong Suc (wknSubst t sub thin)
+wknSubst (Rec t u v) sub thin =
+  cong3 Rec (wknSubst t sub thin) (wknSubst u sub thin) (wknSubst v sub thin)
+
+export
+substWkn :
+  (t : Term ctx ty) ->
+  (thin : ctx `Thins` ctx') ->
+  (sub : Terms ctx'' ctx') ->
+  subst (wkn t thin) sub = subst t (restrict sub thin)
+substWkn (Var i) thin sub =
+  sym (indexRestrict thin sub i)
+substWkn (Abs t) thin sub =
+  cong Abs $ Calc $
+    |~ subst (wkn t $ keep thin) (wknAll sub (Drop Id) :< Var Here)
+    ~~ subst t (restrict (wknAll sub (Drop Id) :< Var Here) (keep thin))
+      ...(substWkn t (keep thin) (wknAll sub (Drop Id) :< Var Here))
+    ~~ subst t (restrict (wknAll sub (Drop Id)) thin :< Var Here)
+      ...(cong (subst t) $ restrictKeep (wknAll sub (Drop Id)) (Var Here) thin)
+    ~~ subst t (wknAll (restrict sub thin) (Drop Id) :< Var Here)
+      ...(cong (subst t . (:< Var Here)) $ wknAllRestrict thin sub (Drop Id))
+substWkn (App t u) thin sub =
+  cong2 App (substWkn t thin sub) (substWkn u thin sub)
+substWkn Zero thin sub =
+  Refl
+substWkn (Suc t) thin sub =
+  cong Suc (substWkn t thin sub)
+substWkn (Rec t u v) thin sub =
+  cong3 Rec (substWkn t thin sub) (substWkn u thin sub) (substWkn v thin sub)
+
+namespace Equiv
+  public export
+  data Equiv : Terms ctx' ctx -> Terms ctx' ctx -> Type where
+    Base : Equiv (Base (keep thin)) (Base (Drop thin) :< Var Here)
+    WknAll :
+      Equiv sub sub' ->
+      Equiv (wknAll sub (Drop Id) :< Var Here) (wknAll sub' (Drop Id) :< Var Here)
+
+  %name Equiv prf
+
+indexCong : Equiv sub sub' -> (i : Elem ty ctx) -> index sub i = index sub' i
+indexCong Base Here = irrelevantEq $ cong Var (indexKeepHere _)
+indexCong Base (There i) = irrelevantEq $ cong Var (indexKeepThere _ i)
+indexCong (WknAll prf) Here = Refl
+indexCong (WknAll {sub, sub'} prf) (There i) = Calc $
+  |~ index (wknAll sub (Drop Id)) i
+  ~~ wkn (index sub i) (Drop Id)     ...(indexWknAll sub (Drop Id) i)
+  ~~ wkn (index sub' i) (Drop Id)    ...(cong (flip wkn (Drop Id)) $ indexCong prf i)
+  ~~ index (wknAll sub' (Drop Id)) i ...(sym $ indexWknAll sub' (Drop Id) i)
+
+substCong : (t : Term ctx ty) -> Equiv sub sub' -> subst t sub = subst t sub'
+substCong (Var i) prf = indexCong prf i
+substCong (Abs t) prf = cong Abs (substCong t (WknAll prf))
+substCong (App t u) prf = cong2 App (substCong t prf) (substCong u prf)
+substCong Zero prf = Refl
+substCong (Suc t) prf = cong Suc (substCong t prf)
+substCong (Rec t u v) prf = cong3 Rec (substCong t prf) (substCong u prf) (substCong v prf)
+
+substBase : (t : Term ctx ty) -> (thin : ctx `Thins` ctx') -> subst t (Base thin) = wkn t thin
+substBase (Var i) thin = Refl
+substBase (Abs t) thin = cong Abs $ Calc $
+  |~ subst t (Base (Drop thin) :< Var Here)
+  ~~ subst t (Base $ keep thin)             ...(sym $ substCong t Base)
+  ~~ wkn t (keep thin)                      ...(substBase t (keep thin))
+substBase (App t u) thin = cong2 App (substBase t thin) (substBase u thin)
+substBase Zero thin = Refl
+substBase (Suc t) thin = cong Suc (substBase t thin)
+substBase (Rec t u v) thin = cong3 Rec (substBase t thin) (substBase u thin) (substBase v thin)
+
+-- Substitution Composition
+
+indexComp :
+  (sub1 : Terms ctx' ctx) ->
+  (sub2 : Terms ctx'' ctx') ->
+  (i : Elem ty ctx) ->
+  index (sub2 . sub1) i = subst (index sub1 i) sub2
+indexComp (Base thin) sub2 i = indexRestrict thin sub2 i
+indexComp (sub1 :< t) sub2 Here = Refl
+indexComp (sub1 :< t) sub2 (There i) = indexComp sub1 sub2 i
+
+wknAllComp :
+  (sub1 : Terms ctx' ctx) ->
+  (sub2 : Terms ctx'' ctx') ->
+  (thin : ctx'' `Thins` ctx''') ->
+  wknAll sub2 thin . sub1 = wknAll (sub2 . sub1) thin
+wknAllComp (Base thin') sub2 thin = wknAllRestrict thin' sub2 thin
+wknAllComp (sub1 :< t) sub2 thin =
+  cong2 (:<)
+    (wknAllComp sub1 sub2 thin)
+    (sym $ wknSubst t sub2 thin)
+
+compDrop :
+  (sub1 : Terms ctx' ctx) ->
+  (thin : ctx' `Thins` ctx'') ->
+  (sub2 : Terms ctx''' ctx'') ->
+  sub2 . wknAll sub1 thin = restrict sub2 thin . sub1
+compDrop (Base thin') thin sub2 = restrictHomo sub2 thin thin'
+compDrop (sub1 :< t) thin sub2 = cong2 (:<) (compDrop sub1 thin sub2) (substWkn t thin sub2)
+
+export
+compWknAll :
+  (sub1 : Terms ctx' ctx) ->
+  (sub2 : Terms ctx''' ctx'') ->
+  (thin : ctx' `Thins` ctx'') ->
+  sub2 . wknAll sub1 thin = restrict sub2 thin . sub1
+compWknAll (Base thin') sub2 thin = restrictHomo sub2 thin thin'
+compWknAll (sub1 :< t) sub2 thin = cong2 (:<) (compWknAll sub1 sub2 thin) (substWkn t thin sub2)
+
+export
+baseComp :
+  (thin : ctx' `Thins` ctx'') ->
+  (sub : Terms ctx' ctx) ->
+  Base thin . sub = wknAll sub thin
+baseComp thin (Base thin') = Refl
+baseComp thin (sub :< t) = cong2 (:<) (baseComp thin sub) (substBase t thin)
+
+-- Substitution
+
+export
+substHomo :
+  (t : Term ctx ty) ->
+  (sub1 : Terms ctx' ctx) ->
+  (sub2 : Terms ctx'' ctx') ->
+  subst (subst t sub1) sub2 = subst t (sub2 . sub1)
+substHomo (Var i) sub1 sub2 =
+  sym $ indexComp sub1 sub2 i
+substHomo (Abs t) sub1 sub2 =
+  cong Abs $ Calc $
+    |~ subst (subst t (wknAll sub1 (Drop Id) :< Var Here)) (wknAll sub2 (Drop Id) :< Var Here)
+    ~~ subst t ((wknAll sub2 (Drop Id) :< Var Here) . (wknAll sub1 (Drop Id) :< Var Here))
+      ...(substHomo t (wknAll sub1 (Drop Id) :< Var Here) (wknAll sub2 (Drop Id) :< Var Here))
+    ~~ subst t ((wknAll sub2 (Drop Id) :< Var Here) . wknAll sub1 (Drop Id) :< Var Here)
+      ...(Refl)
+    ~~ subst t (restrict (wknAll sub2 (Drop Id)) Id . sub1 :< Var Here)
+      ...(cong (subst t . (:< Var Here)) $ compDrop sub1 (Drop Id) (wknAll sub2 (Drop Id) :< Var Here))
+    ~~ subst t (wknAll sub2 (Drop Id) . sub1 :< Var Here)
+      ...(cong (subst t . (:< Var Here) . (. sub1)) $ restrictId (wknAll sub2 (Drop Id)))
+    ~~ subst t (wknAll (sub2 . sub1) (Drop Id) :< Var Here)
+      ...(cong (subst t . (:< Var Here)) $ wknAllComp sub1 sub2 (Drop Id))
+substHomo (App t u) sub1 sub2 =
+  cong2 App (substHomo t sub1 sub2) (substHomo u sub1 sub2)
+substHomo Zero sub1 sub2 =
+  Refl
+substHomo (Suc t) sub1 sub2 =
+  cong Suc (substHomo t sub1 sub2)
+substHomo (Rec t u v) sub1 sub2 =
+  cong3 Rec (substHomo t sub1 sub2) (substHomo u sub1 sub2) (substHomo v sub1 sub2)