From 5a53c75f533f2ae758635e1989c4e7fb2b6469d5 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sun, 16 Apr 2023 14:50:55 +0100
Subject: Prove whnfs do not reduce.

---
 obs.ipkg                     |  1 +
 src/Core/Reduction.idr       | 23 +++++++++++++++++++++++
 src/Core/Term/NormalForm.idr | 22 ++++++++++++++++++++++
 3 files changed, 46 insertions(+)
 create mode 100644 src/Core/Term/NormalForm.idr

diff --git a/obs.ipkg b/obs.ipkg
index bbb996c..be12a16 100644
--- a/obs.ipkg
+++ b/obs.ipkg
@@ -11,6 +11,7 @@ modules
   , Core.Environment
   , Core.Reduction
   , Core.Term
+  , Core.Term.NormalForm
   , Core.Term.Substitution
   , Core.Term.Thinned
   , Core.Thinning
diff --git a/src/Core/Reduction.idr b/src/Core/Reduction.idr
index 7516648..9015d14 100644
--- a/src/Core/Reduction.idr
+++ b/src/Core/Reduction.idr
@@ -3,6 +3,7 @@ module Core.Reduction
 import Core.Environment
 import Core.Declarative
 import Core.Term
+import Core.Term.NormalForm
 import Core.Term.Substitution
 import Core.Term.Thinned
 import Core.Thinning
@@ -131,3 +132,25 @@ termStepImpliesSubjectWf (ConvStep step tyConv) = ConvWf (termStepImpliesSubject
 export
 typeStepImpliesSubjectWf : TypeStep env a b -> TypeWf env a
 typeStepImpliesSubjectWf = LiftWf . termStepImpliesSubjectWf
+
+-- Whnfs Do Not Reduce ---------------------------------------------------------
+
+export
+whnfNoTermStep : Whnf t -> Not (TermStep env t u a)
+whnfNoTermStep (Ntrl (App n)) (AppStep step tmWf) = whnfNoTermStep (Ntrl n) step
+whnfNoTermStep (Ntrl (App n)) (PiBeta tyWf tmWf tmWf1) impossible
+whnfNoTermStep n (ConvStep step tyConv) = whnfNoTermStep n step
+
+export
+whnfNoTypeStep : Whnf a -> Not (TypeStep env a b)
+whnfNoTypeStep = whnfNoTermStep
+
+export
+whnfTypeRedStays : Whnf a -> TypeReduce env a b -> a = b
+whnfTypeRedStays n (Refl tyWf) = Refl
+whnfTypeRedStays n (Step step steps) = absurd (whnfNoTypeStep n step)
+
+export
+whnfTermRedStays : Whnf t -> TermReduce env t u a -> t = u
+whnfTermRedStays n (Refl tmWf) = Refl
+whnfTermRedStays n (Step step steps) = absurd (whnfNoTermStep n step)
diff --git a/src/Core/Term/NormalForm.idr b/src/Core/Term/NormalForm.idr
new file mode 100644
index 0000000..9984bee
--- /dev/null
+++ b/src/Core/Term/NormalForm.idr
@@ -0,0 +1,22 @@
+module Core.Term.NormalForm
+
+import Core.Term
+
+-- Definition ------------------------------------------------------------------
+
+public export
+data Neutral : Term n -> Type where
+  Var : Neutral (Var i)
+  App : Neutral t -> Neutral (App t u)
+
+public export
+data Whnf : Term n -> Type where
+  Ntrl : Neutral t -> Whnf t
+
+  Set : Whnf Set
+
+  Pi : Whnf (Pi a b)
+  Abs : Whnf (Abs t)
+
+%name Neutral n, m
+%name Whnf n, m
-- 
cgit v1.2.3