From 52b9e2f139444f012f3610e60321e4336d888bec Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sun, 23 Apr 2023 14:33:18 +0100
Subject: Prove escape theorems.

---
 src/Core/Generic.idr |  4 +++
 src/Core/LogRel.idr  | 74 ++++++++++++++++++++++++++++++++++++++++++----------
 2 files changed, 64 insertions(+), 14 deletions(-)

diff --git a/src/Core/Generic.idr b/src/Core/Generic.idr
index c2bd1f4..4563063 100644
--- a/src/Core/Generic.idr
+++ b/src/Core/Generic.idr
@@ -118,6 +118,10 @@ interface IsEq (0 eq : Equality) where
     ---
     eq.TypeEq {n} env (Pi a b) (Pi c d)
 
+export
+ntrlEqImpliesTypeEq : IsEq eq => eq.NtrlEq {n = k} env n m Set -> eq.TypeEq env n.fst m.fst
+ntrlEqImpliesTypeEq = termEqImpliesTypeEq . ntrlEqImpliesTermEq
+
 -- Instance 1 ------------------------------------------------------------------
 
 public export
diff --git a/src/Core/LogRel.idr b/src/Core/LogRel.idr
index 9c18f02..19a7071 100644
--- a/src/Core/LogRel.idr
+++ b/src/Core/LogRel.idr
@@ -86,7 +86,7 @@ record NeutralTyRed
   tyWf : TypeWf env a
   steps : TypeReduce env a a'
   tyWf' : TypeWf env a'
-  0 ntrl : Neutral a'
+  ntrl : Neutral a'
   prf : eq.NtrlEq env (Element a' ntrl) (Element a' ntrl) Set
 
 public export
@@ -103,7 +103,7 @@ record NeutralTyEq
   tyWf : TypeWf env b
   steps : TypeReduce env b b'
   tyWf' : TypeWf env b'
-  0 ntrl : Neutral b'
+  ntrl : Neutral b'
   prf : eq.NtrlEq env (Element red.a' red.ntrl) (Element b' ntrl) Set
 
 public export
@@ -120,7 +120,7 @@ record NeutralTmRed
   tmWf : TermWf env t a
   steps : TermReduce env t t' a
   tmWf' : TermWf env t' a
-  0 ntrl : Neutral t'
+  ntrl : Neutral t'
   prf : eq.NtrlEq env (Element t' ntrl) (Element t' ntrl) a
 
 public export
@@ -140,8 +140,8 @@ record NeutralTmEq
   steps2 : TermReduce env u u' a
   tmWf1' : TermWf env t' a
   tmWf2' : TermWf env u' a
-  0 ntrl1 : Neutral t'
-  0 ntrl2 : Neutral u'
+  ntrl1 : Neutral t'
+  ntrl2 : Neutral u'
   prf : eq.NtrlEq env (Element t' ntrl1) (Element u' ntrl2) a
 
 -- Set
@@ -186,9 +186,9 @@ record SetTmRed
   constructor MkSetTmRed
   {0 t' : Term n}
   tmWf : TermWf env t a
-  steps : TypeReduce env t t'
+  steps : TermReduce env t t' a
   tmWf' : TermWf env t' a
-  0 whnf : Whnf t'
+  whnf : Whnf t'
   prf : eq.TermEq env t' t' a
   tyRed : (rec Small red.prf).TypeRed env t
 
@@ -205,12 +205,12 @@ record SetTmEq
   {0 t', u' : Term n}
   tmWf1 : TermWf env t a
   tmWf2 : TermWf env u a
-  steps1 : TypeReduce env t t'
-  steps2 : TypeReduce env u u'
+  steps1 : TermReduce env t t' a
+  steps2 : TermReduce env u u' a
   tmWf1' : TermWf env t' a
   tmWf2' : TermWf env u' a
-  0 whnf1 : Whnf t'
-  0 whnf2 : Whnf u'
+  whnf1 : Whnf t'
+  whnf2 : Whnf u'
   prf : eq.TermEq env t' u' a
   tyRed1 : (rec Small red.prf).TypeRed env t
   tyRed2 : (rec Small red.prf).TypeRed env u
@@ -309,7 +309,7 @@ record PiTmRed
   tmWf : TermWf env t a
   steps : TermReduce env t t' a
   tmWf' : TermWf env t' a
-  0 whnf : Whnf t'
+  whnf : Whnf t'
   prf : eq.TermEq env t' t' a
   codRed :
     forall m.
@@ -354,8 +354,8 @@ record PiTmEq
   steps2 : TermReduce env u u' a
   tmWf1' : TermWf env t' a
   tmWf2' : TermWf env u' a
-  0 whnf1 : Whnf t'
-  0 whnf2 : Whnf u'
+  whnf1 : Whnf t'
+  whnf2 : Whnf u'
   prf : eq.TermEq env t' u' a
   red1 : PiTmRed eq l rec env t a red
   red2 : PiTmRed eq l rec env u a red
@@ -498,3 +498,49 @@ termEqRefl l (RedPiTy red@(MkPiTyRed _ _ _ _ domRed _ _)) (RedPiTm redTm) =
     , red2 = redTm
     , codEq = \thinWf, red' => redTm.codEq thinWf red' red' (termEqRefl l (domRed thinWf) red')
     }
+
+-- Escape ----------------------------------------------------------------------
+
+export
+escapeTypeRed : (l : Level) -> (red : (LogRel eq l).TypeRed env a) -> TypeWf env a
+escapeTypeRed l (RedNtrlTy red) = red.tyWf
+escapeTypeRed l (RedSetTy red) = red.tyWf
+escapeTypeRed l (RedPiTy red) = red.tyWf
+
+export
+escapeTypeEq :
+  IsEq eq =>
+  (l : Level) ->
+  (red : (LogRel eq l).TypeRed env a) ->
+  (LogRel eq l).TypeEq env a b red ->
+  eq.TypeEq env a b
+escapeTypeEq l (RedNtrlTy red) (EqNtrlTy tyEq) =
+  expandType red.steps tyEq.steps (Ntrl red.ntrl) (Ntrl tyEq.ntrl) (ntrlEqImpliesTypeEq tyEq.prf)
+escapeTypeEq l (RedSetTy red) (EqSetTy tyEq) =
+  expandType red.steps tyEq.steps Set Set (typeSet $ typeWfImpliesEnvWf red.tyWf')
+escapeTypeEq l (RedPiTy red) (EqPiTy tyEq) =
+  expandType red.steps tyEq.steps Pi Pi tyEq.prf
+
+export
+escapeTermRed :
+  (l : Level) ->
+  (red : (LogRel eq l).TypeRed env a) ->
+  (LogRel eq l).TermRed env t a red ->
+  TermWf env t a
+escapeTermRed l (RedNtrlTy red) (RedNtrlTm tmRed) = tmRed.tmWf
+escapeTermRed l (RedSetTy red) (RedSetTm tmRed) = tmRed.tmWf
+escapeTermRed l (RedPiTy red) (RedPiTm tmRed) = tmRed.tmWf
+
+export
+escapeTermEq :
+  IsEq eq =>
+  (l : Level) ->
+  (red : (LogRel eq l).TypeRed env a) ->
+  (LogRel eq l).TermEq env t u a red ->
+  eq.TermEq env t u a
+escapeTermEq l (RedNtrlTy red) (EqNtrlTm tmEq) =
+  expandTerm tmEq.steps1 tmEq.steps2 (Ntrl tmEq.ntrl1) (Ntrl tmEq.ntrl2) (ntrlEqImpliesTermEq tmEq.prf)
+escapeTermEq l (RedSetTy red) (EqSetTm tmEq) =
+  expandTerm tmEq.steps1 tmEq.steps2 tmEq.whnf1 tmEq.whnf2 tmEq.prf
+escapeTermEq l (RedPiTy red) (EqPiTm tmEq) =
+  expandTerm tmEq.steps1 tmEq.steps2 tmEq.whnf1 tmEq.whnf2 tmEq.prf
-- 
cgit v1.2.3