diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-01 14:58:09 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-01 14:58:09 +0100 |
| commit | 7644c22ea64379012e7c5388b613b46550bc3896 (patch) | |
| tree | e2a94f206651bdb90bb653b70ab2a52d4ea6cda2 /src | |
| parent | 44d467e58966792c19f363d769906ac5586d9937 (diff) | |
Prove composition of thinnings is well-formed.
Diffstat (limited to 'src')
| -rw-r--r-- | src/Core/Declarative.idr | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/src/Core/Declarative.idr b/src/Core/Declarative.idr index 319b465..4e849fe 100644 --- a/src/Core/Declarative.idr +++ b/src/Core/Declarative.idr @@ -189,3 +189,21 @@ termConvImpliesEnvWf (PiTermConv wf conv conv1) = termConvImpliesEnvWf conv 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, prf = prf2} thinWf2) (KeepWf {thin = thin1, thin', prf = prf1} thinWf1) = + rewrite compKeep thin2 thin1 n in + rewrite compAssoc thin2 thin1 thin' in + KeepWf {prf = compPresNotId prf2 prf1} (CompWf thinWf2 thinWf1) |