Library BoolLattice
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 BoolPoset : Poset bool.
refine
(poset_constr bool (fun x y => x = y) _ _ _ bool_order _ _ _).
auto.
auto.
intros x y z H; rewrite H; auto.
intros x y H; rewrite H; case y; constructor.
simple destruct x; simple destruct y; intros H H1;
(inversion H; fail) || (inversion H1; fail) || auto.
simple destruct x; simple destruct y; intros H H1;
(inversion H; fail) || (inversion H1; fail) || (try constructor; auto).
Defined.
Definition LatticeBool : Lattice bool.
refine
(lattice_constr bool BoolPoset
join_bool _ _ _
_ false _ true _ _).
simple destruct x; simple destruct y; simpl in |- *; constructor.
simple destruct x; simple destruct y; simpl in |- *; constructor.
simple destruct x; simple destruct y; simple destruct z; simpl in |- *;
intros H1 H2;
(inversion H1; fail) || (inversion H2; fail) || (constructor; auto).
destruct y.
left; constructor.
destruct x.
right; red; intros H; inversion H.
left; constructor.
constructor.
constructor.
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.
elim H; clear H; intros.
elim H; inversion_clear H0; auto.
Defined.
Index
This page has been generated by coqdoc