```------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of the inner lexicographic product of two operators.
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

open import Algebra
open import Data.Bool.Base using (false; true)
open import Data.Product using (_×_; _,_; swap; map; uncurry′)
open import Function.Base using (_∘_)
open import Level using (Level; _⊔_)
open import Relation.Binary.Definitions using (Decidable)
open import Relation.Nullary.Decidable using (does; yes; no)
open import Relation.Nullary.Negation
import Relation.Binary.Reasoning.Setoid as SetoidReasoning

import Algebra.Construct.LexProduct.Base as Base

module Algebra.Construct.LexProduct.Inner
{ℓ₁ ℓ₂ ℓ₃ ℓ₄} (M : Magma ℓ₁ ℓ₂) (N : Magma ℓ₃ ℓ₄)
(_≟₁_ : Decidable (Magma._≈_ M))
where

open module M = Magma M
renaming
( Carrier  to A
; _≈_      to _≈₁_
; _≉_      to _≉₁_
)

open module N = Magma N
using ()
renaming
( Carrier to B
; _∙_     to _◦_
; _≈_     to _≈₂_
; ∙-cong  to ◦-cong
)

private
variable
a b c d : A
w x y z : B

------------------------------------------------------------------------
-- Base definition

open Base _∙_ _◦_ _≟₁_ public
using (innerLex)

-- Save ourselves some typing in this file
private
lex = innerLex

------------------------------------------------------------------------
-- Properties

module NaturalOrder where

-- It would be really nice if we could use
-- `Relation.Binary.Construct.NaturalOrder.Left/Right` to prove these
-- properties but the equalities are defined the wrong way around

open SetoidReasoning M.setoid

≤∙ˡ-resp-≈ : a ∙ b ≈₁ b → a ≈₁ c → b ≈₁ d → c ∙ d ≈₁ d
≤∙ˡ-resp-≈ {a} {b} {c} {d} ab≈b a≈c b≈d = begin
c ∙ d ≈⟨ ∙-cong (M.sym a≈c) (M.sym b≈d) ⟩
a ∙ b ≈⟨ ab≈b ⟩
b     ≈⟨ b≈d ⟩
d     ∎

≤∙ʳ-resp-≈ : a ∙ b ≈₁ a → a ≈₁ c → b ≈₁ d → c ∙ d ≈₁ c
≤∙ʳ-resp-≈ {a} {b} {c} {d} ab≈b a≈c b≈d = begin
c ∙ d ≈⟨ ∙-cong (M.sym a≈c) (M.sym b≈d) ⟩
a ∙ b ≈⟨ ab≈b ⟩
a     ≈⟨ a≈c ⟩
c     ∎

≤∙ˡ-trans : Associative _≈₁_ _∙_ → (a ∙ b) ≈₁ b → (b ∙ c) ≈₁ c → (a ∙ c) ≈₁ c
≤∙ˡ-trans {a} {b} {c} ∙-assoc ab≈b bc≈c = begin
a ∙ c        ≈˘⟨ ∙-congˡ bc≈c ⟩
a ∙ (b ∙ c)  ≈˘⟨ ∙-assoc a b c ⟩
(a ∙ b) ∙ c  ≈⟨  ∙-congʳ ab≈b ⟩
b ∙ c        ≈⟨  bc≈c ⟩
c            ∎

≰∙ˡ-trans : Commutative _≈₁_ _∙_ → (a ∙ b) ≉₁ a → (a ∙ c) ≈₁ c → (b ∙ c) ≈₁ c → (a ∙ c) ≉₁ a
≰∙ˡ-trans {a} {b} {c} ∙-comm ab≉a ac≈c bc≈c ac≈a = ab≉a (begin
a ∙ b  ≈⟨ ∙-congʳ (M.trans (M.sym ac≈a) ac≈c) ⟩
c ∙ b  ≈⟨ ∙-comm c b ⟩
b ∙ c  ≈⟨ bc≈c ⟩
c      ≈⟨ M.trans (M.sym ac≈c) ac≈a ⟩
a      ∎)

<∙ˡ-trans : Associative _≈₁_ _∙_ → Commutative _≈₁_ _∙_ →
(a ∙ b) ≈₁ b → (a ∙ b) ≉₁ a → (b ∙ c) ≈₁ c →
(a ∙ c) ≉₁ a × (a ∙ c) ≈₁ c
<∙ˡ-trans {a} {b} {c} ∙-assoc ∙-comm ab≈b ab≉a bc≈c = ac≉a , ac≈c
where
ac≈c = ≤∙ˡ-trans ∙-assoc ab≈b bc≈c
ac≉a = ≰∙ˡ-trans ∙-comm ab≉a ac≈c bc≈c

<∙ʳ-trans : Associative _≈₁_ _∙_ → Commutative _≈₁_ _∙_ →
(a ∙ b) ≈₁ a → (b ∙ c) ≈₁ b → (b ∙ c) ≉₁ c →
(a ∙ c) ≈₁ a × (a ∙ c) ≉₁ c
<∙ʳ-trans {a} {b} {c} assoc comm ab≈a bc≈b bc≉c = map
(M.trans (comm a c))
(_∘ M.trans (comm c a))
(swap (<∙ˡ-trans assoc comm
(M.trans (comm c b) bc≈b)
(bc≉c ∘ M.trans (comm b c))
(M.trans (comm b a) ab≈a)))

------------------------------------------------------------------------
-- Basic properties

open SetoidReasoning N.setoid
open NaturalOrder

case₁ : a ∙ b ≈₁ a → a ∙ b ≉₁ b → lex a b x y ≈₂ x
case₁ {a} {b} ab≈a ab≉b with (a ∙ b) ≟₁ a | (a ∙ b) ≟₁ b
... | no  ab≉a | _        = contradiction ab≈a ab≉a
... | yes _    | yes ab≈b = contradiction ab≈b ab≉b
... | yes _    | no  _    = N.refl

case₂ : a ∙ b ≉₁ a → a ∙ b ≈₁ b → lex a b x y ≈₂ y
case₂ {a} {b} ab≉a ab≈b with (a ∙ b) ≟₁ a | (a ∙ b) ≟₁ b
... | yes ab≈a | _        = contradiction ab≈a ab≉a
... | no _     | no  ab≉b = contradiction ab≈b ab≉b
... | no _     | yes _    = N.refl

case₃ : a ∙ b ≈₁ a → a ∙ b ≈₁ b → lex a b x y ≈₂ (x ◦ y)
case₃ {a} {b} ab≈a ab≈b with (a ∙ b) ≟₁ a | (a ∙ b) ≟₁ b
... | no  ab≉a | _        = contradiction ab≈a ab≉a
... | yes _    | no  ab≉b = contradiction ab≈b ab≉b
... | yes _    | yes _    = N.refl

------------------------------------------------------------------------
-- Algebraic properties

cong : a ≈₁ b → c ≈₁ d → w ≈₂ x → y ≈₂ z → lex a c w y ≈₂ lex b d x z
cong {a} {b} {c} {d} a≈b c≈d w≈x y≈z
with (a ∙ c) ≟₁ a | (a ∙ c) ≟₁ c | (b ∙ d) ≟₁ b | (b ∙ d) ≟₁ d
... | yes _    | yes _    | yes _    | yes _    = ◦-cong w≈x y≈z
... | yes _    | yes _    | no  _    | no  _    = ◦-cong w≈x y≈z
... | no  _    | no  _    | yes _    | yes _    = ◦-cong w≈x y≈z
... | no  _    | no  _    | no  _    | no  _    = ◦-cong w≈x y≈z
... | yes _    | no  _    | yes _    | no  _    = w≈x
... | no  _    | yes _    | no  _    | yes _    = y≈z
... | _        | yes ac≈c | _        | no bd≉d  = contradiction (≤∙ˡ-resp-≈ ac≈c a≈b c≈d) bd≉d
... | yes ac≈a | _        | no  bd≉b | _        = contradiction (≤∙ʳ-resp-≈ ac≈a a≈b c≈d) bd≉b
... | _        | no  ac≉c | _        | yes bd≈d = contradiction (≤∙ˡ-resp-≈ bd≈d (M.sym a≈b) (M.sym c≈d)) ac≉c
... | no  ac≉a | _        | yes bd≈b | _        = contradiction (≤∙ʳ-resp-≈ bd≈b (M.sym a≈b) (M.sym c≈d)) ac≉a

cong₁₂ : a ≈₁ b → c ≈₁ d → lex a c x y ≈₂ lex b d x y
cong₁₂ a≈b c≈d = cong a≈b c≈d N.refl N.refl

cong₁ : a ≈₁ b → lex a c x y ≈₂ lex b c x y
cong₁ a≈b = cong₁₂ a≈b M.refl

cong₂ : b ≈₁ c → lex a b x y ≈₂ lex a c x y
cong₂ = cong₁₂ M.refl

-- It is possible to relax this. Instead of ∙ being selective and ◦ being associative it's also
-- possible for _◦_ to return a single idempotent element.
assoc : Associative _≈₁_ _∙_ → Commutative _≈₁_ _∙_ →
Selective _≈₁_ _∙_ → Associative _≈₂_ _◦_ →
∀ a b c x y z  → lex (a ∙ b) c (lex a b x y) z  ≈₂ lex a (b ∙ c) x (lex b c y z)
assoc ∙-assoc ∙-comm ∙-sel ◦-assoc a b c x y z
with (a ∙ b) ≟₁ a | (a ∙ b) ≟₁ b | (b ∙ c) ≟₁ b | (b ∙ c) ≟₁ c
... | _        | _        | no  bc≉b | no  bc≉c = contradiction₂ (∙-sel b c) bc≉b bc≉c
... | no  ab≉a | no  ab≉b | _        | _        = contradiction₂ (∙-sel a b) ab≉a ab≉b
... | yes ab≈a | no  ab≉b | no  bc≉b | yes bc≈c = cong₁₂ ab≈a (M.sym bc≈c)
... | no ab≉a  | yes ab≈b | yes bc≈b | yes bc≈c = begin
lex (a ∙ b) c y z        ≈⟨  cong₁ ab≈b ⟩
lex b c y z              ≈⟨  case₃ bc≈b bc≈c ⟩
y ◦ z                    ≈˘⟨ case₂ ab≉a ab≈b ⟩
lex a b x (y ◦ z)        ≈˘⟨ cong₂ bc≈b ⟩
lex a (b ∙ c) x (y ◦ z)  ∎
... | no ab≉a  | yes ab≈b | yes bc≈b | no bc≉c = begin
lex (a ∙ b) c y z        ≈⟨  cong₁ ab≈b ⟩
lex b c y z              ≈⟨  case₁ bc≈b bc≉c ⟩
y                        ≈˘⟨ case₂ ab≉a ab≈b ⟩
lex a b x y              ≈˘⟨ cong₂ bc≈b ⟩
lex a (b ∙ c) x y        ∎
... | yes ab≈a | yes ab≈b | yes bc≈b | no bc≉c = begin
lex (a ∙ b) c (x ◦ y) z  ≈⟨  cong₁ ab≈b ⟩
lex b c (x ◦ y) z        ≈⟨  case₁ bc≈b bc≉c ⟩
x ◦ y                    ≈˘⟨ case₃ ab≈a ab≈b ⟩
lex a b x y              ≈˘⟨ cong₂ bc≈b ⟩
lex a (b ∙ c) x y        ∎
... | yes ab≈a | yes ab≈b | yes bc≈b | yes bc≈c = begin
lex (a ∙ b) c (x ◦ y) z  ≈⟨  cong₁ ab≈b ⟩
lex b c (x ◦ y) z        ≈⟨  case₃ bc≈b bc≈c  ⟩
(x ◦ y) ◦ z              ≈⟨  ◦-assoc x y z ⟩
x ◦ (y ◦ z)              ≈˘⟨ case₃ ab≈a ab≈b ⟩
lex a b x (y ◦ z)        ≈˘⟨ cong₂ bc≈b ⟩
lex a (b ∙ c) x (y ◦ z)  ∎
... | yes ab≈a | yes ab≈b | no bc≉b | yes bc≈c = begin
lex (a ∙ b) c (x ◦ y) z  ≈⟨  cong₁ ab≈b ⟩
lex b c (x ◦ y) z        ≈⟨  case₂ bc≉b bc≈c ⟩
z                        ≈˘⟨ case₂ bc≉b bc≈c ⟩
lex b c x z              ≈˘⟨ cong₁₂ (M.trans (M.sym ab≈a) ab≈b) bc≈c ⟩
lex a (b ∙ c) x z        ∎
... | yes ab≈a | no ab≉b | yes bc≈b | yes bc≈c = begin
lex (a ∙ b) c x z        ≈⟨  cong₁₂ ab≈a (M.trans (M.sym bc≈c) bc≈b) ⟩
lex a b x z              ≈⟨  case₁ ab≈a ab≉b ⟩
x                        ≈˘⟨ case₁ ab≈a ab≉b ⟩
lex a b x (y ◦ z)        ≈˘⟨ cong₂ bc≈b ⟩
lex a (b ∙ c) x (y ◦ z)  ∎
... | no ab≉a | yes ab≈b | no bc≉b | yes bc≈c = begin
lex (a ∙ b) c y z        ≈⟨  cong₁ ab≈b ⟩
lex b c y z              ≈⟨  case₂ bc≉b bc≈c ⟩
z                        ≈˘⟨ uncurry′ case₂ (<∙ˡ-trans ∙-assoc ∙-comm ab≈b ab≉a bc≈c) ⟩
lex a c x z              ≈˘⟨ cong₂ bc≈c ⟩
lex a (b ∙ c) x z        ∎
... | yes ab≈a | no ab≉b | yes bc≈b | no bc≉c = begin
lex (a ∙ b) c x z        ≈⟨  cong₁ ab≈a ⟩
lex a c x z              ≈⟨  uncurry′ case₁ (<∙ʳ-trans ∙-assoc ∙-comm ab≈a bc≈b bc≉c) ⟩
x                        ≈˘⟨ case₁ ab≈a ab≉b ⟩
lex a b x y              ≈˘⟨ cong₂ bc≈b ⟩
lex a (b ∙ c) x y        ∎

comm : Commutative _≈₁_ _∙_ → Commutative _≈₂_ _◦_ →
∀ a b x y → lex a b x y ≈₂ lex b a y x
comm ∙-comm ◦-comm a b x y
with (a ∙ b) ≟₁ a | (a ∙ b) ≟₁ b | (b ∙ a) ≟₁ b | (b ∙ a) ≟₁ a
... | yes ab≈a | _        | _        | no  ba≉a = contradiction (M.trans (∙-comm b a) ab≈a) ba≉a
... | no  ab≉a | _        | _        | yes ba≈a = contradiction (M.trans (∙-comm a b) ba≈a) ab≉a
... | _        | yes ab≈b | no  ba≉b | _        = contradiction (M.trans (∙-comm b a) ab≈b) ba≉b
... | _        | no  ab≉b | yes ba≈b | _        = contradiction (M.trans (∙-comm a b) ba≈b) ab≉b
... | yes _    | yes _    | yes _    | yes _    = ◦-comm x y
... | yes _    | no  _    | no  _    | yes _    = N.refl
... | no  _    | yes _    | yes _    | no  _    = N.refl
... | no  _    | no  _    | no  _    | no  _    = ◦-comm x y

idem : Idempotent _≈₂_ _◦_ → ∀ a b x → lex a b x x ≈₂ x
idem ◦-idem a b x with does ((a ∙ b) ≟₁ a) | does ((a ∙ b) ≟₁ b)
... | false | false = ◦-idem x
... | false | true  = N.refl
... | true  | false = N.refl
... | true  | true  = ◦-idem x

zeroʳ : ∀ {e f} → RightZero _≈₁_ e _∙_ → RightZero _≈₂_ f _◦_ →
lex a e x f ≈₂ f
zeroʳ {a} {x} {e} {f} ze₁ ze₂ with (a ∙ e) ≟₁ a | (a ∙ e) ≟₁ e
... | _     | no  a∙e≉e = contradiction (ze₁ a) a∙e≉e
... | no  _ | yes _     = N.refl
... | yes _ | yes _     = ze₂ x

identityʳ : ∀ {e f} → RightIdentity _≈₁_ e _∙_ → RightIdentity _≈₂_ f _◦_ →
lex a e x f ≈₂ x
identityʳ {a} {x} {e} {f} id₁ id₂ with (a ∙ e) ≟₁ a | (a ∙ e) ≟₁ e
... | no  a∙e≉a | _     = contradiction (id₁ a) a∙e≉a
... | yes _     | no  _ = N.refl
... | yes _     | yes _ = id₂ x
```