(************************************************************************)
(*  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        *)
(************************************************************************)

(** * Naturals.

   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 Arith.
Require Import ROmega.

Open Local Scope nat_scope.

Program Instance le_preorder : 
  ! PreOrder nat Peano.le.

  Next Obligation.
  Proof. eauto with arith. Qed.

Program Instance nat_po : 
  PartialOrder _ le_preorder.

  Next Obligation.
  Proof.
    firstorder (subst* ; order).
    apply le_antisym ; auto.
  Qed.

Program Instance nat_so : 
  StrictOrder _ Peano.lt.

  Next Obligation.
  Proof. 
    apply (lt_irrefl _ H). 
  Qed.

  Next Obligation.
  Proof. eauto with arith. Qed.
    
(** Only an infinimum. *)

Instance zero_infimum : Infimum _ 0.
Proof. reduce. auto with arith. Qed.

Require Import Coq.Arith.Min.

Instance binary_glb : BinaryGlb nat_po min.
Proof. 
  reduce_goal ; unfold le in *. intuition.

  rewrite H. auto with arith.
  rewrite H. auto with arith.
  destruct (min_dec x y) ; rewrite e ; auto.
Qed.

Require Import Coq.Arith.Max.

Instance binary_lub : BinaryLub nat_po max.
Proof.
  reduce_goal. unfold flip, le in *. split ; intros.
  
  split ; rewrite <- H ; auto with arith.
  
  destruct(max_dec x y) ; rewrite e ; intuition.
Qed.

Program Instance meet_semi : MeetSemiLattice nat_po min.
Program Instance join_semi : JoinSemiLattice nat_po max.

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

Program Instance nat_lattice : Lattice nat_po meet_semi join_semi.

Example absorb : forall x y, min x (max x y) === x.
Proof.
  clapply lattice_absorb_meet_join.
Qed.