Prove reduction is deterministic.

1 files changed, 22 insertions, 0 deletions

diff --git a/src/Core/Reduction.idr b/src/Core/Reduction.idr
index 5a9622e..b50b8c2 100644
--- a/src/Core/Reduction.idr
+++ b/src/Core/Reduction.idr
@@ -106,6 +106,28 @@ termRedWhnfStays n (step :: steps) = absurd $ termStepWhnfImpossible n step
 -- Reduction is Deterministic --------------------------------------------------
 
 termStepDeterministic : TermStep env t u a -> TermStep env t v b -> u = v
+termStepDeterministic (StepConv step conv) step1 = termStepDeterministic step step1
+termStepDeterministic step (StepConv step1 conv) = termStepDeterministic step step1
+termStepDeterministic (PiBeta _ _ _) (PiBeta _ _ _) = Refl
+termStepDeterministic (PiBeta _ _ _) (AppStep step _) = absurd $ termStepWhnfImpossible Abs step
+termStepDeterministic (AppStep step _) (PiBeta _ _ _) = absurd $ termStepWhnfImpossible Abs step
+termStepDeterministic (AppStep step _) (AppStep step1 _) =
+  cong (flip App _) $
+  termStepDeterministic step step1
+
 typeStepDeterministic : TypeStep env a b -> TypeStep env a c -> b = c
+typeStepDeterministic = termStepDeterministic
+
 typeRedDeterministic : TypeRed env a b -> TypeRed env a c -> Whnf b -> Whnf c -> b = c
+typeRedDeterministic (Stay _) red n m = typeRedWhnfStays n red
+typeRedDeterministic red (Stay _) n m = sym $ typeRedWhnfStays m red
+typeRedDeterministic (step :: steps) (step1 :: steps1) n m =
+  let steps1' = rewrite typeStepDeterministic step step1 in steps1 in
+  typeRedDeterministic steps steps1' n m
+
 termRedDeterministic : TermRed env t u a -> TermRed env t v b -> Whnf u -> Whnf v -> u = v
+termRedDeterministic (Stay _) red n m = termRedWhnfStays n red
+termRedDeterministic red (Stay _) n m = sym $ termRedWhnfStays m red
+termRedDeterministic (step :: steps) (step1 :: steps1) n m =
+  let steps1' : TermRed env _ v b = rewrite termStepDeterministic step step1 in steps1 in
+  termRedDeterministic steps steps1' n m