From 0cce62f5e290d059b1545006c11b33d4329f00a3 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sat, 1 Apr 2023 13:19:46 +0100
Subject: State properties of typing and reduction.

There correspond to lemmata 2.1--2.5 in Abel et. al.
---
 src/Core/Declarative.idr |  7 +++++++
 src/Core/Reduction.idr   | 32 ++++++++++++++++++++++++++++++++
 2 files changed, 39 insertions(+)

diff --git a/src/Core/Declarative.idr b/src/Core/Declarative.idr
index 2561797..99cc1ab 100644
--- a/src/Core/Declarative.idr
+++ b/src/Core/Declarative.idr
@@ -146,3 +146,10 @@ data TermConv where
 %name TypeConv conv
 %name TermWf wf
 %name TermConv conv
+
+-- Well Formed Environment -----------------------------------------------------
+
+typeWfImpliesEnvWf : TypeWf env a -> EnvWf env
+typeConvImpliesEnvWf : TypeConv env a b -> EnvWf env
+termWfImpliesEnvWf : TermWf env t a -> EnvWf env
+termConvImpliesEnvWf : TermConv env t u a -> EnvWf env
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
-- 
cgit v1.2.3