Require Lattice.
Inductive bool_order : bool -> bool -> Prop :=
| true_order : (x:bool)(bool_order x true)
| false_order : (x:bool)(bool_order false x).
Definition join_bool : bool -> bool -> bool :=
[x,y]
Cases x y of
| true _ => true
| _ true => true
| _ _ => false
end.
Definition LatticeBool : (Lattice bool).
Refine (poset_constr
bool
bool_order
[x,y]x=y
join_bool
? ? ? ? ? ? ? ? ?
? false ? true ? ?).
Intros x y H; Rewrite H; Case y; Constructor.
Destruct x; Destruct y; Intros H H1; (Inversion H;Fail) Orelse (Inversion H1; Fail) Orelse Auto.
Destruct x; Destruct y; Intros H H1; (Inversion H;Fail) Orelse (Inversion H1; Fail) Orelse (Try Constructor; Auto).
Auto.
Auto.
Intros x y z H; Rewrite H; Auto.
Destruct x; Destruct y; Simpl; Constructor.
Destruct x; Destruct y; Simpl; Constructor.
Destruct x; Destruct y; Destruct z; Simpl; Intros H1 H2; (Inversion H1; Fail) Orelse (Inversion H2; Fail) Orelse (Constructor; Auto).
Decide Equality.
Constructor.
Constructor.
Unfold well_founded.
Cut (Acc bool [x,y:bool]~y=x/\(bool_order y x) true).
Intros acc_true;
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.