From 87eea439d8d8390c768498c2224268200373f629 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sun, 16 Apr 2023 18:31:20 +0100
Subject: Prove weakening of type judgements.

This is a huge commit that has many more changes. I should split
this up later.
---
 src/Core/Thinning.idr | 80 +++++++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 78 insertions(+), 2 deletions(-)

(limited to 'src/Core/Thinning.idr')

diff --git a/src/Core/Thinning.idr b/src/Core/Thinning.idr
index 51947e0..d56ada8 100644
--- a/src/Core/Thinning.idr
+++ b/src/Core/Thinning.idr
@@ -33,6 +33,16 @@ keep : m `Thins` n -> S m `Thins` S n
 keep IsId = IsId
 keep (IsThinner thin) = IsThinner (IsKeep thin)
 
+public export
+wkn1 : (0 n : Nat) -> n `Thins` S n
+wkn1 n = drop (id n)
+
+-- Properties
+
+export
+keepIdIsId : (0 n : Nat) -> keep (id n) = id (S n)
+keepIdIsId n = Refl
+
 -- Non-Identity ----------------------------------------------------------------
 
 export
@@ -49,6 +59,8 @@ data View : m `Thins` n -> Type where
   Drop : (thin : m `Thins` n) -> View (drop thin)
   Keep : (thin : m `Thins` n) -> {auto 0 prf : IsNotId thin} -> View (keep thin)
 
+%name Thinning.View view
+
 export
 view : (thin : m `Thins` n) -> View thin
 view IsId = Id m
@@ -56,6 +68,38 @@ view (IsThinner IsBase) = Drop (id _)
 view (IsThinner (IsDrop thin)) = Drop (IsThinner thin)
 view (IsThinner (IsKeep thin)) = Keep (IsThinner thin)
 
+-- Eliminators
+
+export
+viewId :
+  (0 n : Nat) ->
+  (0 p : View (id n) -> Type) ->
+  p (Id n) ->
+  p (view $ id n)
+viewId n p x = x
+
+export
+viewDrop :
+  (thin : m `Thins` n) ->
+  (0 p : View (drop thin) -> Type) ->
+  p (Drop thin) ->
+  p (view $ drop thin)
+viewDrop IsId p x = x
+viewDrop (IsThinner thin) p x = x
+
+export
+viewKeep :
+  forall m, n.
+  (thin : m `Thins` n) ->
+  (0 p : View (keep thin) -> Type) ->
+  ((eq1 : m = n) ->
+   (eq2 : thin = (rewrite eq1 in id n)) ->
+   p (rewrite eq2 in rewrite eq1 in Id (S n))) ->
+  ({auto 0 prf : IsNotId thin} -> p (Keep thin)) ->
+  p (view $ keep thin)
+viewKeep IsId p id keep = id Refl Refl
+viewKeep (IsThinner thin) p id keep = keep
+
 -- Composition -----------------------------------------------------------------
 
 comp : Thinner m n -> Thinner k m -> Thinner k n
@@ -119,7 +163,6 @@ compLeftDrop IsId (IsThinner thin1) = Refl
 compLeftDrop (IsThinner thin2) IsId = Refl
 compLeftDrop (IsThinner thin2) (IsThinner thin1) = Refl
 
-
 export
 compRightDrop :
   (thin2 : m `Thins` n) ->
@@ -138,6 +181,18 @@ compKeep IsId thin2 = Refl
 compKeep (IsThinner thin1) IsId = Refl
 compKeep (IsThinner thin1) (IsThinner thin2) = Refl
 
+export
+compLeftWkn1 : (thin : m `Thins` n) -> wkn1 n . thin = drop thin
+compLeftWkn1 thin = trans (compLeftDrop (id n) thin) (cong drop $ compLeftId thin)
+
+export
+compRightWkn1 : (thin : m `Thins` n) -> keep thin . wkn1 m = drop thin
+compRightWkn1 thin = trans (compRightDrop thin (id m)) (cong drop $ compRightId thin)
+
+export
+wkn1Comm : (thin : m `Thins` n) -> keep thin . wkn1 m = wkn1 n . thin
+wkn1Comm thin = trans (compRightWkn1 thin) (sym $ compLeftWkn1 thin)
+
 -- Weakening -------------------------------------------------------------------
 
 wkn' : Fin m -> Thinner m n -> Fin n
@@ -151,7 +206,11 @@ wkn : Fin m -> m `Thins` n -> Fin n
 wkn i IsId = i
 wkn i (IsThinner thin) = wkn' i thin
 
--- Properties
+-- Categorical
+
+export
+wknId : (i : Fin n) -> wkn i (id n) = i
+wknId i = Refl
 
 wkn'Homo :
   (i : Fin k) ->
@@ -174,3 +233,20 @@ wknHomo :
 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
+
+-- Specific Cases
+
+export
+wknDrop : (i : Fin m) -> (thin : m `Thins` n) -> wkn i (drop thin) = FS (wkn i thin)
+wknDrop i IsId = Refl
+wknDrop i (IsThinner thin) = Refl
+
+export
+wknKeepFZ : (thin : m `Thins` n) -> wkn 0 (keep thin) = 0
+wknKeepFZ IsId = Refl
+wknKeepFZ (IsThinner thin) = Refl
+
+export
+wknKeepFS : (i : Fin m) -> (thin : m `Thins` n) -> wkn (FS i) (keep thin) = FS (wkn i thin)
+wknKeepFS i IsId = Refl
+wknKeepFS i (IsThinner thin) = Refl
-- 
cgit v1.2.3