State properties of typing and reduction.

There correspond to lemmata 2.1--2.5 in Abel et. al.

1 files changed, 32 insertions, 0 deletions

diff --git a/src/Core/Reduction.idr b/src/Core/Reduction.idr
index 0b3a651..21e6ee5 100644
--- a/src/Core/Reduction.idr
+++ b/src/Core/Reduction.idr
@@ -4,6 +4,7 @@ import Core.Context
 import Core.Declarative
 import Core.Term
 import Core.Term.Environment
+import Core.Term.NormalForm
 import Core.Term.Substitution
 
 public export
@@ -45,3 +46,34 @@ namespace Term
 %name TermStep step
 %name TypeRed steps
 %name TermRed steps
+
+-- Reduction Subsumed by Conversion --------------------------------------------
+
+termStepImpliesTermConv : TermStep env t u a -> TermConv env t u a
+typeStepImpliesTypeConv : TypeStep env a b -> TypeConv env a b
+typeRedImpliesTypeConv : TypeRed env a b -> TypeConv env a b
+termRedImpliesTermConv : TermRed env t u a -> TermConv env t u a
+
+-- Subject Typing --------------------------------------------------------------
+
+termStepImpliesSubjectWf : TermStep env t u a -> TermWf env t a
+typeStepImpliesSubjectWf : TypeStep env a b -> TypeWf env a
+
+-- Whnfs Do Not Reduce ---------------------------------------------------------
+
+-- Cannot step from whnf
+
+termStepWhnfImpossible : Whnf t -> Not (TermStep env t u a)
+typeStepWhnfImpossible : Whnf a -> Not (TypeStep env a b)
+
+-- Reduction starting from whnf goes nowhere
+
+typeRedWhnfStays : Whnf a -> TypeRed env a b -> a = b
+termRedWhnfStays : Whnf t -> TermRed env t u a -> t = u
+
+-- Reduction is Deterministic --------------------------------------------------
+
+termStepDeterministic : TermStep env t u a -> TermStep env t v b -> u = v
+typeStepDeterministic : TypeStep env a b -> TypeStep env a c -> b = c
+typeRedDeterministic : TypeRed env a b -> TypeRed env a c -> Whnf b -> Whnf c -> b = c
+termRedDeterministic : TermRed env t u a -> TermRed env t v b -> Whnf u -> Whnf v -> u = v