From 12d5b7a16c443417daca46c5870d6b2660d90047 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Sat, 8 Apr 2023 14:30:55 +0100 Subject: Reduce code duplication. --- src/Core/Declarative.idr | 119 +++-------------------------------------------- 1 file changed, 6 insertions(+), 113 deletions(-) (limited to 'src/Core/Declarative.idr') diff --git a/src/Core/Declarative.idr b/src/Core/Declarative.idr index 94822e4..2dd7933 100644 --- a/src/Core/Declarative.idr +++ b/src/Core/Declarative.idr @@ -341,35 +341,7 @@ wknPresTermWf (AbsTerm {f, n} wf wf1) envWf ext = (KeepWf ext)) ((:<) {t = f `Over` thin} Base (sym $ wknId $ expand $ f `Over` thin)) wknPresTermWf (AppTerm {g, u, n} wf wf1) envWf ext = - let - eq0 : (thin . id sx = id _ . thin) - eq0 = Calc $ - |~ thin . id sx - ~~ thin ...(compRightIdentity thin) - ~~ id _ . thin ...(sym $ compLeftIdentity thin) - - eq1 : (Base (thin . id sx) = restrict thin (Base (id _))) - eq1 = Calc $ - |~ Base (thin . id sx) - ~~ Base (id _ . thin) ...(cong Base eq0) - ~~ restrict thin (Base (id _)) ...(sym $ restrictBase thin (id _)) - - eq2 : wkn u (thin . id sx) = wkn (wkn u thin) (id _) - eq2 = Calc $ - |~ wkn u (thin . id sx) - ~~ wkn u (id _ . thin) ...(cong (wkn u) $ eq0) - ~~ wkn (wkn u thin) (id _) ...(sym $ wknHomo u thin (id _)) - - eq : (wkn (subst g (sub1 u)) thin = subst (wkn g (keep thin n)) (sub1 (wkn u thin))) - eq = Calc $ - |~ wkn (subst g (sub1 u)) thin - ~~ subst g (Base (thin . id _) :< (u `Over` thin . id _)) ...(wknSubst g (sub1 u) thin) - ~~ subst g (Base (thin . id _) :< (wkn u thin `Over` id _)) ...(substCong g (Base :< eq2)) - ~~ subst g (restrict thin _ :< (wkn u thin `Over` id _)) ...(cong (subst g . (:< (wkn u thin `Over` id _))) eq1) - ~~ subst g (restrict (keep thin n) (sub1 (wkn u thin))) ...(sym $ cong (subst g) $ restrictKeep thin n (id _) (wkn u thin `Over` id _)) - ~~ subst (wkn g (keep thin n)) (sub1 (wkn u thin)) ...(sym $ substWkn g (keep thin n) (sub1 (wkn u thin))) - in - rewrite eq in + rewrite wknSub1 g u thin in AppTerm (wknPresTermWf wf envWf ext) (wknPresTermWf wf1 envWf ext) wknPresTermWf (ConvTerm wf conv) envWf ext = ConvTerm (wknPresTermWf wf envWf ext) (wknPresTypeConv conv envWf ext) @@ -394,46 +366,9 @@ wknPresTermConv (PiTermConv {f, n} wf conv conv1) envWf ext = (KeepWf ext)) ((:<) {t = f `Over` thin} Base (sym $ wknId $ expand $ f `Over` thin)) wknPresTermConv (PiBeta {f, g, t, u, n} wf wf1 wf2) envWf ext = - let - eq0 : (thin . id sx = id _ . thin) - eq0 = Calc $ - |~ thin . id sx - ~~ thin ...(compRightIdentity thin) - ~~ id _ . thin ...(sym $ compLeftIdentity thin) - - eq1 : (Base (thin . id sx) = restrict thin (Base (id _))) - eq1 = Calc $ - |~ Base (thin . id sx) - ~~ Base (id _ . thin) ...(cong Base eq0) - ~~ restrict thin (Base (id _)) ...(sym $ restrictBase thin (id _)) - - eq2 : wkn u (thin . id sx) = wkn (wkn u thin) (id _) - eq2 = Calc $ - |~ wkn u (thin . id sx) - ~~ wkn u (id _ . thin) ...(cong (wkn u) $ eq0) - ~~ wkn (wkn u thin) (id _) ...(sym $ wknHomo u thin (id _)) - - eq : (wkn (subst g (sub1 u)) thin = subst (wkn g (keep thin n)) (sub1 (wkn u thin))) - eq = Calc $ - |~ wkn (subst g (sub1 u)) thin - ~~ subst g (Base (thin . id _) :< (u `Over` thin . id _)) ...(wknSubst g (sub1 u) thin) - ~~ subst g (Base (thin . id _) :< (wkn u thin `Over` id _)) ...(substCong g (Base :< eq2)) - ~~ subst g (restrict thin _ :< (wkn u thin `Over` id _)) ...(cong (subst g . (:< (wkn u thin `Over` id _))) eq1) - ~~ subst g (restrict (keep thin n) (sub1 (wkn u thin))) ...(sym $ cong (subst g) $ restrictKeep thin n (id _) (wkn u thin `Over` id _)) - ~~ subst (wkn g (keep thin n)) (sub1 (wkn u thin)) ...(sym $ substWkn g (keep thin n) (sub1 (wkn u thin))) - - eq' : (wkn (subst t (sub1 u)) thin = subst (wkn t (keep thin n)) (sub1 (wkn u thin))) - eq' = Calc $ - |~ wkn (subst t (sub1 u)) thin - ~~ subst t (Base (thin . id _) :< (u `Over` thin . id _)) ...(wknSubst t (sub1 u) thin) - ~~ subst t (Base (thin . id _) :< (wkn u thin `Over` id _)) ...(substCong t (Base :< eq2)) - ~~ subst t (restrict thin _ :< (wkn u thin `Over` id _)) ...(cong (subst t . (:< (wkn u thin `Over` id _))) eq1) - ~~ subst t (restrict (keep thin n) (sub1 (wkn u thin))) ...(sym $ cong (subst t) $ restrictKeep thin n (id _) (wkn u thin `Over` id _)) - ~~ subst (wkn t (keep thin n)) (sub1 (wkn u thin)) ...(sym $ substWkn t (keep thin n) (sub1 (wkn u thin))) - in let wf' = wknPresTypeWf wf envWf ext in - rewrite eq in - rewrite eq' in + rewrite wknSub1 g u thin in + rewrite wknSub1 t u thin in PiBeta wf' (termWfRespEnvEq (wknPresTermWf wf1 (envWf :< wf') $ @@ -443,62 +378,20 @@ wknPresTermConv (PiBeta {f, g, t, u, n} wf wf1 wf2) envWf ext = ((:<) {t = f `Over` thin} Base (sym $ wknId $ expand $ f `Over` thin))) (wknPresTermWf wf2 envWf ext) wknPresTermConv (PiEta {f, n, t, u} wf wf1 wf2 conv) envWf ext = - let - eq : (0 t : Term sx) -> (wkn (wkn t thin) (wkn1 _ n) = wkn (wkn t (wkn1 sx n)) (keep thin n)) - eq t = Calc $ - |~ wkn (wkn t thin) (wkn1 _ n) - ~~ wkn t (wkn1 _ n . thin) ...(wknHomo t thin (wkn1 _ n)) - ~~ wkn t (drop thin n) ...(cong (wkn t) $ compLeftWkn1 thin n) - ~~ wkn t (keep thin n . wkn1 sx n) ...(sym $ cong (wkn t) $ compRightWkn1 thin n) - ~~ wkn (wkn t (wkn1 sx n)) (keep thin n) ...(sym $ wknHomo t (wkn1 sx n) (keep thin n)) - - eq' : - (0 t : Term sx) -> - (App (wkn (wkn t thin) (wkn1 _ n)) (Var Var.here) = wkn (App (wkn t (wkn1 sx n)) (Var Var.here)) (keep thin n)) - eq' t = cong2 App (eq t) (sym $ cong Var $ wknKeepHereIsHere thin n) - in let wf' = wknPresTypeWf wf envWf ext in PiEta wf' (wknPresTermWf wf1 envWf ext) (wknPresTermWf wf2 envWf ext) (termConvRespEnvEq - (rewrite eq' t in - rewrite eq' u in + (rewrite sym $ wknEta t thin n in + rewrite sym $ wknEta u thin n in wknPresTermConv conv (envWf :< wf') $ replace {p = \thin' => IsExtension (keep thin n) (Add env2 (f `Over` thin')) (env1 :< f)} (compRightIdentity thin) (KeepWf ext)) ((:<) {t = f `Over` thin} Base (sym $ wknId $ expand $ f `Over` thin))) wknPresTermConv (AppConv {g, n, a} conv conv1) envWf ext = - let - eq0 : (thin . id sx = id _ . thin) - eq0 = Calc $ - |~ thin . id sx - ~~ thin ...(compRightIdentity thin) - ~~ id _ . thin ...(sym $ compLeftIdentity thin) - - eq1 : (Base (thin . id sx) = restrict thin (Base (id _))) - eq1 = Calc $ - |~ Base (thin . id sx) - ~~ Base (id _ . thin) ...(cong Base eq0) - ~~ restrict thin (Base (id _)) ...(sym $ restrictBase thin (id _)) - - eq2 : wkn a (thin . id sx) = wkn (wkn a thin) (id _) - eq2 = Calc $ - |~ wkn a (thin . id sx) - ~~ wkn a (id _ . thin) ...(cong (wkn a) $ eq0) - ~~ wkn (wkn a thin) (id _) ...(sym $ wknHomo a thin (id _)) - - eq : (wkn (subst g (sub1 a)) thin = subst (wkn g (keep thin n)) (sub1 (wkn a thin))) - eq = Calc $ - |~ wkn (subst g (sub1 a)) thin - ~~ subst g (Base (thin . id _) :< (a `Over` thin . id _)) ...(wknSubst g (sub1 a) thin) - ~~ subst g (Base (thin . id _) :< (wkn a thin `Over` id _)) ...(substCong g (Base :< eq2)) - ~~ subst g (restrict thin _ :< (wkn a thin `Over` id _)) ...(cong (subst g . (:< (wkn a thin `Over` id _))) eq1) - ~~ subst g (restrict (keep thin n) (sub1 (wkn a thin))) ...(sym $ cong (subst g) $ restrictKeep thin n (id _) (wkn a thin `Over` id _)) - ~~ subst (wkn g (keep thin n)) (sub1 (wkn a thin)) ...(sym $ substWkn g (keep thin n) (sub1 (wkn a thin))) - in - rewrite eq in + rewrite wknSub1 g a thin in AppConv (wknPresTermConv conv envWf ext) (wknPresTermConv conv1 envWf ext) -- cgit v1.2.3