text:
-- MIT License

-- Copyright (c) 2021 Luca Ciccone and Luca Padovani

-- Permission is hereby granted, free of charge, to any person
-- obtaining a copy of this software and associated documentation
-- files (the "Software"), to deal in the Software without
-- restriction, including without limitation the rights to use,
-- copy, modify, merge, publish, distribute, sublicense, and/or sell
-- copies of the Software, and to permit persons to whom the
-- Software is furnished to do so, subject to the following
-- conditions:

-- The above copyright notice and this permission notice shall be
-- included in all copies or substantial portions of the Software.

-- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
-- EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
-- OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
-- NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
-- HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
-- WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
-- FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
-- OTHER DEALINGS IN THE SOFTWARE.

{-# OPTIONS --guardedness --sized-types #-}

open import Data.Empty
open import Data.Unit
open import Data.Product
open import Data.Maybe
open import Data.Sum
open import Data.List using (_++_; []; _∷_; _∷ʳ_; length)
open import Data.List.Properties using (∷-injective)

open import Relation.Nullary
open import Relation.Nullary.Negation using (contraposition)
open import Relation.Unary using (_∈_; _⊆_)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; sym; subst; cong)

open import Function.Base using (case_of_)

open import Common

module Divergence {ℙ : Set} (message : Message ℙ)
  where

open import SessionType message
open import Session message
open import Trace message
open import HasTrace message
open import TraceSet message
open import Transitions message
open import Semantics message
open import Subtyping message

DivergeForward : SessionType -> SessionType -> Trace -> Set

record _↑_ (T : SessionType) (S : SessionType) : Set where
  coinductive
  field
    trace : Trace
    with-trace : T HasTrace trace
    without-trace : ¬ S HasTrace trace
    divergence : DivergeForward T S trace

DivergeForward T S φ =
  ∀{ψ x}
  (pre : ψ ⊑ φ)
  (tψx : T HasTrace (ψ ∷ʳ O x))
  (sψx : S HasTrace (ψ ∷ʳ O x)) -> after tψx ↑ after sψx

diverge-before-input : ∀{f g x} -> f x .force ↑ g x .force -> inp f ↑ inp g
_↑_.trace (diverge-before-input {_} {_} {x} div) = I x ∷ _↑_.trace div
_↑_.with-trace (diverge-before-input div) = inp-has-trace (_↑_.with-trace div)
_↑_.without-trace (diverge-before-input div) = inp-has-no-trace (_↑_.without-trace div)
_↑_.divergence (diverge-before-input div) none (_ , _ , step () _) _
_↑_.divergence (diverge-before-input div) (some le) (_ , tdef , step inp tr) (_ , sdef , step inp sr) =
  _↑_.divergence div le (_ , tdef , tr) (_ , sdef , sr)

DivergeBackward : ∀{T S φ} -> T HasTrace φ -> S HasTrace φ -> Set
DivergeBackward {_} {_} {φ} tφ sφ =
  ∀{ψ} (pre : ψ ⊑ φ) -> after (⊑-has-trace pre tφ) ↑ after (⊑-has-trace pre sφ)

⊑-diverge-backward :
  ∀{T S φ ψ}
  {tφ  : T HasTrace φ}
  {sφ  : S HasTrace φ}
  (pre : ψ ⊑ φ) ->
  DivergeBackward tφ sφ ->
  DivergeBackward (⊑-has-trace pre tφ) (⊑-has-trace pre sφ)
⊑-diverge-backward {_} {_} {_} {_} {tφ} {sφ} pre div pre'  rewrite ⊑-tran-has-trace pre' pre tφ | ⊑-tran-has-trace pre' pre sφ =
  div (⊑-tran pre' pre)

data DiscSet : SessionType -> SessionType -> Trace -> Set where
  inc : ∀{T S φ}
        (tφ : T HasTrace φ)
        (sφ : S HasTrace φ)
        (div←φ : DivergeBackward tφ sφ) -> DiscSet T S φ
  exc : ∀{T S φ ψ x}
        (eq : φ ≡ ψ ∷ʳ O x)
        (tψ : T HasTrace ψ)
        (sψ : S HasTrace ψ)
        (tφ : T HasTrace φ)
        (nsφ : ¬ S HasTrace φ)
        (div←ψ : DivergeBackward tψ sψ) -> DiscSet T S φ

⊑-proper : ∀{φ ψ α} -> φ ⊑ (ψ ∷ʳ α) -> φ ⊑ ψ ⊎ φ ≡ ψ ∷ʳ α
⊑-proper {[]} {[]} none = inj₁ none
⊑-proper {_ ∷ []} {[]} (some none) = inj₂ refl
⊑-proper {[]} {_ ∷ _} none = inj₁ none
⊑-proper {_} {_ ∷ _} (some pre) with ⊑-proper pre
... | inj₁ pre' = inj₁ (some pre')
... | inj₂ refl = inj₂ refl

disc-set->closed : (T S : SessionType) -> PrefixClosed (DiscSet T S)
disc-set->closed T S pre (inc tφ sφ div←φ) =
  inc (⊑-has-trace pre tφ) (⊑-has-trace pre sφ) (⊑-diverge-backward pre div←φ)
disc-set->closed T S pre (exc refl tψ sψ tφ nsφ div←ψ) with ⊑-proper pre
... | inj₁ pre' = inc (⊑-has-trace pre' tψ) (⊑-has-trace pre' sψ) (⊑-diverge-backward pre' div←ψ)
... | inj₂ refl = exc refl tψ sψ tφ nsφ div←ψ

input-lemma : ∀{φ x ψ χ y} -> φ ++ I x ∷ ψ ≡ χ ∷ʳ O y -> (φ ∷ʳ I x) ⊑ χ
input-lemma {[]} {_} {_} {I x ∷ χ} refl = some none
input-lemma {x ∷ φ} {_} {_} {[]} eq with ∷-injective eq
... | (_ , eq') = ⊥-elim (absurd-++-≡ eq')
input-lemma {x ∷ φ} {_} {_} {y ∷ χ} eq with ∷-injective eq
... | (refl , eq'') = some (input-lemma eq'')

disc-set-input : ∀{φ x ψ} {T S : SessionType} -> DiscSet T S (φ ++ I x ∷ ψ) ->
  T HasTrace (φ ∷ʳ I x) × S HasTrace (φ ∷ʳ I x)
disc-set-input {φ} {x} {ψ} (inc tφ sφ div←φ) with ⊑-precong-++ {φ} {I x ∷ []} {I x ∷ ψ} (some none)
... | pre = ⊑-has-trace pre tφ , ⊑-has-trace pre sφ
disc-set-input (exc eq tχ sχ _ _ _) with input-lemma eq
... | pre = ⊑-has-trace pre tχ , ⊑-has-trace pre sχ

disc-set-output : ∀{φ x ψ} {T S : SessionType} -> DiscSet T S (φ ++ O x ∷ ψ) -> T HasTrace (φ ∷ʳ O x)
disc-set-output {φ} {x} {ψ} (inc tφx sφx _) =
  let pre = ⊑-precong-++ {φ} {O x ∷ []} {O x ∷ ψ} (some none) in
  ⊑-has-trace pre tφx
disc-set-output {φ} {x} {ψ} (exc _ _ _ tφx _ _) =
  let pre = ⊑-precong-++ {φ} {O x ∷ []} {O x ∷ ψ} (some none) in
  ⊑-has-trace pre tφx

disc-set->coherent : (T S : SessionType) -> Coherent (DiscSet T S)
disc-set->coherent T S ti to =
  let (ti[] , _) = disc-set-input ti in
  let to[] = disc-set-output to in
  ⊥-elim (coherent (sem-sound T) ti[] to[])

disc-set->semantics : (T S : SessionType) -> Semantics (DiscSet T S)
closed (disc-set->semantics T S) = disc-set->closed T S
coherent (disc-set->semantics T S) = disc-set->coherent T S

disc-set-subset : ∀{T S} -> DiscSet T S ⊆ ⟦ T ⟧
disc-set-subset (inc tφ _ _) = tφ
disc-set-subset (exc _ _ _ tφ _ _) = tφ

disc-set-disjoint :
  ∀{T S φ} ->
  φ ∈ DiscSet T S ->
  ¬ S HasTrace φ ->
  ∃[ ψ ] ∃[ x ] (φ ≡ ψ ∷ʳ O x × S HasTrace ψ)
disc-set-disjoint (inc _ sφ _) nsφ = ⊥-elim (nsφ sφ)
disc-set-disjoint (exc eq _ sψ _ _ _) nsφ = _ , _ , eq , sψ

-- --| BEGIN MAXIMAL TRACES |--

diverge-forward-input :
  ∀{f g x φ} -> DivergeForward (inp f) (inp g) (I x ∷ φ)
             -> DivergeForward (f x .force) (g x .force) φ
diverge-forward-input div pre (_ , tdef , tr) (_ , sdef , sr) = div (some pre) (_ , tdef , step inp tr) (_ , sdef , step inp sr)

diverge-forward-input' :
  ∀{f g x φ} -> DivergeForward (f x .force) (g x .force) φ
             -> DivergeForward (inp f) (inp g) (I x ∷ φ)
diverge-forward-input' div none (_ , _ , step () _) (_ , _ , _)
diverge-forward-input' div (some le) (_ , tdef , step inp tr) (_ , sdef , step inp sr) = div le (_ , tdef , tr) (_ , sdef , sr)

diverge-forward-output :
  ∀{f g x φ} -> DivergeForward (out f) (out g) (O x ∷ φ)
             -> DivergeForward (f x .force) (g x .force) φ
diverge-forward-output div pre (_ , tdef , tr) (_ , sdef , sr) =
  div (some pre)
      (_ , tdef , step (out (transitions+defined->defined tr tdef)) tr)
      (_ , sdef , step (out (transitions+defined->defined sr sdef)) sr)

-- the next lemma says that if T ↑ S and φ is the trace that
-- discriminates between them, then we have divergence along any
-- common prefix of φ shared by both T and S

diverge-forward->backward :
  ∀{T S φ ψ}
  (tφ  : T HasTrace φ)
  (nsφ : ¬ S HasTrace φ)
  (div : DivergeForward T S φ)
  (pre : ψ ⊑ φ)
  (tψ  : T HasTrace ψ)
  (sψ  : S HasTrace ψ) ->
  DivergeBackward tψ sψ
_↑_.trace (diverge-forward->backward tφ nsφ div pre tψ sψ none) = _
_↑_.with-trace (diverge-forward->backward tφ nsφ div pre tψ sψ none) = tφ
_↑_.without-trace (diverge-forward->backward tφ nsφ div pre tψ sψ none) = nsφ
_↑_.divergence (diverge-forward->backward tφ nsφ div pre tψ sψ none) = div
diverge-forward->backward (_ , tdef , step inp tr) nsφ div (some pre) (_ , tdef' , step (inp {f}) tr') (_ , sdef , step (inp {g}) sr) (some pre') =
  diverge-forward->backward (_ , tdef , tr) (contraposition inp-has-trace nsφ) (diverge-forward-input {f} {g} div) pre (_ , tdef' , tr') (_ , sdef , sr) pre'
diverge-forward->backward (_ , tdef , step (out _) tr) nsφ div (some pre) (_ , tdef' , step (out {f} _) tr') (_ , sdef , step (out {g} _) sr) (some pre') =
  diverge-forward->backward (_ , tdef , tr) (contraposition out-has-trace nsφ) (diverge-forward-output {f} {g} div) pre (_ , tdef' , tr') (_ , sdef , sr) pre'

prefix-last-element : ∀{φ φ' ψ ψ' x y} -> φ ⊑ ψ -> φ ≡ φ' ++ O x ∷ [] -> ψ ≡ ψ' ∷ʳ O y -> ψ ≡ φ ⊎ φ ⊑ ψ'
prefix-last-element none e1 e2 = inj₂ none
prefix-last-element {φ' = []} {ψ' = []} (some pre) e1 e2 with ∷-injective e1 | ∷-injective e2
... | (_ , e1') | (_ , e2') rewrite e1' | e2' = inj₁ refl
prefix-last-element {φ' = []} {ψ' = x ∷ ψ'} (some _) e1 e2 with ∷-injective e1 | ∷-injective e2
... | (eq1 , e1') | (eq2 , e2') rewrite eq1 | eq2 | e1' | e2' = inj₂ (some none)
prefix-last-element {φ' = x ∷ φ'} {ψ' = []} (some pre) e1 e2 with ∷-injective e1 | ∷-injective e2
... | (eq1 , e1') | (eq2 , e2') rewrite e1' | e2' = ⊥-elim (absurd-++-⊑ pre)
prefix-last-element {φ' = x ∷ φ'} {ψ' = x₁ ∷ ψ'} (some pre) e1 e2 with ∷-injective e1 | ∷-injective e2
... | (eq1 , e1') | (eq2 , e2') rewrite eq1 | eq2 with prefix-last-element pre e1' e2'
... | inj₁ eq rewrite eq = inj₁ refl
... | inj₂ pre' = inj₂ (some pre')

disc-set-maximal-1 :
  ∀{T S φ} ->
  φ ∈ DiscSet T S ->
  ¬ S HasTrace φ ->
  φ ∈ Maximal (DiscSet T S)
disc-set-maximal-1 dsφ nsφ with disc-set-disjoint dsφ nsφ
... | _ , _ , refl , sψ =
  maximal dsφ λ le ds' ->
  let _ , _ , eq , sψ' = disc-set-disjoint ds' (contraposition (⊑-has-trace le) nsφ) in
  case prefix-last-element le refl eq of λ
  { (inj₁ refl) → refl
  ; (inj₂ le') → ⊥-elim (contraposition (⊑-has-trace le') nsφ sψ') }

has-trace-after : ∀{T φ ψ} (tφ : T HasTrace φ) -> after tφ HasTrace ψ -> T HasTrace (φ ++ ψ)
has-trace-after (_ , _ , refl) tφψ = tφψ
has-trace-after (_ , tdef , step inp tr) tφψ = inp-has-trace (has-trace-after (_ , tdef , tr) tφψ)
has-trace-after (_ , tdef , step (out _) tr) tφψ = out-has-trace (has-trace-after (_ , tdef , tr) tφψ)

has-no-trace-after : ∀{T φ ψ} (tφ : T HasTrace φ) -> ¬ after tφ HasTrace ψ -> ¬ T HasTrace (φ ++ ψ)
has-no-trace-after (_ , _ , refl) tφ/nψ = tφ/nψ
has-no-trace-after (_ , tdef , step inp tr) tφ/nψ = inp-has-no-trace (has-no-trace-after (_ , tdef , tr) tφ/nψ)
has-no-trace-after (_ , tdef , step (out _) tr) tφ/nψ = out-has-no-trace (has-no-trace-after (_ , tdef , tr) tφ/nψ)

append-diverge-backward :
  ∀{T S φ ψ}
  (tφ : T HasTrace φ)
  (sφ : S HasTrace φ)
  (tφ/ψ : after tφ HasTrace ψ)
  (sφ/ψ : after sφ HasTrace ψ)
  (div←φ : DivergeBackward tφ sφ)
  (divφ←ψ : DivergeBackward tφ/ψ sφ/ψ) ->
  DivergeBackward (has-trace-after tφ tφ/ψ) (has-trace-after sφ sφ/ψ)
append-diverge-backward (_ , tdef , refl) (_ , sdef , refl) tφ/ψ sφ/ψ div←φ divφ←ψ pre = divφ←ψ pre
append-diverge-backward (_ , tdef , step t tr) (_ , sdef , step s sr) tφ/ψ sφ/ψ div←φ divφ←ψ none = div←φ none
append-diverge-backward (_ , tdef , step inp tr) (_ , sdef , step inp sr) tφ/ψ sφ/ψ div←φ divφ←ψ (some pre) =
  append-diverge-backward (_ , tdef , tr) (_ , sdef , sr) tφ/ψ sφ/ψ (λ pre -> div←φ (some pre)) divφ←ψ pre
append-diverge-backward (_ , tdef , step (out _) tr) (_ , sdef , step (out _) sr) tφ/ψ sφ/ψ div←φ divφ←ψ (some pre) =
  append-diverge-backward (_ , tdef , tr) (_ , sdef , sr) tφ/ψ sφ/ψ (λ pre -> div←φ (some pre)) divφ←ψ pre

append-snoc : ∀{φ ψ : Trace}{α : Action} -> φ ++ (ψ ∷ʳ α) ≡ (φ ++ ψ) ∷ʳ α
append-snoc {[]} = refl
append-snoc {β ∷ φ} = cong (β ∷_) (append-snoc {φ})

completion :
  ∀{φ T S} ->
  T <: S ->
  φ ∈ DiscSet T S ->
  (∃[ ψ ] (φ ⊏ ψ × ψ ∈ Maximal (DiscSet T S))) ⊎ (φ ∈ Maximal (DiscSet T S) × ¬ S HasTrace φ)
completion {φ} sub (inc tφ sφ div←φ) with div←φ (⊑-refl _)
... | div rewrite ⊑-has-trace-after tφ | ⊑-has-trace-after sφ =
  let χ = _↑_.trace div in
  let tφ/χ = _↑_.with-trace div in
  let sφ/nχ = _↑_.without-trace div in
  let divφ→χ = _↑_.divergence div in
  let subφ = sub-after tφ sφ sub in
  let ψ , x , ψ⊑χ , tφ/ψ , sφ/ψ , tφ/ψx , sφ/nψx = sub-excluded subφ tφ/χ sφ/nχ in
  let tφψ = has-trace-after tφ tφ/ψ in
  let sφψ = has-trace-after sφ sφ/ψ in
  let tφψx = has-trace-after tφ tφ/ψx in
  let sφnψx = has-no-trace-after sφ sφ/nψx in
  let divφ←ψ = diverge-forward->backward tφ/χ sφ/nχ divφ→χ ψ⊑χ tφ/ψ sφ/ψ in
  let div←ψ  = append-diverge-backward tφ sφ tφ/ψ sφ/ψ div←φ divφ←ψ in
  let ds = exc {_} {_} {φ ++ (ψ ∷ʳ O x)} {φ ++ ψ} {x} (append-snoc {φ} {ψ} {O x}) tφψ sφψ tφψx sφnψx div←ψ in
  inj₁ (φ ++ (ψ ∷ʳ O x) , ⊏-++ , disc-set-maximal-1 ds sφnψx)
completion sub ds@(exc _ _ _ _ nsφ _) =
  inj₂ (disc-set-maximal-1 ds nsφ , nsφ)

disc-set-maximal-2 :
  ∀{T S φ} ->
  T <: S ->
  φ ∈ Maximal (DiscSet T S) ->
  ¬ S HasTrace φ
disc-set-maximal-2 sub (maximal dφ F) sφ with completion sub dφ
... | inj₁ (ψ , φ⊏ψ , maximal dψ _) = ⊏->≢ φ⊏ψ (sym (F (⊏->⊑ φ⊏ψ) dψ))
... | inj₂ (_ , nsφ) = nsφ sφ

--| END MAXIMAL TRACES |--

-- Sia R il session type determinato da disc-set T S quando T ↑
-- S. L'obiettivo è dimostrare che R |- T e ¬ R |- S
--
-- R |- T
--
-- Ogni riduzione di (R # T) può essere completata a (R' # T') in
-- cui Win R' e Defined T'
--
-- Siccome le tracce di R sono incluse in quelle di T, basta
-- dimostrare che ogni traccia di R può essere completata, cioè che
-- ogni traccia di disc-set T S è prefisso di una traccia completa
-- di disc-set T S.
--
-- ∀ φ ∈ R => ∃ ψ : φ ++ ψ ∈ Maximal R
--
-- ¬ R |- S
--
-- Dimostrare che ogni traccia completa di R non è una traccia di S.
--
-- Maximal R ∩ ⟦ S ⟧ ≡ ∅

max_stars_repo_name: boystrange/FairSubtypingAgda

max_issues_repo_name: boystrange/FairSubtypingAgda

max_forks_repo_name: boystrange/FairSubtypingAgda


text:
module Lvl.MultiFunctions.Proofs where

open import Data
open import Lvl hiding (𝐒)
open import Lvl.MultiFunctions
open import Data.Tuple.Raise
open import Data.Tuple.Raiseᵣ.Functions
open import Lvl.MultiFunctions
open import Numeral.Natural
open import Relator.Equals
open import Syntax.Number

max-repeat : ∀{n}{ℓ} → ((ℓ ⊔ (⨆(repeat n ℓ))) ≡ ℓ)
max-repeat {n = 0}       = [≡]-intro
max-repeat {n = 1}       = [≡]-intro
max-repeat {n = 𝐒(𝐒(n))} = max-repeat {n = 𝐒(n)}

{- TODO: Is this possible?

open import Relator.Equals.Proofs
test2 : ∀{a b} → (eq : a ≡ b) → ([≡]-substitutionᵣ eq {\n → Set(n)} (Set(a)) ≡ Set(b))

test2 : ∀{a b} → (a ≡ b) → (Set(a) ≡ Set(b))

postulate ℓ : Level
postulate n : ℕ
postulate s : Set(ℓ ⊔ (⨆{n} (repeat n ℓ)))
postulate p : Set(ℓ) → Set

want : Set
want rewrite max-repeat{n}{ℓ} = p s
-}

ext: agda

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import LogicalFormulae
open import Setoids.Setoids
open import Functions.Definition
open import Sets.EquivalenceRelations
open import Rings.Definition

module Rings.Divisible.Lemmas {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} (R : Ring S _+_ _*_) where

open Setoid S
open Equivalence eq
open Ring R
open import Rings.Divisible.Definition R
open import Rings.Units.Definition R

divisionTransitive : (x y z : A) → x ∣ y → y ∣ z → x ∣ z
divisionTransitive x y z (a , pr) (b , pr2) = (a * b) , transitive (transitive *Associative (*WellDefined pr reflexive)) pr2

divisionReflexive : (x : A) → x ∣ x
divisionReflexive x = 1R , transitive *Commutative identIsIdent

everythingDividesZero : (r : A) → r ∣ 0R
everythingDividesZero r = 0R , timesZero

nonzeroInherits : {x y : A} (nz : (x ∼ 0R) → False) → y ∣ x → (y ∼ 0R) → False
nonzeroInherits {x} {y} nz (c , pr) y=0 = nz (transitive (symmetric pr) (transitive (*WellDefined y=0 reflexive) (transitive *Commutative timesZero)))

nonunitInherits : {x y : A} (nonunit : Unit x → False) → x ∣ y → Unit y → False
nonunitInherits nu (s , pr) (a , b) = nu ((s * a) , transitive (transitive *Associative (*WellDefined pr reflexive)) b)


text:
{-# OPTIONS --without-K --safe #-}
open import Categories.Category

-- Definition of the Arrow Category of a Category C
module Categories.Category.Construction.Arrow {o ℓ e} (C : Category o ℓ e) where

open import Level
open import Data.Product using (_,_; _×_; map; zip)
open import Function using (_$_)
open import Relation.Binary using (Rel)

import Categories.Morphism as M
open M C
open import Categories.Morphism.Reasoning C

open Category C hiding (dom; cod)
open HomReasoning

private
  variable
    A B D E : Obj

record Morphism : Set (o ⊔ ℓ) where
  field
    {dom} : Obj
    {cod} : Obj
    arr   : dom ⇒ cod

record Morphism⇒ (f g : Morphism) : Set (ℓ ⊔ e) where
  constructor mor⇒
  private
    module f = Morphism f
    module g = Morphism g

  field
    {dom⇒} : f.dom ⇒ g.dom
    {cod⇒} : f.cod ⇒ g.cod
    square : CommutativeSquare f.arr dom⇒ cod⇒ g.arr

Arrow : Category _ _ _
Arrow = record
  { Obj       = Morphism
  ; _⇒_       = Morphism⇒
  ; _≈_       = λ f g → dom⇒ f ≈ dom⇒ g × cod⇒ f ≈ cod⇒ g
  ; id        = mor⇒ $ identityˡ ○ ⟺ identityʳ
  ; _∘_       = λ m₁ m₂ → mor⇒ $ glue (square m₁) (square m₂)
  ; assoc     = assoc , assoc
  ; sym-assoc = sym-assoc , sym-assoc
  ; identityˡ = identityˡ , identityˡ
  ; identityʳ = identityʳ , identityʳ
  ; identity² = identity² , identity²
  ; equiv     = record
    { refl  = refl , refl
    ; sym   = map sym sym
    ; trans = zip trans trans
    }
  ; ∘-resp-≈  = zip ∘-resp-≈ ∘-resp-≈
  }
  where open Morphism⇒

private
  module MM = M Arrow

module _ where
  open _≅_

  lift-iso : ∀ {f h} →
               (iso₁ : A ≅ D) → (iso₂ : B ≅ E) →
               CommutativeSquare f (from iso₁) (from iso₂) h →
               record { arr = f } MM.≅ record { arr = h }
  lift-iso {f = f} {h = h} iso₁ iso₂ sq = record
    { from = record { square = sq }
    ; to   = record { square = begin
      to iso₂ ∘ h                           ≈⟨ introʳ (isoʳ iso₁) ⟩
      (to iso₂ ∘ h) ∘ from iso₁ ∘ to iso₁   ≈⟨ assoc ⟩
      to iso₂ ∘ h ∘ from iso₁ ∘ to iso₁     ≈˘⟨ refl ⟩∘⟨ pushˡ sq ⟩
      to iso₂ ∘ (from iso₂ ∘ f) ∘ to iso₁   ≈˘⟨ assoc ⟩
      (to iso₂ ∘ (from iso₂ ∘ f)) ∘ to iso₁ ≈⟨ cancelˡ (isoˡ iso₂) ⟩∘⟨ refl ⟩
      f ∘ to iso₁                           ∎ }
    ; iso  = record
      { isoˡ = isoˡ iso₁ , isoˡ iso₂
      ; isoʳ = isoʳ iso₁ , isoʳ iso₂
      }
    }

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


text:
data Fun (A B : Set) : Set where
  fun : (A → B) → Fun A B

syntax fun (λ x → y) = fn x , y

foo : ∀ {A} → Fun A A → A
foo (fn x , y) = y

max_stars_repo_name: sseefried/agda


text:
------------------------------------------------------------------------
-- Coinductive lists
------------------------------------------------------------------------

module Data.Colist where

open import Coinduction
open import Data.Bool          using (Bool; true; false)
open import Data.Maybe         using (Maybe; nothing; just)
open import Data.Nat           using (ℕ; zero; suc)
open import Data.Conat
open import Data.List          using (List; []; _∷_)
open import Data.List.NonEmpty using (List⁺; _∷_)
                               renaming ([_] to [_]⁺)
open import Data.BoundedVec.Inefficient as BVec
  using (BoundedVec; []; _∷_)
open import Data.Product using (_,_)
open import Data.Function
open import Relation.Binary

------------------------------------------------------------------------
-- The type

infixr 5 _∷_

data Colist (A : Set) : Set where
  []  : Colist A
  _∷_ : (x : A) (xs : ∞ (Colist A)) → Colist A

data Any {A} (P : A → Set) : Colist A → Set where
  here  : ∀ {x xs} (px  : P x)          → Any P (x ∷ xs)
  there : ∀ {x xs} (pxs : Any P (♭ xs)) → Any P (x ∷ xs)

data All {A} (P : A → Set) : Colist A → Set where
  []  : All P []
  _∷_ : ∀ {x xs} (px : P x) (pxs : ∞ (All P (♭ xs))) → All P (x ∷ xs)

------------------------------------------------------------------------
-- Some operations

null : ∀ {A} → Colist A → Bool
null []      = true
null (_ ∷ _) = false

length : ∀ {A} → Colist A → Coℕ
length []       = zero
length (x ∷ xs) = suc (♯ length (♭ xs))

map : ∀ {A B} → (A → B) → Colist A → Colist B
map f []       = []
map f (x ∷ xs) = f x ∷ ♯ map f (♭ xs)

fromList : ∀ {A} → List A → Colist A
fromList []       = []
fromList (x ∷ xs) = x ∷ ♯ fromList xs

take : ∀ {A} (n : ℕ) → Colist A → BoundedVec A n
take zero    xs       = []
take (suc n) []       = []
take (suc n) (x ∷ xs) = x ∷ take n (♭ xs)

replicate : ∀ {A} → Coℕ → A → Colist A
replicate zero    x = []
replicate (suc n) x = x ∷ ♯ replicate (♭ n) x

lookup : ∀ {A} → ℕ → Colist A → Maybe A
lookup n       []       = nothing
lookup zero    (x ∷ xs) = just x
lookup (suc n) (x ∷ xs) = lookup n (♭ xs)

infixr 5 _++_

_++_ : ∀ {A} → Colist A → Colist A → Colist A
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ ♯ (♭ xs ++ ys)

concat : ∀ {A} → Colist (List⁺ A) → Colist A
concat []               = []
concat ([ x ]⁺   ∷ xss) = x ∷ ♯ concat (♭ xss)
concat ((x ∷ xs) ∷ xss) = x ∷ ♯ concat (xs ∷ xss)

[_] : ∀ {A} → A → Colist A
[ x ] = x ∷ ♯ []

------------------------------------------------------------------------
-- Equality and other relations

-- xs ≈ ys means that xs and ys are equal.

infix 4 _≈_

data _≈_ {A} : (xs ys : Colist A) → Set where
  []  :                                       []     ≈ []
  _∷_ : ∀ x {xs ys} (xs≈ : ∞ (♭ xs ≈ ♭ ys)) → x ∷ xs ≈ x ∷ ys

-- x ∈ xs means that x is a member of xs.

infix 4 _∈_

data _∈_ {A : Set} : A → Colist A → Set where
  here  : ∀ {x   xs}                   → x ∈ x ∷ xs
  there : ∀ {x y xs} (x∈xs : x ∈ ♭ xs) → x ∈ y ∷ xs

-- xs ⊑ ys means that xs is a prefix of ys.

infix 4 _⊑_

data _⊑_ {A : Set} : Colist A → Colist A → Set where
  []  : ∀ {ys}                            → []     ⊑ ys
  _∷_ : ∀ x {xs ys} (p : ∞ (♭ xs ⊑ ♭ ys)) → x ∷ xs ⊑ x ∷ ys

------------------------------------------------------------------------
-- Some proofs

setoid : Set → Setoid
setoid A = record
  { carrier       = Colist A
  ; _≈_           = _≈_
  ; isEquivalence = record
    { refl  = refl
    ; sym   = sym
    ; trans = trans
    }
  }
  where
  refl : Reflexive _≈_
  refl {[]}     = []
  refl {x ∷ xs} = x ∷ ♯ refl

  sym : Symmetric _≈_
  sym []        = []
  sym (x ∷ xs≈) = x ∷ ♯ sym (♭ xs≈)

  trans : Transitive _≈_
  trans []        []         = []
  trans (x ∷ xs≈) (.x ∷ ys≈) = x ∷ ♯ trans (♭ xs≈) (♭ ys≈)

poset : Set → Poset
poset A = record
  { carrier        = Colist A
  ; _≈_            = _≈_
  ; _≤_            = _⊑_
  ; isPartialOrder = record
    { isPreorder = record
      { isEquivalence = Setoid.isEquivalence (setoid A)
      ; reflexive     = reflexive
      ; trans         = trans
      ; ∼-resp-≈      = ((λ {_} → ⊑-resp-≈ˡ) , λ {_} → ⊑-resp-≈ʳ)
      }
    ; antisym  = antisym
    }
  }
  where
  reflexive : _≈_ ⇒ _⊑_
  reflexive []        = []
  reflexive (x ∷ xs≈) = x ∷ ♯ reflexive (♭ xs≈)

  trans : Transitive _⊑_
  trans []        _          = []
  trans (x ∷ xs≈) (.x ∷ ys≈) = x ∷ ♯ trans (♭ xs≈) (♭ ys≈)

  ⊑-resp-≈ˡ : {xs : Colist A} →  (λ ys → xs ⊑ ys) Respects _≈_
  ⊑-resp-≈ˡ _         []       = []
  ⊑-resp-≈ˡ (x ∷ xs≈) (.x ∷ p) = x ∷ ♯ ⊑-resp-≈ˡ (♭ xs≈) (♭ p)

  ⊑-resp-≈ʳ : {ys : Colist A} →  (λ xs → xs ⊑ ys) Respects _≈_
  ⊑-resp-≈ʳ []        _        = []
  ⊑-resp-≈ʳ (x ∷ xs≈) (.x ∷ p) = x ∷ ♯ ⊑-resp-≈ʳ (♭ xs≈) (♭ p)

  antisym : Antisymmetric _≈_ _⊑_
  antisym []       []        = []
  antisym (x ∷ p₁) (.x ∷ p₂) = x ∷ ♯ antisym (♭ p₁) (♭ p₂)

map-cong : ∀ {A B} (f : A → B) → _≈_ =[ map f ]⇒ _≈_
map-cong f []        = []
map-cong f (x ∷ xs≈) = f x ∷ ♯ map-cong f (♭ xs≈)

take-⊑ : ∀ {A} n (xs : Colist A) →
         let toColist = fromList ∘ BVec.toList in
         toColist (take n xs) ⊑ xs
take-⊑ zero    xs       = []
take-⊑ (suc n) []       = []
take-⊑ (suc n) (x ∷ xs) = x ∷ ♯ take-⊑ n (♭ xs)

max_issues_repo_name: larrytheliquid/Lemmachine


text:
open import Categories
open import Monads

module Monads.CatofAdj.TermAdj {a b}{C : Cat {a}{b}}(M : Monad C) where

open import Library
open import Functors
open import Monads.CatofAdj M
open import Categories.Terminal
open import Monads.CatofAdj.TermAdjObj M
open import Monads.CatofAdj.TermAdjHom M
open import Monads.CatofAdj.TermAdjUniq M

EMIsTerm : Term CatofAdj EMObj
EMIsTerm = record {
  t   = λ {A} → EMHom A;
  law = λ {A} {V} →
    HomAdjEq _ _  (FunctorEq _ _ (omaplem A V)
                                 (iext λ _ → iext λ _ → ext $ hmaplem A V))}

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
{-
  Finitely presented algebras.
  An R-algebra A is finitely presented, if there merely is an exact sequence
  of R-modules:

    (a₁,⋯,aₘ) → R[X₁,⋯,Xₙ] → A → 0
-}
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommAlgebra.FPAlgebra where
open import Cubical.Foundations.Prelude

open import Cubical.Data.FinData
open import Cubical.Data.Nat
open import Cubical.Data.Vec
open import Cubical.Data.Sigma

open import Cubical.HITs.PropositionalTruncation

open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommAlgebra
open import Cubical.Algebra.CommAlgebra.FreeCommAlgebra
open import Cubical.Algebra.CommAlgebra.QuotientAlgebra
open import Cubical.Algebra.CommAlgebra.Ideal
open import Cubical.Algebra.CommAlgebra.FGIdeal

private
  variable
    ℓ : Level

module _ {R : CommRing ℓ} where
  freeAlgebra : (n : ℕ) → CommAlgebra R ℓ
  freeAlgebra n = R [ Fin n ]

  makeFPAlgebra : {m : ℕ} (n : ℕ) (l : FinVec (fst (freeAlgebra n)) m)
                  → CommAlgebra R ℓ
  makeFPAlgebra n l = freeAlgebra n / generatedIdeal (freeAlgebra n) l

  isFPAlgebra : (A : CommAlgebra R ℓ) → Type _
  isFPAlgebra A = ∃[ ((n , m) , l) ∈ Σ[ (n , m) ∈ ℕ × ℕ ] FinVec (fst (freeAlgebra n)) m ]
                   makeFPAlgebra n l ≡ A

  isFPAlgebraIsProp : {A : CommAlgebra R ℓ} → isProp (isFPAlgebra A)
  isFPAlgebraIsProp = isPropPropTrunc

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
{-# OPTIONS --without-K #-}

open import Level renaming (zero to lzero ; suc to lsuc)
open import Syntax
open import Data.List using (length ; [] ; _∷_ ) renaming ( _++_ to _++L_ )
open import Data.Vec  using ([] ; _∷_  ) renaming ( _++_ to _++V_ )

open import Data.Vec.Relation.Unary.All using (All ; [] ; _∷_)
open import Data.Nat

open import Data.Product
open import Function using () renaming (case_of_ to case*_of_)

open import Size
open import Relation.Binary.PropositionalEquality

-- Sets indexed by invertible environments (that is, Θ and Ξ). This
-- actually is our semantic domain.
Dom : ∀ ℓ -> Set (lsuc ℓ)
Dom ℓ = (Θ : TyEnv) -> (Ξ : MultEnv (length Θ)) -> Set ℓ

-- A pairing operator, inspired by the Day convolution in category theory.
data _⊛_ {ℓ : Level}
         (F : Dom ℓ)
         (G : Dom ℓ)
         (Θ : TyEnv) (Ξ : MultEnv (length Θ)) : Set ℓ where
     tup : ∀ Ξ₁ Ξ₂ -> (spΞ : Ξ₁ +ₘ Ξ₂ ≡ Ξ) ->
           (fst : F Θ Ξ₁) -> (snd : G Θ Ξ₂) -> (F ⊛ G) Θ Ξ

-- mult is used for representing entries in value environments that are aware of multiplicities.
data mult {ℓ : Level} (F : Dom ℓ) : (m : Multiplicity₀) -> Dom ℓ where
  -- An entry corresponds to multiplicity zero, i.e., nothing.
  mult-zero :
    ∀ {Θ Ξ} ->
    (eq : Ξ ≡ ∅) ->
    mult F zero Θ Ξ

  -- An entry corresponds to multiplicity one, a value must be used linearly.
  mult-one :
    ∀ {Θ Ξ} ->
    (v : F Θ Ξ) -> mult F one Θ Ξ

  -- An entry corresponds to multiplicity omega; such values must be indexed by the empty invertible environment.
  mult-omega :
    ∀ {Θ Ξ} ->
    (v : F Θ ∅) -> (eq : Ξ ≡ ∅) -> mult F omega Θ Ξ

-- Values (Value), residuals (Residual) and value environments
-- (ValEnv) are mutually defined.
--
-- The sized types are used for termination checking with the presence
-- of --without-K, which weakens termination analysis for
-- with-abstractions that the original definitions used to have.

data Value (Θ : TyEnv) : MultEnv (length Θ) -> Ty zero -> {i : Size} -> Set
data Residual (Θ : TyEnv) : MultEnv (length Θ) -> Ty zero -> {i : Size} -> Set
ValEnv :
  (Γ : TyEnv) -> (Δ : MultEnv (length Γ)) -> {i : Size} ->
  (Θ : TyEnv) -> MultEnv (length Θ) -> Set

-- ValEnv Γ Δ : Dom 0 represents value environments conforms to Γ Δ.
-- Intuitively, (Θ , Ξ) of ValEnv Γ Δ Θ Ξ represents typed resources contained in
-- value environments.

ValEnv [] Δ {i}            = λ Θ Ξ -> Ξ ≡ ∅
ValEnv (A ∷ Γ) (m ∷ Δ) {i} =
  mult (V A) m ⊛ ValEnv Γ Δ {i}
  where
    V : Ty zero -> Dom 0ℓ
    V A Θ Ξ = Value Θ Ξ A {i}

-- Values
data Value Θ where
  clo :
    ∀ {Ξ Ξ' Γ' Δ' A B Ξₜ i} ->
    (m : Multiplicity) ->
    (spΞ : Ξ' +ₘ Ξₜ ≡ Ξ) ->
    (θ : ValEnv Γ' Δ' {i} Θ Ξ' ) ->
    (t : Term (A ∷ Γ') (M→M₀ m ∷ Δ') Θ Ξₜ B) ->
    Value Θ Ξ (A # m ~> B) {↑ i}

  unit :
    ∀ {Ξ i} ->
    (eq : ∅ ≡ Ξ) ->
    Value Θ Ξ tunit {↑ i}

  pair :
    ∀ {Ξ Ξ₁ Ξ₂ A B i} ->
    (spΞ : Ξ₁ +ₘ Ξ₂ ≡ Ξ) ->
    Value Θ Ξ₁ A {i} ->
    Value Θ Ξ₂ B {i} ->
    Value Θ Ξ (A ⊗ B) {↑ i}

  many :
    ∀ {Ξ Ξ₀ A i} ->
    (m : Multiplicity) ->
    (spΞ : m ×ₘ Ξ₀ ≡ Ξ) ->
    Value Θ Ξ₀ A {i} ->
    Value Θ Ξ (Many m A) {↑ i}

  inl  :
    ∀ {Ξ} {A B i} ->
    Value Θ Ξ A {i} ->
    Value Θ Ξ (A ⊕ B) {↑ i}

  inr :
    ∀ {Ξ} {A B i} ->
    Value Θ Ξ B {i} ->
    Value Θ Ξ (A ⊕ B) {↑ i}

  roll :
    ∀ {Ξ F i} ->
    Value Θ Ξ (substTy F (μ F)) {i} ->
    Value Θ Ξ (μ F) {↑ i}

  inj :
    ∀ {Ξ A B i}
    -> (eq : ∅ ≡ Ξ)
    -> (r : Residual (A ∷ []) (one ∷ ∅) (B ●) {i})
    -> Value Θ Ξ (A ↔ B) {↑ i}

  red :
    ∀ {Ξ A i} ->
    Residual Θ Ξ (A ●) {i} ->
    Value Θ Ξ (A ●) {↑ i}

-- Residuals
data Residual Θ where
  unit● :
    ∀ {i} ->
    Residual Θ ∅ (tunit ●) {↑ i}

  letunit● :
    ∀ {Ξ₀ Ξ A i} ->
    Residual Θ Ξ₀ (tunit ●) {i} ->
    Residual Θ Ξ  (A ●) {i} ->
    Residual Θ (Ξ₀ +ₘ Ξ) (A ●) {↑ i}

  pair● :
    ∀ {Ξ₁ Ξ₂ A B i} ->
    Residual Θ Ξ₁ (A ●) {i} ->
    Residual Θ Ξ₂ (B ●) {i} ->
    Residual Θ (Ξ₁ +ₘ Ξ₂) ((A ⊗ B) ●) {↑ i}

  letpair● :
    ∀ {Ξ₀ Ξ A B C i} ->
    Residual Θ Ξ₀ ((A ⊗ B) ●) {i} ->
    Residual (A ∷ B ∷ Θ) (one ∷ one ∷ Ξ) (C ●) {i} ->
    Residual Θ (Ξ₀ +ₘ Ξ) (C ●) {↑ i}

  inl● :
    ∀ {Ξ} {A B} {i} ->
    Residual Θ Ξ (A ●) {i} ->
    Residual Θ Ξ ((A ⊕ B) ●) {↑ i}

  inr● :
    ∀ {Ξ} {A B} {i} ->
    Residual Θ Ξ (B ●) {i} ->
    Residual Θ Ξ ((A ⊕ B) ●) {↑ i}

  case● :
    ∀ {Ξ₀ Ξ Ξₑ Ξₜ Γ₁ Γ₂ Δ₁ Δ₂ A B C i} ->
    Residual Θ Ξ₀ ((A ⊕ B) ●) {i} ->
    (spΞ : Ξₑ +ₘ Ξₜ ≡ Ξ) ->
    (θ₁ : ValEnv Γ₁ Δ₁ {i} Θ Ξₑ) ->
    (t₁ : Term Γ₁ Δ₁ (A ∷ Θ) (one ∷ Ξₜ) (C ●)) ->
    (θ₂ : ValEnv Γ₂ Δ₂ {i} Θ Ξₑ) ->
    (t₂ : Term Γ₂ Δ₂ (B ∷ Θ) (one ∷ Ξₜ) (C ●)) ->
    (v : Value [] ∅ (C # omega ~> tbool) {i}) ->
    Residual Θ (Ξ₀ +ₘ Ξ) (C ●) {↑ i}

  var● : ∀ {Ξ A i} ->
         (x : Θ ∋ A) -> (ok : varOk● Θ x Ξ) ->
         Residual Θ Ξ (A ●) {↑ i}

  pin : ∀ {Ξ₁ Ξ₂ A B i} ->
        Residual Θ Ξ₁ (A ●) {i} ->
        (v : Value    Θ Ξ₂ (A # omega ~> B ●) {i}) ->
        Residual Θ (Ξ₁ +ₘ Ξ₂) ((A ⊗ B) ●) {↑ i}

open ≡-Reasoning

-- A property on value environments that says discardable value environments cannot contain any resources.

discardable-has-no-resources : ∀ {Γ Δ Θ Ξ} -> ValEnv Γ Δ Θ Ξ -> All discardable Δ -> Ξ ≡ ∅
discardable-has-no-resources {[]} {Δ} θ ad = θ
discardable-has-no-resources {A ∷ Γ} {.omega ∷ Δ} (tup .∅ Ξ₂ spΞ (mult-omega v refl) snd) (omega ∷ ad) =
     begin
      _
     ≡⟨ sym spΞ ⟩
      ∅ +ₘ Ξ₂
     ≡⟨ ∅-lid Ξ₂ ⟩
      Ξ₂
     ≡⟨ discardable-has-no-resources {Γ} {Δ} snd ad ⟩
      ∅
     ∎
discardable-has-no-resources {A ∷ Γ} {.zero ∷ Δ} (tup .∅ Ξ₂ spΞ (mult-zero refl) snd) (zero ∷ ad) =
     begin
      _
     ≡⟨ sym spΞ ⟩
      ∅ +ₘ Ξ₂
     ≡⟨ ∅-lid Ξ₂ ⟩
      Ξ₂
     ≡⟨ discardable-has-no-resources {Γ} {Δ} snd ad ⟩
      ∅
     ∎

-- Looking up variables in an environment. Unlike the usual variable looking-up functions, this version
-- takes varOk Γ x Δ instead of x to ensure that the variable can be looked up. Notice
-- for example that we cannot look up variables with multiplicity zero. Also, the fact that the
-- return type is Value Θ Ξ A means that the value environment cannot contain other resources.

lookupVar : ∀ {Γ Δ Θ Ξ A} {x : Γ ∋ A} -> ValEnv Γ Δ Θ Ξ -> varOk Γ x Δ -> Value Θ Ξ A
lookupVar (tup .(∅) Ξ₂ spΞ (mult-omega v refl) snd) (there omega ok) with (trans (sym (∅-lid _)) spΞ)
... | refl = lookupVar snd ok
lookupVar (tup .∅ Ξ₂ spΞ (mult-zero refl) snd) (there zero ok) with (trans (sym (∅-lid _)) spΞ)
... | refl = lookupVar snd ok
lookupVar {Γ = A ∷ Γ} {Δ = m ∷ Δ} (tup Ξ₁ Ξ₂ spΞ fst snd) (here u ad) with discardable-has-no-resources {Γ} {Δ} snd ad
... | refl with trans (sym (∅-rid _)) spΞ
lookupVar {A ∷ Γ} {.omega ∷ Δ} (tup .∅ .∅ spΞ (mult-omega v refl) snd) (here omega ad) | refl | refl = v
lookupVar {A ∷ Γ} {.one ∷ Δ} (tup Ξ₁ .∅ spΞ (mult-one v) snd) (here one ad) | refl | refl = v

-- separateEnv separates value environments according to separation of
-- (unidirectional) type environments.

separateEnv : ∀ {Γ Θ Ξ} -> ∀ Δ₁ Δ₂ ->
              ValEnv Γ (Δ₁ +ₘ Δ₂) Θ Ξ ->
              (ValEnv Γ Δ₁ ⊛ ValEnv Γ Δ₂) Θ Ξ
separateEnv {[]} Δ₁ Δ₂ refl = tup ∅ ∅ (∅-lid ∅) refl refl
separateEnv {A ∷ Γ} (m₁ ∷ Δ₁) (m₂ ∷ Δ₂) (tup Ξ₁ Ξ₂ spΞ fst snd) with separateEnv {Γ} Δ₁ Δ₂ snd
separateEnv {A ∷ Γ} {Θ = Θ} {Ξ = Ξ} (zero ∷ Δ₁) (m₂ ∷ Δ₂) (tup Ξ₁ Ξ₂ spΞ fst snd) | tup Ξ₁' Ξ₂' spΞ₂ θ₁ θ₂ =
            tup Ξ₁' (Ξ₁ +ₘ Ξ₂') lemma (tup ∅ Ξ₁'   (∅-lid _) (mult-zero refl) θ₁)
                                             (tup Ξ₁ Ξ₂' refl      fst θ₂)
  where
    open import Algebra.Solver.CommutativeMonoid (+ₘ-commutativeMonoid (length Θ))
                renaming (_⊕_ to _⊞_)

    lemma : Ξ₁' +ₘ (Ξ₁ +ₘ Ξ₂') ≡ Ξ
    lemma =
      begin
        Ξ₁' +ₘ (Ξ₁ +ₘ Ξ₂')
      ≡⟨ solve 3 (λ x y z -> x ⊞ (y ⊞ z) ⊜ y ⊞ (x ⊞ z)) refl Ξ₁' Ξ₁ Ξ₂' ⟩
        Ξ₁ +ₘ (Ξ₁' +ₘ Ξ₂')
      ≡⟨ cong (_ +ₘ_) spΞ₂ ⟩
        Ξ₁ +ₘ Ξ₂
      ≡⟨ spΞ ⟩
        Ξ
      ∎

separateEnv {A ∷ Γ} {Ξ = Ξ} (one ∷ Δ₁) (zero ∷ Δ₂) (tup Ξ₁ Ξ₂ spΞ fst snd) | tup Ξ₁' Ξ₂' spΞ₂ θ₁ θ₂ =
  tup (Ξ₁ +ₘ Ξ₁') Ξ₂' lemma (tup Ξ₁ Ξ₁' refl fst θ₁)
                               (tup ∅   Ξ₂' (∅-lid _) (mult-zero refl) θ₂)
  where
    lemma : Ξ₁ +ₘ Ξ₁' +ₘ Ξ₂' ≡ Ξ
    lemma =
      begin
        Ξ₁ +ₘ Ξ₁' +ₘ Ξ₂'
      ≡⟨ +ₘ-assoc Ξ₁ Ξ₁' _ ⟩
        Ξ₁ +ₘ (Ξ₁' +ₘ Ξ₂')
      ≡⟨ cong (_ +ₘ_) spΞ₂ ⟩
        Ξ₁ +ₘ Ξ₂
      ≡⟨ spΞ ⟩
        Ξ
      ∎
separateEnv {A ∷ Γ} (one ∷ Δ₁) (one ∷ Δ₂) (tup .(∅) .(Ξ₁' +ₘ Ξ₂') refl (mult-omega v refl) snd) | tup Ξ₁' Ξ₂' refl θ₁ θ₂ =
  tup Ξ₁' Ξ₂' (sym (∅-lid _)) (tup ∅ Ξ₁' (∅-lid _) (mult-one v) θ₁)
                                (tup ∅ Ξ₂' (∅-lid _) (mult-one v) θ₂)
separateEnv {A ∷ Γ} (one ∷ Δ₁) (omega ∷ Δ₂) (tup .(∅) .(Ξ₁' +ₘ Ξ₂') refl (mult-omega v refl) snd) | tup Ξ₁' Ξ₂' refl θ₁ θ₂ =
  tup Ξ₁' Ξ₂' (sym (∅-lid _)) (tup ∅ Ξ₁' (∅-lid _) (mult-one v) θ₁)
                                (tup ∅ Ξ₂' (∅-lid _) (mult-omega v refl) θ₂)

separateEnv {A ∷ Γ} (omega ∷ Δ₁) (zero ∷ Δ₂) (tup .(∅) .(Ξ₁' +ₘ Ξ₂') refl (mult-omega v refl) snd) | tup Ξ₁' Ξ₂' refl θ₁ θ₂ =
  tup Ξ₁' Ξ₂' (sym (∅-lid _)) (tup ∅ Ξ₁' (∅-lid _) (mult-omega v refl) θ₁)
                                (tup ∅ Ξ₂' (∅-lid _) (mult-zero refl) θ₂)

separateEnv {A ∷ Γ} (omega ∷ Δ₁) (one ∷ Δ₂) (tup .(∅) .(Ξ₁' +ₘ Ξ₂') refl (mult-omega v refl) snd) | tup Ξ₁' Ξ₂' refl θ₁ θ₂ =
   tup Ξ₁' Ξ₂' (sym (∅-lid _)) (tup ∅ Ξ₁' (∅-lid _) (mult-omega v refl) θ₁)
                                 (tup ∅ Ξ₂' (∅-lid _) (mult-one v) θ₂)

separateEnv {A ∷ Γ} (omega ∷ Δ₁) (omega ∷ Δ₂) (tup .(∅) .(Ξ₁' +ₘ Ξ₂') refl (mult-omega v refl) snd) | tup Ξ₁' Ξ₂' refl θ₁ θ₂ =
  tup Ξ₁' Ξ₂' (sym (∅-lid _)) (tup ∅ Ξ₁' (∅-lid _) (mult-omega v refl) θ₁)
                                (tup ∅ Ξ₂' (∅-lid _) (mult-omega v refl) θ₂)

-- un×ₘ-valEnv is a counter of separateEnv for ×ₘ.

un×ₘ-valEnv : ∀ Γ {m Δ Θ Ξ} -> ValEnv Γ (m ×ₘ Δ) Θ Ξ -> ∃[ Ξ' ] (ValEnv Γ Δ Θ Ξ' × m ×ₘ Ξ' ≡ Ξ)
un×ₘ-valEnv [] {m} θ = ∅ , refl , trans (×ₘ∅ m) (sym θ)
un×ₘ-valEnv (_ ∷ Γ) {Δ = mₓ ∷ Δ} (tup Ξ₁ Ξ₂ refl fst snd) with un×ₘ-valEnv Γ snd
un×ₘ-valEnv (_ ∷ Γ) {one} {mₓ ∷ Δ} (tup Ξ₁ .(Data.Vec.map (λ y → y) Ξ') refl fst snd) | Ξ' , θ' , refl = Ξ₁ +ₘ Ξ' , tup Ξ₁ Ξ' refl fst θ' , lemma
  where
    open import Data.Vec.Properties using (map-id)

    lemma : Data.Vec.map (λ x -> x) (Ξ₁ +ₘ Ξ') ≡ Ξ₁ +ₘ Data.Vec.map (λ x -> x) Ξ'
    lemma = begin
              Data.Vec.map (λ x -> x) (Ξ₁ +ₘ Ξ')
            ≡⟨ map-id _ ⟩
              Ξ₁ +ₘ Ξ'
            ≡⟨ cong (_ +ₘ_) (sym (map-id _)) ⟩
              Ξ₁ +ₘ Data.Vec.map (λ x -> x) Ξ'
            ∎

un×ₘ-valEnv (_ ∷ Γ) {omega} {zero ∷ Δ} (tup .(∅) .(Data.Vec.map (mul₀ omega) Ξ') refl (mult-zero refl) snd) | Ξ' , θ' , refl = Ξ' , tup ∅ Ξ' (∅-lid _) (mult-zero refl) θ' , sym (∅-lid _)
un×ₘ-valEnv (_ ∷ Γ) {omega} {one ∷ Δ} (tup .(∅) .(Data.Vec.map (mul₀ omega) Ξ') refl (mult-omega v refl) snd) | Ξ' , θ' , refl = Ξ' , tup ∅ Ξ' (∅-lid _) (mult-one v) θ' , sym (∅-lid _)
un×ₘ-valEnv (_ ∷ Γ) {omega} {omega ∷ Δ} (tup .(∅) .(Data.Vec.map (mul₀ omega) Ξ') refl (mult-omega v refl) snd) | Ξ' , θ' , refl = Ξ' , tup ∅ Ξ' (∅-lid _) (mult-omega v refl) θ' , sym (∅-lid _)

-- weakenΘ-value and weakenΘ-residual are counterparts of
-- weakenΘ-term for values and residuals.

weakenΘ-value :
  ∀ {Θ Ξ Θ' Ξ' A i} ->
  compatΘ Θ Ξ Θ' Ξ' ->
  Value Θ Ξ A {i} -> Value Θ' Ξ' A
weakenΘ-residual :
  ∀ {Θ Ξ Θ' Ξ' A i} ->
  compatΘ Θ Ξ Θ' Ξ' ->
  Residual Θ Ξ A {i} -> Residual Θ' Ξ' A

weakenΘ-valEnv :
  ∀ Γ {Δ Θ Ξ Θ' Ξ' i} ->
  compatΘ Θ Ξ Θ' Ξ' ->
  ValEnv Γ Δ {i} Θ Ξ -> ValEnv Γ Δ Θ' Ξ'

weakenΘ-mult :
  ∀ {Θ Ξ Θ' Ξ' m A i} ->
  compatΘ Θ Ξ Θ' Ξ' ->
  mult (λ Θ Ξ -> Value Θ Ξ A {i}) m Θ  Ξ ->
  mult (λ Θ Ξ -> Value Θ Ξ A) m Θ' Ξ'

weakenΘ-value ext (clo {Γ' = Γ'} m refl θ t) =
  case* compatΘ-split ext of λ {
    (_ , _ , ext₁ , ext₂ , refl) ->
      clo m refl (weakenΘ-valEnv Γ' ext₁ θ)
                 (weakenΘ-term ext₂ t)
  }

weakenΘ-value ext (unit refl) =
  case* compatΘ-∅ ext of λ where
    refl -> unit refl

weakenΘ-value ext (pair refl v₁ v₂) =
  case* compatΘ-split ext of λ where
   (_ , _ , ext₁ , ext₂ , refl) ->
     pair refl (weakenΘ-value ext₁ v₁) (weakenΘ-value ext₂ v₂)

weakenΘ-value ext (many m refl v) =
  case* compatΘ-×ₘ ext of λ where
    (_ , ext' , refl) -> many m refl (weakenΘ-value ext' v)

weakenΘ-value ext (inl v) = inl (weakenΘ-value ext v)
weakenΘ-value ext (inr v) = inr (weakenΘ-value ext v)
weakenΘ-value ext (roll v) = roll (weakenΘ-value ext v)
weakenΘ-value ext (red x) = red (weakenΘ-residual ext x)
weakenΘ-value ext (inj refl r) =
  case* compatΘ-∅ ext of λ {
    refl -> inj refl (weakenΘ-residual ext-id r)
  }

weakenΘ-mult ext (mult-zero refl) =
  case* compatΘ-∅ ext  of λ {
    refl -> mult-zero refl
  }

weakenΘ-mult ext (mult-one v) = mult-one (weakenΘ-value ext v)
weakenΘ-mult ext (mult-omega v refl) =
  case* compatΘ-∅ ext of λ {
    refl -> mult-omega (weakenΘ-value ext v) refl
  }

weakenΘ-valEnv [] ext refl =
  case* compatΘ-∅ ext of λ {
    refl -> refl
  }
weakenΘ-valEnv (_ ∷ Γ) {_ ∷ Δ} ext (tup Ξ₁ Ξ₂ refl mv θ) =
  case* compatΘ-split ext of λ {
    (Ξ₁' , Ξ₂' , ext₁ , ext₂ , refl) ->
      tup Ξ₁' Ξ₂' refl (weakenΘ-mult ext₁ mv) (weakenΘ-valEnv Γ ext₂ θ)
  }

weakenΘ-residual ext unit● =
  case* compatΘ-∅ ext of λ {
    refl -> unit●
  }

weakenΘ-residual ext (letunit● r₁ r₂) =
  case* compatΘ-split ext of λ {
    (_ , _ , ext₁ , ext₂ , refl) ->
      letunit● (weakenΘ-residual ext₁ r₁)
               (weakenΘ-residual ext₂ r₂)
  }

weakenΘ-residual ext (pair● r₁ r₂) =
  case* compatΘ-split ext of λ {
    (_ , _ , ext₁ , ext₂ , refl) ->
      pair● (weakenΘ-residual ext₁ r₁)
            (weakenΘ-residual ext₂ r₂)
  }

weakenΘ-residual ext (letpair● r₁ r₂) =
  case* compatΘ-split ext of λ {
    (_ , _ , ext₁ , ext₂ , refl) ->
      letpair● (weakenΘ-residual ext₁ r₁)
               (weakenΘ-residual (compat-skip (compat-skip ext₂)) r₂)
  }

weakenΘ-residual ext (inl● r) = inl● (weakenΘ-residual ext r)
weakenΘ-residual ext (inr● r) = inr● (weakenΘ-residual ext r)
weakenΘ-residual ext (case● {Γ₁ = Γ₁} {Γ₂} r refl θ₁ t₁ θ₂ t₂ v) with compatΘ-split ext
... | _ , _ , ext₁ , ext₂ , refl
   with compatΘ-split ext₂
... | _ , _ , extₑ , extₜ , refl =
    case● (weakenΘ-residual ext₁ r)
          refl
          (weakenΘ-valEnv Γ₁ extₑ θ₁)
          (weakenΘ-term   (compat-skip extₜ) t₁)
          (weakenΘ-valEnv Γ₂ extₑ θ₂)
          (weakenΘ-term   (compat-skip extₜ) t₂)
          (weakenΘ-value  adjust∅Θ v)

weakenΘ-residual ext (var● x ok) =
  case* compatΘ-preserves-varOk● ext ok of λ {
    (x' , ok') -> var● x' ok'
  }

weakenΘ-residual ext (pin r v) =
  case* compatΘ-split ext of λ {
    (_ , _ , ext₁ , ext₂ , refl) ->
       pin (weakenΘ-residual ext₁ r)
           (weakenΘ-value ext₂ v)
  }

-- Converting a value (of multiplicty m) into an entry to be inserted to a value environment.

value-to-multM :
  ∀ {Θ m Ξ A} ->
  all-no-omega (m ×ₘ Ξ) -> Value Θ Ξ A -> mult (λ Θ' Ξ' -> Value Θ' Ξ' A) (M→M₀ m) Θ (m ×ₘ Ξ)
value-to-multM {Θ} {one} ano v = mult-one (subst (λ x -> Value Θ x _) (sym (one×ₘ _)) v )
value-to-multM {Θ} {omega} {Ξ} ano v with all-no-omega-omega×ₘ Ξ ano
... | refl = mult-omega v (×ₘ∅ _)

-- Some specialized versions of subst.

substV : ∀ {Θ Ξ Ξ' A} -> Ξ ≡ Ξ' -> Value Θ Ξ A -> Value Θ Ξ' A
substV refl v = v

substR : ∀ {Θ Ξ Ξ' A} -> Ξ ≡ Ξ' -> Residual Θ Ξ A -> Residual Θ Ξ' A
substR refl E = E

max_stars_repo_name: kztk-m/sparcl-agda

max_issues_repo_name: kztk-m/sparcl-agda

max_forks_repo_name: kztk-m/sparcl-agda


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.Polynomials.Multivariate.Properties where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Nat renaming(_+_ to _+n_; _·_ to _·n_)
open import Cubical.Data.Vec

open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing

open import Cubical.Algebra.Polynomials.Multivariate.Base

private variable
  ℓ ℓ' : Level

module Nth-Poly-structure (A' : CommRing ℓ) (n : ℕ) where

  private
    A = fst A'
    Ar = CommRing→Ring A'

  open CommRingStr (snd A')
  open RingTheory Ar

-----------------------------------------------------------------------------

  Poly-com-adv : (P Q R S : Poly A' n) →  ((P Poly+ Q) Poly+ (R Poly+ S) ≡ (P Poly+ R) Poly+ (Q Poly+ S))
  Poly-com-adv P Q R S = ((P Poly+ Q) Poly+ (R Poly+ S) ≡⟨ Poly+-assoc (P Poly+ Q) R S ⟩
                     (((P Poly+ Q) Poly+ R) Poly+ S) ≡⟨ cong (λ X → X Poly+ S) (sym (Poly+-assoc P Q R)) ⟩
                     ((P Poly+ (Q Poly+ R)) Poly+ S) ≡⟨ cong (λ X → (P Poly+ X) Poly+ S) (Poly+-comm Q R) ⟩
                     ((P Poly+ (R Poly+ Q)) Poly+ S) ≡⟨ cong (λ X → X Poly+ S) (Poly+-assoc P R Q) ⟩
                     (((P Poly+ R) Poly+ Q) Poly+ S) ≡⟨ sym (Poly+-assoc (P Poly+ R) Q S) ⟩
                     ((P Poly+ R) Poly+ (Q Poly+ S)) ∎)

  Poly+-Lid : (P : Poly A' n) → 0P Poly+ P ≡ P
  Poly+-Lid P = (Poly+-comm 0P P) ∙ (Poly+-Rid P)

  Poly-inv : Poly A' n → Poly A' n
  Poly-inv = Poly-Rec-Set.f A' n (Poly A' n) trunc
             0P
             (λ v a → base v (- a))
             (λ PS RS → PS Poly+ RS)
             Poly+-assoc
             Poly+-Rid
             Poly+-comm
             (λ v → base v (- 0r) ≡⟨ cong (base v) 0Selfinverse ⟩ base v 0r ≡⟨ base-0P v ⟩ 0P ∎)
             λ v a b → (base-Poly+ v (- a) (- b)) ∙ (cong (base v) (-Dist a b))

  Poly-invinv : (P : Poly A' n) → Poly-inv (Poly-inv P) ≡ P
  Poly-invinv = Poly-Ind-Prop.f A' n (λ P → Poly-inv (Poly-inv P) ≡ P) (λ _ → trunc _ _)
                refl
                (λ v a → cong (base v) (-Idempotent a))
                λ {P Q} ind-P ind-Q → cong₂ _Poly+_ ind-P ind-Q

  Poly+-rinv : (P : Poly A' n ) → P Poly+ (Poly-inv P) ≡ 0P
  Poly+-rinv = Poly-Ind-Prop.f A' n (λ P → (P Poly+ Poly-inv P) ≡ 0P) (λ _ → trunc _ _)
               (Poly+-Rid 0P)
               (λ v a → (base-Poly+ v a (- a)) ∙ cong (base v) (+Rinv a) ∙ base-0P v)
               λ {P Q} ind-P ind-Q → ((P Poly+ Q) Poly+ ((Poly-inv P) Poly+ (Poly-inv Q)))
                                               ≡⟨ Poly-com-adv P Q (Poly-inv P) (Poly-inv Q) ⟩
                                      ((P Poly+ Poly-inv P) Poly+ (Q Poly+ Poly-inv Q))
                                               ≡⟨ cong₂ _Poly+_ ind-P ind-Q ⟩
                                      (0P Poly+ 0P)
                                               ≡⟨ Poly+-Rid 0P ⟩
                                      0P ∎

  Poly+-linv : (P  : Poly A' n) → (Poly-inv P) Poly+ P ≡ 0P
  Poly+-linv = Poly-Ind-Prop.f A' n _ (λ _ → trunc _ _)
               (Poly+-Rid 0P)
               (λ v a → (base-Poly+ v (- a) a) ∙ cong (base v) (snd (+Inv a)) ∙ base-0P v)
               λ {U V} ind-U ind-V → Poly-com-adv (Poly-inv U) (Poly-inv V) U V ∙ cong₂ _Poly+_ ind-U ind-V ∙ Poly+-Rid 0P

-----------------------------------------------------------------------------

  _Poly*_ : Poly A' n → Poly A' n → Poly A' n
  _Poly*_ = -- Induction Left Argument
            Poly-Rec-Set.f A' n (Poly A' n → Poly A' n)
            (λ f g p q i j Q → trunc (f Q) (g Q) (λ X → p X Q) (λ X → q X Q) i j )
            (λ Q    → 0P)
            (λ v a  → -- Induction Right Argument
                       Poly-Rec-Set.f A' n (Poly A' n) trunc
                       0P
                       (λ v' a' → base (v +n-vec v') (a · a'))
                       _Poly+_
                       Poly+-assoc
                       Poly+-Rid
                       Poly+-comm
                       (λ v' → (cong (base (v +n-vec v')) (0RightAnnihilates a)) ∙ (base-0P (v +n-vec v')))
                       λ v' b c → (base-Poly+ (v +n-vec v') (a · b) (a · c)) ∙ (cong (base (v +n-vec v')) (sym (·Rdist+ a b c))))
                       -- End Right induction
            (λ PS QS Q → (PS Q) Poly+ (QS Q) )
            (λ PS QS RS i Q → Poly+-assoc (PS Q) (QS Q) (RS Q) i)
            (λ PS i Q       → Poly+-Rid (PS Q) i)
            (λ PS QS i Q    → Poly+-comm (PS Q) (QS Q) i)
            (λ v    → funExt (
                             -- Induction Right Argument
                             Poly-Ind-Prop.f A' n _ (λ _ → trunc _ _)
                             refl
                             (λ v' a' → (cong (base (v +n-vec v')) (0LeftAnnihilates a')) ∙ (base-0P (v +n-vec v')))
                             λ {P Q} ind-P ind-Q → (cong₂ _Poly+_ ind-P ind-Q) ∙ (Poly+-Rid 0P) ))
                             -- End Right Induction
            λ v a b → funExt (
                             -- Induction Right Argument
                             Poly-Ind-Prop.f A' n _ (λ _ → trunc _ _)
                             (Poly+-Rid 0P)
                             (λ v' c → (base-Poly+ (v +n-vec v') (a · c) (b · c)) ∙ (cong (base (v +n-vec v')) (sym (·Ldist+ a b c))))
                             λ {P Q} ind-P ind-Q → (Poly-com-adv _ _ _ _) ∙ (cong₂ _Poly+_ ind-P ind-Q))
                             -- End Right Induction
            -- End Left Induction

  Poly*-assoc : (P Q R : Poly A' n) → P Poly* (Q Poly* R) ≡ (P Poly* Q) Poly* R
  Poly*-assoc = Poly-Ind-Prop.f A' n _
                (λ P p q i Q R j → trunc (P Poly* (Q Poly* R)) ((P Poly* Q) Poly* R) (p Q R) (q Q R) i j)
                (λ _ _ → refl)
                (λ v a → Poly-Ind-Prop.f A' n _
                          (λ Q p q i R j → trunc (base v a Poly* (Q Poly* R)) ((base v a Poly* Q) Poly* R) (p R) (q R) i j)
                          (λ _ → refl)
                          (λ v' a' → Poly-Ind-Prop.f A' n _ (λ _ → trunc _ _)
                                      refl
                                      (λ v'' a'' → cong₂ base (+n-vec-assoc v v' v'') (·Assoc a a' a''))
                                      (λ {U V} ind-U ind-V → cong₂ _Poly+_ ind-U ind-V))
                          (λ {U V} ind-U ind-V R → cong₂ _Poly+_ (ind-U R) (ind-V R)))
                λ {U V} ind-U ind-V Q R → cong₂ _Poly+_ (ind-U Q R) (ind-V Q R)

  0PLeftAnnihilatesPoly : (P : Poly A' n) → 0P Poly* P ≡ 0P
  0PLeftAnnihilatesPoly P = refl

  0PRightAnnihilatesPoly : (P : Poly A' n) → P Poly* 0P ≡ 0P
  0PRightAnnihilatesPoly = Poly-Ind-Prop.f A' n (λ P → (P Poly* 0P) ≡ 0P) (λ _ → trunc _ _)
                           refl
                           (λ _ _ → refl)
                           λ {P Q} ind-P ind-Q → (cong₂ _Poly+_ ind-P ind-Q) ∙ (Poly+-Rid 0P)

  1P : Poly A' n
  1P = base (replicate zero) 1r

  Poly*-Rid : (P : Poly A' n) → P Poly* 1P ≡ P
  Poly*-Rid = Poly-Ind-Prop.f A' n (λ P → (P Poly* 1P) ≡ P) (λ _ → trunc _ _)
              refl
              (λ v a → cong₂ base (+n-vec-rid v) (·Rid a))
              (λ {P Q} ind-P ind-Q → cong₂ _Poly+_ ind-P ind-Q)

  Poly*-Lid : (P : Poly A' n) → 1P Poly* P ≡ P
  Poly*-Lid = Poly-Ind-Prop.f A' n (λ P → (1P Poly* P) ≡ P) (λ _ → trunc _ _)
              refl
              (λ v a → cong₂ base (+n-vec-lid v) (·Lid a))
              λ {P Q} ind-P ind-Q → cong₂ _Poly+_ ind-P ind-Q

  Poly*-Rdist : (P Q R : Poly A' n) → P Poly* (Q Poly+ R) ≡ (P Poly* Q) Poly+ (P Poly* R)
  Poly*-Rdist = Poly-Ind-Prop.f A' n _
                (λ P p q i Q R j → trunc (P Poly* (Q Poly+ R)) ((P Poly* Q) Poly+ (P Poly* R)) (p Q R) (q Q R) i j)
                (λ _ _ → sym (Poly+-Rid 0P))
                (λ v a → λ Q R → refl)
                λ {U V} ind-U ind-V Q R → (cong₂ _Poly+_ (ind-U Q R) (ind-V Q R)) ∙ Poly-com-adv (U Poly* Q) (U Poly* R) (V Poly* Q) (V Poly* R)

  Poly*-Ldist : (P Q R : Poly A' n) → (P Poly+ Q) Poly* R ≡ (P Poly* R) Poly+ (Q Poly* R)
  Poly*-Ldist P Q R = refl

  Poly*-comm : (P Q : Poly A' n) → P Poly* Q ≡ Q Poly* P
  Poly*-comm = Poly-Ind-Prop.f A' n _
               (λ P p q i Q j → trunc (P Poly* Q) (Q Poly* P) (p Q) (q Q) i j)
               (λ Q → sym (0PRightAnnihilatesPoly Q))
               (λ v a → Poly-Ind-Prop.f A' n _ (λ _ → trunc _ _)
                          refl
                          (λ v' a' → cong₂ base (+n-vec-comm v v') (·Comm a a'))
                          (λ {U V} ind-U ind-V → cong₂ _Poly+_ ind-U ind-V))
               λ {U V} ind-U ind-V Q → ((cong₂ _Poly+_ (ind-U Q) (ind-V Q)) ∙ sym (Poly*-Rdist Q U V))


text:
{-# OPTIONS --cubical --no-import-sorts  #-}

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Function.Base using (_∋_; _$_)
open import Cubical.Data.Sum.Base renaming (_⊎_ to infixr 4 _⊎_)
open import Cubical.HITs.PropositionalTruncation.Base -- ∣_∣
open import Cubical.HITs.PropositionalTruncation.Properties using (propTruncIsProp) renaming (elim to ∣∣-elim)
open import Cubical.Foundations.Logic renaming
  ( inl to inlᵖ
  ; inr to inrᵖ
  ; _⇒_ to infixr 0 _⇒_                  -- shifting by -6
  ; _⇔_ to infixr -2 _⇔_                 --
  ; ∃[]-syntax to infix  -4 ∃[]-syntax   --
  ; ∃[∶]-syntax to infix  -4 ∃[∶]-syntax --
  ; ∀[∶]-syntax to infix  -4 ∀[∶]-syntax --
  ; ∀[]-syntax to infix  -4 ∀[]-syntax   --
  )

open import Utils
open import MorePropAlgebra.Bundles
open import MoreLogic.Definitions hiding (≡ˢ-syntax)
open import MoreLogic.Reasoning
open import MoreLogic.Properties

module MorePropAlgebra.Properties.Lattice {ℓ} {ℓ'} (assumptions : Lattice {ℓ} {ℓ'}) where
open Lattice assumptions renaming (Carrier to A)

module OnType where
  abstract
    ≤-reflectsʳ-≡ : ∀ x y → [ (∀[ z ] z ≤ x ⇔ z ≤ y) ⇔ x ≡ₚ y ]
    ≤-reflectsʳ-≡ x y .fst z≤x⇔z≤y    = ≤-antisym x y (z≤x⇔z≤y x .fst (≤-refl x)) (z≤x⇔z≤y y .snd (≤-refl y))
    ≤-reflectsʳ-≡ x y .snd x≡y z .fst = substₚ (λ p → z ≤ p) x≡y
    ≤-reflectsʳ-≡ x y .snd x≡y z .snd = substₚ (λ p → z ≤ p) (symₚ x≡y)

    ≤-reflectsˡ-≡ : ∀ x y → [ (∀[ z ] x ≤ z ⇔ y ≤ z) ⇔ x ≡ₚ y ]
    ≤-reflectsˡ-≡ x y .fst x≤z⇔y≤z    = ≤-antisym x y (x≤z⇔y≤z y .snd (≤-refl y)) (x≤z⇔y≤z x .fst (≤-refl x))
    ≤-reflectsˡ-≡ x y .snd x≡y z .fst = substₚ (λ p → p ≤ z) x≡y
    ≤-reflectsˡ-≡ x y .snd x≡y z .snd = substₚ (λ p → p ≤ z) (symₚ x≡y)

    min-≤ : ∀ x y → [ (min x y ≤ x) ⊓ (min x y ≤ y) ]
    min-≤ x y = is-min x y (min x y) .fst (≤-refl (min x y))

    max-≤ : ∀ x y → [ (x ≤ max x y) ⊓ (y ≤ max x y) ]
    max-≤ x y = is-max x y (max x y) .fst (≤-refl (max x y))

    min-identity-≤ : ∀ x y → [ x ≤ y ] → [ min x y ≡ₚ x ]
    min-identity-≤ x y x≤y = symₚ $ ≤-antisym x (min x y) (is-min x y x .snd (≤-refl x , x≤y)) (min-≤ x y .fst)

    max-identity-≤ : ∀ x y → [ x ≤ y ] → [ max x y ≡ₚ y ]
    max-identity-≤ x y x≤y = symₚ $ ≤-antisym y (max x y) (max-≤ x y .snd) (is-max x y y .snd (x≤y , ≤-refl y))

    -- min-≤-⊔ : ∀ x y z → [ min x y ≤ z ] → [ (x ≤ z) ⊔ (y ≤ z) ]
    -- min-≤-⊔ x y z mxy≤z = {! contraposition (x ≤ y) ⊓ (y ≤ z) (x ≤ z) $ uncurryₚ (x ≤ y) (y ≤ z) (x ≤ z)$ ≤-trans x y z  !}

    min-identity : ∀ x → [ min x x ≡ₚ x ]
    min-identity x =
      let p = is-min x x x .snd (≤-refl x , ≤-refl x)
          q = min-≤ x x .fst
      in ≤-antisym (min x x) x q p

    min-comm : ∀ x y → [ min x y ≡ₚ min y x ]
    min-comm x y = ≤-reflectsʳ-≡ (min x y) (min y x) .fst γ where
      γ : ∀ z → [ (z ≤ min x y) ⇔ (z ≤ min y x) ]
      γ z .fst p = is-min y x z .snd (swap (is-min x y z .fst p))
      γ z .snd p = is-min x y z .snd (swap (is-min y x z .fst p))

    min-assoc : ∀ x y z → [ min (min x y) z ≡ₚ min x (min y z) ]
    min-assoc x y z =  ≤-reflectsʳ-≡ (min (min x y) z) (min x (min y z)) .fst γ where
      γ : ∀ w → [ (w ≤ min (min x y) z) ⇔ (w ≤ min x (min y z)) ]
      γ w .fst p = let (w≤mxy , w≤z) = is-min (min x y) z w .fst p
                       (w≤x   , w≤y) = is-min x y w .fst w≤mxy
                       w≤myz         = is-min y z w .snd (w≤y , w≤z)
                   in  is-min x (min y z) w .snd (w≤x , w≤myz)
      γ w .snd p = let (w≤x , w≤myz) = is-min x (min y z) w .fst p
                       (w≤y , w≤z  ) = is-min y z w .fst w≤myz
                       w≤mxy         = is-min x y w .snd (w≤x , w≤y)
                   in is-min (min x y) z w .snd (w≤mxy , w≤z)

    max-identity : ∀ x → [ max x x ≡ₚ x ]
    max-identity x =
      let p = is-max x x x .snd (≤-refl x , ≤-refl x)
          q = max-≤ x x .fst
      in symₚ $ ≤-antisym x (max x x) q p

    max-comm : ∀ x y → [ max x y ≡ₚ max y x ]
    max-comm x y = ≤-reflectsˡ-≡ (max x y) (max y x) .fst γ where
      γ : ∀ z → [ (max x y ≤ z) ⇔ (max y x ≤ z) ]
      γ z .fst p = is-max y x z .snd (swap (is-max x y z .fst p))
      γ z .snd p = is-max x y z .snd (swap (is-max y x z .fst p))

    max-assoc : ∀ x y z → [ max (max x y) z ≡ₚ max x (max y z) ]
    max-assoc x y z =  ≤-reflectsˡ-≡ (max (max x y) z) (max x (max y z)) .fst γ where
      γ : ∀ w → [ (max (max x y) z ≤ w) ⇔ (max x (max y z)) ≤ w ]
      γ w .fst p = let (mxy≤w , z≤w) = is-max (max x y) z w .fst p
                       (x≤w   , y≤w) = is-max x y w .fst mxy≤w
                       myz≤w         = is-max y z w .snd (y≤w , z≤w)
                   in  is-max x (max y z) w .snd (x≤w , myz≤w)
      γ w .snd p = let (x≤w , myz≤w) = is-max x (max y z) w .fst p
                       (y≤w , z≤w  ) = is-max y z w .fst myz≤w
                       mxy≤w         = is-max x y w .snd (x≤w , y≤w)
                   in is-max (max x y) z w .snd (mxy≤w , z≤w)

    min-max-absorptive : ∀ x y → [ min x (max x y) ≡ₚ x ]
    min-max-absorptive x y = ≤-reflectsʳ-≡ (min x (max x y)) x .fst γ where
      γ : ∀ z → [ (z ≤ min x (max x y)) ⇔ (z ≤ x) ]
      γ z .fst p = is-min x (max x y) z .fst p .fst
      γ z .snd p = is-min x (max x y) z .snd (p , ≤-trans _ _ _ p (max-≤ x y .fst))

    max-min-absorptive : ∀ x y → [ max x (min x y) ≡ₚ x ]
    max-min-absorptive x y = ≤-reflectsˡ-≡ (max x (min x y)) x .fst γ where
      γ : ∀ z → [ (max x (min x y) ≤ z) ⇔ (x ≤ z) ]
      γ z .fst p = is-max x (min x y) z .fst p .fst
      γ z .snd p = is-max x (min x y) z .snd (p , ≤-trans _ _ _ (min-≤ x y .fst) p)

  -- min-split : ∀ x y → [ x ≤ min x y ⊔ y ≤ min x y ]
  -- min-split x y = {! is-min x y x  !}

  -- min-elim : ∀ x y → P x → P y → P (min x y)

  -- w < x + z → w <
  -- w ≤ a + b → w ≤ a ⊔ w ≤ b

  -- also interesting: interaction of max and abs
  --   https://math.stackexchange.com/questions/3149575/max-and-min-inequality

  module +-inv⇒
    (_+_ : A → A → A)
    (0f : A)
    (+-creates-≤ : ∀ a b x → [ (a ≤ b) ⇔ ((a + x) ≤ (b + x)) ])
    (+-assoc     : ∀ a b c → [ ((a + b) + c) ≡ₚ (a + (b + c)) ])
    (+-identityʳ : ∀ x → [ (x + 0f) ≡ₚ x ])
    (+-comm      : ∀ a b → [ (a + b) ≡ₚ (b + a) ])
    (+-inv''     : ∀ x → [ ∃[ y ] (x + y) ≡ₚ 0f ])
    where

    ≤-min-+ : ∀ a b c w → [ w ≤ (a + c) ] → [ w ≤ (b + c) ] → [ w ≤ (min a b + c) ]
    ≤-min-+ a b c w w≤a+c w≤b+c = ∣∣-elim (λ _ → isProp[] (w ≤ (min a b + c))) (λ{ (-c , p) → γ -c p }) (+-inv'' c) where
      γ : ∀ -c → [ (c + -c) ≡ₚ 0f ] → [ w ≤ (min a b + c) ]
      γ -c p = (
        (w      ≤ (a + c)     ) ⊓ (w      ≤ (b + c)     ) ⇒ᵖ⟨ (λ{ (q , r) → +-creates-≤ w (a + c) -c .fst q , +-creates-≤ w (b + c) -c .fst r}) ⟩
        (w + -c ≤ (a + c) + -c) ⊓ (w + -c ≤ (b + c) + -c) ⇒ᵖ⟨ (λ{ (q , r) → substₚ (λ p → w + -c ≤ p) (+-assoc a c -c) q , substₚ (λ p → w + -c ≤ p) (+-assoc b c -c) r}) ⟩
        (w + -c ≤ a + (c + -c)) ⊓ (w + -c ≤ b + (c + -c)) ⇒ᵖ⟨ (λ{ (q , r) → substₚ (λ p → w + -c ≤ a + p) p q , substₚ (λ p → w + -c ≤ b + p) p r}) ⟩
        (w + -c ≤ a + 0f      ) ⊓ (w + -c ≤ b + 0f      ) ⇒ᵖ⟨ (λ{ (q , r) → substₚ (λ p → w + -c ≤ p) (+-identityʳ a) q , substₚ (λ p → w + -c ≤ p) (+-identityʳ b) r}) ⟩
        (w + -c ≤ a           ) ⊓ (w + -c ≤ b           ) ⇒ᵖ⟨ is-min a b (w + -c) .snd ⟩
        (w + -c       ≤ min a b    )                      ⇒ᵖ⟨ +-creates-≤ (w + -c) (min a b) c .fst ⟩
        ((w + -c) + c ≤ min a b + c)                      ⇒ᵖ⟨ substₚ (λ p → p ≤ min a b + c) (+-assoc w -c c) ⟩
        (w + (-c + c) ≤ min a b + c)                      ⇒ᵖ⟨ substₚ (λ p → w + p ≤ min a b + c) (substₚ (λ p → p ≡ₚ 0f) (+-comm c -c) p) ⟩
        (w + 0f       ≤ min a b + c)                      ⇒ᵖ⟨ substₚ (λ p → p ≤ min a b + c) (+-identityʳ w) ⟩
        (w            ≤ min a b + c)                      ◼ᵖ) .snd (w≤a+c , w≤b+c)

    ≤-max-+ : ∀ a b c w → [ (a + c) ≤ w ] → [ (b + c) ≤ w ] → [ (max a b + c) ≤ w ]
    ≤-max-+ a b c w a+c≤w b+c≤ = ∣∣-elim (λ _ → isProp[] ((max a b + c) ≤ w)) (λ{ (-c , p) → γ -c p }) (+-inv'' c) where
      γ : ∀ -c → [ (c + -c) ≡ₚ 0f ] → [ (max a b + c) ≤ w ]
      γ -c p = (
        ((a + c)      ≤ w     ) ⊓ ((b + c)      ≤ w     ) ⇒ᵖ⟨ (λ{ (q , r) → +-creates-≤ (a + c) w -c .fst q , +-creates-≤ (b + c) w -c .fst r }) ⟩
        ((a + c) + -c ≤ w + -c) ⊓ ((b + c) + -c ≤ w + -c) ⇒ᵖ⟨ (λ{ (q , r) → substₚ (λ p → p ≤ w + -c) (+-assoc a c -c) q , substₚ (λ p → p ≤ w + -c) (+-assoc b c -c) r }) ⟩
        (a + (c + -c) ≤ w + -c) ⊓ (b + (c + -c) ≤ w + -c) ⇒ᵖ⟨ (λ{ (q , r) → substₚ (λ p → a + p ≤ w + -c) p q , substₚ (λ p → b + p ≤ w + -c) p r }) ⟩
        (a + 0f       ≤ w + -c) ⊓ (b + 0f       ≤ w + -c) ⇒ᵖ⟨ (λ{ (q , r) → substₚ (λ p → p ≤ w + -c) (+-identityʳ a) q , substₚ (λ p → p ≤ w + -c) (+-identityʳ b) r }) ⟩
        (a            ≤ w + -c) ⊓ (b            ≤ w + -c) ⇒ᵖ⟨ is-max a b (w + -c) .snd ⟩
        (max a b ≤ w + -c)                                ⇒ᵖ⟨ +-creates-≤ (max a b) (w + -c) c .fst ⟩
        (max a b + c ≤ (w + -c)  + c)                     ⇒ᵖ⟨ substₚ (λ p → max a b + c ≤ p) (+-assoc w -c c) ⟩
        (max a b + c ≤ w + (-c + c))                      ⇒ᵖ⟨ substₚ (λ p → max a b + c ≤ w + p) (substₚ (λ p → p ≡ₚ 0f) (+-comm c -c) p) ⟩
        (max a b + c ≤ w + 0f)                            ⇒ᵖ⟨ substₚ (λ p → max a b + c ≤ p) (+-identityʳ w) ⟩
        (max a b + c ≤ w)                                 ◼ᵖ) .snd (a+c≤w , b+c≤)

  module ·-inv⇒
    {ℓ}
    (_·_ : A → A → A)
    (_#_ : hPropRel A A ℓ)
    (0f 1f : A)
    (·-creates-≤ : ∀ a b x → [ 0f ≤ x ] → [ (a ≤ b) ⇔ ((a · x) ≤ (b · x)) ])
    (·-assoc     : ∀ a b c → [ ((a · b) · c) ≡ₚ (a · (b · c)) ])
    (·-identityʳ : ∀ x → [ (x · 0f) ≡ₚ x ])
    (·-comm      : ∀ a b → [ (a · b) ≡ₚ (b · a) ])
    (·-inv''     : ∀ x → [ ∃[ y ] (x · y) ≡ₚ 1f ])
    where

    -- ≤-min-· : ∀ a b c w → [ w ≤ (a · c) ] → [ w ≤ (b · c) ] → [ w ≤ (min a b · c) ]
    -- ≤-min-· a b c w w≤a·c w≤b· = {! is-min a b  !}
    --
    -- ≤-max-· : ∀ a b c w → [ (a · c) ≤ w ] → [ (b · c) ≤ w ] → [ (max a b · c) ≤ w ]
    -- ≤-max-· a b c w a·c≤w b·c≤ = {!   !}

  module ≤-dicho⇒+
    (_+_ : A → A → A)
    (≤-dicho : ∀ x y → [ (x ≤ y) ⊔ (y ≤ x) ])
    where

    ≤-min-+ : ∀ a b c w → [ w ≤ (a + c) ] → [ w ≤ (b + c) ] → [ w ≤ (min a b + c) ]
    ≤-min-+ a b c w w≤a+c w≤b+c = case ≤-dicho a b as (a ≤ b) ⊔ (b ≤ a) ⇒ (w ≤ (min a b + c)) of λ
     { (inl a≤b) → substₚ (λ p → w ≤ p + c) (symₚ (min-identity-≤ a b a≤b)) w≤a+c
     ; (inr b≤a) → substₚ (λ p → w ≤ p + c) (substₚ (λ p → b ≡ₚ p) (min-comm b a) (symₚ (min-identity-≤ b a b≤a))) w≤b+c
     }

    ≤-max-+ : ∀ a b c w → [ (a + c) ≤ w ] → [ (b + c) ≤ w ] → [ (max a b + c) ≤ w ]
    ≤-max-+ a b c w a+c≤w b+c≤w = case ≤-dicho a b as (a ≤ b) ⊔ (b ≤ a) ⇒ ((max a b + c) ≤ w) of λ
     { (inl a≤b) → substₚ (λ p → p + c ≤ w) (symₚ (max-identity-≤ a b a≤b)) b+c≤w
     ; (inr b≤a) → substₚ (λ p → p + c ≤ w) (substₚ (λ p → a ≡ₚ p) (max-comm b a) (symₚ (max-identity-≤ b a b≤a))) a+c≤w
     }

  module ≤-dicho⇒·
    (_·_ : A → A → A)
    (≤-dicho : ∀ x y → [ (x ≤ y) ⊔ (y ≤ x) ])
    where

    ≤-min-· : ∀ a b c w → [ w ≤ (a · c) ] → [ w ≤ (b · c) ] → [ w ≤ (min a b · c) ]
    ≤-min-· a b c w w≤a·c w≤b·c = case ≤-dicho a b as (a ≤ b) ⊔ (b ≤ a) ⇒ (w ≤ (min a b · c)) of λ
     { (inl a≤b) → substₚ (λ p → w ≤ p · c) (symₚ (min-identity-≤ a b a≤b)) w≤a·c
     ; (inr b≤a) → substₚ (λ p → w ≤ p · c) (substₚ (λ p → b ≡ₚ p) (min-comm b a) (symₚ (min-identity-≤ b a b≤a))) w≤b·c
     }

    ≤-max-· : ∀ a b c w → [ (a · c) ≤ w ] → [ (b · c) ≤ w ] → [ (max a b · c) ≤ w ]
    ≤-max-· a b c w a·c≤w b·c≤w = case ≤-dicho a b as (a ≤ b) ⊔ (b ≤ a) ⇒ ((max a b · c) ≤ w) of λ
     { (inl a≤b) → substₚ (λ p → p · c ≤ w) (symₚ (max-identity-≤ a b a≤b)) b·c≤w
     ; (inr b≤a) → substₚ (λ p → p · c ≤ w) (substₚ (λ p → a ≡ₚ p) (max-comm b a) (symₚ (max-identity-≤ b a b≤a))) a·c≤w
     }

  +-min-distribʳ' : (_+_ : A → A → A) (+-creates-≤ : ∀ a b x → [ (a ≤ b) ⇔ ((a + x) ≤ (b + x)) ])
                  → ∀ x y z w → [ (w ≤ (min x y + z)) ⇒ (w ≤ min (x + z) (y + z)) ]
  +-min-distribʳ' _+_ +-creates-≤ x y z w p = (
    ( min x y       ≤  x     ) ⊓ ( min x y      ≤  y     ) ⇒ᵖ⟨ (λ{ (q , r) → +-creates-≤ (min x y) x z .fst q , +-creates-≤ (min x y) y z .fst r}) ⟩
    ((min x y + z ) ≤ (x + z)) ⊓ ((min x y + z) ≤ (y + z)) ⇒ᵖ⟨ (λ{ (q , r) → ≤-trans _ _ _ p q , ≤-trans _ _ _ p r}) ⟩
    ( w             ≤ (x + z)) ⊓ ( w            ≤ (y + z)) ⇒ᵖ⟨ is-min (x + z) (y + z) w .snd ⟩
    ( w ≤ min (x + z) (y + z))                             ◼ᵖ) .snd (min-≤ x y)

  ·-min-distribʳ' : (0f : A) (_·_ : A → A → A) (·-creates-≤ : ∀ a b x → [ 0f ≤ x ] → [ (a ≤ b) ⇔ ((a · x) ≤ (b · x)) ])
                  → ∀ x y z w → [ 0f ≤ z ] → [ (w ≤ (min x y · z)) ⇒ (w ≤ min (x · z) (y · z)) ]
  ·-min-distribʳ' 0f _·_ ·-creates-≤ x y z w 0≤z p = (
    ( min x y      ≤  x     ) ⊓ ( min x y      ≤ y      ) ⇒ᵖ⟨ (λ{ (q , r) → ·-creates-≤ (min x y) x z 0≤z .fst q , ·-creates-≤ (min x y) y z 0≤z .fst r}) ⟩
    ((min x y · z) ≤ (x · z)) ⊓ ((min x y · z) ≤ (y · z)) ⇒ᵖ⟨ (λ{ (q , r) → ≤-trans _ _ _ p q , ≤-trans _ _ _ p r}) ⟩
    ( w            ≤ (x · z)) ⊓ ( w            ≤ (y · z)) ⇒ᵖ⟨ is-min (x · z) (y · z) w .snd ⟩
    ( w ≤ min (x · z) (y · z))                            ◼ᵖ) .snd (min-≤ x y)

  +-max-distribʳ' : (_+_ : A → A → A) (+-creates-≤ : ∀ a b x → [ (a ≤ b) ⇔ ((a + x) ≤ (b + x)) ])
                  → ∀ x y z w → [ ((max x y + z) ≤ w) ⇒ (max (x + z) (y + z) ≤ w) ]
  +-max-distribʳ' _+_ +-creates-≤ x y z w p = (
    ( x      ≤  max x y      ) ⊓ ( y      ≤  max x y     ) ⇒ᵖ⟨ (λ{ (q , r) → +-creates-≤ x (max x y) z .fst q , +-creates-≤ y (max x y) z .fst r}) ⟩
    ((x + z) ≤ (max x y + z )) ⊓ ((y + z) ≤ (max x y + z)) ⇒ᵖ⟨ (λ{ (q , r) → ≤-trans _ _ _ q p , ≤-trans _ _ _ r p}) ⟩
    ((x + z) ≤  w            ) ⊓ ((y + z) ≤  w           ) ⇒ᵖ⟨ is-max (x + z) (y + z) w .snd ⟩
    ( max (x + z) (y + z) ≤ w)                             ◼ᵖ) .snd (max-≤ x y)

  ·-max-distribʳ' : (0f : A) (_·_ : A → A → A) (·-creates-≤ : ∀ a b x → [ 0f ≤ x ] → [ (a ≤ b) ⇔ ((a · x) ≤ (b · x)) ])
                  → ∀ x y z w → [ 0f ≤ z ] → [ ((max x y · z) ≤ w) ⇒ (max (x · z) (y · z) ≤ w) ]
  ·-max-distribʳ' 0f _·_ ·-creates-≤ x y z w 0≤z p = (
    ( x      ≤  max x y     ) ⊓ (y       ≤  max x y     ) ⇒ᵖ⟨ (λ{ (q , r) → ·-creates-≤ x (max x y) z 0≤z .fst q , ·-creates-≤ y (max x y) z 0≤z .fst r}) ⟩
    ((x · z) ≤ (max x y · z)) ⊓ ((y · z) ≤ (max x y · z)) ⇒ᵖ⟨ (λ{ (q , r) → ≤-trans _ _ _ q p , ≤-trans _ _ _ r p}) ⟩
    ((x · z) ≤  w           ) ⊓ ((y · z) ≤  w           ) ⇒ᵖ⟨ is-max (x · z) (y · z) w .snd ⟩
    ( max (x · z) (y · z) ≤ w)                            ◼ᵖ) .snd (max-≤ x y)

  +-min-distribʳ : (_+_ : A → A → A)
                 → (+-creates-≤ : ∀ a b x → [ (a ≤ b) ⇔ ((a + x) ≤ (b + x)) ])
                 → (≤-min-+ : ∀ a b c w → [ w ≤ (a + c) ] → [ w ≤ (b + c) ] → [ w ≤ (min a b + c) ])
                 → ∀ x y z → [ (min x y + z) ≡ₚ min (x + z) (y + z) ]
  +-min-distribʳ _+_ +-creates-≤ ≤-min-+ x y z = ≤-reflectsʳ-≡ (min x y + z) (min (x + z) (y + z)) .fst γ where
    γ : ∀ w → [ (w ≤ (min x y + z)) ⇔ (w ≤ min (x + z) (y + z)) ]
    γ w .fst p = +-min-distribʳ' _+_ +-creates-≤ x y z w p
    γ w .snd p = let (w≤x+z , w≤y+z) = is-min (x + z) (y + z) w .fst p
                 in ≤-min-+ x y z w w≤x+z w≤y+z

  ·-min-distribʳ : (0f : A) (_·_ : A → A → A)
                 → (·-creates-≤ : ∀ a b x → [ 0f ≤ x ] → [ (a ≤ b) ⇔ ((a · x) ≤ (b · x)) ])
                 → (≤-min-· : ∀ a b c w → [ w ≤ (a · c) ] → [ w ≤ (b · c) ] → [ w ≤ (min a b · c) ])
                 → ∀ x y z → [ 0f ≤ z ] → [ (min x y · z) ≡ₚ min (x · z) (y · z) ]
  ·-min-distribʳ 0f _·_ ·-creates-≤ ≤-min-· x y z 0≤z = ≤-reflectsʳ-≡ (min x y · z) (min (x · z) (y · z)) .fst γ where
    γ : ∀ w → [ (w ≤ (min x y · z)) ⇔ (w ≤ min (x · z) (y · z)) ]
    γ w .fst p = ·-min-distribʳ' 0f _·_ ·-creates-≤ x y z w 0≤z p
    γ w .snd p = let (w≤x·z , w≤y·z) = is-min (x · z) (y · z) w .fst p
                 in ≤-min-· x y z w w≤x·z w≤y·z

  +-max-distribʳ : (_+_ : A → A → A)
                 → (+-creates-≤ : ∀ a b x → [ (a ≤ b) ⇔ ((a + x) ≤ (b + x)) ])
                 → (≤-max-+ : ∀ a b c w → [ (a + c) ≤ w ] → [ (b + c) ≤ w ] → [ (max a b + c) ≤ w ])
                 → ∀ x y z → [ (max x y + z) ≡ₚ max (x + z) (y + z) ]
  +-max-distribʳ _+_ +-creates-≤ ≤-max-+ x y z = ≤-reflectsˡ-≡ (max x y + z) (max (x + z) (y + z)) .fst γ where
    γ : ∀ w → [ ((max x y + z) ≤ w) ⇔ (max (x + z) (y + z) ≤ w) ]
    γ w .fst p = +-max-distribʳ' _+_ +-creates-≤ x y z w p
    γ w .snd p = let (w≤x+z , w≤y+z) = is-max (x + z) (y + z) w .fst p
                 in ≤-max-+ x y z w w≤x+z w≤y+z

  ·-max-distribʳ : (0f : A) (_·_ : A → A → A)
                 → (·-creates-≤ : ∀ a b x → [ 0f ≤ x ] → [ (a ≤ b) ⇔ ((a · x) ≤ (b · x)) ])
                 → (≤-max-· : ∀ a b c w → [ (a · c) ≤ w ] → [ (b · c) ≤ w ] → [ (max a b · c) ≤ w ])
                 → ∀ x y z → [ 0f ≤ z ] → [ (max x y · z) ≡ₚ max (x · z) (y · z) ]
  ·-max-distribʳ 0f _·_ ·-creates-≤ ≤-max-· x y z 0≤z = ≤-reflectsˡ-≡ (max x y · z) (max (x · z) (y · z)) .fst γ where
    γ : ∀ w → [ ((max x y · z) ≤ w) ⇔ (max (x · z) (y · z) ≤ w) ]
    γ w .fst p = ·-max-distribʳ' 0f _·_ ·-creates-≤ x y z w 0≤z p
    γ w .snd p = let (w≤x·z , w≤y·z) = is-max (x · z) (y · z) w .fst p
                 in ≤-max-· x y z w w≤x·z w≤y·z

-- -flips-min : ∀ x y → min (- x) (- y) ≡ - max x y
-- -flips-min x y = ?
--
-- -·-flips-min : ∀ x y z → [ z < 0 ] → min x y · z ≡ max (x · z) (y · z)
-- -·-flips-min x y z = ?

module OnSet (is-set : isSet A)
  (let _≡ˢ_ = λ(x y : A) → MoreLogic.Definitions.≡ˢ-syntax x y {is-set}
       infixl 4 _≡ˢ_
  ) where

  open OnType public using (min-≤; max-≤)
  module ≤-dicho⇒+ = OnType.≤-dicho⇒+
  module ≤-dicho⇒· = OnType.≤-dicho⇒·

  ≤-reflectsʳ-≡ : ∀ x y → [ (∀[ z ] z ≤ x ⇔ z ≤ y) ⇔ x ≡ˢ y ]
  ≤-reflectsʳ-≡ x y .fst p = ∣∣-elim (λ c → is-set x y) (λ x → x) (OnType.≤-reflectsʳ-≡ x y .fst p)
  ≤-reflectsʳ-≡ x y .snd p = OnType.≤-reflectsʳ-≡ x y .snd ∣ p ∣

  ≤-reflectsˡ-≡ : ∀ x y → [ (∀[ z ] x ≤ z ⇔ y ≤ z) ⇔ x ≡ˢ y ]
  ≤-reflectsˡ-≡ x y .fst p = ∣∣-elim (λ c → is-set x y) (λ x → x) (OnType.≤-reflectsˡ-≡ x y .fst p)
  ≤-reflectsˡ-≡ x y .snd p = OnType.≤-reflectsˡ-≡ x y .snd ∣ p ∣

  min-identity : ∀ x → [ min x x ≡ˢ x ]
  min-identity x = ∣∣-elim (λ c → is-set (min x x) x) (λ x → x) (OnType.min-identity x)

  min-identity-≤ : ∀ x y → [ x ≤ y ] → [ min x y ≡ˢ x ]
  min-identity-≤ x y p = ∣∣-elim (λ c → is-set (min x y) x) (λ x → x) (OnType.min-identity-≤ x y p)

  max-identity-≤ : ∀ x y → [ x ≤ y ] → [ max x y ≡ˢ y ]
  max-identity-≤ x y p = ∣∣-elim (λ c → is-set (max x y) y) (λ x → x) (OnType.max-identity-≤ x y p)

  min-comm : ∀ x y → [ min x y ≡ˢ min y x ]
  min-comm x y = ∣∣-elim (λ c → is-set (min x y) (min y x)) (λ x → x) (OnType.min-comm x y)

  min-assoc : ∀ x y z → [ min (min x y) z ≡ˢ min x (min y z) ]
  min-assoc x y z = ∣∣-elim (λ c → is-set (min (min x y) z) (min x (min y z))) (λ x → x) (OnType.min-assoc x y z)

  max-identity : ∀ x → [ max x x ≡ˢ x ]
  max-identity x = ∣∣-elim (λ c → is-set (max x x) x) (λ x → x) (OnType.max-identity x)

  max-comm : ∀ x y → [ max x y ≡ˢ max y x ]
  max-comm x y = ∣∣-elim (λ c → is-set (max x y) (max y x)) (λ x → x) (OnType.max-comm x y)

  max-assoc : ∀ x y z → [ max (max x y) z ≡ˢ max x (max y z) ]
  max-assoc x y z = ∣∣-elim (λ c → is-set (max (max x y) z) (max x (max y z))) (λ x → x) (OnType.max-assoc x y z)

  min-max-absorptive : ∀ x y → [ min x (max x y) ≡ˢ x ]
  min-max-absorptive x y = ∣∣-elim (λ c → is-set (min x (max x y)) x) (λ x → x) (OnType.min-max-absorptive x y)

  max-min-absorptive : ∀ x y → [ max x (min x y) ≡ˢ x ]
  max-min-absorptive x y = ∣∣-elim (λ c → is-set (max x (min x y)) x) (λ x → x) (OnType.max-min-absorptive x y)

  +-min-distribʳ : (_+_ : A → A → A)
                 → (+-creates-≤ : ∀ a b x → [ (a ≤ b) ⇔ ((a + x) ≤ (b + x)) ])
                 → (≤-min-+ : ∀ a b c w → [ w ≤ (a + c) ] → [ w ≤ (b + c) ] → [ w ≤ (min a b + c) ])
                 → ∀ x y z → [ (min x y + z) ≡ˢ min (x + z) (y + z) ]
  +-min-distribʳ _+_ +-creates-≤ ≤-min-+ x y z = ∣∣-elim (λ c → is-set (min x y + z) (min (x + z) (y + z))) (λ x → x) (OnType.+-min-distribʳ _+_ +-creates-≤ ≤-min-+ x y z)

  ·-min-distribʳ : (0f : A) (_·_ : A → A → A)
                 → (·-creates-≤ : ∀ a b x → [ 0f ≤ x ] → [ (a ≤ b) ⇔ ((a · x) ≤ (b · x)) ])
                 → (≤-min-· : ∀ a b c w → [ w ≤ (a · c) ] → [ w ≤ (b · c) ] → [ w ≤ (min a b · c) ])
                 → ∀ x y z → [ 0f ≤ z ] → [ (min x y · z) ≡ˢ min (x · z) (y · z) ]
  ·-min-distribʳ 0f _·_ ·-creates-≤ ≤-min-· x y z 0≤z = ∣∣-elim (λ c → is-set (min x y · z) (min (x · z) (y · z))) (λ x → x) (OnType.·-min-distribʳ 0f _·_ ·-creates-≤ ≤-min-· x y z 0≤z)

  +-max-distribʳ : (_+_ : A → A → A)
                 → (+-creates-≤ : ∀ a b x → [ (a ≤ b) ⇔ ((a + x) ≤ (b + x)) ])
                 → (≤-max-+ : ∀ a b c w → [ (a + c) ≤ w ] → [ (b + c) ≤ w ] → [ (max a b + c) ≤ w ])
                 → ∀ x y z → [ (max x y + z) ≡ˢ max (x + z) (y + z) ]
  +-max-distribʳ _+_ +-creates-≤ ≤-max-+ x y z = ∣∣-elim (λ c → is-set (max x y + z) (max (x + z) (y + z))) (λ x → x) (OnType.+-max-distribʳ _+_ +-creates-≤ ≤-max-+ x y z)

  ·-max-distribʳ : (0f : A) (_·_ : A → A → A)
                 → (·-creates-≤ : ∀ a b x → [ 0f ≤ x ] → [ (a ≤ b) ⇔ ((a · x) ≤ (b · x)) ])
                 → (≤-max-· : ∀ a b c w → [ (a · c) ≤ w ] → [ (b · c) ≤ w ] → [ (max a b · c) ≤ w ])
                 → ∀ x y z → [ 0f ≤ z ] → [ (max x y · z) ≡ˢ max (x · z) (y · z) ]
  ·-max-distribʳ 0f _·_ ·-creates-≤ ≤-max-· x y z 0≤z = ∣∣-elim (λ c → is-set (max x y · z) (max (x · z) (y · z))) (λ x → x) (OnType.·-max-distribʳ 0f _·_ ·-creates-≤ ≤-max-· x y z 0≤z)

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
-- Liang-Ting, 2022-01-14, issue #5734

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

open import Agda.Builtin.Unit
open import Agda.Builtin.List
open import Agda.Builtin.Sigma
open import Agda.Builtin.Reflection
  renaming (returnTC to return; bindTC to _>>=_)
open import Agda.Primitive

private variable
  A B : Set _

reverseApp : List A → List A → List A
reverseApp []       ys = ys
reverseApp (x ∷ xs) ys = reverseApp xs (x ∷ ys)

reverse : List A → List A
reverse xs = reverseApp xs []

extend*Context : Telescope → TC A → TC A
extend*Context []              m = m
extend*Context ((s , a) ∷ tel) m = extendContext s a (extend*Context tel m)

pattern vArg x = arg (arg-info visible (modality relevant quantity-ω)) x
pattern visible-relevant-erased = arg-info visible (modality relevant quantity-0)
pattern var₀ x = var x []

Γ : Telescope
Γ =   ("ℓ" , arg visible-relevant-erased (quoteTerm Level))
    ∷ ("A" , vArg (agda-sort (set (var₀ 0))))
    ∷ []

macro
  m : Term → TC ⊤
  m hole = do
    _ ← extend*Context Γ do
      _ ← checkType (var₀ 0) (agda-sort (set (var₀ 1)))
      return tt
    inContext (reverse Γ) do
      return tt

_ : ⊤
_ = m


text:
module _ where

open import Common.IO
  renaming (then to _>>_
           )
open import Agda.Builtin.Unit
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality using (_≡_; refl)
open import Agda.Builtin.Float
  renaming ( primFloatEquality       to _≡ᵇ_
           ; primFloatInequality     to _≤ᵇ_
           ; primFloatLess           to _<ᵇ_
           ; primFloatPlus           to infixl 6 _+_
           ; primFloatMinus          to infixl 6 _-_
           ; primFloatTimes          to infixl 7 _*_
           ; primFloatDiv            to infixl 7 _÷_
           ; primFloatPow            to infix  8 _**_
           ; primFloatNegate         to infix  9 -_
           ; primFloatSqrt           to sqrt
           ; primFloatExp            to e^_
           ; primFloatLog            to log
           ; primFloatSin            to sin
           ; primFloatCos            to cos
           ; primFloatTan            to tan
           ; primFloatASin           to asin
           ; primFloatACos           to acos
           ; primFloatATan           to atan
           ; primFloatATan2          to atan2
           ; primFloatSinh           to sinh
           ; primFloatCosh           to cosh
           ; primFloatTanh           to tanh
           ; primFloatASinh          to asinh
           ; primFloatACosh          to acosh
           ; primFloatATanh          to atanh
           ; primFloatRound          to round
           ; primFloatFloor          to floor
           ; primFloatCeiling        to ceiling
           ; primShowFloat           to showF
           ; primFloatToWord64       to toWord
           ; primFloatToRatio        to toRatio
           ; primRatioToFloat        to fromRatio
           ; primFloatDecode         to decode
           ; primFloatEncode         to encode
           ; primFloatIsInfinite     to isInfinite
           ; primFloatIsNaN          to isNaN
           ; primFloatIsNegativeZero to isNegativeZero
           ; primFloatIsSafeInteger  to isSafeInteger
           )
open import Agda.Builtin.Int
  using (Int; pos; negsuc)
  renaming ( primShowInteger         to showI
           )
open import Agda.Builtin.Nat
  using (Nat)
  renaming ( _==_                    to _==N_
           )
open import Agda.Builtin.Maybe
open import Agda.Builtin.Sigma
open import Agda.Builtin.String
  using (String)
  renaming ( primStringEquality      to _==S_
           ; primShowNat             to showN
           ; primStringAppend        to _++_
           )
open import Agda.Builtin.Word
  using (Word64)
  renaming ( primWord64ToNat         to toℕ
           )

-- Prelude

data ⊥ : Set where

_≢_ : {A : Set} (P Q : A) → Set
P ≢ Q = P ≡ Q → ⊥

NaN : Float
NaN = 0.0 ÷ 0.0

-NaN : Float
-NaN = - NaN

Infinity : Float
Infinity = 1.0 ÷ 0.0

-Infinity : Float
-Infinity = - Infinity

MaxFloat : Float
MaxFloat = 1.7976931348623157e308

MinFloat : Float
MinFloat = 2.2250738585072014e-308

MaxSafeIntF : Float
MaxSafeIntF = 9007199254740991.0

MaxSafeIntZ : Int
MaxSafeIntZ = pos 9007199254740991

-- * Tests

showB : Bool → String
showB false = "false"
showB true  = "true"

maybeShow : {A : Set} (show : A → String) → Maybe A → String
maybeShow show (just x) = "(just (" ++ (show x ++ "))")
maybeShow show nothing  = "nothing"

pairShow : {A B : Set} (showA : A → String) (showB : B → String) → Σ A (λ _ → B) → String
pairShow showA showB (x , y) = "(" ++ (showA x ++ (" , " ++ (showB y ++ ")")))

showR = pairShow showI showI

newline : IO ⊤
newline = putStr "\n"

T : Bool → Set
T false = ⊥
T true  = ⊤

_==F_ : Float → Float → Bool
x ==F y = toℕ (toWord x) ==N toℕ (toWord x)

_==B_ : Bool → Bool → Bool
false ==B false = true
false ==B true  = false
true  ==B false = false
true  ==B true  = true

_==I_ : Int → Int → Bool
pos    n ==I pos    m = n ==N m
pos    n ==I negsuc m = false
negsuc n ==I pos    m = false
negsuc n ==I negsuc m = n ==N m

maybeEq : {A : Set} (eq : A → A → Bool) → Maybe A → Maybe A → Bool
maybeEq eq (just x) (just y) = eq x y
maybeEq eq (just x) nothing  = false
maybeEq eq nothing  (just y) = false
maybeEq eq nothing  nothing  = true

pairEq : {A B : Set} (eqA : A → A → Bool) (eqB : B → B → Bool) → Σ A (λ _ → B) → Σ A (λ _ → B) → Bool
pairEq eqA eqB (x , y) (z , w) = eqA x z && eqB y w
  where
    _&&_ : Bool → Bool → Bool
    true && true = true
    x    && y    = false

_==R_  = pairEq _==I_ _==I_

check : {A : Set} (show : A → String) (eq : A → A → Bool) (str : String) (exp act : A) {p : T (eq act exp)} → IO ⊤
check show eq str exp act = do
  putStr str; putStr " = "; putStr (show exp); putStr " = "; putStr (show act); newline

checkB  = check showB _==B_
checkS  = check (λ x → x) _==S_
checkN  = check showN _==N_
checkI  = check showI _==I_
checkMI = check (maybeShow showI) (maybeEq _==I_)
checkR  = check showR _==R_
checkF  = check showF _==F_
checkMR = check (maybeShow showR) (maybeEq _==R_)
checkMF = check (maybeShow showF) (maybeEq _==F_)

-- ** Relations

main : IO ⊤
main = do
  -- ** Relations
  checkB " NaN      ≡ᵇ  NaN     " false ( NaN      ≡ᵇ  NaN     )
  checkB "-NaN      ≡ᵇ  NaN     " false (-NaN      ≡ᵇ  NaN     )
  checkB " NaN      ≡ᵇ -NaN     " false ( NaN      ≡ᵇ -NaN     )
  checkB "-NaN      ≡ᵇ -NaN     " false (-NaN      ≡ᵇ -NaN     )
  checkB " Infinity ≡ᵇ  Infinity" true  ( Infinity ≡ᵇ  Infinity)
  checkB "-Infinity ≡ᵇ  Infinity" false (-Infinity ≡ᵇ  Infinity)
  checkB " Infinity ≡ᵇ -Infinity" false ( Infinity ≡ᵇ -Infinity)
  checkB "-Infinity ≡ᵇ -Infinity" true  (-Infinity ≡ᵇ -Infinity)
  checkB " MaxFloat ≡ᵇ  MaxFloat" true  ( MaxFloat ≡ᵇ  MaxFloat)
  checkB " MinFloat ≡ᵇ  MinFloat" true  ( MinFloat ≡ᵇ  MinFloat)
  checkB " 1.0      ≡ᵇ  1.5     " false ( 1.0      ≡ᵇ  1.5     )
  checkB " 1.0      ≡ᵇ  1.0     " true  ( 1.0      ≡ᵇ  1.0     )
  checkB " 1.5      ≡ᵇ  1.5     " true  ( 1.5      ≡ᵇ  1.5     )

  checkB " NaN      ≤ᵇ  NaN     " false ( NaN      ≤ᵇ  NaN     )
  checkB "-NaN      ≤ᵇ  NaN     " false (-NaN      ≤ᵇ  NaN     )
  checkB " NaN      ≤ᵇ -NaN     " false ( NaN      ≤ᵇ -NaN     )
  checkB "-NaN      ≤ᵇ -NaN     " false (-NaN      ≤ᵇ -NaN     )
  checkB " NaN      ≤ᵇ  5.0     " false ( NaN      ≤ᵇ  5.0     )
  checkB "-NaN      ≤ᵇ  5.0     " false (-NaN      ≤ᵇ  5.0     )
  checkB " 5.0      ≤ᵇ -NaN     " false ( 5.0      ≤ᵇ -NaN     )
  checkB "-5.0      ≤ᵇ -NaN     " false (-5.0      ≤ᵇ -NaN     )
  checkB " NaN      ≤ᵇ  Infinity" false ( NaN      ≤ᵇ  Infinity)
  checkB "-NaN      ≤ᵇ  Infinity" false (-NaN      ≤ᵇ  Infinity)
  checkB " Infinity ≤ᵇ -NaN     " false ( Infinity ≤ᵇ -NaN     )
  checkB "-Infinity ≤ᵇ -NaN     " false (-Infinity ≤ᵇ -NaN     )
  checkB " Infinity ≤ᵇ  Infinity" true  ( Infinity ≤ᵇ  Infinity)
  checkB "-Infinity ≤ᵇ  Infinity" true  (-Infinity ≤ᵇ  Infinity)
  checkB " Infinity ≤ᵇ -Infinity" false ( Infinity ≤ᵇ -Infinity)
  checkB "-Infinity ≤ᵇ -Infinity" true  (-Infinity ≤ᵇ -Infinity)
  checkB " MaxFloat ≤ᵇ  MaxFloat" true  ( MaxFloat ≤ᵇ  MaxFloat)
  checkB " MinFloat ≤ᵇ  MinFloat" true  ( MinFloat ≤ᵇ  MinFloat)
  checkB " 1.0      ≤ᵇ  1.5     " true  ( 1.0      ≤ᵇ  1.5     )
  checkB " 1.0      ≤ᵇ  1.0     " true  ( 1.0      ≤ᵇ  1.0     )
  checkB " 1.5      ≤ᵇ  1.5     " true  ( 1.5      ≤ᵇ  1.5     )

  checkB " NaN      <ᵇ  NaN     " false ( NaN      <ᵇ  NaN     )
  checkB "-NaN      <ᵇ  NaN     " false (-NaN      <ᵇ  NaN     )
  checkB " NaN      <ᵇ -NaN     " false ( NaN      <ᵇ -NaN     )
  checkB "-NaN      <ᵇ -NaN     " false (-NaN      <ᵇ -NaN     )
  checkB " NaN      <ᵇ  5.0     " false ( NaN      <ᵇ  5.0     )
  checkB "-NaN      <ᵇ  5.0     " false (-NaN      <ᵇ  5.0     )
  checkB " 5.0      <ᵇ -NaN     " false ( 5.0      <ᵇ -NaN     )
  checkB "-5.0      <ᵇ -NaN     " false (-5.0      <ᵇ -NaN     )
  checkB " NaN      <ᵇ  Infinity" false ( NaN      <ᵇ  Infinity)
  checkB "-NaN      <ᵇ  Infinity" false (-NaN      <ᵇ  Infinity)
  checkB " Infinity <ᵇ -NaN     " false ( Infinity <ᵇ -NaN     )
  checkB "-Infinity <ᵇ -NaN     " false (-Infinity <ᵇ -NaN     )
  checkB " Infinity <ᵇ  Infinity" false ( Infinity <ᵇ  Infinity)
  checkB "-Infinity <ᵇ  Infinity" true  (-Infinity <ᵇ  Infinity)
  checkB " Infinity <ᵇ -Infinity" false ( Infinity <ᵇ -Infinity)
  checkB "-Infinity <ᵇ -Infinity" false (-Infinity <ᵇ -Infinity)
  checkB " MaxFloat <ᵇ  MaxFloat" false ( MaxFloat <ᵇ  MaxFloat)
  checkB " MinFloat <ᵇ  MinFloat" false ( MinFloat <ᵇ  MinFloat)
  checkB " 1.0      <ᵇ  1.5     " true  ( 1.0      <ᵇ  1.5     )
  checkB " 1.0      <ᵇ  1.0     " false ( 1.0      <ᵇ  1.0     )
  checkB " 1.5      <ᵇ  1.5     " false ( 1.5      <ᵇ  1.5     )

  checkB "isNaN  NaN                " true  (isNaN  NaN                )
  checkB "isNaN -NaN                " true  (isNaN -NaN                )
  checkB "isNaN  Infinity           " false (isNaN  Infinity           )
  checkB "isNaN -Infinity           " false (isNaN -Infinity           )
  checkB "isNaN  0.0                " false (isNaN  0.0                )
  checkB "isNaN -0.0                " false (isNaN -0.0                )
  checkB "isNaN  1.0                " false (isNaN  1.0                )
  checkB "isNaN  1.5                " false (isNaN  1.5                )
  checkB "isInfinite  NaN           " false (isInfinite  NaN           )
  checkB "isInfinite -NaN           " false (isInfinite -NaN           )
  checkB "isInfinite  Infinity      " true  (isInfinite  Infinity      )
  checkB "isInfinite -Infinity      " true  (isInfinite -Infinity      )
  checkB "isInfinite  0.0           " false (isInfinite  0.0           )
  checkB "isInfinite -0.0           " false (isInfinite -0.0           )
  checkB "isInfinite  1.0           " false (isInfinite  1.0           )
  checkB "isInfinite  1.5           " false (isInfinite  1.5           )

  -- Depends on optimisation settings:
  --
  --   - with -O0 the test succeeds
  --   - with -O  the test fails
  --
  -- checkB "isInfinite ((MaxFloat * MaxFloat) ÷ MaxFloat)"
  --        true
  --        (isInfinite ((MaxFloat * MaxFloat) ÷ MaxFloat))

  checkB "isNegativeZero  NaN       " false (isNegativeZero  NaN       )
  checkB "isNegativeZero -NaN       " false (isNegativeZero -NaN       )
  checkB "isNegativeZero  Infinity  " false (isNegativeZero  Infinity  )
  checkB "isNegativeZero -Infinity  " false (isNegativeZero -Infinity  )
  checkB "isNegativeZero  0.0       " false (isNegativeZero  0.0       )
  checkB "isNegativeZero -0.0       " true  (isNegativeZero -0.0       )
  checkB "isNegativeZero  1.0       " false (isNegativeZero  1.0       )
  checkB "isNegativeZero  1.5       " false (isNegativeZero  1.5       )
  checkB "isSafeInteger 1.0         " true  (isSafeInteger 1.0         )
  checkB "isSafeInteger 1.5         " false (isSafeInteger 1.5         )
  checkB "isSafeInteger MaxFloat    " false (isSafeInteger MaxFloat    )
  checkB "isSafeInteger MinFloat    " false (isSafeInteger MinFloat    )
  checkB "isSafeInteger MaxSafeIntF " true  (isSafeInteger MaxSafeIntF )

  -- ** Conversions

  checkS "show  NaN     " "NaN"       (showF  NaN     )
  checkS "show -NaN     " "NaN"       (showF -NaN     )
  checkS "show  0.0     " "0.0"       (showF  0.0     )
  checkS "show -0.0     " "-0.0"      (showF -0.0     )
  checkS "show  Infinity" "Infinity"  (showF  Infinity)
  checkS "show -Infinity" "-Infinity" (showF -Infinity)
  checkS "show  1.0     " "1.0"       (showF  1.0     )
  checkS "show  1.5     " "1.5"       (showF  1.5     )

  -- Breaks the JavaScript backend, on account of it being... too big:
  --
  -- checkN "toℕ (toWord 1.0)      " 4607182418800017408  (toℕ (toWord 1.0)      )
  -- checkN "toℕ (toWord 1.5)      " 4609434218613702656  (toℕ (toWord 1.5)      )
  -- checkN "toℕ (toWord 0.0)      " 0                    (toℕ (toWord 0.0)      )
  -- checkN "toℕ (toWord -0.0)     " 9223372036854775808  (toℕ (toWord -0.0)     )
  -- checkN "toℕ (toWord NaN)      " 18444492273895866368 (toℕ (toWord NaN)      )
  -- checkN "toℕ (toWord -NaN)     " 18444492273895866368 (toℕ (toWord -NaN)     )
  -- checkN "toℕ (toWord Infinity) " 9218868437227405312  (toℕ (toWord Infinity) )
  -- checkN "toℕ (toWord -Infinity)" 18442240474082181120 (toℕ (toWord -Infinity))

  checkMI "round 1.0      " (just (pos 1)) (round 1.0      )
  checkMI "round 1.5      " (just (pos 2)) (round 1.5      )
  checkMI "round NaN      " (nothing     ) (round NaN      )
  checkMI "round -NaN     " (nothing     ) (round -NaN     )
  checkMI "round Infinity " (nothing     ) (round Infinity )
  checkMI "round -Infinity" (nothing     ) (round -Infinity)
  checkMI "round MinFloat " (just (pos 0)) (round MinFloat )
  --
  -- Breaks the JavaScript backend, on account of it being... too big:
  --
  -- checkMI "round MaxFloat " (just (pos 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368)) (round MaxFloat )

  checkMI "floor 1.0      " (just (pos 1)) (floor 1.0      )
  checkMI "floor 1.5      " (just (pos 1)) (floor 1.5      )
  checkMI "floor NaN      " (nothing     ) (floor NaN      )
  checkMI "floor -NaN     " (nothing     ) (floor -NaN     )
  checkMI "floor Infinity " (nothing     ) (floor Infinity )
  checkMI "floor -Infinity" (nothing     ) (floor -Infinity)
  checkMI "floor MinFloat " (just (pos 0)) (floor MinFloat )
  --
  -- Breaks the JavaScript backend, on account of it being... too big:
  --
  -- checkMI "floor MaxFloat " (just (pos 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368)) (floor MaxFloat )

  checkMI "ceiling 1.0      " (just (pos 1)) (ceiling 1.0      )
  checkMI "ceiling 1.5      " (just (pos 2)) (ceiling 1.5      )
  checkMI "ceiling NaN      " (nothing     ) (ceiling NaN      )
  checkMI "ceiling -NaN     " (nothing     ) (ceiling -NaN     )
  checkMI "ceiling Infinity " (nothing     ) (ceiling Infinity )
  checkMI "ceiling -Infinity" (nothing     ) (ceiling -Infinity)
  checkMI "ceiling MinFloat " (just (pos 1)) (ceiling MinFloat )
  --
  -- Breaks the JavaScript backend, on account of it being... too big:
  --
  -- checkMI "ceiling MaxFloat " (just (pos 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368)) (ceiling MaxFloat )

  checkMR "decode  NaN     " (nothing                         ) (decode  NaN     )
  checkMR "decode  Infinity" (nothing                         ) (decode  Infinity)
  checkMR "decode -Infinity" (nothing                         ) (decode -Infinity)
  checkMR "decode  1.0     " (just (pos       1 , pos       0)) (decode  1.0     )
  checkMR "decode  1.5     " (just (pos       3 , negsuc    0)) (decode  1.5     )
  checkMR "decode  MinFloat" (just (pos       1 , negsuc 1021)) (decode  MinFloat)
  --
  -- Breaks the JavaScript backend, on account of it being... too big:
  --
  -- checkMR "decode  MaxFloat" (just (MaxSafeIntZ , pos     971)) (decode  MaxFloat)

  checkMF "encode  (pos     1) (pos       0)" (just 1.0        ) (encode  (pos     1) (pos       0))
  checkMF "encode  (pos     3) (negsuc    0)" (just 1.5        ) (encode  (pos     3) (negsuc    0))
  --
  -- Breaks the JavaScript backend, on account of it being... too big:
  --
  -- checkMF "encode  MaxSafeIntZ (pos       0)" (just MaxSafeIntF) (encode  MaxSafeIntZ (pos       0))
  -- checkMF "encode  MaxSafeIntZ (pos     971)" (just MaxFloat   ) (encode  MaxSafeIntZ (pos     971))
  -- checkMF "encode  MaxSafeIntZ (pos     972)" (nothing         ) (encode  MaxSafeIntZ (pos     972))
  -- checkMF "encode  (pos     1) (negsuc 1021)" (just MinFloat   ) (encode  (pos     1) (negsuc 1021))
  -- checkMF "encode  MaxSafeIntZ (negsuc 1075)" (nothing         ) (encode  MaxSafeIntZ (negsuc 1075))

  checkR "toRatio  NaN     " (pos 0    , pos 0) (toRatio  NaN     )
  checkR "toRatio  Infinity" (pos 1    , pos 0) (toRatio  Infinity)
  checkR "toRatio -Infinity" (negsuc 0 , pos 0) (toRatio -Infinity)
  checkR "toRatio  1.0     " (pos 1    , pos 1) (toRatio  1.0     )
  checkR "toRatio  1.5     " (pos 3    , pos 2) (toRatio  1.5     )

  checkF "fromRatio (pos 0)    (pos 0)" ( NaN     ) (fromRatio (pos 0)    (pos 0))
  checkF "fromRatio (pos 1)    (pos 0)" ( Infinity) (fromRatio (pos 1)    (pos 0))
  checkF "fromRatio (negsuc 0) (pos 0)" (-Infinity) (fromRatio (negsuc 0) (pos 0))
  checkF "fromRatio (pos 1)    (pos 1)" ( 1.0     ) (fromRatio (pos 1)    (pos 1))
  checkF "fromRatio (pos 3)    (pos 2)" ( 1.5     ) (fromRatio (pos 3)    (pos 2))

  checkF "e^ 1.0             " 2.718281828459045 (e^ 1.0             )
  checkF "sin (asin 0.6)     " 0.6               (sin (asin 0.6)     )
  checkF "cos (acos 0.6)     " 0.6               (cos (acos 0.6)     )
  checkF "tan (atan 0.4)     " 0.4               (tan (atan 0.4)     )
  checkF "tan (atan2 0.4 1.0)" 0.4               (tan (atan2 0.4 1.0))

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Prelude
open import core

module ground-decidable where
  ground-decidable : (τ : htyp) → (τ ground) + ((τ ground) → ⊥)
  ground-decidable b = Inl GBase
  ground-decidable ⦇-⦈ = Inr (λ ())
  ground-decidable (b ==> b) = Inr (λ ())
  ground-decidable (b ==> ⦇-⦈) = Inr (λ ())
  ground-decidable (b ==> τ' ==> τ'') = Inr (λ ())
  ground-decidable (⦇-⦈ ==> b) = Inr (λ ())
  ground-decidable (⦇-⦈ ==> ⦇-⦈) = Inl GHole
  ground-decidable (⦇-⦈ ==> τ' ==> τ'') = Inr (λ ())
  ground-decidable ((τ ==> τ₁) ==> b) = Inr (λ ())
  ground-decidable ((τ ==> τ₁) ==> ⦇-⦈) = Inr (λ ())
  ground-decidable ((τ ==> τ₁) ==> τ' ==> τ'') = Inr (λ ())

  ground-arr-lem : (τ : htyp) → ((τ ground) → ⊥) → (τ ≠  ⦇-⦈) → Σ[ τ1 ∈ htyp ] Σ[ τ2 ∈ htyp ] ((τ == (τ1 ==> τ2)) × ((τ1 ==> τ2) ≠ (⦇-⦈ ==> ⦇-⦈)))
  ground-arr-lem b ng nh = abort (ng GBase)
  ground-arr-lem ⦇-⦈ ng nh = abort (nh refl)
  ground-arr-lem (τ1 ==> τ2) ng nh = τ1 , τ2 , refl , (λ x → ng (lem' x))
    where
      lem' : ∀{τ1 τ2} → τ1 ==> τ2 == ⦇-⦈ ==> ⦇-⦈ → (τ1 ==> τ2) ground
      lem' refl = GHole

max_stars_repo_name: hazelgrove/hazelnut-dynamics-agda

max_issues_repo_name: hazelgrove/hazelnut-dynamics-agda

max_forks_repo_name: hazelgrove/hazelnut-dynamics-agda


text:
module ListsWithIrrelevantProofs where

data _≡_ {A : Set}(a : A) : A → Set where
  refl : a ≡ a

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

{-# BUILTIN NATURAL ℕ    #-}

postulate
  _≤_ : ℕ → ℕ → Set
  p1 : 0 ≤ 1
  p2 : 0 ≤ 1

-- descending lists indexed by upper bound for largest element

data SList (bound : ℕ) : Set where
  []    : SList bound
  scons : (head : ℕ) →
          .(head ≤ bound) →   -- irrelevant proof, dotted non-dependent domain
          (tail : SList head) →
          SList bound

l1 : SList 1
l1 = scons 0 p1 []

l2 : SList 1
l2 = scons 0 p2 []

-- proofs in list are irrelevant

l1≡l2 : l1 ≡ l2
l1≡l2 = refl

max_stars_repo_name: masondesu/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda