Skip to content

Commit 9bd3b43

Browse files
jamesmckinnaandreasabel
jamesmckinna
authored and
andreasabel
committed
[fixes #2130] Moving Properties.HeytingAlgebra from Relation.Binary to Relation.Binary.Lattice (#2131)
1 parent 2d45ecb commit 9bd3b43

File tree

3 files changed

+208
-187
lines changed

3 files changed

+208
-187
lines changed

‎CHANGELOG.md

+1
Original file line numberDiff line numberDiff line change
@@ -1253,6 +1253,7 @@ Deprecated modules
12531253
Relation.Binary.Properties.BoundedLattice.agda ↦ Relation.Binary.Lattice.Properties.BoundedLattice.agda
12541254
Relation.Binary.Properties.BoundedMeetSemilattice.agda ↦ Relation.Binary.Lattice.Properties.BoundedMeetSemilattice.agda
12551255
Relation.Binary.Properties.DistributiveLattice.agda ↦ Relation.Binary.Lattice.Properties.DistributiveLattice.agda
1256+
Relation.Binary.Properties.HeytingAlgebra.agda ↦ Relation.Binary.Lattice.Properties.HeytingAlgebra.agda
12561257
Relation.Binary.Properties.JoinSemilattice.agda ↦ Relation.Binary.Lattice.Properties.JoinSemilattice.agda
12571258
Relation.Binary.Properties.Lattice.agda ↦ Relation.Binary.Lattice.Properties.Lattice.agda
12581259
Relation.Binary.Properties.MeetSemilattice.agda ↦ Relation.Binary.Lattice.Properties.MeetSemilattice.agda

‎src/Relation/Binary/Lattice/Properties/HeytingAlgebra.agda

+199
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,199 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Properties satisfied by Heyting Algebra
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --cubical-compatible --safe #-}
8+
9+
open import Relation.Binary.Lattice
10+
11+
module Relation.Binary.Lattice.Properties.HeytingAlgebra
12+
{c ℓ₁ ℓ₂} (L : HeytingAlgebra c ℓ₁ ℓ₂) where
13+
14+
open HeytingAlgebra L
15+
16+
open import Algebra.Core
17+
open import Algebra.Definitions _≈_
18+
open import Data.Product.Base using (_,_)
19+
open import Function.Base using (_$_; flip; _∘_)
20+
open import Level using (_⊔_)
21+
open import Relation.Binary.Core using (_Preserves_⟶_; _Preserves₂_⟶_⟶_)
22+
import Relation.Binary.Reasoning.PartialOrder as POR
23+
open import Relation.Binary.Lattice.Properties.MeetSemilattice meetSemilattice
24+
open import Relation.Binary.Lattice.Properties.JoinSemilattice joinSemilattice
25+
import Relation.Binary.Lattice.Properties.BoundedMeetSemilattice boundedMeetSemilattice as BM
26+
open import Relation.Binary.Lattice.Properties.Lattice lattice
27+
open import Relation.Binary.Lattice.Properties.BoundedLattice boundedLattice
28+
import Relation.Binary.Reasoning.Setoid as EqReasoning
29+
30+
------------------------------------------------------------------------
31+
-- Useful lemmas
32+
33+
⇨-eval : ∀ {x y} → (x ⇨ y) ∧ x ≤ y
34+
⇨-eval {x} {y} = transpose-∧ refl
35+
36+
swap-transpose-⇨ : ∀ {x y w} → x ∧ w ≤ y → w ≤ x ⇨ y
37+
swap-transpose-⇨ x∧w≤y = transpose-⇨ $ trans (reflexive $ ∧-comm _ _) x∧w≤y
38+
39+
------------------------------------------------------------------------
40+
-- Properties of exponential
41+
42+
⇨-unit : ∀ {x} → x ⇨ x ≈ ⊤
43+
⇨-unit = antisym (maximum _) (transpose-⇨ $ reflexive $ BM.identityˡ _)
44+
45+
y≤x⇨y : ∀ {x y} → y ≤ x ⇨ y
46+
y≤x⇨y = transpose-⇨ (x∧y≤x _ _)
47+
48+
⇨-drop : ∀ {x y} → (x ⇨ y) ∧ y ≈ y
49+
⇨-drop = antisym (x∧y≤y _ _) (∧-greatest y≤x⇨y refl)
50+
51+
⇨-app : ∀ {x y} → (x ⇨ y) ∧ x ≈ y ∧ x
52+
⇨-app = antisym (∧-greatest ⇨-eval (x∧y≤y _ _)) (∧-monotonic y≤x⇨y refl)
53+
54+
⇨ʳ-covariant : ∀ {x} → (x ⇨_) Preserves _≤_ ⟶ _≤_
55+
⇨ʳ-covariant y≤z = transpose-⇨ (trans ⇨-eval y≤z)
56+
57+
⇨ˡ-contravariant : ∀ {x} → (_⇨ x) Preserves (flip _≤_) ⟶ _≤_
58+
⇨ˡ-contravariant z≤y = transpose-⇨ (trans (∧-monotonic refl z≤y) ⇨-eval)
59+
60+
⇨-relax : _⇨_ Preserves₂ (flip _≤_) ⟶ _≤_ ⟶ _≤_
61+
⇨-relax {x} {y} {u} {v} y≤x u≤v = begin
62+
x ⇨ u ≤⟨ ⇨ʳ-covariant u≤v ⟩
63+
x ⇨ v ≤⟨ ⇨ˡ-contravariant y≤x ⟩
64+
y ⇨ v ∎
65+
where open POR poset
66+
67+
⇨-cong : _⇨_ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_
68+
⇨-cong x≈y u≈v = antisym (⇨-relax (reflexive $ Eq.sym x≈y) (reflexive u≈v))
69+
(⇨-relax (reflexive x≈y) (reflexive $ Eq.sym u≈v))
70+
71+
⇨-applyˡ : ∀ {w x y} → w ≤ x → (x ⇨ y) ∧ w ≤ y
72+
⇨-applyˡ = transpose-∧ ∘ ⇨ˡ-contravariant
73+
74+
⇨-applyʳ : ∀ {w x y} → w ≤ x → w ∧ (x ⇨ y) ≤ y
75+
⇨-applyʳ w≤x = trans (reflexive (∧-comm _ _)) (⇨-applyˡ w≤x)
76+
77+
⇨-curry : ∀ {x y z} → x ∧ y ⇨ z ≈ x ⇨ y ⇨ z
78+
⇨-curry = antisym (transpose-⇨ $ transpose-⇨ $ trans (reflexive $ ∧-assoc _ _ _) ⇨-eval)
79+
(transpose-⇨ $ trans (reflexive $ Eq.sym $ ∧-assoc _ _ _)
80+
(transpose-∧ $ ⇨-applyˡ refl))
81+
82+
------------------------------------------------------------------------
83+
-- Various proofs of distributivity
84+
85+
∧-distribˡ-∨-≤ : ∀ x y z → x ∧ (y ∨ z) ≤ x ∧ y ∨ x ∧ z
86+
∧-distribˡ-∨-≤ x y z = trans (reflexive $ ∧-comm _ _)
87+
(transpose-∧ $ ∨-least (swap-transpose-⇨ (x≤x∨y _ _)) $ swap-transpose-⇨ (y≤x∨y _ _))
88+
89+
∧-distribˡ-∨-≥ : ∀ x y z → x ∧ y ∨ x ∧ z ≤ x ∧ (y ∨ z)
90+
∧-distribˡ-∨-≥ x y z = let
91+
x∧y≤x , x∧y≤y , _ = infimum x y
92+
x∧z≤x , x∧z≤z , _ = infimum x z
93+
y≤y∨z , z≤y∨z , _ = supremum y z
94+
in ∧-greatest (∨-least x∧y≤x x∧z≤x)
95+
(∨-least (trans x∧y≤y y≤y∨z) (trans x∧z≤z z≤y∨z))
96+
97+
∧-distribˡ-∨ : _∧_ DistributesOverˡ _∨_
98+
∧-distribˡ-∨ x y z = antisym (∧-distribˡ-∨-≤ x y z) (∧-distribˡ-∨-≥ x y z)
99+
100+
⇨-distribˡ-∧-≤ : ∀ x y z → x ⇨ y ∧ z ≤ (x ⇨ y) ∧ (x ⇨ z)
101+
⇨-distribˡ-∧-≤ x y z = let
102+
y∧z≤y , y∧z≤z , _ = infimum y z
103+
in ∧-greatest (transpose-⇨ $ trans ⇨-eval y∧z≤y)
104+
(transpose-⇨ $ trans ⇨-eval y∧z≤z)
105+
106+
⇨-distribˡ-∧-≥ : ∀ x y z → (x ⇨ y) ∧ (x ⇨ z) ≤ x ⇨ y ∧ z
107+
⇨-distribˡ-∧-≥ x y z = transpose-⇨ (begin
108+
(((x ⇨ y) ∧ (x ⇨ z)) ∧ x) ≈⟨ ∧-cong Eq.refl $ Eq.sym $ ∧-idempotent _ ⟩
109+
(((x ⇨ y) ∧ (x ⇨ z)) ∧ x ∧ x) ≈⟨ Eq.sym $ ∧-assoc _ _ _ ⟩
110+
(((x ⇨ y) ∧ (x ⇨ z)) ∧ x) ∧ x ≈⟨ ∧-cong (∧-assoc _ _ _) Eq.refl ⟩
111+
(((x ⇨ y) ∧ (x ⇨ z) ∧ x) ∧ x) ≈⟨ ∧-cong (∧-cong Eq.refl $ ∧-comm _ _) Eq.refl ⟩
112+
(((x ⇨ y) ∧ x ∧ (x ⇨ z)) ∧ x) ≈⟨ ∧-cong (Eq.sym $ ∧-assoc _ _ _) Eq.refl ⟩
113+
(((x ⇨ y) ∧ x) ∧ (x ⇨ z)) ∧ x ≈⟨ ∧-assoc _ _ _ ⟩
114+
(((x ⇨ y) ∧ x) ∧ (x ⇨ z) ∧ x) ≤⟨ ∧-monotonic ⇨-eval ⇨-eval ⟩
115+
y ∧ z ∎)
116+
where open POR poset
117+
118+
⇨-distribˡ-∧ : _⇨_ DistributesOverˡ _∧_
119+
⇨-distribˡ-∧ x y z = antisym (⇨-distribˡ-∧-≤ x y z) (⇨-distribˡ-∧-≥ x y z)
120+
121+
⇨-distribˡ-∨-∧-≤ : ∀ x y z → x ∨ y ⇨ z ≤ (x ⇨ z) ∧ (y ⇨ z)
122+
⇨-distribˡ-∨-∧-≤ x y z = let x≤x∨y , y≤x∨y , _ = supremum x y
123+
in ∧-greatest (transpose-⇨ $ trans (∧-monotonic refl x≤x∨y) ⇨-eval)
124+
(transpose-⇨ $ trans (∧-monotonic refl y≤x∨y) ⇨-eval)
125+
126+
⇨-distribˡ-∨-∧-≥ : ∀ x y z → (x ⇨ z) ∧ (y ⇨ z) ≤ x ∨ y ⇨ z
127+
⇨-distribˡ-∨-∧-≥ x y z = transpose-⇨ (trans (reflexive $ ∧-distribˡ-∨ _ _ _)
128+
(∨-least (trans (transpose-∧ (x∧y≤x _ _)) refl)
129+
(trans (transpose-∧ (x∧y≤y _ _)) refl)))
130+
131+
⇨-distribˡ-∨-∧ : ∀ x y z → x ∨ y ⇨ z ≈ (x ⇨ z) ∧ (y ⇨ z)
132+
⇨-distribˡ-∨-∧ x y z = antisym (⇨-distribˡ-∨-∧-≤ x y z) (⇨-distribˡ-∨-∧-≥ x y z)
133+
134+
------------------------------------------------------------------------
135+
-- Heyting algebras are distributive lattices
136+
137+
isDistributiveLattice : IsDistributiveLattice _≈_ _≤_ _∨_ _∧_
138+
isDistributiveLattice = record
139+
{ isLattice = isLattice
140+
; ∧-distribˡ-∨ = ∧-distribˡ-∨
141+
}
142+
143+
distributiveLattice : DistributiveLattice _ _ _
144+
distributiveLattice = record
145+
{ isDistributiveLattice = isDistributiveLattice
146+
}
147+
148+
------------------------------------------------------------------------
149+
-- Heyting algebras can define pseudo-complement
150+
151+
infix 8 ¬_
152+
153+
¬_ : Op₁ Carrier
154+
¬ x = x ⇨ ⊥
155+
156+
x≤¬¬x : ∀ x → x ≤ ¬ ¬ x
157+
x≤¬¬x x = transpose-⇨ (trans (reflexive (∧-comm _ _)) ⇨-eval)
158+
159+
------------------------------------------------------------------------
160+
-- De-Morgan laws
161+
162+
de-morgan₁ : ∀ x y → ¬ (x ∨ y) ≈ ¬ x ∧ ¬ y
163+
de-morgan₁ x y = ⇨-distribˡ-∨-∧ _ _ _
164+
165+
de-morgan₂-≤ : ∀ x y → ¬ (x ∧ y) ≤ ¬ ¬ (¬ x ∨ ¬ y)
166+
de-morgan₂-≤ x y = transpose-⇨ $ begin
167+
¬ (x ∧ y) ∧ ¬ (¬ x ∨ ¬ y) ≈⟨ ∧-cong ⇨-curry (de-morgan₁ _ _) ⟩
168+
(x ⇨ ¬ y) ∧ ¬ ¬ x ∧ ¬ ¬ y ≈⟨ ∧-cong Eq.refl (∧-comm _ _) ⟩
169+
(x ⇨ ¬ y) ∧ ¬ ¬ y ∧ ¬ ¬ x ≈⟨ Eq.sym $ ∧-assoc _ _ _ ⟩
170+
((x ⇨ ¬ y) ∧ ¬ ¬ y) ∧ ¬ ¬ x ≤⟨ ⇨-applyʳ $ transpose-⇨ $
171+
begin
172+
((x ⇨ ¬ y) ∧ ¬ ¬ y) ∧ x ≈⟨ ∧-cong (∧-comm _ _) Eq.refl ⟩
173+
((¬ ¬ y) ∧ (x ⇨ ¬ y)) ∧ x ≈⟨ ∧-assoc _ _ _ ⟩
174+
(¬ ¬ y) ∧ (x ⇨ ¬ y) ∧ x ≤⟨ ∧-monotonic refl ⇨-eval ⟩
175+
¬ ¬ y ∧ ¬ y ≤⟨ ⇨-eval ⟩
176+
⊥ ∎ ⟩
177+
⊥ ∎
178+
where open POR poset
179+
180+
de-morgan₂-≥ : ∀ x y → ¬ ¬ (¬ x ∨ ¬ y) ≤ ¬ (x ∧ y)
181+
de-morgan₂-≥ x y = transpose-⇨ $ ⇨-applyˡ $ transpose-⇨ $ begin
182+
(x ∧ y) ∧ (¬ x ∨ ¬ y) ≈⟨ ∧-distribˡ-∨ _ _ _ ⟩
183+
(x ∧ y) ∧ ¬ x ∨ (x ∧ y) ∧ ¬ y ≤⟨ ∨-monotonic (⇨-applyʳ (x∧y≤x _ _))
184+
(⇨-applyʳ (x∧y≤y _ _)) ⟩
185+
⊥ ∨ ⊥ ≈⟨ ∨-idempotent _ ⟩
186+
⊥ ∎
187+
where open POR poset
188+
189+
de-morgan₂ : ∀ x y → ¬ (x ∧ y) ≈ ¬ ¬ (¬ x ∨ ¬ y)
190+
de-morgan₂ x y = antisym (de-morgan₂-≤ x y) (de-morgan₂-≥ x y)
191+
192+
weak-lem : ∀ {x} → ¬ ¬ (¬ x ∨ x) ≈ ⊤
193+
weak-lem {x} = begin
194+
¬ ¬ (¬ x ∨ x) ≈⟨ ⇨-cong (de-morgan₁ _ _) Eq.refl ⟩
195+
¬ (¬ ¬ x ∧ ¬ x) ≈⟨ ⇨-cong ⇨-app Eq.refl ⟩
196+
⊥ ∧ (x ⇨ ⊥) ⇨ ⊥ ≈⟨ ⇨-cong (∧-zeroˡ _) Eq.refl ⟩
197+
⊥ ⇨ ⊥ ≈⟨ ⇨-unit ⟩
198+
⊤ ∎
199+
where open EqReasoning setoid

0 commit comments

Comments
 (0)