From ba63f18dafd54e49c863d6c25f7de6ca2d60987c Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 6 Apr 2023 17:00:46 +0100
Subject: Move and rename ThinWf.

Correct statement for weakening preservation.
---
 src/Core/Declarative.idr | 44 ++++++++++++--------------------------------
 src/Core/Environment.idr | 33 +++++++++++++++++++++++++++++++++
 2 files changed, 45 insertions(+), 32 deletions(-)

diff --git a/src/Core/Declarative.idr b/src/Core/Declarative.idr
index 2fff434..b6cd55e 100644
--- a/src/Core/Declarative.idr
+++ b/src/Core/Declarative.idr
@@ -147,16 +147,6 @@ data TermConv where
 %name TermWf wf
 %name TermConv conv
 
-public export
-data ThinWf : sx `Thins` sy -> Env sy -> Env sx -> Type where
-  IdWf : ThinWf (id sx) env env
-  DropWf : ThinWf thin env2 env1 -> ThinWf (drop thin n) (Add env2 t) env1
-  KeepWf :
-    ThinWf thin env2 env1 ->
-    ThinWf (keep thin n) (Add env2 (shift t thin)) (Add env1 t)
-
-%name ThinWf thinWf
-
 -- Environment Equality --------------------------------------------------------
 
 envWfRespEnvEq : EnvWf env1 -> EnvEq env1 env2 -> EnvWf env2
@@ -268,39 +258,29 @@ termConvImpliesEnvWf (PiBeta wf wf1 wf2) = typeWfImpliesEnvWf wf
 termConvImpliesEnvWf (PiEta wf wf1 wf2 conv) = typeWfImpliesEnvWf wf
 termConvImpliesEnvWf (AppConv conv conv1) = termConvImpliesEnvWf conv
 
--- Weakening Composition -------------------------------------------------------
-
-CompWf : ThinWf thin2 env3 env2 -> ThinWf thin1 env2 env1 -> ThinWf (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)
-
 -- Weakening Preservation ------------------------------------------------------
 
 wknPresTypeWf :
+  {0 env1 : Env sx} ->
   TypeWf env1 a ->
-  ThinWf thin env2 env1 ->
+  EnvWf env2 ->
+  IsExtension thin env2 env1 ->
   TypeWf env2 (wkn a thin)
 wknPresTypeConv :
+  {0 env1 : Env sx} ->
   TypeConv env1 a b ->
-  ThinWf thin env2 env1 ->
+  EnvWf env2 ->
+  IsExtension thin env2 env1 ->
   TypeConv env2 (wkn a thin) (wkn b thin)
 wknPresTermWf :
+  {0 env1 : Env sx} ->
   TermWf env1 t a ->
-  ThinWf thin env2 env1 ->
+  EnvWf env2 ->
+  IsExtension thin env2 env1 ->
   TermWf env2 (wkn t thin) (wkn a thin)
 wknPresTermConv :
+  {0 env1 : Env sx} ->
   TermConv env1 t u a ->
-  ThinWf thin env2 env1 ->
+  EnvWf env2 ->
+  IsExtension thin env2 env1 ->
   TermConv env2 (wkn t thin) (wkn u thin) (wkn a thin)
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
-- 
cgit v1.2.3