----------------------------------------------------------------------------------------------------
-- Arithmetic of Extensional Wellfounded orders
----------------------------------------------------------------------------------------------------

{-# OPTIONS --cubical #-}

module ExtensionalWellfoundedOrder.Arithmetic where

open import Cubical.Foundations.Prelude

open import Cubical.Relation.Binary
open BinaryRelation renaming (isTrans to isTransitive)
open import Cubical.Induction.WellFounded
  renaming (WellFounded to isWellFounded)

open import Cubical.Data.Sum.Base
open import Cubical.Data.Sigma
open import Cubical.Data.Unit
open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Unit.Properties
open import Cubical.Data.Empty.Properties

open import Cubical.Induction.WellFounded
  renaming (WellFounded to isWellFounded)

open import General-Properties

open import ExtensionalWellfoundedOrder.Base

open import Abstract.Arithmetic _<_ _≤_ public

open Ord

{- # Addition -}

_+_ : Ord → Ord → Ord
Carrier (A + B) = Carrier A ⊎ Carrier B

_≺_ (A + B) (inl x) (inl y) = _≺_ A x y
_≺_ (A + B) (inl x) (inr y) = Unit
_≺_ (A + B) (inr x) (inl y) = ⊥
_≺_ (A + B) (inr x) (inr y) = _≺_ B x y

truncated (A + B) (inl x) (inl y) = truncated A x y
truncated (A + B) (inl x) (inr y) = isPropUnit
truncated (A + B) (inr x) (inl y) = isProp⊥
truncated (A + B) (inr x) (inr y) = truncated B x y

wellfounded (A + B) (inl x) = helper x (wellfounded A x) where
  helper : ∀ y → Acc (_≺_ A) y → Acc (_≺_ (A + B)) (inl y)
  helper y (acc p) = acc λ { (inl z) z<y → helper z (p z z<y) }
wellfounded (A + B) (inr x) = helper x (wellfounded B x) where
  helper-inl : ∀ y → Acc (_≺_ A) y → Acc (_≺_ (A + B)) (inl y)
  helper-inl y (acc p) = acc λ { (inl z) z<y → helper-inl z (p z z<y) }

  helper : ∀ y → Acc (_≺_ B) y → Acc (_≺_ (A + B)) (inr y)
  helper y (acc p) = acc λ { (inl z) _ → helper-inl z (wellfounded A z)
                           ; (inr z) z<y → helper z (p z z<y) }

extensional (A + B) (inl a) (inl a') ext =
   cong inl (extensional A a a' λ c → (λ c<a  → fst (ext (inl c)) c<a) ,
                                      (λ c<a' → snd (ext (inl c)) c<a'))
extensional (A + B) (inl a) (inr b') ext =
   ⊥.rec (wellfounded→irreflexive (wellfounded A) _ (snd (ext (inl a)) tt))
extensional (A + B) (inr b) (inl a') ext =
   ⊥.rec (wellfounded→irreflexive (wellfounded A) _ (fst (ext (inl a')) tt))
extensional (A + B) (inr b) (inr b') ext =
   cong inr (extensional B b b' λ c → (λ c<b  → fst (ext (inr c)) c<b) ,
                                      (λ c<b' → snd (ext (inr c)) c<b'))

transitive (A + B) (inl x) (inl x₁) (inl x₂) p q = transitive A _ _ _ p q
transitive (A + B) (inl x) (inl x₁) (inr x₂) p q = tt
transitive (A + B) (inl x) (inr x₁) (inr x₂) p q = tt
transitive (A + B) (inr x) (inr x₁) (inr x₂) p q = transitive B _ _ _ p q

postulate
  +-is-add : is-add _+_

open Subtraction ((_+_ , +-is-add)) public using (has-sub)

{- # Multiplication -}

open Multiplication ((_+_ , +-is-add)) public using (has-mul)

_·_ : Ord → Ord → Ord
Carrier (A · B) = Carrier A × Carrier B

_≺_ (A · B) (a , b) (a' , b') = _≺_ A a a' ⊎ ((a ≡ a') × _≺_ B b b')

truncated (A · B) (a , b) (a' , b') (inl p) (inl q)
  = cong inl (truncated A _ _ p q)
truncated (A · B) (a , b) (a' , b') (inl p) (inr (a=a' , q))
  = ⊥.rec (wellfounded→irreflexive (wellfounded A) a
                                   (subst (_≺_ A a) (sym a=a') p))
truncated (A · B) (a , b) (a' , b') (inr (a=a' , p)) (inl q)
  = ⊥.rec (wellfounded→irreflexive (wellfounded A) a
                                   (subst (_≺_ A a) (sym a=a') q))
truncated (A · B) (a , b) (a' , b') (inr (p , p')) (inr (q , q'))
  = cong inr (≡-× (isSetCarrier A _ _ p q) (truncated B _ _ p' q'))

wellfounded (A · B) (a , b) = WFI.induction (wellfounded A) {P = λ x → ∀ y → Acc (_≺_ (A · B)) (x , y)} step a b
  where
   P = (λ (a , b) (a' , b') → _≺_ A a a' ⊎ ((a ≡ a') × _≺_ B b b'))
   step : (x : Carrier A) →
           ((y : Carrier A) → (A ≺ y) x → (y₁ : Carrier B) → Acc (_≺_ (A · B)) (y , y₁)) →
          (y : Carrier B) → Acc (_≺_ (A · B)) (x , y)
   step x s = WFI.induction (wellfounded B) {P = λ y → Acc P (x , y)} (λ y s' → acc (step' y s')) where
     step' : ∀ y → (∀ z → (B ≺ z) y → Acc P (x , z)) → (z' : Carrier A × Carrier B) → P z' (x , y) → Acc P z'
     step' y s' (x' , y') (inl x'<x) = s x' x'<x y'
     step' y s' (x' , y') (inr (x'=x , y'<y)) = subst (λ w → Acc P (w , y') ) (sym x'=x) (s' y' y'<y)

extensional (A · B) (a , b) (a' , b') p = ≡-× (extensional A a a' (λ x → (ea₁ x , ea₂ x))) (extensional B b b' (λ y → (eb₁ y , eb₂ y))) where
  ea₁ : (c : Carrier A) → ((A ≺ c) a → (A ≺ c) a')
  ea₁ x x<a with fst (p (x , b')) (inl x<a)
  ... | inl x<a' = x<a'
  ... | inr (_ , b'<b') = ⊥.rec (wellfounded→irreflexive (wellfounded B) _ b'<b')

  ea₂ : (c : Carrier A) → ((A ≺ c) a' → (A ≺ c) a)
  ea₂ x x<a' with snd (p (x , b)) (inl x<a')
  ... | inl x<a = x<a
  ... | inr (_ , b<b) = ⊥.rec (wellfounded→irreflexive (wellfounded B) _ b<b)

  eb₁ : (c : Carrier B) → ((B ≺ c) b → (B ≺ c) b')
  eb₁ y y<b with fst (p (a , y)) (inr (refl , y<b))
  eb₁ y y<b | inl a<a' with snd (p (a , b)) (inl a<a')
  ... | inl a<a = ⊥.rec (wellfounded→irreflexive (wellfounded A) _ a<a)
  ... | inr (_ , b<b) = ⊥.rec (wellfounded→irreflexive (wellfounded B) _ b<b)
  eb₁ y y<b | inr (a=a' , y<b') = y<b'

  eb₂ : (c : Carrier B) → (B ≺ c) b' → (B ≺ c) b
  eb₂ y y<b' with snd (p (a' , y)) (inr (refl , y<b'))
  eb₂ y y<b' | inl a'<a with fst (p (a' , b')) (inl a'<a)
  ... | inl a'<a' = ⊥.rec (wellfounded→irreflexive (wellfounded A) _ a'<a')
  ... | inr (_ , b'<b') = ⊥.rec (wellfounded→irreflexive (wellfounded B) _ b'<b')
  eb₂ y y<b' | inr (_ , y<b) = y<b

transitive (A · B) (a , b) (a' , b') (a'' , b'') (inl a<a') (inl a'<a'')
  = inl (transitive A a a' a'' a<a' a'<a'')
transitive (A · B) (a , b) (a' , b') (a'' , b'') (inl a<a') (inr (a'=a'' , b'<b''))
  = inl (subst (_≺_ A a) a'=a'' a<a')
transitive (A · B) (a , b) (a' , b') (a'' , b'') (inr (a=a' , b<b')) (inl a'<a'')
  = inl (subst (λ z → _≺_ A z a'') (sym a=a') a'<a'')
transitive (A · B) (a , b) (a' , b') (a'' , b'') (inr (a=a' , b<b')) (inr (a'=a'' , b'<b''))
  = inr ((a=a' ∙ a'=a'') , transitive B b b' b'' b<b' b'<b'')