(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* Institution: LRI, CNRS UMR 8623 - Université Paris Sud 91405 Orsay, France *) Set Implicit Arguments. Require Import Coq.Program.Program. Require Export Order.Lattice. Open Local Scope order_scope. Section OptionSet. Context [ eqa : Equivalence A eqA ]. Definition option_eq (x y : option A) := match x, y with | None, None => True | Some x, Some y => eqA x y | _, _ => False end. Instance option_equiv : Equivalence _ option_eq. Proof. reduce. destruct x ; auto. order. reduce. destruct x ; destruct y; firstorder. reduce. destruct x ; destruct y ; destruct z ; firstorder. Qed. Context [ po : PartialOrder A eqA (equ:=eqa) ordA ]. Definition option_le (x y : option A) := match x, y with | None, _ => True | Some x, Some y => x <= y | _, _ => False end. Instance option_preorder : PreOrder _ option_le. Proof. reduce. destruct x ; auto. order. reduce. destruct x ; destruct y ; destruct z; try (solve [ firstorder ]). simpl in *. order. Qed. Instance option_po : ! PartialOrder (option A) _ _. Proof. reduce. unfold option_eq, option_le, flip. split ; intros. reduce. destruct x ; destruct y; try (solve [firstorder]). rewrite H. split ; reflexivity. repeat red in H. destruct x ; destruct y; intuition. order. Qed. Instance option_inf : Infimum _ None. Proof. firstorder. Qed. Context [ ms : ! MeetSemiLattice po glb ]. Definition option_glb x y := match x, y with | None, _ => None | _, None => None | Some x, Some y => Some (glb x y) end. Instance option_binary_glb : BinaryGlb _ option_glb. Proof. reduce. destruct x ; destruct y ; destruct z ; unfold le in * ; simpl in * ; auto ; try solve [ intuition ]. apply (binary_glb a a0). Qed. Instance option_ms : MeetSemiLattice _ option_glb. Proof. reduce. destruct x ; destruct x0 ; destruct y ; destruct y0 ; unfold le in * ; simpl in * ; auto ; try solve [ intuition ]. rewrite H. rewrite H0. reflexivity. apply option_binary_glb. Qed. End OptionSet. Existing Instance option_preorder. Existing Instance option_equiv. Existing Instance option_po. Existing Instance option_binary_glb. Existing Instance option_ms. Section Bounded. Context [ eqa : Equivalence A eqA ]. Inductive bounded : Type := | top : bounded | elem : A -> bounded | bot : bounded. Definition bounded_eq x y := match x, y with | top, top => True | bot, bot => True | elem x, elem y => eqA x y | _, _ => False end. Instance bounded_equiv : Equivalence _ bounded_eq. Proof. reduce. destruct x ; auto. order. reduce. destruct x ; destruct y; firstorder. reduce. destruct x ; destruct y ; destruct z ; firstorder. Qed. Context [ po : PartialOrder A eqA (equ:=eqa) ordA ]. Definition bounded_le x y := match x, y with | bot, _ => True | elem x, elem y => x <= y | _, top => True | _, _ => False end. Definition bounded_ge := flip bounded_le. Instance bounded_preorder : PreOrder _ bounded_le. Proof. reduce. destruct x ; auto. order. reduce. destruct x ; destruct y ; destruct z; try (solve [ firstorder ]). simpl in *. order. Qed. Instance bounded_po : ! PartialOrder bounded _ _. Proof. reduce. unfold bounded_eq, bounded_le, flip. split ; intros. reduce. destruct x ; destruct y; try (solve [firstorder]). rewrite H. split ; reflexivity. repeat red in H. destruct x ; destruct y; intuition. order. Qed. Instance bounded_dual_po : ! PartialOrder bounded bounded_eq (flip bounded_le). Proof. apply @partial_order_dual. apply bounded_po. Defined. Instance bounded_inf : Infimum _ bot. Proof. firstorder. Qed. Context [ ms : ! MeetSemiLattice po glb ]. Definition bounded_glb x y := match x, y with | None, _ => None | _, None => None | Some x, Some y => Some (glb x y) end. Instance bounded_binary_glb : BinaryGlb _ bounded_glb. Proof. reduce. destruct x ; destruct y ; destruct z ; unfold le in * ; simpl in * ; auto ; try solve [ intuition ]. apply (binary_glb a a0). Qed. Instance bounded_ms : MeetSemiLattice _ bounded_glb. Proof. reduce. destruct x ; destruct x0 ; destruct y ; destruct y0 ; unfold le in * ; simpl in * ; auto ; try solve [ intuition ]. rewrite H. rewrite H0. reflexivity. apply bounded_binary_glb. Qed. End OptionSet. (* Context [ po : PartialOrder A eqA (equ:=eqa) ordA ]. Definition bounded := option (option A). Definition bounded_equiv := option_equiv (eqA:=option_eq (eqA:=eqA)). Definition bounded_pre := option_preorder (ordA:=option_le (ordA:=ordA)). Instance bounded_po : PartialOrder bounded_equiv bounded_pre. Proof. exact (option_po (eqA:=option_eq (eqA:=eqA)) (ordA:=option_le (ordA:=ordA))). Defined. Definition bounded_dual_pre := option_preorder (ordA:=option_le (ordA:=flip ordA)). Instance bounded_dual_po : PartialOrder bounded_equiv bounded_dual_pre. Proof. exact (option_po (eqA:=option_eq (eqA:=eqA)) (ordA:=option_le (ordA:=flip ordA))). Defined. Context [ ms : ! MeetSemiLattice po glb ]. Typeclasses eauto := bfs 10. Definition bounded_glb := option_glb (eqA:=option_eq (eqA:=eqA)) (glb:=option_glb (glb:=glb)). Definition bounded_msl : MeetSemiLattice bounded_po bounded_glb. Proof. exact (option_ms (eqA:=option_eq (eqA:=eqA)) (ordA:=option_le (ordA:=ordA))). Defined. Definition bounded_jsl : JoinSemiLattice bounded_po bounded_glb. Proof. unfold JoinSemiLattice. exact (option_ms (eqA:=option_eq (eqA:=eqA)) (po:=partial_order_dual (po:=option_po)) (ordA:=option_le (ordA:=flip ordA))). Defined. Instance option_bms : BoundedJoinSemiLattice (po:=partial_order _ None. Proof. reduce. destruct x. destruct x ; destruct x0 ; destruct y ; destruct y0 ; unfold le in * ; simpl in * ; auto ; try solve [ intuition ]. rewrite H. rewrite H0. reflexivity. apply option_binary_glb. Qed. End Bounded. *)