refactor: introduce 'strict-or' and upgrade 1lab (#46)

Dockerfile

@@ -6,7 +6,7 @@ ARG GHC_VERSION=9.4.7
 FROM fossa/haskell-static-alpine:ghc-${GHC_VERSION} AS agda
 
 WORKDIR /build/agda
-ARG AGDA_VERSION=5c8116227e2d9120267aed43f0e545a65d9c2fe2
+ARG AGDA_VERSION=8ede3561ae32257eb7a102b8301c61fae1debb23
 RUN \
   git init && \
   git remote add origin https://github.com/agda/agda.git && \
@@ -31,7 +31,7 @@ FROM alpine AS onelab
 RUN apk add --no-cache git
 
 WORKDIR /dist/1lab
-ARG ONELAB_VERSION=a84319a523d866afc828535ce669ed114fbb5fd1
+ARG ONELAB_VERSION=ab2c18bb879a9944dac6e0ba61c662197a7f1965
 RUN \
   git init && \
   git remote add origin https://github.com/plt-amy/1lab && \

README.md

@@ -37,21 +37,9 @@ This is a formalization of the displacement algebras, their properties, and part
 
 ## Building
 
-### Docker (tested by CI)
-
 Run the following command to check formalization.
 
 ```sh
 docker build -t agda-mugen:edge .
 docker run agda-mugen:edge
 ```
-
-### Direct
-
-1. Set up a working Haskell toolchain, for example using [ghcup](https://www.haskell.org/ghcup/).
-
-2. Compile and install [Agda](https://github.com/agda/agda) at the commit `5c8116227e2d9120267aed43f0e545a65d9c2fe2`. You will have to build Agda from the source.
-
-3. Install [1Lab](https://github.com/plt-amy/1lab) and add the path to its `1lab.agda-lib` to `${AGDA_DIR}/libraries`. This formalization was checked against the commit `a84319a523d866afc828535ce669ed114fbb5fd1` of the 1lab library.
-
-4. Type check the formalization by running `make`.

src/Mugen/Algebra/Displacement/FiniteSupport.agda

@@ -23,10 +23,10 @@ open import Mugen.Algebra.OrderedMonoid
 -- These are a special case of the Nearly Constant functions where the base is always ε
 -- and are implemented as such.
 
-module FinSupport {o r} (𝒟 : Displacement-algebra o r) (_≡?_ : Discrete ⌞ 𝒟 ⌟) where
+module FinSupport {o r} (𝒟 : Displacement-algebra o r) ⦃ _ : Discrete ⌞ 𝒟 ⌟ ⦄ where
   private
     module 𝒟 = Displacement-algebra 𝒟
-    open NearlyConst 𝒟 _≡?_
+    open NearlyConst 𝒟
 
   --------------------------------------------------------------------------------
   -- Finite Support Lists
@@ -78,10 +78,10 @@ module FinSupport {o r} (𝒟 : Displacement-algebra o r) (_≡?_ : Discrete ⌞
 --------------------------------------------------------------------------------
 -- Displacement Algebra
 
-module _ {o r} (𝒟 : Displacement-algebra o r) (_≡?_ : Discrete ⌞ 𝒟 ⌟) where
-  open FinSupport 𝒟 _≡?_
+module _ {o r} (𝒟 : Displacement-algebra o r) ⦃ _ : Discrete ⌞ 𝒟 ⌟ ⦄ where
+  open FinSupport 𝒟
   open FinSupportList
-  private module 𝒩 = Displacement-algebra (NearlyConstant 𝒟 _≡?_)
+  private module 𝒩 = Displacement-algebra (NearlyConstant 𝒟)
 
   FiniteSupport : Displacement-algebra o r
   FiniteSupport = to-displacement-algebra mk where
@@ -113,11 +113,11 @@ module _
   {o r}
   {𝒟 : Displacement-algebra o r}
   (let module 𝒟 = Displacement-algebra 𝒟)
-  (_≡?_ : Discrete ⌞ 𝒟 ⌟)
+  ⦃ _ : Discrete ⌞ 𝒟 ⌟ ⦄
   where
-  open FinSupport 𝒟 _≡?_
+  open FinSupport 𝒟
 
-  FinSupport⊆NearlyConstant : is-displacement-subalgebra (FiniteSupport 𝒟 _≡?_) (NearlyConstant 𝒟 _≡?_)
+  FinSupport⊆NearlyConstant : is-displacement-subalgebra (FiniteSupport 𝒟) (NearlyConstant 𝒟)
   FinSupport⊆NearlyConstant = to-displacement-subalgebra mk where
     mk : make-displacement-subalgebra _ _
     mk .make-displacement-subalgebra.into = FinSupportList.support
@@ -126,11 +126,11 @@ module _
     mk .make-displacement-subalgebra.mono _ _ xs<ys = xs<ys
     mk .make-displacement-subalgebra.inj = fin-support-list-path
 
-  FinSupport⊆IdxProd : is-displacement-subalgebra (FiniteSupport 𝒟 _≡?_) (IdxProd Nat λ _ → 𝒟)
+  FinSupport⊆IdxProd : is-displacement-subalgebra (FiniteSupport 𝒟) (IdxProd Nat λ _ → 𝒟)
   FinSupport⊆IdxProd =
     is-displacement-subalgebra-trans
       FinSupport⊆NearlyConstant
-      (NearlyConstant⊆IdxProd _≡?_)
+      NearlyConstant⊆IdxProd
 
 --------------------------------------------------------------------------------
 -- Ordered Monoid
@@ -140,14 +140,14 @@ module _
   {𝒟 : Displacement-algebra o r}
   (let module 𝒟 = Displacement-algebra 𝒟)
   (𝒟-ordered-monoid : has-ordered-monoid 𝒟)
-  (_≡?_ : Discrete ⌞ 𝒟 ⌟)
+  ⦃ _ : Discrete ⌞ 𝒟 ⌟ ⦄
   where
-  open FinSupport 𝒟 _≡?_
+  open FinSupport 𝒟
   open FinSupportList
 
-  fin-support-ordered-monoid : has-ordered-monoid (FiniteSupport 𝒟 _≡?_)
-  fin-support-ordered-monoid = right-invariant→has-ordered-monoid (FiniteSupport 𝒟 _≡?_) λ {xs} {ys} {zs} xs≤ys →
-    supp≤-right-invariant {𝒟 = 𝒟} 𝒟-ordered-monoid _≡?_ {xs .support} {ys .support} {zs .support} xs≤ys
+  fin-support-ordered-monoid : has-ordered-monoid (FiniteSupport 𝒟)
+  fin-support-ordered-monoid = right-invariant→has-ordered-monoid (FiniteSupport 𝒟) λ {xs} {ys} {zs} xs≤ys →
+    supp≤-right-invariant {𝒟 = 𝒟} 𝒟-ordered-monoid {xs .support} {ys .support} {zs .support} xs≤ys
 
 --------------------------------------------------------------------------------
 -- Extensionality based on 'finite-support-list' and eventually 'index-inj'
@@ -156,10 +156,10 @@ module _
 module _ {o r}
   {𝒟 : Displacement-algebra o r}
   (let module 𝒟 = Displacement-algebra 𝒟)
-  {_≡?_ : Discrete ⌞ 𝒟 ⌟}
+  ⦃ _ : Discrete ⌞ 𝒟 ⌟ ⦄
   where
-  open NearlyConst 𝒟 _≡?_
-  open FinSupport 𝒟 _≡?_
+  open NearlyConst 𝒟
+  open FinSupport 𝒟
   open FinSupportList
 
   Extensional-FinSupportList : ∀ {ℓr} ⦃ s : Extensional SupportList ℓr ⦄ → Extensional FinSupportList ℓr

src/Mugen/Algebra/Displacement/Fractal.agda

@@ -50,7 +50,8 @@ module _
 
   data fractal[_≤_] : List⁺ ⌞ 𝒟 ⌟ → List⁺ ⌞ 𝒟 ⌟ → Type (o ⊔ r) where
     single≤ : ∀ {x y} → x 𝒟.≤ y → fractal[ [ x ] ≤ [ y ] ]
-    tail≤   : ∀ {x xs y ys} → x 𝒟.≤ y → (x ≡ y → fractal[ xs ≤ ys ]) → fractal[ x ∷ xs ≤ y ∷ ys ]
+    tail≤'   : ∀ {x xs y ys} → strict-or 𝒟._≤_ x y fractal[ xs ≤ ys ] → fractal[ x ∷ xs ≤ y ∷ ys ]
+  pattern tail≤ α β = tail≤' (α , β)
 
   ≤ᶠ-refl : ∀ (xs : List⁺ ⌞ 𝒟 ⌟) → fractal[ xs ≤ xs ]
   ≤ᶠ-refl [ x ] = single≤ 𝒟.≤-refl

src/Mugen/Algebra/Displacement/Int.agda

@@ -1,5 +1,7 @@
 module Mugen.Algebra.Displacement.Int where
 
+open import Data.Int.Inductive
+
 open import Mugen.Prelude
 open import Mugen.Algebra.Displacement
 

src/Mugen/Algebra/Displacement/Lexicographic.agda

@@ -30,7 +30,7 @@ module Lex {o r} (𝒟₁ 𝒟₂ : Displacement-algebra o r) where
   -- Ordering
 
   lex≤ : ∀ (x : ⌞ 𝒟₁ ⌟ × ⌞ 𝒟₂ ⌟) (y : ⌞ 𝒟₁ ⌟ × ⌞ 𝒟₂ ⌟) → Type (o ⊔ r)
-  lex≤ x y = (fst x 𝒟₁.≤ fst y) × (fst x ≡ fst y → snd x 𝒟₂.≤ snd y)
+  lex≤ x y = strict-or 𝒟₁._≤_ (x .fst) (y .fst) (snd x 𝒟₂.≤ snd y)
 
   lex≤-refl : ∀ x → lex≤ x x
   lex≤-refl x = 𝒟₁.≤-refl , λ _ → 𝒟₂.≤-refl
@@ -124,7 +124,7 @@ module LexProperties {o r} {𝒟₁ 𝒟₂ : Displacement-algebra o r} where
     → (∀ x y → Dec (x ≡ 𝒟₁-joins.join x y) × Dec (y ≡ 𝒟₁-joins.join x y))
     → (𝒟₂-joins : has-joins 𝒟₂) → has-bottom 𝒟₂
     → has-joins (Lex 𝒟₁ 𝒟₂)
-                
+
   lex-has-joins 𝒟₁-joins _≡∨₁?_ 𝒟₂-joins 𝒟₂-bottom = joins
     where
       module 𝒟₁-joins = has-joins 𝒟₁-joins

src/Mugen/Algebra/Displacement/Nat.agda

@@ -1,5 +1,7 @@
 module Mugen.Algebra.Displacement.Nat where
 
+open import Data.Int.Inductive
+
 open import Mugen.Prelude
 open import Mugen.Algebra.Displacement
 open import Mugen.Algebra.Displacement.Int
@@ -56,11 +58,11 @@ nat-+-has-bottom .has-bottom.is-bottom x = Nat.0≤x
 Nat+⊆Int+ : is-displacement-subalgebra Nat+ Int+
 Nat+⊆Int+ = to-displacement-subalgebra subalg where
     subalg : make-displacement-subalgebra _ _
-    subalg .make-displacement-subalgebra.into = Int.pos
+    subalg .make-displacement-subalgebra.into = pos
     subalg .make-displacement-subalgebra.pres-ε = refl
     subalg .make-displacement-subalgebra.pres-⊗ = Int.+ℤ-pos
     subalg .make-displacement-subalgebra.mono _ _ x≤y = x≤y
-    subalg .make-displacement-subalgebra.inj = Int.pos-inj
+    subalg .make-displacement-subalgebra.inj = pos-injective
 
 Nat-is-subsemilattice : is-displacement-subsemilattice nat-+-has-joins Int+-has-joins
 Nat-is-subsemilattice .is-displacement-subsemilattice.has-displacement-subalgebra = Nat+⊆Int+

src/Mugen/Algebra/Displacement/NearlyConstant.agda

@@ -41,7 +41,7 @@ open import Mugen.Algebra.OrderedMonoid
 module NearlyConst
   {o r}
   (𝒟 : Displacement-algebra o r)
-  (_≡?_ : Discrete ⌞ 𝒟 ⌟)
+  ⦃ _ : Discrete ⌞ 𝒟 ⌟ ⦄
   where
   private module 𝒟 = Displacement-algebra 𝒟
   open Idx Nat (λ _ → 𝒟)
@@ -254,11 +254,11 @@ module NearlyConst
       index-compacted-inj (raw (x ∷ xs) b1) (raw [] b2) x∷xs-compact []-compact p =
         let xs-compact = tail-is-compact x (raw xs b1) x∷xs-compact in
         let xs=[] = index-compacted-inj (raw xs b1) (raw [] b2) xs-compact []-compact (p ⊙ suc) in
-        absurd $ base-singleton-isnt-compact (p 0) xs=[] x∷xs-compact
+        absurd (base-singleton-isnt-compact (p 0) xs=[] x∷xs-compact)
       index-compacted-inj (raw [] b1) (raw (y ∷ ys) b2) []-compact y∷ys-compact p =
         let ys-compact = tail-is-compact y (raw ys b2) y∷ys-compact in
         let []=ys = index-compacted-inj (raw [] b1) (raw ys b2) []-compact ys-compact (p ⊙ suc) in
-        absurd $ base-singleton-isnt-compact (sym (p 0)) (sym []=ys) y∷ys-compact
+        absurd $ᵢ base-singleton-isnt-compact (sym (p 0)) (sym []=ys) y∷ys-compact
       index-compacted-inj (raw (x ∷ xs) b1) (raw (y ∷ ys) b2) x∷xs-compact y∷ys-compact p =
         let xs-compact = tail-is-compact x (raw xs b1) x∷xs-compact in
         let ys-compact = tail-is-compact y (raw ys b2) y∷ys-compact in
@@ -346,10 +346,10 @@ module NearlyConst
 --------------------------------------------------------------------------------
 -- Bundled Instances
 
-module _ {o r} (𝒟 : Displacement-algebra o r) (_≡?_ : Discrete ⌞ 𝒟 ⌟) where
+module _ {o r} (𝒟 : Displacement-algebra o r) ⦃ _ : Discrete ⌞ 𝒟 ⌟ ⦄ where
   private module 𝒟 = Displacement-algebra 𝒟
   open Idx Nat (λ _ → 𝒟)
-  open NearlyConst 𝒟 _≡?_
+  open NearlyConst 𝒟
 
   NearlyConstant : Displacement-algebra o r
   NearlyConstant = to-displacement-algebra mk where
@@ -386,12 +386,12 @@ module _ {o r} (𝒟 : Displacement-algebra o r) (_≡?_ : Discrete ⌞ 𝒟 ⌟
 --------------------------------------------------------------------------------
 -- Subalgebra Structure
 
-module _ {o r} {𝒟 : Displacement-algebra o r} (_≡?_ : Discrete ⌞ 𝒟 ⌟) where
-  open NearlyConst 𝒟 _≡?_
+module _ {o r} {𝒟 : Displacement-algebra o r} ⦃ _ : Discrete ⌞ 𝒟 ⌟ ⦄ where
+  open NearlyConst 𝒟
 
-  NearlyConstant⊆IdxProd : is-displacement-subalgebra (NearlyConstant 𝒟 _≡?_) (IdxProd Nat λ _ → 𝒟)
+  NearlyConstant⊆IdxProd : is-displacement-subalgebra (NearlyConstant 𝒟) (IdxProd Nat λ _ → 𝒟)
   NearlyConstant⊆IdxProd = to-displacement-subalgebra mk where
-    mk : make-displacement-subalgebra (NearlyConstant 𝒟 _≡?_) (IdxProd Nat λ _ → 𝒟)
+    mk : make-displacement-subalgebra (NearlyConstant 𝒟) (IdxProd Nat λ _ → 𝒟)
     mk .make-displacement-subalgebra.into = index
     mk .make-displacement-subalgebra.pres-ε = refl
     mk .make-displacement-subalgebra.pres-⊗ xs ys = index-merge xs ys
@@ -405,20 +405,20 @@ module _
   {o r}
   {𝒟 : Displacement-algebra o r}
   (𝒟-ordered-monoid : has-ordered-monoid 𝒟)
-  (_≡?_ : Discrete ⌞ 𝒟 ⌟)
+  ⦃ _ : Discrete ⌞ 𝒟 ⌟ ⦄
   where
   private module 𝒟 = Displacement-algebra 𝒟
   open Idx Nat (λ _ → 𝒟)
-  open NearlyConst 𝒟 _≡?_
+  open NearlyConst 𝒟
   open is-ordered-monoid (idx⊗-has-ordered-monoid Nat (λ _ → 𝒟) (λ _ → 𝒟-ordered-monoid))
 
   supp≤-right-invariant : ∀ {xs ys zs} → xs supp≤ ys → merge xs zs supp≤ merge ys zs
   supp≤-right-invariant {xs} {ys} {zs} xs≤ys =
     coe1→0 (λ i → index-merge xs zs i idx≤ index-merge ys zs i) $
     right-invariant xs≤ys
 
-  nearly-constant-has-ordered-monoid : has-ordered-monoid (NearlyConstant 𝒟 _≡?_)
-  nearly-constant-has-ordered-monoid = right-invariant→has-ordered-monoid (NearlyConstant 𝒟 _≡?_) $ λ {xs} {ys} {zs} →
+  nearly-constant-has-ordered-monoid : has-ordered-monoid (NearlyConstant 𝒟)
+  nearly-constant-has-ordered-monoid = right-invariant→has-ordered-monoid (NearlyConstant 𝒟) $ λ {xs} {ys} {zs} →
     supp≤-right-invariant {xs} {ys} {zs}
 
 --------------------------------------------------------------------------------
@@ -428,10 +428,10 @@ module NearlyConstJoins
   {o r}
   {𝒟 : Displacement-algebra o r}
   (𝒟-joins : has-joins 𝒟)
-  (_≡?_ : Discrete ⌞ 𝒟 ⌟)
+  ⦃ _ : Discrete ⌞ 𝒟 ⌟ ⦄
   where
   open Idx Nat (λ _ → 𝒟)
-  open NearlyConst 𝒟 _≡?_
+  open NearlyConst 𝒟
   private module 𝒟 = Displacement-algebra 𝒟
   private module 𝒥 = has-joins 𝒟-joins
   private module idx𝒥 = has-joins (idx⊗-has-joins Nat (λ _ → 𝒟) (λ _ → 𝒟-joins))
@@ -442,7 +442,7 @@ module NearlyConstJoins
   index-preserves-join : ∀ xs ys → index (join xs ys) ≡ idx𝒥.join (index xs) (index ys)
   index-preserves-join = index-merge-with 𝒥.join
 
-  nearly-constant-has-joins : has-joins (NearlyConstant 𝒟 _≡?_)
+  nearly-constant-has-joins : has-joins (NearlyConstant 𝒟)
   nearly-constant-has-joins .has-joins.join = join
   nearly-constant-has-joins .has-joins.joinl {xs} {ys} n =
     𝒟.≤+=→≤ 𝒥.joinl (sym $ happly (index-preserves-join xs ys) n)
@@ -452,7 +452,7 @@ module NearlyConstJoins
     𝒟.=+≤→≤ (happly (index-preserves-join xs ys) n) (𝒥.universal (xs≤zs n) (ys≤zs n))
 
   nearly-constant-is-subsemilattice : is-displacement-subsemilattice nearly-constant-has-joins (idx⊗-has-joins Nat (λ _ → 𝒟) (λ _ → 𝒟-joins))
-  nearly-constant-is-subsemilattice .is-displacement-subsemilattice.has-displacement-subalgebra = NearlyConstant⊆IdxProd _≡?_
+  nearly-constant-is-subsemilattice .is-displacement-subsemilattice.has-displacement-subalgebra = NearlyConstant⊆IdxProd
   nearly-constant-is-subsemilattice .is-displacement-subsemilattice.pres-joins x y = index-preserves-join x y
 
 --------------------------------------------------------------------------------
@@ -462,18 +462,18 @@ module _
   {o r}
   {𝒟 : Displacement-algebra o r}
   (𝒟-bottom : has-bottom 𝒟)
-  (_≡?_ : Discrete ⌞ 𝒟 ⌟)
+  ⦃ _ : Discrete ⌞ 𝒟 ⌟ ⦄
   where
   private module 𝒟 = Displacement-algebra 𝒟
-  open NearlyConst 𝒟 _≡?_
+  open NearlyConst 𝒟
   open has-bottom 𝒟-bottom
 
-  nearly-constant-has-bottom : has-bottom (NearlyConstant 𝒟 _≡?_)
+  nearly-constant-has-bottom : has-bottom (NearlyConstant 𝒟)
   nearly-constant-has-bottom .has-bottom.bot = support-list (raw [] bot) (lift tt)
   nearly-constant-has-bottom .has-bottom.is-bottom xs n = is-bottom _
 
   nearly-constant-is-bounded-subalgebra : is-bounded-displacement-subalgebra nearly-constant-has-bottom (idx⊗-has-bottom Nat (λ _ → 𝒟) (λ _ → 𝒟-bottom))
-  nearly-constant-is-bounded-subalgebra .is-bounded-displacement-subalgebra.has-displacement-subalgebra = NearlyConstant⊆IdxProd _≡?_
+  nearly-constant-is-bounded-subalgebra .is-bounded-displacement-subalgebra.has-displacement-subalgebra = NearlyConstant⊆IdxProd
   nearly-constant-is-bounded-subalgebra .is-bounded-displacement-subalgebra.pres-bottom = refl
 
 --------------------------------------------------------------------------------
@@ -484,10 +484,10 @@ module _
 -- So we re-parametrize things with implicit '𝒟' and '_≡?_'.
 module _ {o r}
   {𝒟 : Displacement-algebra o r}
-  {_≡?_ : Discrete ⌞ 𝒟 ⌟}
+  ⦃ _ : Discrete ⌞ 𝒟 ⌟ ⦄
   where
   private module 𝒟 = Displacement-algebra 𝒟
-  open NearlyConst 𝒟 _≡?_
+  open NearlyConst 𝒟
 
   Extensional-SupportList : ∀ {ℓr} ⦃ s : Extensional ⌞ 𝒟 ⌟ ℓr ⦄ → Extensional SupportList ℓr
   Extensional-SupportList ⦃ s ⦄ .Pathᵉ xs ys =