------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties satisfied by Heyting Algebra
------------------------------------------------------------------------

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

open import Relation.Binary.Lattice

module Relation.Binary.Properties.HeytingAlgebra
{c ℓ₁ ℓ₂} (L : HeytingAlgebra c ℓ₁ ℓ₂) where

open HeytingAlgebra L

open import Algebra.Core
open import Algebra.Definitions _≈_
open import Data.Product using (_,_)
open import Function.Base using (_\$_; flip; _∘_)
open import Level using (_⊔_)
open import Relation.Binary
import Relation.Binary.Reasoning.PartialOrder as POR
open import Relation.Binary.Lattice.Properties.MeetSemilattice meetSemilattice
open import Relation.Binary.Lattice.Properties.JoinSemilattice joinSemilattice
import Relation.Binary.Lattice.Properties.BoundedMeetSemilattice boundedMeetSemilattice as BM
open import Relation.Binary.Lattice.Properties.Lattice lattice
open import Relation.Binary.Lattice.Properties.BoundedLattice boundedLattice
import Relation.Binary.Reasoning.Setoid as EqReasoning

------------------------------------------------------------------------
-- Useful lemmas

⇨-eval :  {x y}  (x  y)  x  y
⇨-eval {x} {y} = transpose-∧ refl

swap-transpose-⇨ :  {x y w}  x  w  y  w  x  y
swap-transpose-⇨ x∧w≤y = transpose-⇨ \$ trans (reflexive \$ ∧-comm _ _) x∧w≤y

------------------------------------------------------------------------
-- Properties of exponential

⇨-unit :  {x}  x  x
⇨-unit = antisym (maximum _) (transpose-⇨ \$ reflexive \$ BM.identityˡ _)

y≤x⇨y :  {x y}  y  x  y
y≤x⇨y = transpose-⇨ (x∧y≤x _ _)

⇨-drop :  {x y}  (x  y)  y  y
⇨-drop = antisym (x∧y≤y _ _) (∧-greatest y≤x⇨y refl)

⇨-app :  {x y}  (x  y)  x  y  x
⇨-app = antisym (∧-greatest ⇨-eval (x∧y≤y _ _)) (∧-monotonic y≤x⇨y refl)

⇨ʳ-covariant :  {x}  (x ⇨_) Preserves _≤_  _≤_
⇨ʳ-covariant y≤z = transpose-⇨ (trans ⇨-eval y≤z)

⇨ˡ-contravariant :  {x}  (_⇨ x) Preserves (flip _≤_)  _≤_
⇨ˡ-contravariant z≤y = transpose-⇨ (trans (∧-monotonic refl z≤y) ⇨-eval)

⇨-relax : _⇨_ Preserves₂ (flip _≤_)  _≤_  _≤_
⇨-relax {x} {y} {u} {v} y≤x u≤v = begin
x  u ≤⟨ ⇨ʳ-covariant u≤v
x  v ≤⟨ ⇨ˡ-contravariant y≤x
y  v
where open POR poset

⇨-cong : _⇨_ Preserves₂ _≈_  _≈_  _≈_
⇨-cong x≈y u≈v = antisym (⇨-relax (reflexive \$ Eq.sym x≈y) (reflexive u≈v))
(⇨-relax (reflexive x≈y) (reflexive \$ Eq.sym u≈v))

⇨-applyˡ :  {w x y}  w  x  (x  y)  w  y
⇨-applyˡ = transpose-∧  ⇨ˡ-contravariant

⇨-applyʳ :  {w x y}  w  x  w  (x  y)  y
⇨-applyʳ w≤x = trans (reflexive (∧-comm _ _)) (⇨-applyˡ w≤x)

⇨-curry :  {x y z}  x  y  z  x  y  z
⇨-curry = antisym (transpose-⇨ \$ transpose-⇨ \$ trans (reflexive \$ ∧-assoc _ _ _) ⇨-eval)
(transpose-⇨ \$ trans (reflexive \$ Eq.sym \$ ∧-assoc _ _ _)
(transpose-∧ \$ ⇨-applyˡ refl))

------------------------------------------------------------------------
-- Various proofs of distributivity

∧-distribˡ-∨-≤ :  x y z  x  (y  z)  x  y  x  z
∧-distribˡ-∨-≤ x y z = trans (reflexive \$ ∧-comm _ _)
(transpose-∧ \$ ∨-least (swap-transpose-⇨ (x≤x∨y _ _)) \$ swap-transpose-⇨ (y≤x∨y _ _))

∧-distribˡ-∨-≥ :  x y z  x  y  x  z  x  (y  z)
∧-distribˡ-∨-≥ x y z = let
x∧y≤x , x∧y≤y , _ = infimum x y
x∧z≤x , x∧z≤z , _ = infimum x z
y≤y∨z , z≤y∨z , _ = supremum y z
in ∧-greatest (∨-least x∧y≤x x∧z≤x)
(∨-least (trans x∧y≤y y≤y∨z) (trans x∧z≤z z≤y∨z))

∧-distribˡ-∨ : _∧_ DistributesOverˡ _∨_
∧-distribˡ-∨ x y z = antisym (∧-distribˡ-∨-≤ x y z) (∧-distribˡ-∨-≥ x y z)

⇨-distribˡ-∧-≤ :  x y z  x  y  z  (x  y)  (x  z)
⇨-distribˡ-∧-≤ x y z = let
y∧z≤y , y∧z≤z , _ = infimum y z
in ∧-greatest (transpose-⇨ \$ trans ⇨-eval y∧z≤y)
(transpose-⇨ \$ trans ⇨-eval y∧z≤z)

⇨-distribˡ-∧-≥ :  x y z  (x  y)  (x  z)  x  y  z
⇨-distribˡ-∧-≥ x y z = transpose-⇨ (begin
(((x  y)  (x  z))  x)      ≈⟨ ∧-cong Eq.refl \$ Eq.sym \$ ∧-idempotent _
(((x  y)  (x  z))  x   x) ≈⟨ Eq.sym \$ ∧-assoc _ _ _
(((x  y)  (x  z))  x)  x  ≈⟨ ∧-cong (∧-assoc _ _ _) Eq.refl
(((x  y)  (x  z)   x)  x) ≈⟨ ∧-cong (∧-cong Eq.refl \$ ∧-comm _ _) Eq.refl
(((x  y)  x   (x  z))  x) ≈⟨ ∧-cong (Eq.sym \$ ∧-assoc _ _ _) Eq.refl
(((x  y)  x)  (x  z))  x  ≈⟨ ∧-assoc _ _ _
(((x  y)  x)  (x  z)   x) ≤⟨ ∧-monotonic ⇨-eval ⇨-eval
y  z                          )
where open POR poset

⇨-distribˡ-∧ : _⇨_ DistributesOverˡ _∧_
⇨-distribˡ-∧ x y z = antisym (⇨-distribˡ-∧-≤ x y z) (⇨-distribˡ-∧-≥ x y z)

⇨-distribˡ-∨-∧-≤ :  x y z  x  y  z  (x  z)  (y  z)
⇨-distribˡ-∨-∧-≤ x y z = let x≤x∨y , y≤x∨y , _ = supremum x y
in ∧-greatest (transpose-⇨ \$ trans (∧-monotonic refl x≤x∨y) ⇨-eval)
(transpose-⇨ \$ trans (∧-monotonic refl y≤x∨y) ⇨-eval)

⇨-distribˡ-∨-∧-≥ :  x y z  (x  z)  (y  z)  x  y  z
⇨-distribˡ-∨-∧-≥ x y z = transpose-⇨ (trans (reflexive \$ ∧-distribˡ-∨ _ _ _)
(∨-least (trans (transpose-∧ (x∧y≤x _ _)) refl)
(trans (transpose-∧ (x∧y≤y _ _)) refl)))

⇨-distribˡ-∨-∧ :  x y z  x  y  z  (x  z)  (y  z)
⇨-distribˡ-∨-∧ x y z = antisym (⇨-distribˡ-∨-∧-≤ x y z) (⇨-distribˡ-∨-∧-≥ x y z)

------------------------------------------------------------------------
-- Heyting algebras are distributive lattices

isDistributiveLattice : IsDistributiveLattice _≈_ _≤_ _∨_ _∧_
isDistributiveLattice = record
{ isLattice    = isLattice
; ∧-distribˡ-∨ = ∧-distribˡ-∨
}

distributiveLattice : DistributiveLattice _ _ _
distributiveLattice = record
{ isDistributiveLattice = isDistributiveLattice
}

------------------------------------------------------------------------
-- Heyting algebras can define pseudo-complement

infix 8 ¬_

¬_ : Op₁ Carrier
¬ x = x

x≤¬¬x :  x  x  ¬ ¬ x
x≤¬¬x x = transpose-⇨ (trans (reflexive (∧-comm _ _)) ⇨-eval)

------------------------------------------------------------------------
-- De-Morgan laws

de-morgan₁ :  x y  ¬ (x  y)  ¬ x  ¬ y
de-morgan₁ x y = ⇨-distribˡ-∨-∧ _ _ _

de-morgan₂-≤ :  x y  ¬ (x  y)  ¬ ¬ (¬ x  ¬ y)
de-morgan₂-≤ x y = transpose-⇨ \$ begin
¬ (x  y)  ¬ (¬ x  ¬ y)     ≈⟨ ∧-cong ⇨-curry (de-morgan₁ _ _)
(x  ¬ y)  ¬ ¬ x  ¬ ¬ y     ≈⟨ ∧-cong Eq.refl (∧-comm _ _)
(x  ¬ y)  ¬ ¬ y  ¬ ¬ x     ≈⟨ Eq.sym \$ ∧-assoc _ _ _
((x  ¬ y)  ¬ ¬ y)  ¬ ¬ x   ≤⟨ ⇨-applyʳ \$ transpose-⇨ \$
begin
((x  ¬ y)  ¬ ¬ y)  x   ≈⟨ ∧-cong (∧-comm _ _) Eq.refl
((¬ ¬ y)  (x  ¬ y))  x ≈⟨ ∧-assoc _ _ _
(¬ ¬ y)  (x  ¬ y)  x   ≤⟨ ∧-monotonic refl ⇨-eval
¬ ¬ y  ¬ y               ≤⟨ ⇨-eval

where open POR poset

de-morgan₂-≥ :  x y  ¬ ¬ (¬ x  ¬ y)  ¬ (x  y)
de-morgan₂-≥ x y = transpose-⇨ \$ ⇨-applyˡ \$ transpose-⇨ \$ begin
(x  y)  (¬ x  ¬ y)         ≈⟨ ∧-distribˡ-∨ _ _ _
(x  y)  ¬ x  (x  y)  ¬ y ≤⟨ ∨-monotonic (⇨-applyʳ (x∧y≤x _ _))
(⇨-applyʳ (x∧y≤y _ _))
≈⟨ ∨-idempotent _

where open POR poset

de-morgan₂ :  x y  ¬ (x  y)  ¬ ¬ (¬ x  ¬ y)
de-morgan₂ x y = antisym (de-morgan₂-≤ x y) (de-morgan₂-≥ x y)

weak-lem :  {x}  ¬ ¬ (¬ x  x)
weak-lem {x} = begin
¬ ¬ (¬ x  x)   ≈⟨ ⇨-cong (de-morgan₁ _ _) Eq.refl
¬ (¬ ¬ x  ¬ x) ≈⟨ ⇨-cong ⇨-app Eq.refl
(x  )   ≈⟨ ⇨-cong (∧-zeroˡ _) Eq.refl
≈⟨ ⇨-unit

where open EqReasoning setoid