(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(** * Booleans.

   Author: Matthieu Sozeau <sozeau@lri.fr>
   Institution: LRI, CNRS UMR 8623 - Université Paris Sud
                91405 Orsay, France 

*)

Require Export Order.Lattice.
Require Import Coq.Program.Tactics.

Require Import Coq.Classes.EquivDec.
Require Import Coq.Bool.Bool.

Program Instance leb_preorder : 
  ! PreOrder bool leb.

  Solve Obligations using reduce_goal ; destruct x ; auto with datatypes.

  Next Obligation.
  Proof.
    destruct x ; destruct y ; destruct z ; simpl in * ; auto with datatypes.
  Qed.

Program Instance bool_po : 
  ! PartialOrder bool eq leb.

  Next Obligation.
  Proof.
    firstorder (subst* ; order).
    destruct x ; destruct x0 ; simpl in * ; auto with datatypes.
  Qed.

Instance false_infimum : Infimum bool_po false.
Proof. constructor. Qed.

Instance true_supremum : Supremum _ true.
Proof. reduce_goal. destruct x ; auto. Qed.

(** Boolean greatest lower bound, left-biased. *)

Definition glb (x y : bool) := 
  if x then y else x.

(** Boolean least upper bound, right-biased. *)

Definition lub (x y : bool) :=
  if y then y else x.

Instance binary_glb : BinaryGlb bool_po glb.
Proof.
  reduce_goal. destruct x ; destruct y ; destruct z ; intuition order.
Qed.

Instance binary_lub : BinaryLub bool_po lub.
Proof.
  reduce_goal. destruct x ; destruct y ; destruct z ; intuition order.
  constructor.
  constructor.
Qed.

Program Instance meet_semi : MeetSemiLattice bool_po glb.
Program Instance join_semi : JoinSemiLattice bool_po lub.

  Next Obligation.
  Proof.
    constructor. obligations_tactic. 
    red. apply binary_lub.
  Qed.

Program Instance bool_lattice : Lattice bool_po meet_semi join_semi.

Example absorb : forall x y, glb x (lub x y) === x.
Proof.
  apply (lattice_absorb_meet_join (la:=@bool_lattice)).
Qed.