From 7644c22ea64379012e7c5388b613b46550bc3896 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Sat, 1 Apr 2023 14:58:09 +0100 Subject: Prove composition of thinnings is well-formed. --- src/Core/Declarative.idr | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) (limited to 'src') 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) -- cgit v1.2.3