shttpd/coq/Lattice.v

(* Copyright © 2019 Ariadne Devos
   SPDX-License-Identifier: GPL-2.0 or GPL-3.0 *)

Require Import Coq.Classes.Equivalence.
Require Import Coq.Classes.Morphisms.
Require Import Coq.Relations.Relations.
Require Import Coq.Setoids.Setoid.

(* Proof further properties on an as-needed basis *)

Section lattice.

Variable A : Type.
Variable eqv : relation A.
Variable eqv_equiv : Equivalence eqv.

Section definition.
Variable join : A -> A -> A.
Variable meet : A -> A -> A.

Local Open Scope signature_scope.

Variable join_morphism : Proper (eqv ==> eqv ==> eqv) join.
Variable meet_morphism : Proper (eqv ==> eqv ==> eqv) meet.

Local Notation "a '≡' b" := (eqv (a : A) (b : A)) (at level 100).
Local Notation "a '∨' b" := (join (a : A) (b : A)) (at level 50).
Local Notation "a '∧' b" := (meet (a : A) (b : A)) (at level 50).

Record lattice_theory := {
  join_comm : forall x y, x ∨ y ≡ y ∨ x;
  join_assoc : forall x y z, x ∨ (y ∨ z) ≡ (x ∨ y) ∨ z;
  meet_comm : forall x y, x ∧ y ≡ y ∧ x;
  meet_assoc : forall x y z, x ∧ (y ∧ z) ≡ (x ∧ y) ∧ z;
  join_absorb : forall x y, x ∨ (x ∧ y) ≡ x;
  meet_absorb : forall x y, x ∧ (x ∨ y) ≡ x;
}.

Section laws.

Variable lattice : lattice_theory.

Theorem join_idempotent : forall x, x ∨ x ≡ x.
Proof.
  intros.
  (* Wikipedia note 1 (from Richard Dedekind):
    a ∨ a = a ∨ (a ∧ (a ∨ a)) = a *)
  rewrite <- (join_absorb lattice x (x ∨ x)).
  rewrite meet_absorb.
  + reflexivity.
  + assumption.
Qed.

Theorem meet_idempotent : forall x, x ∧ x ≡ x.
Proof.
  intros.
  (* Wikipedia note 1 (from Richard Dedekind):
    a ∨ a = a ∨ (a ∧ (a ∨ a)) = a *)
  rewrite <- (meet_absorb lattice x (x ∧ x)).
  rewrite join_absorb.
  + reflexivity.
  + assumption.
Qed.

End laws.
Section bounded.

Variable bottom : A.
Variable top : A.

Record bounded_lattice_theory := {
  lattice : lattice_theory;
  join_bottom : forall x, x ∨ bottom ≡ x;
  join_top : forall x, x ∨ top ≡ top;
  meet_bottom : forall x, x ∧ bottom ≡ bottom;
  meet_top : forall x, x ∧ top ≡ x;
}.

End bounded.
Section distributive.

Record distributive_theory := {
  join_meet_distr : forall x y z, (x ∧ y) ∨ (x ∧ z) ≡ x ∧ (y ∨ z);
  meet_join_distr : forall x y z, (x ∨ y) ∧ (x ∨ z) ≡ x ∨ (y ∧ z);
}.

End distributive.
End definition.
Section duality.
Variable join : A -> A -> A.
Variable meet : A -> A -> A.
Variable join_morphism : Proper (eqv ==> eqv ==> eqv) join.
Variable meet_morphism : Proper (eqv ==> eqv ==> eqv) meet.

Theorem lattice_dual : lattice_theory join meet -> lattice_theory meet join.
Proof. firstorder. Qed.

Theorem distributive_dual : distributive_theory join meet -> distributive_theory join meet.
Proof. firstorder. Qed.

End duality.
End lattice.