dan
/
HITs-Examples
mirror of https://github.com/nmvdw/HITs-Examples
1
0
Fork 0
Code Issues Releases Wiki Activity

Added join-semilattice

This commit is contained in:
Niels 2017-08-08 13:45:27 +02:00
parent c1dfef3cc1
commit de335c3955
2 changed files with 32 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
FiniteSets/fsets/properties.v
View File

@ -1,6 +1,7 @@
Require Import HoTT HitTactics.
From fsets Require Import operations extensionality.
Require Export representations.definition disjunction.
Require Import lattice.
(* Lemmas relating operations to the membership predicate *)
Section characterize_isIn.
@ -119,6 +120,14 @@ Section properties.
Context {A : Type}.
Context `{Univalence}.
Instance: bottom(FSet A) := ∅.
Instance: maximum(FSet A) := U.
Global Instance joinsemilattice_fset : JoinSemiLattice (FSet A).
Proof.
split ; toHProp.
Defined.
(** comprehension properties *)
Lemma comprehension_false Y : comprehension (fun (_ : A) => false) Y = ∅.
Proof.

23
FiniteSets/lattice.v
View File

@ -55,6 +55,29 @@ Arguments NeutralL {_} _ _.
Arguments NeutralR {_} _ _.
Arguments Absorption {_} _ _.
Section JoinSemiLattice.
Variable A : Type.
Context {max_L : maximum A} {empty_L : bottom A}.
Class JoinSemiLattice :=
{
commutative_max_js :> Commutative max_L ;
associative_max_js :> Associative max_L ;
idempotent_max_js :> Idempotent max_L ;
neutralL_max_js :> NeutralL max_L empty_L ;
neutralR_max_js :> NeutralR max_L empty_L ;
}.
End JoinSemiLattice.
Arguments JoinSemiLattice _ {_} {_}.
Create HintDb joinsemilattice_hints.
Hint Resolve associativity : joinsemilattice_hints.
Hint Resolve commutative : joinsemilattice_hints.
Hint Resolve idempotency : joinsemilattice_hints.
Hint Resolve neutralityL : joinsemilattice_hints.
Hint Resolve neutralityR : joinsemilattice_hints.
Section Lattice.
Variable A : Type.
Context {max_L : maximum A} {min_L : minimum A} {empty_L : bottom A}.