diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-16 15:24:51 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-16 15:24:51 +0100 |
| commit | b7a8063be92fb6c83de1ea60ac09c49f895886ff (patch) | |
| tree | cd822f902c829087b59d24156013045bcfe48656 | |
| parent | 2ab0a78d642c602599f4d6a23372c0c91b9f27f0 (diff) | |
Prove more properties about thinning composition.
| -rw-r--r-- | src/Core/Thinning.idr | 53 |
1 files changed, 52 insertions, 1 deletions
diff --git a/src/Core/Thinning.idr b/src/Core/Thinning.idr index 959702d..51947e0 100644 --- a/src/Core/Thinning.idr +++ b/src/Core/Thinning.idr @@ -71,13 +71,64 @@ IsId . thin2 = thin2 IsThinner thin1 . IsId = IsThinner thin1 IsThinner thin1 . IsThinner thin2 = IsThinner (comp thin1 thin2) --- Specific Cases +-- Categorical + +comp'Assoc : + (thin3 : Thinner m n) -> + (thin2 : Thinner k m) -> + (thin1 : Thinner j k) -> + comp thin3 (comp thin2 thin1) = comp (comp thin3 thin2) thin1 +comp'Assoc IsBase thin2 thin1 = Refl +comp'Assoc (IsDrop thin3) thin2 thin1 = cong IsDrop (comp'Assoc thin3 thin2 thin1) +comp'Assoc (IsKeep thin3) IsBase thin1 = Refl +comp'Assoc (IsKeep thin3) (IsDrop thin2) thin1 = cong IsDrop (comp'Assoc thin3 thin2 thin1) +comp'Assoc (IsKeep thin3) (IsKeep thin2) IsBase = Refl +comp'Assoc (IsKeep thin3) (IsKeep thin2) (IsDrop thin1) = cong IsDrop (comp'Assoc thin3 thin2 thin1) +comp'Assoc (IsKeep thin3) (IsKeep thin2) (IsKeep thin1) = cong IsKeep (comp'Assoc thin3 thin2 thin1) + +export +compAssoc : + (thin3 : m `Thins` n) -> + (thin2 : k `Thins` m) -> + (thin1 : j `Thins` k) -> + thin3 . (thin2 . thin1) = (thin3 . thin2) . thin1 +compAssoc IsId thin2 thin1 = Refl +compAssoc (IsThinner thin3) IsId thin1 = Refl +compAssoc (IsThinner thin3) (IsThinner thin2) IsId = Refl +compAssoc (IsThinner thin3) (IsThinner thin2) (IsThinner thin1) = + cong IsThinner (comp'Assoc thin3 thin2 thin1) + +export +compLeftId : (thin : m `Thins` n) -> id n . thin = thin +compLeftId thin = Refl export compRightId : (thin : m `Thins` n) -> thin . id m = thin compRightId IsId = Refl compRightId (IsThinner thin) = Refl +-- Specific Cases + +export +compLeftDrop : + (thin2 : m `Thins` n) -> + (thin1 : k `Thins` m) -> + drop thin2 . thin1 = drop (thin2 . thin1) +compLeftDrop IsId IsId = Refl +compLeftDrop IsId (IsThinner thin1) = Refl +compLeftDrop (IsThinner thin2) IsId = Refl +compLeftDrop (IsThinner thin2) (IsThinner thin1) = Refl + + +export +compRightDrop : + (thin2 : m `Thins` n) -> + (thin1 : k `Thins` m) -> + keep thin2 . drop thin1 = drop (thin2 . thin1) +compRightDrop IsId thin1 = Refl +compRightDrop (IsThinner thin2) IsId = Refl +compRightDrop (IsThinner thin2) (IsThinner thin1) = Refl + export compKeep : (thin1 : m `Thins` n) -> |