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

Shortened proofs

This commit is contained in:
Niels 2017-06-19 17:54:44 +02:00
parent 5f4c834cbe
commit 229df7b270
1 changed files with 18 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

29
FiniteSets/Lattice.v
View File

@ -136,6 +136,11 @@ End BoolLattice.
Require Import definition. Require Import definition.
Require Import properties. Require Import properties.
Hint Resolve
min_com max_com min_assoc max_assoc min_idem max_idem min_nl min_nr
bool_absorption_min_max bool_absorption_max_min
: bool_lattice_hints.
Section SetLattice. Section SetLattice.
Context {A : Type}. Context {A : Type}.
@ -155,57 +160,57 @@ Section SetLattice.
repeat (rewrite ?intersection_isIn ; repeat (rewrite ?intersection_isIn ;
rewrite ?union_isIn). rewrite ?union_isIn).
Ltac toBool := Ltac toBool := try (intro) ;
intros ; apply ext ; intros ; simplify_isIn. intros ; apply ext ; intros ; simplify_isIn ; eauto with bool_lattice_hints.
Instance union_com : Commutative (@U A). Instance union_com : Commutative (@U A).
Proof. Proof.
unfold Commutative ; toBool ; apply min_com. toBool.
Defined. Defined.
Instance intersection_com : Commutative intersection. Instance intersection_com : Commutative intersection.
Proof. Proof.
unfold Commutative ; toBool ; apply max_com. toBool.
Defined. Defined.
Instance union_assoc : Associative (@U A). Instance union_assoc : Associative (@U A).
Proof. Proof.
unfold Associative ; toBool ; apply min_assoc. toBool.
Defined. Defined.
Instance intersection_assoc : Associative intersection. Instance intersection_assoc : Associative intersection.
Proof. Proof.
unfold Associative ; toBool ; apply max_assoc. toBool.
Defined. Defined.
Instance union_idem : Idempotent (@U A). Instance union_idem : Idempotent (@U A).
Proof. Proof.
unfold Idempotent ; toBool ; apply min_idem. toBool.
Defined. Defined.
Instance intersection_idem : Idempotent intersection. Instance intersection_idem : Idempotent intersection.
Proof. Proof.
unfold Idempotent ; toBool ; apply max_idem. toBool.
Defined. Defined.
Instance union_nl : NeutralL (@U A) (@E A). Instance union_nl : NeutralL (@U A) (@E A).
Proof. Proof.
unfold NeutralL ; toBool ; apply min_nl. toBool.
Defined. Defined.
Instance union_nr : NeutralR (@U A) (@E A). Instance union_nr : NeutralR (@U A) (@E A).
Proof. Proof.
unfold NeutralR ; toBool ; apply min_nr. toBool.
Defined. Defined.
Instance set_absorption_intersection_union : Absorption (@U A) intersection. Instance set_absorption_intersection_union : Absorption (@U A) intersection.
Proof. Proof.
unfold Absorption ; toBool ; apply bool_absorption_min_max. toBool.
Defined. Defined.
Instance set_absorption_union_intersection : Absorption intersection (@U A). Instance set_absorption_union_intersection : Absorption intersection (@U A).
Proof. Proof.
unfold Absorption ; toBool ; apply bool_absorption_max_min. toBool.
Defined. Defined.
Instance lattice_set : Lattice (@U A) intersection (@E A) := Instance lattice_set : Lattice (@U A) intersection (@E A) :=