(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* 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 Import Order.Order. Require Export Order.Bounds. Require Export Order.Operations. Open Local Scope order_scope. (** 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 BinaryGlb `(po : PartialOrder A) (glb : A -> A -> A) := binary_is_glb : forall x y, binary_greatest_lower_bound x y (glb x y). Class BinaryLub `(po : PartialOrder A) (lub : A -> A -> A) := lub_is_glb : BinaryGlb (partial_order_dual po) lub. Class MeetSemiLattice `(po : PartialOrder A eqA) (meet : A -> A -> A) := { meet_morphism :> Proper (eqA ==> eqA ==> eqA) meet ; meet_glb :> BinaryGlb po meet }. Class JoinSemiLattice `(po : PartialOrder A eqA ord) join := join_is_meet : MeetSemiLattice (partial_order_dual po) join. Class SemiLattice `(eq : Equivalence A eqA) op := { semi_morphism :> Proper (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 `{e : Equivalence A} `(s : ! SemiLattice e lub) : relation A := (fun x y => x === lub x y)%type. Program Instance semilattice_preorder `(s : SemiLattice A eqA lub) : PreOrder (semi_order s). 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_partial_order `(s : SemiLattice A eqA lub) : PartialOrder _ (semi_order s). Next Obligation. Proof. unfold semi_order. split ; intros. reduce. substitute H. rewrite (semi_idempotent x0). split ; reflexivity. repeat red in H. intuition. rewrite H0. setoid_rewrite H1 at 2. rewrite <- (semi_commutative x x0). 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)). reflexivity. 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. Qed. Lemma meet_semi_idempotent x : meet x x === x. Proof. intros. destruct (meet_le x x). pose (le_le_meet (reflexivity x)). apply (antisymmetry H0 l). 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'. apply (antisymmetry P' P). Qed. Program Instance meet_le_morphism : Proper (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. assert(Hle:=le_le_meet H1). apply (antisymmetry Hle H). rewrite H1. assumption. Qed. End MeetSemiLatticeTheory. Program Instance meet_semilattice_semilattice `(ms : MeetSemiLattice A eqA ord glb) : ! SemiLattice A eqA glb. 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 y x). pose (meet_semi_le_meet y x). apply i. 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 Lattice `(po : PartialOrder A eqA ord, ms : ! MeetSemiLattice po meet, js : ! JoinSemiLattice po join). 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 *. 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 BoundedMeetSemiLattice `(ms : MeetSemiLattice A (po:=po)) (bound : A) := { bounded_sup :> Supremum po bound ; meet_semi_neutral : neutral meet bound }. Class BoundedJoinSemiLattice `(js : JoinSemiLattice A (po:=po)) (bound : A) := bounded_join_is_meet : BoundedMeetSemiLattice js bound. Class BoundedLattice `(Lattice A (po:=po) (ms:=ms) (js:=js), ! BoundedMeetSemiLattice ms la_sup, ! BoundedJoinSemiLattice js la_inf). (** Prop version, works for infinitary domains as well as finite ones. *) Class Glb `(po : PartialOrder A) (glb : subset A -> A -> Prop) := is_glb : forall x y, glb x y <-> greatest_lower_bound x y. Class Lub `(po : PartialOrder A) (lub : subset A -> A -> Prop) := lub_glb :> Glb (partial_order_dual po) lub. (** Meet and join infinite semilattices. Just a partial order with glbs or lubs. *) Require Import Ensembles. Class InfMeetSemiLattice `(po : PartialOrder A) meet := { glb_meet :> Glb po meet ; binary_glb : forall x y, ex (meet (Couple _ x y)) }. Class InfJoinSemiLattice `(po : PartialOrder A) join := inf_join_is_meet :> InfMeetSemiLattice (partial_order_dual po) join. Definition binary_lub `{InfJoinSemiLattice A} := binary_glb. (** A lattice has both glbs and lubs and absorption laws between them. *) Class InfLattice `(po : PartialOrder A, ms : ! InfMeetSemiLattice po meet, js : ! InfJoinSemiLattice po join). (** An abstract interpretation as a. *) Class AbstractInterpretation `(pa : PartialOrder A, pb : PartialOrder B) alpha gamma `{! Monotone pa pb alpha, ! Monotone pb pa gamma} (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 `{Proper (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 CompleteLattice `(la : Lattice A) := subset_lub : forall s : subset A, exists y : A, least_upper_bound s y. Class CompleteInfLattice `(la : InfLattice A (join:=join)) := inf_subset_lub : forall s : subset A, exists y : A, join s y. Section InfSemiLattices. Context `{js : InfJoinSemiLattice A eqA ordA join}. Lemma join_full_supremum : forall x, join full_subset x -> Supremum po x. Proof. intros. destruct js. specialize (glb_meet0 full_subset). intro. destruct (glb_meet0 x). specialize (H0 H x). unfold upper_bound in *. destruct H0 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. intro. destruct (glb_meet0 empty_subset x). specialize (H0 H x0). unfold upper_bound in *. destruct H0 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. Instance lub_mor `(po : PartialOrder A eqA) : Proper (subset_equality ==> eqA ==> iff) least_upper_bound. Proof. simpl_relation. unfold least_upper_bound, upper_bound. setoid_rewrite H0. unfold subset_equality in H. (* Truely dependent rewrite needed: rewrite in the domain type of a dependent product *) split ; intros. rewrite <- H1. split ; intros ; program_simpl. rewrite H in H3 ; apply (H2 (exist _ y1 H3)). rewrite <- H in H3 ; apply (H2 (exist _ y1 H3)). rewrite <- H1. split ; intros ; program_simpl. rewrite <- H in H3 ; apply (H2 (exist _ y1 H3)). rewrite H in H3 ; apply (H2 (exist _ y1 H3)). Qed. (* Instance [ po : PartialOrder A eqA ordA ] => *) (* Morphism (subset_inclusion ==> eqA ==> impl) least_upper_bound. *) (* Proof. *) (* unfold least_upper_bound, upper_bound. simpl_relation. *) (* rewrite <- H0. rewrite <- H1. *) (* red in H. *) (* split ; intros ; program_simpl. *) (* apply H in H3. apply (H2 (exist _ y1 H3)). *) (* setoid_rewrite H0. *) (* unfold subset_equality in H. *) (* (* Truely dependent rewrite needed: rewrite in the domain type of a dependent product *) *) (* split ; intros. *) (* rewrite <- H1. split ; intros ; program_simpl. *) (* rewrite H in H3 ; apply (H2 (exist _ y1 H3)). *) (* rewrite <- H in H3 ; apply (H2 (exist _ y1 H3)). *) (* rewrite <- H1. split ; intros ; program_simpl. *) (* rewrite <- H in H3 ; apply (H2 (exist _ y1 H3)). *) (* rewrite H in H3 ; apply (H2 (exist _ y1 H3)). *) (* Qed. *) 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. split; red ; auto. 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. constructor. red ; intros x influb. split ; red ; intro. do 2 red in H. intro. pose (H influb). unfold flip, le, upper_bound, least_upper_bound in *. destruct i as [inflb Hglb]. specialize (Hglb (reflexivity influb)). split ; intros. pose (Hglb (exist _ b H0)). apply l. unfold flip, le in *. transitivity influb ; auto. apply -> (H (`y)). intros [y' Hy']. simpl in *. apply Hy'. red. red in H. unfold least_upper_bound, upper_bound, flip, le in *. intro. split ; intros. assert (infs x influb). red. apply <- (H influb). order. apply (H0 (exist _ influb H1)). destruct (subset_lub (infs x)). specialize (H1 b). apply <- H1. Admitted. (* intros. *) (* apply subset_lub. *) (* Qed. *) End CompleteFromOrder. Require Import Finite_sets. Require Import Finite_sets_facts. Class Finite (A : Type) := full_finite : Finite_sets.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 FiniteLattice `(la : InfLattice A) := 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. assert(HA0:=is_glb H4). assert(Hx1x:=is_glb 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. *)