Move and rename ThinWf.

Correct statement for weakening preservation.

1 files changed, 33 insertions, 0 deletions

diff --git a/src/Core/Environment.idr b/src/Core/Environment.idr
index a0a10f4..1fe8e28 100644
--- a/src/Core/Environment.idr
+++ b/src/Core/Environment.idr
@@ -34,6 +34,39 @@ namespace Eq
 
   %name EnvEq prf
 
+-- Extension -------------------------------------------------------------------
+
+public export
+data IsExtension : sx `Thins` sy -> Env sy -> Env sx -> Type where
+  IdWf : IsExtension (id sx) env env
+  DropWf : IsExtension thin env2 env1 -> IsExtension (drop thin n) (Add env2 t) env1
+  KeepWf :
+    IsExtension thin env2 env1 ->
+    IsExtension (keep thin n) (Add env2 (shift t thin)) (Add env1 t)
+
+%name IsExtension ext
+
+-- Composition
+
+CompWf :
+  IsExtension thin2 env3 env2 ->
+  IsExtension thin1 env2 env1 ->
+  IsExtension (thin2 . thin1) env3 env1
+CompWf IdWf thinWf1 = rewrite compLeftIdentity thin1 in thinWf1
+CompWf (DropWf {thin = thin2, n} thinWf2) thinWf1 =
+  rewrite compLeftDrop thin2 thin1 n in
+  DropWf (CompWf thinWf2 thinWf1)
+CompWf (KeepWf {thin = thin2, n} thinWf2) IdWf =
+  rewrite compRightIdentity $ keep thin2 n in
+  KeepWf thinWf2
+CompWf (KeepWf {thin = thin2, n} thinWf2) (DropWf {thin = thin1} thinWf1) =
+  rewrite compRightDrop thin2 thin1 n in
+  DropWf (CompWf thinWf2 thinWf1)
+CompWf (KeepWf {thin = thin2, n} thinWf2) (KeepWf {thin = thin1, t} thinWf1) =
+  rewrite compKeep thin2 thin1 n in
+  rewrite shiftHomo t thin1 thin2 in
+  KeepWf (CompWf thinWf2 thinWf1)
+
 -- Indexing --------------------------------------------------------------------
 
 doIndex : Env sx -> {0 i : Var sx} -> View i -> Thinned sx