----------------------------------------------------------------------------------------------------
-- Some general properties for the development
----------------------------------------------------------------------------------------------------

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

module General-Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Data.Sigma
open import Cubical.Data.Nat
open import Cubical.Data.Empty as ⊥
open import Cubical.Relation.Nullary
open import Cubical.Relation.Binary
open BinaryRelation
open import Cubical.Induction.WellFounded
  renaming (WellFounded to isWellFounded)

open import Iff

{- A *truncated relation* is a set `A` and a relation `A → A → Set`
   that is valued in propositions. -}

isTruncatedRelation : {A : Set} -> (_<_ : A -> A -> Set) -> Set
isTruncatedRelation {A} _<_ = isSet A × isPropValued _<_

{- Extensionality -}

isExtensional : {A : Set} -> (_<_ : A -> A -> Set) -> Set
isExtensional {A} _<_ = (a b : A) → ((c : A) → (c < a ↔ c < b)) → a ≡ b

{- Law of excluded middle -}

LEM : Type₁
LEM = (P : Type) -> isProp P -> Dec P

LEM-¬∀-∃ : ∀ {A : Set} (P : A -> Set) -> LEM -> ¬ ((x : A) -> ¬ P x) -> ∃ A P
LEM-¬∀-∃ {A} P lem P-impossible with lem (∃ A P) ∥_∥.squash
... | yes p = p
... | no ¬a,p = ⊥.elim (P-impossible λ a → λ p → ¬a,p ∣ a , p ∣)

DNE : Type₁
DNE = (P : Type) → isProp P → ¬ (¬ P) → P

LEM-to-DNE : LEM → DNE
LEM-to-DNE lem P pP ¬¬p with (lem P pP)
... | yes p = p
... | no ¬p = ⊥.elim (¬¬p ¬p)

LEM-¬∀-∃¬ : ∀ {A : Type} (P : A → Type) → (∀ a → isProp (P a)) →
            LEM → ¬ (∀ x → P x) → ∃ A (\x → ¬ P x)
LEM-¬∀-∃¬ {A} P pvP lem f = LEM-¬∀-∃ _ lem g
 where
  g : ¬ (∀ x → ¬ (¬ P x))
  g h = f (λ x → LEM-to-DNE lem (P x) (pvP x) (h x))

{- Wellfoundedness implies that there is no infinite descending sequence. -}

no-infinite-descending-sequence : ∀ {A _<_} → isWellFounded _<_ →
                                  ¬ (Σ[ f ∈ (ℕ -> A) ] (∀ i → f (suc i) < f i))
no-infinite-descending-sequence {A} {_<_} wf (f , inf-desc) =
  WFI.induction wf {P = P} step (f ) (f , refl , inf-desc)
  where
    P : A -> Set
    P a = ¬ (Σ[ f ∈ (ℕ -> A) ] (f  ≡ a) × (∀ i → f (suc i) < f i))
    step : (x : A) → ((y : A) → y < x → P y) → P x
    step x q (f , f0≡x , inf-desc-f) =
      q (f ) (subst (f  <_) f0≡x (inf-desc-f ))
              (f ∘ suc , refl , λ i → inf-desc-f (suc i))

{- Wellfoundedness implies irreflexivity. -}

wellfounded→irreflexive : ∀ {A _<_} → isWellFounded _<_ → (x : A) → ¬ (x < x)
wellfounded→irreflexive is-wf x x<x = no-infinite-descending-sequence is-wf ((λ n → x) , λ n → x<x)