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

(** * Certified Prelude.

   This module implements classes for the lattice structures, starting from semilattices
   and showing their correspondence with partial orders. The lattices and bounded lattices are
   defined.

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

*)

(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)

Set Implicit Arguments.
Unset Strict Implicit.

Require Export Order.Bounds.

Open Local Scope order_scope.

(** We define properties of [operation]s up-to an arbitrary setoid equality on the carrier.
   Note how we generalize statements to avoid implicit use of the leibniz equality. *)

Program Definition associative [ Equivalence A ] (op : binary_operation A) := 
  forall x y z, op x (op y z) === op (op x y) z.

Program Definition commutative [ Equivalence A ] (op : binary_operation A) := 
  forall x y, op x y === op y x.

Program Definition idempotent [ Equivalence A ] (op : binary_operation A) := 
  forall x, op x x === x.

Program Definition neutral [ Equivalence A ] (op : binary_operation A) (e : A) := 
  forall x, op e x === x.

(** Lattices in Set, with binary meets and joins only. *)

(** Meet and join semilattices. Just a partial order with glbs or lubs. *)

Definition binary_greatest_lower_bound [ po : PartialOrder A ] (x y glb : A) : Prop :=
  forall z : A, z <= glb <-> z <= x /\ z <= y.

Class [ po : PartialOrder A ] => BinaryGlb (glb : A -> A -> A) :=
  binary_is_glb : forall x y, binary_greatest_lower_bound x y (glb x y).

Class [ po : PartialOrder A ] => BinaryLub (lub : A -> A -> A) :=
  lub_is_glb : BinaryGlb partial_order_dual lub.

Class [ po : PartialOrder A eqA ] => MeetSemiLattice (meet : A -> A -> A) :=
  meet_morphism :> Morphism (eqA ==> eqA ==> eqA) meet ;
  meet_glb :> BinaryGlb po meet.

Class [ po : PartialOrder A eqA ord ] => JoinSemiLattice join := 
  join_is_meet : MeetSemiLattice partial_order_dual join.

Class [ s : Equivalence A eqA ] => SemiLattice op :=
  semi_morphism :> Morphism (eqA ==> eqA ==> eqA) op ;
  semi_associative : associative op ;
  semi_commutative : commutative op ;
  semi_idempotent : idempotent op.

(** Every semilattice gives rise to a partial order. *)

Definition semi_order [ s : Equivalence A, ! SemiLattice s lub ] : relation A := 
  (fun x y => x === lub x y)%type.

Program Instance [ SemiLattice A eqA lub ] =>
  semilattice_preorder : PreOrder A semi_order.

  Next Obligation.
  Proof.
    unfold semi_order.
    rewrite (semi_idempotent x).
    reflexivity.
  Qed.

  Next Obligation.
  Proof.
    unfold semi_order in *.
    rewrite H. 
    rewrite <- (semi_associative x y z).
    rewrite <- H0.
    reflexivity.
  Qed.

Program Instance [ SemiLattice A eqA lub ] =>
  semilattice_partial_order : PartialOrder _ semilattice_preorder.

  Next Obligation.
  Proof.
    unfold semi_order. split ; intros.
    red. substitute H. rewrite (semi_idempotent y). split ; reflexivity.

    red in H. intuition. 
    rewrite H0.
    setoid_rewrite H1 at 2.
    rewrite <- (semi_commutative x y).
    reflexivity.
  Qed.

(* Program Instance [ s : DecidableEquivalence A, ! SemiLattice _ lub ] => *)
(*   semilattice_meetsemilattice : MeetSemiLattice semilattice_partial_order lub. *)

(*   Next Obligation. *)
(*   Proof. *)
(*     red ; intros. *)

(*     split ; intros. *)
    
(*     unfold le, semi_order in H. *)

(*     destruct(setoid_decidable z (lub z x)) ; destruct(setoid_decidable z (lub z y)) ; *)
(*       try solve [ split ; auto ]. *)

(*     clrewrite (semi_associative z x y) in H. *)
(*     clrewrite <- H0 in H. *)
(*     contradiction.  *)

(*     clrewrite (semi_commutative x y) in H. *)
(*     clrewrite (semi_associative z y x) in H. *)
(*     clrewrite <- H1 in H. *)
(*     contradiction. *)

(*     clrewrite H in H0. *)
(*     clrewrite (semi_associative z x y) in H0. *)
(*     clrewrite (semi_commutative (lub z x) y) in H0. *)
(*     clrewrite <- (semi_associative y (lub z x) x) in H0. *)
(*     clrewrite <- (semi_associative z x x) in H0. *)
(*     clrewrite (semi_idempotent x) in H0. *)
(*     order. *)

(*     destruct H ; order. *)
(*     unfold le, semi_order in *. *)
(*     clrewrite H at 1. *)
(*     clrewrite H0 at 1. *)
(*     clrewrite <- (semi_associative z y x). *)
(*     clrewrite <- (semi_commutative y x). *)
(*     refl. *)
(*   Qed. *)

Require Import Coq.Program.Program.

Section MeetSemiLatticeTheory.
  Context [ m : MeetSemiLattice A eqA ord ].

  Implicit Types x y z w : A.

  Lemma meet_le : forall x y, meet x y <= x /\ meet x y <= y.
  Proof.
    intros ; apply -> (meet_glb x y (meet x y)).
    refl.
  Qed.

  Lemma meet_le_l : forall x y, meet x y <= x.
  Proof.
    intros ; destruct (meet_le x y) ; auto.
  Qed.

  Lemma meet_le_r : forall x y, meet x y <= y.
  Proof.
    intros ; destruct (meet_le x y) ; auto.
  Qed.

  Lemma le_meet_l : forall x y z, z <= meet x y -> z <= x.
  Proof.
    intros ; destruct (proj1 (meet_glb x y z)) ; auto.
  Qed.

  Lemma le_meet_r : forall x y z, z <= meet x y -> z <= y.
  Proof.
    intros ; destruct (proj1 (meet_glb x y z)) ; auto.
  Qed.

  Lemma le_meet : forall x y z, z <= x -> z <= y -> z <= meet x y.
  Proof.
    intros ; apply <- (meet_glb x y z). auto.
  Qed.

  Lemma le_le_meet : forall x y, x <= y -> x <= meet x y.
  Proof.
    intros.
    apply <- (meet_glb x y x).
    intuition order.
  Qed.

  Lemma meet_semi_idempotent x : meet x x === x.
  Proof.
    intros.
    destruct (meet_le x x).
    pose (le_le_meet (reflexivity x)).
    order.
  Qed.

  Lemma meet_semi_commutative x y : meet x y === meet y x.
  Proof.
    intros.
    destruct (meet_le x y) ; destruct (meet_le y x).
    pose (le_meet H2 H1) as P.
    pose (le_meet H0 H) as P'.
    order.
  Qed.
    
  Program Instance meet_le_morphism : Morphism (le ==> le ==> le) meet.
  
    Next Obligation.
    Proof.
      destruct (meet_le x x0).
      apply le_meet.
      rewrite H1. assumption.
      rewrite H2. assumption.
    Qed.

  Lemma meet_semi_associative x y z : meet x (meet y z) === meet (meet x y) z.
  Proof.
    intros.
    order_antisymmetry le.
    apply le_meet.
      rewrite (meet_le_l y z). reflexivity.
      rewrite (meet_le_r y z). apply meet_le_r. 
      
    apply le_meet.
      rewrite (meet_le_l x y). apply meet_le_l. 
      rewrite (meet_le_r x y). reflexivity.
  Qed.
    
  Lemma meet_semi_le_meet : forall x y, x <= y <-> x === meet x y.
  Proof.
    intros.
    destruct (meet_le x y).
    split ; intros.

      pose (le_le_meet H1) as Hle.
      order.
    
      rewrite H1.
      assumption.
  Qed.

End MeetSemiLatticeTheory.

Program Instance [ MeetSemiLattice A eqA ord glb ] => 
  meet_semilattice_semilattice : ! SemiLattice A eqA glb.

  Next Obligation.
  Proof. rewrite H. rewrite H0. reflexivity. Qed.

  Next Obligation.
  Proof. eapply meet_semi_associative ; eauto. Qed.

  Next Obligation.
  Proof. eapply meet_semi_commutative ; eauto. Qed.

  Next Obligation.
  Proof. eapply meet_semi_idempotent ; eauto. Qed.

Section JoinSemiLatticeTheory.  

  Context [ po : PartialOrder A eqA ord ]. 
  Context [ js : ! JoinSemiLattice po join ].

  Implicit Types x y z w : A.

  Lemma join_semi_le_join x y : x <= y <-> y === join x y.
  Proof.
    intros.
    unfold JoinSemiLattice in js.
    rewrite (meet_semi_commutative x y).
    apply (meet_semi_le_meet y x).
  Qed.
  
  (** We get the dual proofs by just applying the original proofs. *)

  Lemma le_join x y : join x y >= x /\ join x y >= y.
  Proof. apply (meet_le (m:=js)). Qed.

  Lemma join_is_ge x y z : z >= x -> z >= y -> z >= join x y.
  Proof. apply (le_meet (m:=js)). Qed.

End JoinSemiLatticeTheory.

(** Note that we share the partial order implementation (and the setoid) 
   so that the orders are related by conversion. *)

Class [ po : PartialOrder A eqA ord, 
  ms : ! MeetSemiLattice po meet, 
  js : ! JoinSemiLattice po join ] => Lattice.

Section LatticeTheory.
  Context [ la : Lattice A eqA ord meet join ].

  Implicit Type x y z w : A.

  Lemma lattice_absorb_meet_join : forall x y, meet x (join x y) === x.
  Proof.
    intros.
    destruct (le_join (js:=js) x y).
    unfold flip, le in * ; orderify.
    symmetry. 
    apply (proj1 (meet_semi_le_meet _ _) H).
  Qed.
  
  (** Dual statement. *)

  Lemma lattice_absorb_join_meet : forall x y, join x (meet x y) === x.
  Proof.
    intros. 
    destruct (meet_le x y).
    symmetry.
    apply (proj1 (meet_semi_le_meet (m:=js) _ _) H).
  Qed.

End LatticeTheory.

(* Class [ po : PartialOrder A, ! Glb po join ] => GlbSemiLattice. *)

(* Class [ po : PartialOrder A, ! Lub po join ] => LubSemiLattice. *)

Require Import Coq.Program.Tactics.

(** A lattice has both glbs and lubs and absorption laws between them. *)

(* Class [ po : PartialOrder A eqA ord, ? MeetSemiLattice po meet, ? MeetSemiLattice partial_order_dual join ] => Lattice :=   *)
(*   absorb_meet_join : forall x y, meet x (join x y) === x ; *)
(*   absorb_join_meet : forall x y, join x (meet x y) === x. *)

(* Class [ po : PartialOrder A, ! BinaryGlb po meet, ! BinaryLub po join ] => AlgebraicLattice := *)
(*   absorb_meet_join : forall x y, meet x (join x y) === x ; *)
(*   absorb_join_meet : forall x y, join x (meet x y) === x. *)

(** A bounded lattice has top and bottom with the proper neutrality laws for meet and join. *)

Class [ ms : MeetSemiLattice A (po:=po) ] => BoundedMeetSemiLattice (bound : A) :=
  bounded_sup :> Supremum po bound ;
  meet_semi_neutral : neutral meet bound.

Class [ js : JoinSemiLattice A (po:=po) ] => BoundedJoinSemiLattice (bound : A) :=
  bounded_join_is_meet : BoundedMeetSemiLattice js bound.

Class [ Lattice A (po:=po) (ms:=ms) (js:=js), 
  ! BoundedMeetSemiLattice ms la_sup, ! BoundedJoinSemiLattice js la_inf ] => BoundedLattice.

(** Prop version, works for infinitary domains as well as finite ones. *)

Definition LUB [ po : PartialOrder A eqA ] (sub : subset A) :=
  { sup : A | least_upper_bound sub sup }.

Class [ po : PartialOrder A ] => Glb (glb : subset A -> A -> Prop) :=
  is_glb : forall x y, glb x y -> greatest_lower_bound x y.

Class [ po : PartialOrder A ] => Lub (lub : subset A -> A -> Prop) :=
  lub_glb : Glb partial_order_dual lub.

Definition is_lub [ po : Lub A (lub:=lub) ] :=
  is_glb (glb:=lub).

(** Meet and join infinite semilattices. Just a partial order with glbs or lubs. *)

Require Import Ensembles.

Class [ po : PartialOrder A ] => InfMeetSemiLattice :=
  binary_glb : forall x y : A, ex (greatest_lower_bound (Couple _ x y)).

Class [ po : PartialOrder A ] => InfJoinSemiLattice :=
  inf_join_is_meet :> InfMeetSemiLattice partial_order_dual.

Definition binary_lub [ InfJoinSemiLattice A ] := 
  binary_glb.

(** A lattice has both glbs and lubs and absorption laws between them. *)

Class [ po : PartialOrder A, ms : ! InfMeetSemiLattice po, 
  js : ! InfJoinSemiLattice po ] => InfLattice.

(** An abstract interpretation as a. *)

Class [ pa : PartialOrder A, pb : PartialOrder B, ! Monotone pa pb alpha, ! Monotone pb pa gamma ] => 
  AbstractInterpretation (f : A -> A) (f' : B -> B)  :=
  abstraction : forall x, (f ∘ gamma) x <= (gamma ∘ f') x.

Definition image A B (f : A -> B) := { y : B | exists x, y = f x }.

Program Definition complete [ Morphism (A -> B) (eqA ==> eqB) m ]
  (O : (A -> Prop) -> A) (O' : (B -> Prop) -> B) :=
  forall X : A -> Prop, m (O X) === O' (fun b => exists x : sig X, b === m x).

Class [ la : Lattice A ] => CompleteLattice :=
  subset_lub : forall s : subset A, exists y : A, least_upper_bound s y.

Class [ la : InfLattice A ] => CompleteInfLattice :=
  join : forall s : subset A, { y : A | least_upper_bound s y }.

Typeclasses eauto := dfs 15.

Section InfSemiLattices.
  
  Context [ js : InfJoinSemiLattice A eqA ordA ].

  Program Lemma join_full_supremum : Supremum po (join (A:=A) full_subset).
  Proof.
    intros.
    destruct js.
    specialize (glb_meet0 full_subset).
    intro.
    specialize (glb_meet0 _ H x).
    unfold upper_bound in *.
    destruct glb_meet0 as [_ Hl].
    specialize (Hl (reflexivity x) (exist _ x0 I)).
    apply Hl.
  Qed.

  Lemma join_empty_infimum : forall x, join empty_subset x -> Infimum po x.
  Proof.
    intros.
    destruct js.
    specialize (glb_meet0 empty_subset).
    intro.
    specialize (glb_meet0 _ H x0).
    unfold upper_bound in *.
    destruct glb_meet0 as [Hl _].
    apply Hl. intros. inversion y. inversion H0.
  Qed.

End InfSemiLattices.

Class Inhabited A := 
  inhabits : inhabited A.

Section CompleteLattices.

  Context [ cla : CompleteInfLattice A eqA ordA meet join ].
  
  Lemma complete_supremum : exists x, Supremum po x.
  Proof.
    destruct (inf_subset_lub full_subset). exists x.
    apply (join_full_supremum H).
  Qed.

  Lemma complete_infimum : exists x, Infimum po x.
  Proof.
    destruct (inf_subset_lub empty_subset). exists x.
    apply (join_empty_infimum H).
  Qed.

  Require Import Epsilon.

  Instance Inhabited A.
  Proof. red ; intros. constructor.
    destruct (constructive_indefinite_description _ (inf_subset_lub empty_subset)).
    exact x.
  Qed.
  
  Lemma complete_infimum_epsilon : Infimum po (epsilon inhabits (join empty_subset)).
  Proof.
    apply join_empty_infimum.
    apply epsilon_spec. apply inf_subset_lub.
  Qed.

  Lemma complete_supremum_epsilon : Supremum po (epsilon inhabits (join full_subset)).
  Proof.
    apply join_full_supremum.
    apply epsilon_spec. apply inf_subset_lub.
  Qed.

End CompleteLattices.

Section CompleteFromOrder.

  Context [ po : PartialOrder A eqA ordA ].

  Variable subset_lub : forall s : subset A, exists sup, least_upper_bound s sup.

  Definition join := least_upper_bound. 

  Instance subset_lub_join : InfJoinSemiLattice po join.
  Proof.
    reduce. unfold join. constructor.
    red. intros. red. apply H.

    intros.
    apply subset_lub.
  Qed.
  
  Definition infs s := fun y : A => forall x : object s, y <= `x.

  Definition meet s := join (infs s).

  Instance subset_lub_meet : InfMeetSemiLattice po meet.
  Proof.
    red. intros x influb.
    intros. red ; intro. do 2 red in H. 
    assert (infglb:=is_glb H).
    specialize (H b).
    do 2 red in infglb.
    unfold flip, le, upper_bound, least_upper_bound in *.
    destruct (infglb influb) as [_ Hglb].
    specialize (Hglb (reflexivity influb)).
    split ; intros.
    pose (Hglb (exist _ b H0)). apply l.

    unfold flip, le in *.
    transitivity influb ; auto.
    apply -> (infglb (`y)).
    intros [y' Hy'].
    simpl in *. apply Hy'.

    intros.
    apply subset_lub.
  Qed.

End CompleteFromOrder.

Require Import Finite_sets.
Require Import Finite_sets_facts.

Class Finite (A : Type) :=
  full_finite : Finite A full_subset.

Lemma finite_subsets [ Finite A ] : forall (s : subset A), Finite_sets.Finite A s.
Proof.
  intros.
  eapply Finite_downward_closed. apply full_finite.
  constructor.
Qed.
  
Class [ la : InfLattice A ] => FiniteLattice :=
  finite_lattice :> Finite A.

Section FiniteLattices.
  Context [ fla : FiniteLattice A ].

  Instance CompleteInfLattice la.
  Proof.
    intro.
    generalize (finite_subsets s).
    intro Hfin.
    cut (Ensembles.Inhabited A s).
    induction Hfin using Generalized_induction_on_finite_sets.
    intros.
    inversion Hfin; subst.
    inversion H0. inversion H1.
    
    inversion H0.
    induction H3.

    destruct (H A0).
    constructor; auto with sets.
    intro HAdd ; rewrite HAdd in H2.
    apply H2. auto with sets.
    exists x0. auto.
    destruct (binary_lub x1 x).
    exists x2. 
    pose (is_lub H5).
    

    constructor ; auto. constructor ; auto.
    red ; intro. discriminate.

    pose (binary_gb 
    exists ()

    elim Hfin using Generalized_induction_on_finite_sets.
    clear s Hfin.
    intros.
    induction H.
    exists (infimum (A:=A)).
    simpl.