{-# OPTIONS --without-K --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.Properties.MeetSemilattice meetSemilattice
open import Relation.Binary.Properties.JoinSemilattice joinSemilattice
import Relation.Binary.Properties.BoundedMeetSemilattice boundedMeetSemilattice as BM
open import Relation.Binary.Properties.Lattice lattice
open import Relation.Binary.Properties.BoundedLattice boundedLattice
import Relation.Binary.Reasoning.Setoid as EqReasoning
⇨-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
⇨-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))
∧-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)
isDistributiveLattice : IsDistributiveLattice _≈_ _≤_ _∨_ _∧_
isDistributiveLattice = record
{ isLattice = isLattice
; ∧-distribˡ-∨ = ∧-distribˡ-∨
}
distributiveLattice : DistributiveLattice _ _ _
distributiveLattice = record
{ isDistributiveLattice = isDistributiveLattice
}
infix 8 ¬_
¬_ : Op₁ Carrier
¬ x = x ⇨ ⊥
x≤¬¬x : ∀ x → x ≤ ¬ ¬ x
x≤¬¬x x = transpose-⇨ (trans (reflexive (∧-comm _ _)) ⇨-eval)
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