Library BoolLat
Require Import Lattice.
Inductive bool_order : bool -> bool -> Prop :=
| true_order : forall x : bool, bool_order x true
| false_order : forall x : bool, bool_order false x.
Definition join_bool (x y : bool) : bool :=
match x, y with
| true, _ => true
| _, true => true
| _, _ => false
end.
Definition inter_bool (x y : bool) : bool :=
match x, y with
| false, _ => false
| _, false => false
| _, _ => true
end.
Module BoolPoset <: Poset.
Definition set:=bool.
Definition eq:=(fun (x y:bool) => x = y).
Definition order:=bool_order.
Lemma eq_refl : forall x : set, eq x x.
unfold eq; auto.
Qed.
Lemma eq_sym : forall x y : set, eq x y -> eq y x.
unfold eq; auto.
Qed.
Lemma eq_trans : forall x y z : set, eq x y -> eq y z -> eq x z.
intros x y z H; rewrite H; auto.
Qed.
Lemma order_refl : forall x y : set, eq x y -> order x y.
intros x y H; rewrite H; case y; constructor.
Qed.
Lemma order_antisym : forall x y : set, order x y -> order y x -> eq x y.
unfold eq, order; simple destruct x; simple destruct y; intros H H1;
(inversion H; fail) || (inversion H1; fail) || auto.
Qed.
Lemma order_trans : forall x y z : set, order x y -> order y z -> order x z.
unfold eq, order; simple destruct x; simple destruct y; intros H H1;
(inversion H; fail) || (inversion H1; fail) || (try constructor; auto).
Qed.
End BoolPoset.
Module BoolLattice <: Lattice.
Module Pos:=BoolPoset.
Export Pos.
Definition inter := inter_bool.
Lemma inter_bound1 : forall x y : set, order (inter x y) x.
simple destruct x; simple destruct y; simpl in |- *; constructor.
Qed.
Lemma inter_bound2 : forall x y : set, order (inter x y) y.
simple destruct x; simple destruct y; simpl in |- *; constructor.
Qed.
Lemma inter_greater_bound : forall x y z : set, order z x -> order z y -> order z (inter x y).
simple destruct x; simple destruct y; simple destruct z; simpl in |- *;
intros H1 H2;
(inversion H1; fail) || (inversion H2; fail) || (constructor; auto).
Qed.
Definition join := join_bool.
Definition bottom := false.
Definition top := true.
Lemma join_bound1 : forall x y : set, order x (join x y).
simple destruct x; simple destruct y; simpl in |- *; constructor.
Qed.
Lemma join_bound2 : forall x y : set, order y (join x y).
simple destruct x; simple destruct y; simpl in |- *; constructor.
Qed.
Lemma join_least_bound : forall x y z : set, order x z -> order y z -> order (join x y) z.
simple destruct x; simple destruct y; simple destruct z; simpl in |- *;
intros H1 H2;
(inversion H1; fail) || (inversion H2; fail) || (constructor; auto).
Qed.
Lemma order_dec : forall x y : set, {order x y} + {~ order x y}.
destruct y.
left; constructor.
destruct x.
right; red; intros H; inversion H.
left; constructor.
Qed.
Lemma eq_dec : forall x y : set, {eq x y} + {~ eq x y}.
destruct y.
destruct x.
left; constructor.
right; red; intros H; inversion H.
destruct x.
right; red; intros H; inversion H.
left; constructor.
Qed.
Lemma bottom_is_a_bottom : forall x : set, order bottom x.
constructor.
Qed.
Lemma top_is_top : forall x : set, order x top.
constructor.
Qed.
Lemma acc_property : well_founded (fun x y => ~ eq y x /\ order y x).
unfold well_founded in |- *.
cut (Acc (fun x y : bool => y <> x /\ bool_order y x) true).
intros acc_true; simple destruct a; constructor; intros.
elim H; clear H; intros.
inversion_clear H0; auto.
elim H; clear H; intros.
generalize H; clear H H0; case y; auto.
intros H; elim H; auto.
constructor; intros.
constructor; intros.
elim H; clear H; intros.
elim H; inversion_clear H0; auto.
Qed.
End BoolLattice.
Index
This page has been generated by coqdoc