diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-15 16:35:15 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-15 16:35:15 +0100 |
| commit | a38b0b5a6ee30e7dd22bc91765ba5361ed807dda (patch) | |
| tree | b2e4006c3d2feef19281aafb559f001bc3986693 /src/Core/Thinning.idr | |
| parent | 5f83999f483e241158706522a35364ba32f7f203 (diff) | |
Prove substitution respects the quotient.
Diffstat (limited to 'src/Core/Thinning.idr')
| -rw-r--r-- | src/Core/Thinning.idr | 62 |
1 files changed, 51 insertions, 11 deletions
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 |