WIP : use smarter weakenings.better-thinning

1 files changed, 17 insertions, 29 deletions

diff --git a/src/Total/Reduction.idr b/src/Total/Reduction.idr
index a424515..4566724 100644
--- a/src/Total/Reduction.idr
+++ b/src/Total/Reduction.idr
@@ -4,13 +4,11 @@ import Syntax.PreorderReasoning
 import Total.Term
 
 public export
-data (>) : Term ctx ty -> Term ctx ty -> Type where
+data (>) : Term ty ctx -> Term ty ctx -> Type where
   AbsCong : t > u -> Abs t > Abs u
   AppCong1 : t > u -> App t v > App u v
   AppCong2 : u > v -> App t u > App t v
-  AppBeta :
-    (0 len : Len ctx) ->
-    App (Abs t) u > subst t (Base (id @{len}) :< u)
+  AppBeta : App (Abs t) u > subst t (Base Id :< u)
   SucCong : t > u -> Suc t > Suc u
   RecCong1 : t1 > t2 -> Rec t1 u v > Rec t2 u v
   RecCong2 : u1 > u2 -> Rec t u1 v > Rec t u2 v
@@ -21,7 +19,7 @@ data (>) : Term ctx ty -> Term ctx ty -> Type where
 %name Reduction.(>) step
 
 public export
-data (>=) : Term ctx ty -> Term ctx ty -> Type where
+data (>=) : Term ty ctx -> Term ty ctx -> Type where
   Lin : t >= t
   (:<) : t >= u -> u > v -> t >= v
 
@@ -70,37 +68,27 @@ RecCong3' (steps :< step) = RecCong3' steps :< RecCong3 step
 -- Properties ------------------------------------------------------------------
 
 lemma :
-  (t : Term (ctx :< ty) ty') ->
+  (t : Term ty' (ctx :< ty)) ->
   (thin : ctx `Thins` ctx') ->
-  (u : Term ctx ty) ->
-  subst (wkn t (Keep thin)) (Base Thinning.id :< wkn u thin) =
-  wkn (subst t (Base Thinning.id :< u)) thin
-lemma t thin u =
-  Calc $
-    |~ subst (wkn t (Keep thin)) (Base id :< wkn u thin)
-    ~~ subst t (restrict (Base id :< wkn u thin) (Keep thin))
-      ...(substWkn t (Keep thin) (Base id :< wkn u thin))
-    ~~ subst t (Base (id . thin) :< wkn u thin)
-      ...(Refl)
-    ~~ subst t (Base (thin . id) :< wkn u thin)
-      ...(cong (subst t . (:< wkn u thin) . Base) $ trans (identityLeft thin) (sym $ identityRight thin))
-    ~~ wkn (subst t (Base (id) :< u)) thin
-      ...(sym $ wknSubst t (Base (id @{length ctx}) :< u) thin)
+  (u : Term ty ctx) ->
+  wkn (subst t (Base Id :< u)) thin =
+  subst (wkn t (Keep thin)) (Base Id :< wkn u thin)
+lemma t thin u = Calc $
+  |~ wkn (subst t (Base Id :< u)) thin
+  ~~ subst t (wkn (Base Id :< u) thin)                      ...(wknSubst t (Base Id :< u) thin)
+  ~~ subst t (Base (thin . Id) :< wkn u thin)               ...(Refl)
+  ~~ subst t (Base thin :< wkn u thin)                      ...(substCong t (Base (identityRight thin) :< Refl))
+  ~~ subst t (Base (Id . thin) :< wkn u thin)               ...(Refl)
+  ~~ subst t (restrict (Base Id) thin :< wkn u thin)        ...(substCong t (restrictBase Id thin :< Refl))
+  ~~ subst t (restrict (Base Id :< wkn u thin) (Keep thin)) ...(Refl)
+  ~~ subst (wkn t (Keep thin)) (Base Id :< wkn u thin)      ..<(substWkn t (Base Id :< wkn u thin) (Keep thin))
 
 export
 wknStep : t > u -> wkn t thin > wkn u thin
 wknStep (AbsCong step) = AbsCong (wknStep step)
 wknStep (AppCong1 step) = AppCong1 (wknStep step)
 wknStep (AppCong2 step) = AppCong2 (wknStep step)
-wknStep (AppBeta len {ctx, t, u}) {thin} =
-  let
-    0 eq :
-      (subst (wkn t (Keep thin)) (Base Thinning.id :< wkn u thin) =
-       wkn (subst t (Base (id @{len}) :< u)) thin)
-    eq = rewrite lenUnique len (length ctx) in lemma t thin u
-  in
-    rewrite sym eq in
-    AppBeta _
+wknStep (AppBeta {t, u}) {thin} = rewrite lemma t thin u in AppBeta
 wknStep (SucCong step) = SucCong (wknStep step)
 wknStep (RecCong1 step) = RecCong1 (wknStep step)
 wknStep (RecCong2 step) = RecCong2 (wknStep step)