From aa6aeb440ee83b92348b170b7a7312e0e85a7a95 Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Wed, 28 Jun 2023 11:39:16 -0700
Subject: [PATCH] def: normal forms, confluence implies uniqueness

---
 .../Rel/Closure/ReflexiveTransitive.lagda.md  | 23 ++++++
 src/Rewriting/Base.lagda.md                   | 73 +++++++++++++++++++
 src/Rewriting/Confluent.lagda.md              | 23 ++++++
 src/Rewriting/StronglyNormalising.lagda.md    |  2 +-
 4 files changed, 120 insertions(+), 1 deletion(-)

diff --git a/src/Data/Rel/Closure/ReflexiveTransitive.lagda.md b/src/Data/Rel/Closure/ReflexiveTransitive.lagda.md
index 37207f1ab..fc59f59c7 100644
--- a/src/Data/Rel/Closure/ReflexiveTransitive.lagda.md
+++ b/src/Data/Rel/Closure/ReflexiveTransitive.lagda.md
@@ -132,6 +132,29 @@ Refl-trans-case-fork {R' = R'} {R = R} S refll reflr fork prop {a} {x} {y} a→*
     a→*x a→*y
 ```
 
+Similarly, we provide an eliminator for inspecting wedges.
+
+```agda
+Refl-trans-case-wedge
+  : (S : A → A → A → Type ℓ)
+  → (∀ {z} → S z z z)
+  → (∀ {x y y' z} → R' y y' → Refl-trans R' y' z → S x y z)
+  → (∀ {x x' y z} → R x x' → Refl-trans R x' z → S x y z)
+  → (∀ {x y z} → is-prop (S x y z))
+  → ∀ {x y z} → Refl-trans R x z → Refl-trans R' y z → S x y z
+Refl-trans-case-wedge {R' = R'} {R = R} S refl2 wedgel wedger prop {x} {y} {z} x→*z y→*z =
+  Refl-trans-rec-chain (λ x z → Refl-trans R' y z → S x y z)
+    (λ y→*z → Refl-trans-rec-chain (λ y z → S z y z)
+      refl2
+      (λ y→y' y'→*z _ → wedgel y→y' y'→*z)
+      prop
+      y→*z)
+    (λ x→x' x'→z _ _ → wedger x→x' x'→z)
+    (Π-is-hlevel 1 λ _ → prop)
+    x→*z y→*z
+```
+
+
 ## As a closure operator
 
 ```agda
diff --git a/src/Rewriting/Base.lagda.md b/src/Rewriting/Base.lagda.md
index dd882ab57..989cd1ad7 100644
--- a/src/Rewriting/Base.lagda.md
+++ b/src/Rewriting/Base.lagda.md
@@ -126,3 +126,76 @@ resolvable-⊆
 resolvable-⊆ p q r s sq {x = x} {y = y} x↝y x↝z =
   joinable-⊆ r s x y (sq (p x↝y) (q x↝z))
 ```
+
+## Normal Forms
+
+Let $R$ be an abstract rewriting relation on a type $A$. We say
+that an element $x : A$ is a **normal form** if it cannot be reduced
+by $R$.
+
+```agda
+is-normal-form : (R : Rel A A ℓ) → A → Type _
+is-normal-form {A = A} R x = ¬ Σ[ y ∈ A ] R x y
+```
+
+A normal form of $x : A$ is another $y : A$ such that $y$ is a normal form
+and $R^{*}(x,y)$. Note that this is untruncated; uniqueness of normal forms
+shall be derived from other properties of $R$.
+
+```agda
+record Normal-form {A : Type ℓ} (R : Rel A A ℓ') (x : A) : Type (ℓ ⊔ ℓ') where
+  constructor normal-form
+  no-eta-equality
+  field
+    nf : A
+    reduces : Refl-trans R x nf
+    has-normal-form : is-normal-form R nf
+
+open Normal-form
+```
+
+If $A$ is a set, then the type of normal forms is also a set.
+
+```agda
+private unquoteDecl eqv = declare-record-iso eqv (quote Normal-form)
+
+Normal-form-is-hlevel
+  : ∀ {R : A → A → Type ℓ} {x}
+  → (n : Nat) → is-hlevel A (2 + n) → is-hlevel (Normal-form R x) (2 + n)
+Normal-form-is-hlevel n A-set =
+  Iso→is-hlevel (2 + n) eqv (Σ-is-hlevel (2 + n) A-set hlevel!)
+```
+
+<!--
+```agda
+instance
+  H-Level-normal-form
+    : ∀ {R : A → A → Type ℓ} {x} {n}
+    → ⦃ A-hlevel : ∀ {n} → H-Level A (2 + n) ⦄ → H-Level (Normal-form R x) (2 + n)
+  H-Level-normal-form ⦃ A-hlevel ⦄ =
+    basic-instance 2 (Normal-form-is-hlevel 0 (H-Level.has-hlevel {n = 2} A-hlevel))
+
+Normal-form-pathp
+  : ∀ {x y}
+  → (p : x ≡ y)
+  → (x-nf : Normal-form R x) → (y-nf : Normal-form R y)
+  → x-nf .nf ≡ y-nf. nf
+  → PathP (λ i → Normal-form R (p i)) x-nf y-nf
+Normal-form-pathp p x-nf y-nf nf-path i .nf = nf-path i
+Normal-form-pathp {R = R} p x-nf y-nf nf-path i .reduces =
+  is-prop→pathp {B = λ i → Refl-trans R (p i) (nf-path i)}
+    (λ i → trunc)
+    (x-nf .reduces) (y-nf .reduces) i
+Normal-form-pathp {R = R} p x-nf y-nf nf-path i .has-normal-form =
+  is-prop→pathp {B = λ i → is-normal-form R (nf-path i)}
+    (λ i → hlevel!)
+    (x-nf .has-normal-form) (y-nf .has-normal-form) i
+
+Normal-form-path
+  : ∀ {x}
+  → (x-nf x-nf' : Normal-form R x)
+  → x-nf .nf ≡ x-nf'. nf
+  → x-nf ≡ x-nf'
+Normal-form-path x-nf x-nf' p = Normal-form-pathp refl x-nf x-nf' p
+```
+-->
diff --git a/src/Rewriting/Confluent.lagda.md b/src/Rewriting/Confluent.lagda.md
index 144066369..ee3233ab2 100644
--- a/src/Rewriting/Confluent.lagda.md
+++ b/src/Rewriting/Confluent.lagda.md
@@ -103,6 +103,29 @@ refl-trans-clo-equiv+confluent→confluent eqv R-conf {x} {y} {z} =
     R-conf {x} {y} {z}
 ```
 
+If a rewrite system on a set is confluent, then every element of $A$
+has at most one normal form.
+
+```agda
+confluent→unique-normal-forms
+  : ∀ {R : A → A → Type ℓ}
+  → is-set A
+  → is-confluent R 
+  → ∀ x → is-prop (Normal-form R x)
+confluent→unique-normal-forms {R = R} A-set conf x y-nf z-nf =
+  ∥-∥-proj (Normal-form-is-hlevel 0 A-set y-nf z-nf) $ do
+    w , y↝w , z↝w ← conf (y-nf .reduces) (z-nf .reduces)
+    p ← Refl-trans-case-wedge
+         (λ y z w → is-normal-form R y → is-normal-form R z → ∥ y ≡ z ∥)
+         (λ _ _ → inc refl)
+         (λ z→z' _ _ z-nf → absurd (z-nf (_ , z→z')))
+         (λ y→y' _ y-nf _ → absurd (y-nf (_ , y→y')))
+         hlevel!
+         y↝w z↝w (y-nf .has-normal-form) (z-nf .has-normal-form)
+    pure (Normal-form-path y-nf z-nf p)
+    where open Normal-form
+```
+
 
 ## The Church-Rosser Property
 
diff --git a/src/Rewriting/StronglyNormalising.lagda.md b/src/Rewriting/StronglyNormalising.lagda.md
index 81354cb28..02f281549 100644
--- a/src/Rewriting/StronglyNormalising.lagda.md
+++ b/src/Rewriting/StronglyNormalising.lagda.md
@@ -56,7 +56,7 @@ step $a_0 \leadsto a_1$ of the sequence.
 ```agda
 strongly-normalising→terminating : is-strongly-normalising _↝_ → is-terminating _↝_
 strongly-normalising→terminating {_↝_ = _↝_} sn ∥chain∥ =
-  ∥-∥-proj $ do
+  ∥-∥-proj! $ do
     (aₙ , step) ← ∥chain∥
     inc $ Wf-induction _ sn
       (λ a → ∀ n → ¬ Trans _↝_ a (aₙ (suc n)))