From 8abf6f86709fc79835302b6e8f04b614f78befd4 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 4 Jan 2025 17:27:38 -0800 Subject: [PATCH] Make 'isLattice' for simple types be an instance Signed-off-by: Danila Fedorin --- Lattice/Nat.agda | 74 ++++++++++++++++--------------- Lattice/Unit.agda | 110 +++++++++++++++++++++++----------------------- 2 files changed, 92 insertions(+), 92 deletions(-) diff --git a/Lattice/Nat.agda b/Lattice/Nat.agda index 64f1247..0fe5d29 100644 --- a/Lattice/Nat.agda +++ b/Lattice/Nat.agda @@ -18,31 +18,32 @@ private ≡-⊓-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≡ a₂ → a₃ ≡ a₄ → (a₁ ⊓ a₃) ≡ (a₂ ⊓ a₄) ≡-⊓-cong a₁≡a₂ a₃≡a₄ rewrite a₁≡a₂ rewrite a₃≡a₄ = refl -isMaxSemilattice : IsSemilattice ℕ _≡_ _⊔_ -isMaxSemilattice = record - { ≈-equiv = record - { ≈-refl = refl - ; ≈-sym = sym - ; ≈-trans = trans +instance + isMaxSemilattice : IsSemilattice ℕ _≡_ _⊔_ + isMaxSemilattice = record + { ≈-equiv = record + { ≈-refl = refl + ; ≈-sym = sym + ; ≈-trans = trans + } + ; ≈-⊔-cong = ≡-⊔-cong + ; ⊔-assoc = ⊔-assoc + ; ⊔-comm = ⊔-comm + ; ⊔-idemp = ⊔-idem } - ; ≈-⊔-cong = ≡-⊔-cong - ; ⊔-assoc = ⊔-assoc - ; ⊔-comm = ⊔-comm - ; ⊔-idemp = ⊔-idem - } -isMinSemilattice : IsSemilattice ℕ _≡_ _⊓_ -isMinSemilattice = record - { ≈-equiv = record - { ≈-refl = refl - ; ≈-sym = sym - ; ≈-trans = trans + isMinSemilattice : IsSemilattice ℕ _≡_ _⊓_ + isMinSemilattice = record + { ≈-equiv = record + { ≈-refl = refl + ; ≈-sym = sym + ; ≈-trans = trans + } + ; ≈-⊔-cong = ≡-⊓-cong + ; ⊔-assoc = ⊓-assoc + ; ⊔-comm = ⊓-comm + ; ⊔-idemp = ⊓-idem } - ; ≈-⊔-cong = ≡-⊓-cong - ; ⊔-assoc = ⊓-assoc - ; ⊔-comm = ⊓-comm - ; ⊔-idemp = ⊓-idem - } private max-bound₁ : {x y z : ℕ} → x ⊔ y ≡ z → x ≤ z @@ -74,18 +75,19 @@ private helper : x ⊔ (x ⊓ y) ≤ x ⊔ x → x ⊔ x ≡ x → x ⊔ (x ⊓ y) ≤ x helper x⊔x⊓y≤x⊔x x⊔x≡x rewrite x⊔x≡x = x⊔x⊓y≤x⊔x -isLattice : IsLattice ℕ _≡_ _⊔_ _⊓_ -isLattice = record - { joinSemilattice = isMaxSemilattice - ; meetSemilattice = isMinSemilattice - ; absorb-⊔-⊓ = λ x y → maxmin-absorb {x} {y} - ; absorb-⊓-⊔ = λ x y → minmax-absorb {x} {y} - } +instance + isLattice : IsLattice ℕ _≡_ _⊔_ _⊓_ + isLattice = record + { joinSemilattice = isMaxSemilattice + ; meetSemilattice = isMinSemilattice + ; absorb-⊔-⊓ = λ x y → maxmin-absorb {x} {y} + ; absorb-⊓-⊔ = λ x y → minmax-absorb {x} {y} + } -lattice : Lattice ℕ -lattice = record - { _≈_ = _≡_ - ; _⊔_ = _⊔_ - ; _⊓_ = _⊓_ - ; isLattice = isLattice - } + lattice : Lattice ℕ + lattice = record + { _≈_ = _≡_ + ; _⊔_ = _⊔_ + ; _⊓_ = _⊓_ + ; isLattice = isLattice + } diff --git a/Lattice/Unit.agda b/Lattice/Unit.agda index e4d0685..7889b3d 100644 --- a/Lattice/Unit.agda +++ b/Lattice/Unit.agda @@ -45,14 +45,15 @@ tt ⊓ tt = tt ⊔-idemp : (x : ⊤) → (x ⊔ x) ≈ x ⊔-idemp tt = Eq.refl -isJoinSemilattice : IsSemilattice ⊤ _≈_ _⊔_ -isJoinSemilattice = record - { ≈-equiv = ≈-equiv - ; ≈-⊔-cong = ≈-⊔-cong - ; ⊔-assoc = ⊔-assoc - ; ⊔-comm = ⊔-comm - ; ⊔-idemp = ⊔-idemp - } +instance + isJoinSemilattice : IsSemilattice ⊤ _≈_ _⊔_ + isJoinSemilattice = record + { ≈-equiv = ≈-equiv + ; ≈-⊔-cong = ≈-⊔-cong + ; ⊔-assoc = ⊔-assoc + ; ⊔-comm = ⊔-comm + ; ⊔-idemp = ⊔-idemp + } ≈-⊓-cong : ∀ {ab₁ ab₂ ab₃ ab₄} → ab₁ ≈ ab₂ → ab₃ ≈ ab₄ → (ab₁ ⊓ ab₃) ≈ (ab₂ ⊓ ab₄) ≈-⊓-cong {tt} {tt} {tt} {tt} _ _ = Eq.refl @@ -66,36 +67,32 @@ isJoinSemilattice = record ⊓-idemp : (x : ⊤) → (x ⊓ x) ≈ x ⊓-idemp tt = Eq.refl -isMeetSemilattice : IsSemilattice ⊤ _≈_ _⊓_ -isMeetSemilattice = record - { ≈-equiv = ≈-equiv - ; ≈-⊔-cong = ≈-⊓-cong - ; ⊔-assoc = ⊓-assoc - ; ⊔-comm = ⊓-comm - ; ⊔-idemp = ⊓-idemp - } +instance + isMeetSemilattice : IsSemilattice ⊤ _≈_ _⊓_ + isMeetSemilattice = record + { ≈-equiv = ≈-equiv + ; ≈-⊔-cong = ≈-⊓-cong + ; ⊔-assoc = ⊓-assoc + ; ⊔-comm = ⊓-comm + ; ⊔-idemp = ⊓-idemp + } -absorb-⊔-⊓ : (x y : ⊤) → (x ⊔ (x ⊓ y)) ≈ x -absorb-⊔-⊓ tt tt = Eq.refl +instance + isLattice : IsLattice ⊤ _≈_ _⊔_ _⊓_ + isLattice = record + { joinSemilattice = isJoinSemilattice + ; meetSemilattice = isMeetSemilattice + ; absorb-⊔-⊓ = λ { tt tt → Eq.refl } + ; absorb-⊓-⊔ = λ { tt tt → Eq.refl } + } -absorb-⊓-⊔ : (x y : ⊤) → (x ⊓ (x ⊔ y)) ≈ x -absorb-⊓-⊔ tt tt = Eq.refl - -isLattice : IsLattice ⊤ _≈_ _⊔_ _⊓_ -isLattice = record - { joinSemilattice = isJoinSemilattice - ; meetSemilattice = isMeetSemilattice - ; absorb-⊔-⊓ = absorb-⊔-⊓ - ; absorb-⊓-⊔ = absorb-⊓-⊔ - } - -lattice : Lattice ⊤ -lattice = record - { _≈_ = _≈_ - ; _⊔_ = _⊔_ - ; _⊓_ = _⊓_ - ; isLattice = isLattice - } + lattice : Lattice ⊤ + lattice = record + { _≈_ = _≈_ + ; _⊔_ = _⊔_ + ; _⊓_ = _⊓_ + ; isLattice = isLattice + } open Chain _≈_ ≈-equiv (IsLattice._≺_ isLattice) (IsLattice.≺-cong isLattice) @@ -107,25 +104,26 @@ private isLongest {tt} {tt} (step (tt⊔tt≈tt , tt̷≈tt) _ _) = ⊥-elim (tt̷≈tt refl) isLongest (done _) = z≤n -fixedHeight : IsLattice.FixedHeight isLattice 0 -fixedHeight = record - { ⊥ = tt - ; ⊤ = tt - ; longestChain = longestChain - ; bounded = isLongest - } +instance + fixedHeight : IsLattice.FixedHeight isLattice 0 + fixedHeight = record + { ⊥ = tt + ; ⊤ = tt + ; longestChain = longestChain + ; bounded = isLongest + } -isFiniteHeightLattice : IsFiniteHeightLattice ⊤ 0 _≈_ _⊔_ _⊓_ -isFiniteHeightLattice = record - { isLattice = isLattice - ; fixedHeight = fixedHeight - } + isFiniteHeightLattice : IsFiniteHeightLattice ⊤ 0 _≈_ _⊔_ _⊓_ + isFiniteHeightLattice = record + { isLattice = isLattice + ; fixedHeight = fixedHeight + } -finiteHeightLattice : FiniteHeightLattice ⊤ -finiteHeightLattice = record - { height = 0 - ; _≈_ = _≈_ - ; _⊔_ = _⊔_ - ; _⊓_ = _⊓_ - ; isFiniteHeightLattice = isFiniteHeightLattice - } + finiteHeightLattice : FiniteHeightLattice ⊤ + finiteHeightLattice = record + { height = 0 + ; _≈_ = _≈_ + ; _⊔_ = _⊔_ + ; _⊓_ = _⊓_ + ; isFiniteHeightLattice = isFiniteHeightLattice + }