Reduce code duplication.

2 files changed, 59 insertions, 113 deletions

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)
diff --git a/src/Core/Term/Substitution.idr b/src/Core/Term/Substitution.idr
index 136c0d4..15de859 100644
--- a/src/Core/Term/Substitution.idr
+++ b/src/Core/Term/Substitution.idr
@@ -363,3 +363,56 @@ substWkn (App t u) thin sub = cong2 App (substWkn t thin sub) (substWkn u thin s
 public export
 sub1 : Term sx -> Subst (sx :< n) sx
 sub1 t = Base (id sx) :< (t `Over` id sx)
+
+-- Concrete Cases --------------------------------------------------------------
+
+export
+wknSub1 :
+  (t : Term (sx :< n)) ->
+  (u : Term sx) ->
+  (thin : sx `Thins` sy) ->
+  wkn (subst t (sub1 u)) thin = subst (wkn t (keep thin n)) (sub1 (wkn u thin))
+wknSub1 t u thin =
+  let
+    eq0 : (thin . id sx = id sy . thin)
+    eq0  = Calc $
+      |~ thin . id sx
+      ~~ thin          ...(compRightIdentity thin)
+      ~~ id sy . thin  ...(sym $ compLeftIdentity thin)
+
+    eq1 : (Base (thin . id sx) = restrict thin (Base (id sy)))
+    eq1 = Calc $
+      |~ Base (thin . id sx)
+      ~~ Base (id sy . thin)          ...(cong Base eq0)
+      ~~ restrict thin (Base (id sy)) ...(sym $ restrictBase thin (id sy))
+
+    eq2 : wkn u (thin . id sx) = wkn (wkn u thin) (id sy)
+    eq2 = Calc $
+      |~ wkn u (thin . id sx)
+      ~~ wkn u (id sy . thin)     ...(cong (wkn u) $ eq0)
+      ~~ wkn (wkn u thin) (id sy) ...(sym $ wknHomo u thin (id sy))
+  in
+  Calc $
+    |~ wkn (subst t (sub1 u)) thin
+    ~~ subst t (Base (thin . id sx) :< (u `Over` thin . id sx))            ...(wknSubst t (sub1 u) thin)
+    ~~ subst t (Base (thin . id sx) :< (wkn u thin `Over` id sy))          ...(substCong t (Base :< eq2))
+    ~~ subst t (restrict thin (Base $ id sy) :< (wkn u thin `Over` id sy)) ...(cong (subst t . (:< (wkn u thin `Over` id sy))) eq1)
+    ~~ subst t (restrict (keep thin n) (sub1 (wkn u thin)))                ...(sym $ cong (subst t) $ restrictKeep thin n _ (wkn u thin `Over` id sy))
+    ~~ subst (wkn t (keep thin n)) (sub1 (wkn u thin))                     ...(sym $ substWkn t (keep thin n) (sub1 (wkn u thin)))
+
+export
+wknEta :
+  (t : Term sx) ->
+  (thin : sx `Thins` sy) ->
+  (0 n : Name) ->
+  wkn (App (wkn t (wkn1 sx n)) (Var Var.here)) (keep thin n) =
+  App (wkn (wkn t thin) (wkn1 sy n)) (Var Var.here)
+wknEta t thin n =
+  cong2 App
+    (Calc $
+      |~ wkn (wkn t (wkn1 sx n)) (keep thin n)
+      ~~ wkn t (keep thin n . wkn1 sx n)       ...(wknHomo t (drop (id sx) n) (keep thin n))
+      ~~ wkn t (drop thin n)                   ...(cong (wkn t) $ compRightWkn1 thin n)
+      ~~ wkn t (wkn1 sy n . thin)              ...(sym $ cong (wkn t) $ compLeftWkn1 thin n)
+      ~~ wkn (wkn t thin) (wkn1 sy n)          ...(sym $ wknHomo t thin (wkn1 sy n)))
+    (cong Var $ wknKeepHereIsHere thin n)