From ce97db7ea3bf91d3e8496d1135162f5cfbde495d Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Fri, 31 May 2024 09:34:27 -0500
Subject: [PATCH] feat: the "incorrect" Fractal resurges (#57)

---
 .../Instances/IncorrectFractal.agda           | 103 ++++++++++++++++++
 src/Mugen/Everything.agda                     |   1 +
 2 files changed, 104 insertions(+)
 create mode 100644 src/Mugen/Algebra/Displacement/Instances/IncorrectFractal.agda

diff --git a/src/Mugen/Algebra/Displacement/Instances/IncorrectFractal.agda b/src/Mugen/Algebra/Displacement/Instances/IncorrectFractal.agda
new file mode 100644
index 0000000..1236d8b
--- /dev/null
+++ b/src/Mugen/Algebra/Displacement/Instances/IncorrectFractal.agda
@@ -0,0 +1,103 @@
+module Mugen.Algebra.Displacement.Instances.IncorrectFractal where
+
+open import Mugen.Prelude
+open import Mugen.Algebra.Displacement
+open import Mugen.Data.NonEmpty
+open import Mugen.Order.Instances.Fractal
+
+import Mugen.Order.Reasoning as Reasoning
+
+variable
+  o r : Level
+
+--------------------------------------------------------------------------------
+-- "Incorrect" Fractal Displacements from our previous incorrect Agda
+-- formalization of Section 3.3.7 of the POPL 2023 paper. They come with
+-- a different composition operator. Miraculously, it leads to a valid
+-- (but different) displacement algebra.
+--
+-- The correct fractal displacements are available under
+--   Mugen.Algebra.Displacement.Instances.Fractal
+--
+-- This file was created so that we can further study this "wrong" version
+-- of fractal displacements. What is the intuitive explanation of the
+-- "wrong" composition operator?
+
+module _ {A : Poset o r} (𝒟 : Displacement-on A) where
+  private
+    module A = Reasoning A
+    module F = Reasoning (Fractal A)
+    module 𝒟 = Displacement-on 𝒟
+
+    --------------------------------------------------------------------------------
+    -- Algebra
+
+    -- This function is defined differently from the one in Fractal.
+    -- What is the intuitive explanation of this operator?
+    _⊗_ : List⁺ ⌞ A ⌟ → List⁺ ⌞ A ⌟ → List⁺ ⌞ A ⌟
+    [ x ] ⊗ [ y ] = [ x 𝒟.⊗ y ]
+    [ x ] ⊗ (y ∷ ys) = (x 𝒟.⊗ y) ∷ ys
+    (x ∷ xs) ⊗ [ y ] = (x 𝒟.⊗ y) ∷ xs
+    (x ∷ xs) ⊗ (y ∷ ys) = (x 𝒟.⊗ y) ∷ (xs ⊗ ys)
+
+    ε : List⁺ ⌞ A ⌟
+    ε = [ 𝒟.ε ]
+
+    abstract
+      associative : (xs ys zs : List⁺ ⌞ A ⌟) → (xs ⊗ (ys ⊗ zs)) ≡ ((xs ⊗ ys) ⊗ zs)
+      associative [ x ] [ y ] [ z ] = ap [_] 𝒟.associative
+      associative [ x ] [ y ] (z ∷ zs) = ap (_∷ zs) 𝒟.associative
+      associative [ x ] (y ∷ ys) [ z ] = ap (_∷ ys) 𝒟.associative
+      associative [ x ] (y ∷ ys) (z ∷ zs) = ap (_∷ (ys ⊗ zs)) 𝒟.associative
+      associative (x ∷ xs) [ y ] [ z ] = ap (_∷ xs) 𝒟.associative
+      associative (x ∷ xs) [ y ] (z ∷ zs) = ap (_∷ (xs ⊗ zs)) 𝒟.associative
+      associative (x ∷ xs) (y ∷ ys) [ z ] = ap (_∷ (xs ⊗ ys)) 𝒟.associative
+      associative (x ∷ xs) (y ∷ ys) (z ∷ zs) = ap₂ _∷_ 𝒟.associative (associative xs ys zs)
+
+      idl : (xs : List⁺ ⌞ A ⌟) → (ε ⊗ xs) ≡ xs
+      idl [ x ] = ap [_] 𝒟.idl
+      idl (x ∷ xs) = ap (_∷ xs) 𝒟.idl
+
+      idr : (xs : List⁺ ⌞ A ⌟) → (xs ⊗ ε) ≡ xs
+      idr [ x ] = ap [_] 𝒟.idr
+      idr (x ∷ xs) = ap (_∷ xs) 𝒟.idr
+
+    --------------------------------------------------------------------------------
+    -- Left Invariance
+
+    abstract
+      left-invariant : (xs ys zs : List⁺ ⌞ A ⌟) → ys F.≤ zs → (xs ⊗ ys) F.≤ (xs ⊗ zs)
+      left-invariant [ x ] [ y ] [ z ] (single≤ y≤z) =
+        single≤ (𝒟.left-invariant y≤z)
+      left-invariant [ x ] (y ∷ ys) (z ∷ zs) (tail≤ y≤z ys≤zs) =
+        tail≤ (𝒟.left-invariant y≤z) λ xy=xz → ys≤zs (𝒟.injectiver-on-related y≤z xy=xz)
+      left-invariant (x ∷ xs) [ y ] [ z ] (single≤ y≤z) =
+        tail≤ (𝒟.left-invariant y≤z) λ _ → F.≤-refl
+      left-invariant (x ∷ xs) (y ∷ ys) (z ∷ zs) (tail≤ y≤z ys≤zs) =
+        tail≤ (𝒟.left-invariant y≤z) λ xy=xz →
+        left-invariant xs ys zs $ ys≤zs (𝒟.injectiver-on-related y≤z xy=xz)
+
+      injectiver-on-related : (xs ys zs : List⁺ ⌞ A ⌟) → ys F.≤ zs → xs ⊗ ys ≡ xs ⊗ zs → ys ≡ zs
+      injectiver-on-related [ x ] [ y ] [ z ] (single≤ y≤z) p =
+        ap [_] $ 𝒟.injectiver-on-related y≤z $ []-inj p
+      injectiver-on-related [ x ] (y ∷ ys) (z ∷ zs) (tail≤ y≤z _) p =
+        ap₂ _∷_ (𝒟.injectiver-on-related y≤z (∷-head-inj p)) (∷-tail-inj p)
+      injectiver-on-related (x ∷ xs) [ y ] [ z ] (single≤ y≤z) p =
+        ap [_] $ 𝒟.injectiver-on-related y≤z (∷-head-inj p)
+      injectiver-on-related (x ∷ xs) (y ∷ ys) (z ∷ zs) (tail≤ y≤z ys≤zs) p =
+        let y=z = 𝒟.injectiver-on-related y≤z (∷-head-inj p) in
+        ap₂ _∷_ y=z (injectiver-on-related xs ys zs (ys≤zs y=z) (∷-tail-inj p))
+
+  --------------------------------------------------------------------------------
+  -- Displacement Algebra
+
+  IncorrectFractal-displacement : Displacement-on (Fractal A)
+  IncorrectFractal-displacement = to-displacement-on mk where
+    mk : make-displacement (Fractal A)
+    mk .make-displacement.ε = ε
+    mk .make-displacement._⊗_ = _⊗_
+    mk .make-displacement.idl = idl _
+    mk .make-displacement.idr = idr  _
+    mk .make-displacement.associative = associative _ _ _
+    mk .make-displacement.left-strict-invariant p =
+      left-invariant _ _ _ p , injectiver-on-related _ _ _ p
diff --git a/src/Mugen/Everything.agda b/src/Mugen/Everything.agda
index 13e2574..ac91efa 100644
--- a/src/Mugen/Everything.agda
+++ b/src/Mugen/Everything.agda
@@ -8,6 +8,7 @@ import Mugen.Algebra.Displacement.Action
 import Mugen.Algebra.Displacement.Instances.Constant
 import Mugen.Algebra.Displacement.Instances.Endomorphism
 import Mugen.Algebra.Displacement.Instances.Fractal
+import Mugen.Algebra.Displacement.Instances.IncorrectFractal
 import Mugen.Algebra.Displacement.Instances.IndexedProduct
 import Mugen.Algebra.Displacement.Instances.Int
 import Mugen.Algebra.Displacement.Instances.Lexicographic