Qcert.Basic.Util.Lattice
Definition of a lattice, loosely based on ideas from
"A reflection-based proof tactic for lattices in Coq" and
http://www.pps.univ-paris-diderot.fr/~sozeau/repos/coq/order/
Definition part_le {A} {eqA} {R} `{part:PartialOrder A eqA R} : _ := R.
Infix "≤" := part_le (at level 70, no associativity).
Definition associative {A} eqA `{equivA : Equivalence A eqA} (op : A→A→ A)
:= ∀ x₁ x₂ x₃, equiv (op (op x₁ x₂) x₃) (op x₁ (op x₂ x₃)).
Definition commutative {A} eqA `{equivA : Equivalence A eqA} (op : A→A→A)
:= ∀ x₁ x₂, equiv (op x₁ x₂) (op x₂ x₁).
Definition idempotent {A} eqA `{equivA : Equivalence A eqA} (op : A→A→A)
:= ∀ x, equiv (op x x) x.
Definition absorptive {A} eqA `{equivA : Equivalence A eqA}
(op1 op2 : A→A→A)
:= ∀ x y, op1 x (op2 x y) === x.
Class Lattice (A:Type) (eqA:A→A→Prop) {equivA:Equivalence eqA}
:= {
meet : A → A → A;
join : A → A → A;
meet_morphism :> Proper (eqA ==> eqA ==> eqA) meet ;
join_morphism :> Proper (eqA ==> eqA ==> eqA) join ;
meet_commutative : commutative eqA meet;
meet_associative : associative eqA meet;
meet_idempotent : idempotent eqA meet;
join_commutative : commutative eqA join;
join_associative : associative eqA join;
join_idempotent : idempotent eqA join;
meet_absorptive : absorptive eqA meet join;
join_absorptive : absorptive eqA join meet
}.
Infix "⊓" := meet (at level 70). Infix "⊔" := join (at level 70).
Infix "≤" := part_le (at level 70, no associativity).
Definition associative {A} eqA `{equivA : Equivalence A eqA} (op : A→A→ A)
:= ∀ x₁ x₂ x₃, equiv (op (op x₁ x₂) x₃) (op x₁ (op x₂ x₃)).
Definition commutative {A} eqA `{equivA : Equivalence A eqA} (op : A→A→A)
:= ∀ x₁ x₂, equiv (op x₁ x₂) (op x₂ x₁).
Definition idempotent {A} eqA `{equivA : Equivalence A eqA} (op : A→A→A)
:= ∀ x, equiv (op x x) x.
Definition absorptive {A} eqA `{equivA : Equivalence A eqA}
(op1 op2 : A→A→A)
:= ∀ x y, op1 x (op2 x y) === x.
Class Lattice (A:Type) (eqA:A→A→Prop) {equivA:Equivalence eqA}
:= {
meet : A → A → A;
join : A → A → A;
meet_morphism :> Proper (eqA ==> eqA ==> eqA) meet ;
join_morphism :> Proper (eqA ==> eqA ==> eqA) join ;
meet_commutative : commutative eqA meet;
meet_associative : associative eqA meet;
meet_idempotent : idempotent eqA meet;
join_commutative : commutative eqA join;
join_associative : associative eqA join;
join_idempotent : idempotent eqA join;
meet_absorptive : absorptive eqA meet join;
join_absorptive : absorptive eqA join meet
}.
Infix "⊓" := meet (at level 70). Infix "⊔" := join (at level 70).
A lattice that is consistent with a specified partial order.
Class OLattice {A:Type}
(eqA:A→A→Prop)
(ordA:A→A→Prop)
{equivA:Equivalence eqA}
{lattice:Lattice A eqA}
{pre:PreOrder ordA}
{po:PartialOrder eqA ordA}
:= {
consistent_meet: ∀ a b, a ≤ b ↔ a ⊓ b === a
}.
Section props.
Context {A eqA ordA} `{olattice:OLattice A eqA ordA}.
Lemma consistent_join
: ∀ a b, a ≤ b ↔ a ⊔ b === b.
Lemma meet_leq_l a b: (a ⊓ b) ≤ a.
Lemma meet_leq_r a b: (a ⊓ b) ≤ b.
Theorem meet_most {a b c} : a ≤ b → a ≤ c → a ≤ (b ⊓ c).
Lemma join_leq_l a b: a ≤ (a ⊔ b).
Lemma join_leq_r a b: b ≤ (a ⊔ b).
Theorem join_least {a b c} : a ≤ c → b ≤ c → (a ⊔ b) ≤ c.
Global Instance meet_leq_proper :
Proper (part_le ==> part_le ==> part_le) meet.
Global Instance join_leq_proper :
Proper (part_le ==> part_le ==> part_le) join.
Lemma leq_dec_meet `{dec:EqDec A eqA} a b : {a ≤ b} + {¬ a ≤ b}.
Lemma leq_dec_join `{dec:EqDec A eqA} a b : {a ≤ b} + {¬ a ≤ b}.
End props.
End Lattice.
Infix "≤" := part_le (at level 70, no associativity).
Infix "⊓" := meet (at level 70). Infix "⊔" := join (at level 70).