Prove substitution respects the quotient.

4 files changed, 116 insertions, 11 deletions

diff --git a/src/Core/Term.idr b/src/Core/Term.idr
index 1b050ca..74ef7af 100644
--- a/src/Core/Term.idr
+++ b/src/Core/Term.idr
@@ -27,3 +27,24 @@ wkn Set thin = Set
 wkn (Pi t u) thin = Pi (wkn t thin) (wkn u $ keep thin)
 wkn (Abs t) thin = Abs (wkn t $ keep thin)
 wkn (App t u) thin = App (wkn t thin) (wkn u thin)
+
+export
+wknHomo :
+  (t : Term k) ->
+  (thin1 : k `Thins` m) ->
+  (thin2 : m `Thins` n) ->
+  wkn (wkn t thin1) thin2 = wkn t (thin2 . thin1)
+wknHomo (Var i) thin1 thin2 = cong Var (wknHomo i thin1 thin2)
+wknHomo Set thin1 thin2 = Refl
+wknHomo (Pi t u) thin1 thin2 =
+  cong2 Pi
+    (wknHomo t thin1 thin2)
+    (trans
+      (wknHomo u (keep thin1) (keep thin2))
+      (cong (wkn u) $ compKeep thin2 thin1))
+wknHomo (Abs t) thin1 thin2 =
+  cong Abs
+    (trans
+      (wknHomo t (keep thin1) (keep thin2))
+      (cong (wkn t) $ compKeep thin2 thin1))
+wknHomo (App t u) thin1 thin2 = cong2 App (wknHomo t thin1 thin2) (wknHomo u thin1 thin2)
diff --git a/src/Core/Term/Substitution.idr b/src/Core/Term/Substitution.idr
index 6846d80..abeb487 100644
--- a/src/Core/Term/Substitution.idr
+++ b/src/Core/Term/Substitution.idr
@@ -30,6 +30,16 @@ index (Wkn thin) i = Var i `Over` thin
 index (sub :< t) FZ = t
 index (sub :< t) (FS i) = index sub i
 
+export
+indexCong :
+  {0 sub1, sub2 : Subst m n} ->
+  sub1 =~= sub2 ->
+  (i : Fin m) ->
+  index sub1 i =~= index sub2 i
+indexCong Refl i = Refl
+indexCong (prf :< prf') FZ = prf'
+indexCong (prf :< prf') (FS i) = indexCong prf i
+
 -- Weakening -------------------------------------------------------------------
 
 public export
@@ -37,6 +47,15 @@ wkn : Subst k m -> m `Thins` n -> Subst k n
 wkn (Wkn thin') thin = Wkn (thin . thin')
 wkn (sub :< t) thin = wkn sub thin :< wkn t thin
 
+export
+wknCong :
+  {0 sub1, sub2 : Subst k m} ->
+  sub1 =~= sub2 ->
+  (thin : m `Thins` n) ->
+  wkn sub1 thin =~= wkn sub2 thin
+wknCong Refl thin = Refl
+wknCong (prf :< prf') thin = wknCong prf thin :< wknCong prf' thin
+
 -- Constructors ----------------------------------------------------------------
 
 public export
@@ -52,3 +71,18 @@ subst Set sub = Set
 subst (Pi t u) sub = Pi (subst t sub) (subst u $ lift sub)
 subst (Abs t) sub = Abs (subst t $ lift sub)
 subst (App t u) sub = App (subst t sub) (subst u sub)
+
+export
+substCong :
+  (t : Term m) ->
+  {0 sub1, sub2 : Subst m n} ->
+  sub1 =~= sub2 ->
+  subst t sub1 = subst t sub2
+substCong (Var i) prf = indexCong prf i
+substCong Set prf = Refl
+substCong (Pi t u) prf =
+  cong2 Pi
+    (substCong t prf)
+    (substCong u $ wknCong prf (drop $ id n) :< Refl)
+substCong (Abs t) prf = cong Abs (substCong t $ wknCong prf (drop $ id n) :< Refl)
+substCong (App t u) prf = cong2 App (substCong t prf) (substCong u prf)
diff --git a/src/Core/Term/Thinned.idr b/src/Core/Term/Thinned.idr
index 0bc6dcf..824439a 100644
--- a/src/Core/Term/Thinned.idr
+++ b/src/Core/Term/Thinned.idr
@@ -3,6 +3,8 @@ module Core.Term.Thinned
 import Core.Term
 import Core.Thinning
 
+import Syntax.PreorderReasoning
+
 %prefix_record_projections off
 
 infix 4 =~=
@@ -32,3 +34,11 @@ t =~= u = expand t = expand u
 public export
 wkn : Thinned m -> m `Thins` n -> Thinned n
 wkn t thin = { thin $= (thin .) } t
+
+export
+wknCong : t =~= u -> (thin : m `Thins` n) -> wkn t thin =~= wkn u thin
+wknCong {t = t `Over` thin1, u = u `Over` thin2} prf thin = Calc $
+  |~ wkn t (thin . thin1)
+  ~~ wkn (wkn t thin1) thin ...(sym $ wknHomo t thin1 thin)
+  ~~ wkn (wkn u thin2) thin ...(cong (flip wkn thin) prf)
+  ~~ wkn u (thin . thin2)   ...(wknHomo u thin2 thin)
diff --git a/src/Core/Thinning.idr b/src/Core/Thinning.idr
index a2500e9..959702d 100644
--- a/src/Core/Thinning.idr
+++ b/src/Core/Thinning.idr
@@ -56,6 +56,37 @@ view (IsThinner IsBase) = Drop (id _)
 view (IsThinner (IsDrop thin)) = Drop (IsThinner thin)
 view (IsThinner (IsKeep thin)) = Keep (IsThinner thin)
 
+-- Composition -----------------------------------------------------------------
+
+comp : Thinner m n -> Thinner k m -> Thinner k n
+comp IsBase thin2 = IsDrop thin2
+comp (IsDrop thin1) thin2 = IsDrop (comp thin1 thin2)
+comp (IsKeep thin1) IsBase = IsDrop thin1
+comp (IsKeep thin1) (IsDrop thin2) = IsDrop (comp thin1 thin2)
+comp (IsKeep thin1) (IsKeep thin2) = IsKeep (comp thin1 thin2)
+
+export
+(.) : m `Thins` n -> k `Thins` m -> k `Thins` n
+IsId . thin2 = thin2
+IsThinner thin1 . IsId = IsThinner thin1
+IsThinner thin1 . IsThinner thin2 = IsThinner (comp thin1 thin2)
+
+-- Specific Cases
+
+export
+compRightId : (thin : m `Thins` n) -> thin . id m = thin
+compRightId IsId = Refl
+compRightId (IsThinner thin) = Refl
+
+export
+compKeep :
+  (thin1 : m `Thins` n) ->
+  (thin2 : k `Thins` m) ->
+  keep thin1 . keep thin2 = keep (thin1 . thin2)
+compKeep IsId thin2 = Refl
+compKeep (IsThinner thin1) IsId = Refl
+compKeep (IsThinner thin1) (IsThinner thin2) = Refl
+
 -- Weakening -------------------------------------------------------------------
 
 wkn' : Fin m -> Thinner m n -> Fin n
@@ -69,17 +100,26 @@ wkn : Fin m -> m `Thins` n -> Fin n
 wkn i IsId = i
 wkn i (IsThinner thin) = wkn' i thin
 
--- Composition -----------------------------------------------------------------
+-- Properties
 
-comp : Thinner m n -> Thinner k m -> Thinner k n
-comp IsBase thin2 = IsDrop thin2
-comp (IsDrop thin1) thin2 = IsDrop (comp thin1 thin2)
-comp (IsKeep thin1) IsBase = IsDrop thin1
-comp (IsKeep thin1) (IsDrop thin2) = IsDrop (comp thin1 thin2)
-comp (IsKeep thin1) (IsKeep thin2) = IsKeep (comp thin1 thin2)
+wkn'Homo :
+  (i : Fin k) ->
+  (thin2 : Thinner m n) ->
+  (thin1 : Thinner k m) ->
+  wkn' (wkn' i thin1) thin2 = wkn' i (comp thin2 thin1)
+wkn'Homo i IsBase thin1 = Refl
+wkn'Homo i (IsDrop thin2) thin1 = cong FS (wkn'Homo i thin2 thin1)
+wkn'Homo i (IsKeep thin2) IsBase = Refl
+wkn'Homo i (IsKeep thin2) (IsDrop thin1) = cong FS (wkn'Homo i thin2 thin1)
+wkn'Homo FZ (IsKeep thin2) (IsKeep thin1) = Refl
+wkn'Homo (FS i) (IsKeep thin2) (IsKeep thin1) = cong FS (wkn'Homo i thin2 thin1)
 
 export
-(.) : m `Thins` n -> k `Thins` m -> k `Thins` n
-IsId . thin2 = thin2
-IsThinner thin1 . IsId = IsThinner thin1
-IsThinner thin1 . IsThinner thin2 = IsThinner (comp thin1 thin2)
+wknHomo :
+  (i : Fin k) ->
+  (thin1 : k `Thins` m) ->
+  (thin2 : m `Thins` n) ->
+  wkn (wkn i thin1) thin2 = wkn i (thin2 . thin1)
+wknHomo i IsId thin2 = sym $ cong (wkn i) $ compRightId thin2
+wknHomo i (IsThinner thin1) IsId = Refl
+wknHomo i (IsThinner thin1) (IsThinner thin2) = wkn'Homo i thin2 thin1