(************************************************************************) (* 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 Export Order.Lattice. Require Export Order.Quotients. Open Local Scope order_scope. Print CompleteLattice. Print InfMeetSemiLattice. Set Transparent Obligations. Require Import Program. Class [ ms : MeetSemiLattice A eqA ordA meetA ] => PreservesBinaryMeet (sub : subset A) := preserves_binary_meet : forall x y : sig sub, sub (meetA (`x) (`y)). Program Definition subset_meet [ ms : MeetSemiLattice A eqA ordA meetA, pm : ! PreservesBinaryMeet ms sub ] := fun x x' : sig sub => (meetA x x' : sig sub). Program Definition quotient_meet [ ms : InfMeetSemiLattice A eqA ordA meetA ] (sub : subset A) := fun (s : subset (sig sub)) (t : sig sub) => meetA (fun x => exists subx : sub x, s (exist _ x subx)) t. Obligations Tactic := idtac. Program Instance [ ms : MeetSemiLattice A eqA ordA meetA, pm : ! PreservesBinaryMeet ms sub ] => quotient_meet_glb : BinaryGlb (quotient_partial_order sub) (subset_meet (pm:=pm)). Next Obligation. Proof with simpl in *. intros. red. intros. unfold subset_meet. split ; intros. rewrite H. split ; [ apply meet_le_l | apply meet_le_r ]. destruct H. apply le_meet ; auto. Qed. (* Class [ ms : InfMeetSemiLattice A eqA ordA meetA ] => PreservesMeet (sub : subset A) := *) (* preserves_meet : forall (s : subset A) (y : A), *) (* greatest_lower_bound (fun a => { suba : sub a & s (exist _ a suba) }) y <-> *) (* (exists suby : sub y, greatest_lower_bound s (exist _ y suby)). *) Require Import Ensembles. Class [ ms : InfMeetSemiLattice A eqA ordA meetA ] => PreservesMeet (sub : subset A) := preserves_meet : forall (s : subset A) (H : subset_inclusion s sub) (y : A), greatest_lower_bound s y <-> (exists suby : sub y, greatest_lower_bound (fun a : sig sub => s (`a)) (exist _ y suby)). Program Instance [ ms : InfMeetSemiLattice A eqA ordA meetA, pm : ! PreservesMeet ms sub ] => quotient_meet_glb' : Glb (quotient_partial_order sub) (quotient_meet (ms:=ms) (sub:=sub)). Next Obligation. Proof with simpl in *. split ; intros. red in H. unfold greatest_lower_bound, least_upper_bound, upper_bound in *. rewrite is_glb in H. do 2 red in H. intros. setoid_rewrite <- (H (proj1_sig b)). unfold upper_bound. split; intros H' [y0 Hy0]... destruct Hy0 as [suby0 xy0]... specialize (H' (exist _ _ xy0))... apply H'. destruct y0 as [y0 suby0]... apply (H' (exist _ y0 (ex_intro (fun s : sub y0 => x (exist sub y0 s)) _ Hy0))). red. rewrite is_glb. rewrite preserves_meet. destruct y ; simpl. exists s. unfold greatest_lower_bound. setoid_replace (fun a : sig sub => exists subx : sub (`a), x (exist _ (`a) subx)) with x using relation (@subset_equality (sig sub)). assumption. intro el. split ; program_simpl; try exists H1 ; auto. rewrite (proof_irrelevance _ H2 H0) ; auto. firstorder. Qed. Obligations Tactic := my_simplify. Ltac my_simplify ::= intros ; auto with typeclass_instances; try reduce_goal ; unfold flip, impl, arrow in |- *; try reduce_goal ; try tauto; try (solve [ intuition ]). Hint Unfold greatest_lower_bound : typeclass_instances. Program Instance [ ms : InfMeetSemiLattice A eqA ordA meetA, pm : ! PreservesMeet ms sub ] => quotient_meet_semilattice : InfMeetSemiLattice (quotient_partial_order sub) (quotient_meet (ms:=ms) (sub:=sub)). Next Obligation. Proof. unfold quotient_meet. destruct (binary_glb (`x) (`y)). rewrite is_glb in H. setoid_rewrite is_glb. setoid_replace (fun a => exists suba : sub a, Couple (sig sub) x y (exist _ a suba)) with (Couple A (`x) (`y)) using relation (@subset_equality A). rewrite preserves_meet in H. destruct H. exists (exist _ _ x1). simpl. rewrite preserves_meet. exists x1. assumption. red; intros x2 Hc ; inversion Hc ; subst ; program_simpl ; auto. red; intros x2 Hc ; inversion Hc ; subst ; program_simpl ; auto. red ; intros. split ; program_simpl. inversion H1 ; subst ; constructor. inversion H0 ; subst. exists H2 ; constructor. exists H1 ; constructor. Qed. Section Tarski. Context [ CompleteInfLattice A eqA leA meetA joinA ]. Context [ ! Monotone po po f ]. Variable ina : inhabited A. Definition postfixpoint x := f x <= x. Definition prefixpoint x := x <= f x. Definition fixpoint x := x === f x. Definition fixpoints := sig fixpoint. Definition prefixpoints := sig prefixpoint. Definition postfixpoints := sig postfixpoint. Print MeetSemiLattice. Definition fixpoints_po := quotient_partial_order fixpoint. Existing Instance fixpoints_po. Program Lemma monot : forall x : prefixpoints, prefixpoint (f x). Proof. intros [x Hx] ; unfold prefixpoint in * ; simpl. apply monotonicity. assumption. Qed. Variable x : prefixpoints. Require Import Epsilon. Program Definition u : exists b, joinA prefixpoint b := inf_subset_lub prefixpoint. Program Lemma le_x_u : (x : A) <= u. Proof. unfold u. destruct x. simpl. unfold epsilon. destruct epsilon_statement. simpl. unfold least_upper_bound. intros [x Hx] ; unfold prefixpoint in * ; simpl. apply monotonicity. assumption. Qed. Instance PreservesMeet ms prefixpoint. Proof. constructor. n intros Glb. Lemma u_meet := quotient_meet_semilattice. Definition meet (s : subset fixpoints) Lemma complete_lattice :