diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-16 15:05:52 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-16 15:05:52 +0100 |
| commit | 2ab0a78d642c602599f4d6a23372c0c91b9f27f0 (patch) | |
| tree | 0ee014644d849850b4e47d6e371093b0edccbf4d /src | |
| parent | 5a53c75f533f2ae758635e1989c4e7fb2b6469d5 (diff) | |
Prove reduction is deterministic.
Diffstat (limited to 'src')
| -rw-r--r-- | src/Core/Reduction.idr | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/src/Core/Reduction.idr b/src/Core/Reduction.idr index 9015d14..9e1d318 100644 --- a/src/Core/Reduction.idr +++ b/src/Core/Reduction.idr @@ -8,6 +8,8 @@ import Core.Term.Substitution import Core.Term.Thinned import Core.Thinning +%prefix_record_projections off + -- Definition ------------------------------------------------------------------ public export @@ -154,3 +156,34 @@ 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) + +-- Reduction is Deterministic -------------------------------------------------- + +export +termStepDeterministic : TermStep env t u a -> TermStep env t v b -> u = v +termStepDeterministic (ConvStep step1 tyConv) step2 = termStepDeterministic step1 step2 +termStepDeterministic step1 (ConvStep step2 tyConv) = termStepDeterministic step1 step2 +termStepDeterministic (AppStep step1 _) (AppStep step2 _) = + cong (flip App _) $ + termStepDeterministic step1 step2 +termStepDeterministic (AppStep step1 _) (PiBeta _ _ _) = absurd (whnfNoTermStep Abs step1) +termStepDeterministic (PiBeta _ _ _) (AppStep step2 _) = absurd (whnfNoTermStep Abs step2) +termStepDeterministic (PiBeta _ _ _) (PiBeta _ _ _) = Refl + +export +typeStepDeterministic : TypeStep env a b -> TypeStep env a c -> b = c +typeStepDeterministic = termStepDeterministic + +export +typeRedDeterministic : TypeReduce env a b -> TypeReduce env a c -> Whnf b -> Whnf c -> b = c +typeRedDeterministic (Refl _) steps2 n m = whnfTypeRedStays n steps2 +typeRedDeterministic steps1 (Refl _) n m = sym $ whnfTypeRedStays m steps1 +typeRedDeterministic (Step step1 steps1) (Step step2 steps2) n m = + typeRedDeterministic steps1 (rewrite typeStepDeterministic step1 step2 in steps2) n m + +export +termRedDeterministic : TermReduce env t u a -> TermReduce env t v b -> Whnf u -> Whnf v -> u = v +termRedDeterministic (Refl _) steps2 n m = whnfTermRedStays n steps2 +termRedDeterministic steps1 (Refl _) n m = sym $ whnfTermRedStays m steps1 +termRedDeterministic (Step step1 steps1) (Step step2 steps2) n m = + termRedDeterministic steps1 (rewrite termStepDeterministic step1 step2 in steps2) n m |