hunk ./CartesianProduct.v 39 -Program Instance [ pa : PreOrder A R₁, pb : PreOrder B R₂ ] => - pointwise_preorder : PreOrder (A * B) (pointwise_product R₁ R₂). +Program Instance pointwise_preorder `(pa : PreOrder A R₁, pb : PreOrder B R₂) + : PreOrder (pointwise_product R₁ R₂). hunk ./CartesianProduct.v 44 -Program Instance [ pa : Equivalence A R₁, pb : Equivalence B R₂ ] => - pointwise_equivalence : Equivalence (A * B) (pointwise_product R₁ R₂). +Program Instance pointwise_equivalence `(pa : Equivalence A R₁, pb : Equivalence B R₂) + : Equivalence (pointwise_product R₁ R₂). hunk ./CartesianProduct.v 49 -Instance [ pa : PartialOrder A eqA R₁, pb : PartialOrder B eqB R₂ ] => - pointwise_partial_order : ! PartialOrder (A * B) (pointwise_product eqA eqB) (pointwise_product R₁ R₂). +Instance pointwise_partial_order `(pa : PartialOrder A eqA R₁, pb : PartialOrder B eqB R₂) + : PartialOrder (pointwise_product eqA eqB) (pointwise_product R₁ R₂). hunk ./CartesianProduct.v 56 -Definition lexicographic_product {A} (R₁ : relation A) [ pa : PartialOrder A eqA R₁ ] {B} (R₂ : relation B) : relation (A * B) := +Definition lexicographic_product {A} (R₁ : relation A) `{pa : PartialOrder A eqA R₁} + {B} (R₂ : relation B) : relation (A * B) := hunk ./CartesianProduct.v 63 -Program Instance [ pa : PartialOrder A eqA R₁, pb : PreOrder B R₂ ] => - lexicographic_preorder : PreOrder (A * B) (lexicographic_product R₁ R₂). +Program Instance lexicographic_preorder `(pa : PartialOrder A eqA R₁, pb : PreOrder B R₂) + : PreOrder (lexicographic_product R₁ R₂). hunk ./CartesianProduct.v 87 -Instance [ pa : PartialOrder A eqA R₁, pb : PartialOrder B eqB R₂ ] => - lexicographic_partial_order : ! PartialOrder (A * B) (pointwise_product eqA eqB) (lexicographic_product R₁ R₂). +Instance lexicographic_partial_order `(pa : PartialOrder A eqA R₁, pb : PartialOrder B eqB R₂) + : PartialOrder (pointwise_product eqA eqB) (lexicographic_product R₁ R₂). hunk ./CartesianProduct.v 92 - destruct_conjs. split ; right ; intuition order. + destruct_conjs. split ; right ; intuition order. rewrite H0 ; reflexivity. + symmetry ; auto. rewrite H0 ; reflexivity. hunk ./CartesianProduct.v 101 - rewrite H0 in H. order. + rewrite H0 in H. elim (irreflexivity H). hunk ./CartesianProduct.v 104 - rewrite H in H0. order. - firstorder order. + rewrite H in H0. elim (irreflexivity H0). + rewrite (antisymmetry H1 HR). now rewrite Heq. hunk ./CartesianProduct.v 109 - -Instance [ pa : PartialOrder A eqA ordA, pb : PartialOrder B eqB ordB, - acca : ! DescendingChainCondition pa, accb : ! DescendingChainCondition pb ] => - lexicographic_dcc : - DescendingChainCondition (lexicographic_partial_order (pa:=pa) (pb:=pb)). + +Instance lexicographic_dcc `{pa : PartialOrder A eqA ordA, pb : PartialOrder B eqB ordB} + `{acca : ! DescendingChainCondition pa, accb : ! DescendingChainCondition pb} + : DescendingChainCondition (lexicographic_partial_order pa pb). hunk ./CartesianProduct.v 134 - apply IHAcc'. order. + apply IHAcc'. split ; auto. hunk ./CartesianProduct.v 142 -Instance well_founded_subrelation_morphism : Morphism (subrelation --> impl) (@well_founded A). +Instance well_founded_subrelation_morphism : Proper (subrelation --> impl) (@well_founded A). hunk ./CartesianProduct.v 149 -Lemma subrelation_wf [ sa : StrictOrder A eqA (equ:=equ) ordA, sb : ! StrictOrder equ ordB, - subrelation _ ordB ordA, acca : ! WellFounded sa ] : +Lemma subrelation_wf `(sa : StrictOrder A eqA (equ:=equ) ordA, sb : ! StrictOrder (equ:=equ) ordB, + subrelation _ ordB ordA, acca : ! WellFounded sa) : hunk ./CartesianProduct.v 157 -Lemma subrelation_dsc [ pa : PartialOrder A eqA (equ:=equ) ordA, pb : PartialOrder A eqA (equ:=equ) ordB, - subrelation _ ordB ordA, acca : ! DescendingChainCondition pa ] : +Lemma subrelation_dsc `(pa : PartialOrder A eqA (equ:=equ) ordA, pb : PartialOrder A eqA (equ:=equ) ordB, + subrelation _ ordB ordA, acca : ! DescendingChainCondition pa) : hunk ./CartesianProduct.v 161 - intros. clapply subrelation_wf. firstorder. + intros. eapply subrelation_wf; firstorder. hunk ./CartesianProduct.v 164 -Lemma lexicographic_pointwise [ pa : PartialOrder A eqA ordA, pb : PartialOrder B eqB ordB ] : +Lemma lexicographic_pointwise `{pa : PartialOrder A eqA ordA, pb : PartialOrder B eqB ordB} : hunk ./CartesianProduct.v 173 -Instance [ pa : PartialOrder A eqA ordA, pb : PartialOrder B eqB ordB, - acca : ! DescendingChainCondition pa, accb : ! DescendingChainCondition pb ] => - DescendingChainCondition (pointwise_partial_order (pa:=pa) (pb:=pb)). +Instance dcc_pointwise `(pa : PartialOrder A eqA ordA, pb : PartialOrder B eqB ordB, + acca : ! DescendingChainCondition pa, accb : ! DescendingChainCondition pb) +: DescendingChainCondition (pointwise_partial_order pa pb). hunk ./CartesianProduct.v 177 - intros. refine (subrelation_dsc (pa:=lexicographic_partial_order (pa:=pa) (pb:=pb))). - clapply lexicographic_pointwise. - clapply lexicographic_dcc. + intros. apply (subrelation_dsc (lexicographic_partial_order pa pb)). + apply lexicographic_pointwise. + apply lexicographic_dcc. hunk ./Lattice.v 254 - Hint Extern 2 (PreOrder ?X) => check_not_inverse_evar X ; - class_apply preorder_dual : typeclass_instances. - hunk ./Lattice.v 257 - unfold JoinSemiLattice in js. Typeclasses eauto := debug. - pose (meet_semi_commutative x y). - apply (meet_semi_le_meet (m:=js) y x). + unfold JoinSemiLattice in js. + rewrite <- (meet_semi_commutative y x). + pose (meet_semi_le_meet y x). apply i. hunk ./Lattice.v 275 -Class [ po : PartialOrder A eqA ord, +Class Lattice `(po : PartialOrder A eqA ord, hunk ./Lattice.v 277 - js : ! JoinSemiLattice po join ] => Lattice. + js : ! JoinSemiLattice po join). hunk ./Lattice.v 280 - Context [ la : Lattice A eqA ord meet join ]. + Context `{la : Lattice A eqA ord meet join}. hunk ./Lattice.v 288 - unfold flip, le in * ; orderify. + unfold flip, le in *. hunk ./Lattice.v 323 -Class [ ms : MeetSemiLattice A (po:=po) ] => BoundedMeetSemiLattice (bound : A) := - bounded_sup :> Supremum po bound ; - meet_semi_neutral : neutral meet bound. +Class BoundedMeetSemiLattice `(ms : MeetSemiLattice A (po:=po)) (bound : A) := + { bounded_sup :> Supremum po bound ; + meet_semi_neutral : neutral meet bound }. hunk ./Lattice.v 327 -Class [ js : JoinSemiLattice A (po:=po) ] => BoundedJoinSemiLattice (bound : A) := +Class BoundedJoinSemiLattice `(js : JoinSemiLattice A (po:=po)) (bound : A) := hunk ./Lattice.v 330 -Class [ Lattice A (po:=po) (ms:=ms) (js:=js), - ! BoundedMeetSemiLattice ms la_sup, ! BoundedJoinSemiLattice js la_inf ] => BoundedLattice. +Class BoundedLattice `(Lattice A (po:=po) (ms:=ms) (js:=js), + ! BoundedMeetSemiLattice ms la_sup, ! BoundedJoinSemiLattice js la_inf). hunk ./Lattice.v 335 -Class `(PartialOrder A) => Glb (glb : subset A -> A -> Prop) := +Class Glb `(po : PartialOrder A) (glb : subset A -> A -> Prop) := hunk ./Lattice.v 338 -Class `(PartialOrder A) => Lub (lub : subset A -> A -> Prop) := - lub_glb :> Glb partial_order_dual lub. +Class Lub `(po : PartialOrder A) (lub : subset A -> A -> Prop) := + lub_glb :> Glb (partial_order_dual po) lub. hunk ./Lattice.v 346 - glb_meet :> Glb po meet ; - binary_glb : forall x y, ex (meet (Couple _ x y)). + { glb_meet :> Glb po meet ; + binary_glb : forall x y, ex (meet (Couple _ x y)) }. hunk ./Lattice.v 350 - inf_join_is_meet :> InfMeetSemiLattice partial_order_dual join. + inf_join_is_meet :> InfMeetSemiLattice (partial_order_dual po) join. hunk ./Lattice.v 352 -Definition binary_lub [ InfJoinSemiLattice A ] := +Definition binary_lub `{InfJoinSemiLattice A} := hunk ./Lattice.v 357 -Class [ po : PartialOrder A, ms : ! InfMeetSemiLattice po meet, - js : ! InfJoinSemiLattice po join ] => InfLattice. +Class InfLattice `(po : PartialOrder A, ms : ! InfMeetSemiLattice po meet, + js : ! InfJoinSemiLattice po join). hunk ./Lattice.v 362 -Class [ pa : PartialOrder A, pb : PartialOrder B, ! Monotone pa pb alpha, ! Monotone pb pa gamma ] => - AbstractInterpretation (f : A -> A) (f' : B -> B) := +Class AbstractInterpretation `(pa : PartialOrder A, pb : PartialOrder B) alpha gamma + `{! Monotone pa pb alpha, ! Monotone pb pa gamma} (f : A -> A) (f' : B -> B) := hunk ./Lattice.v 368 -Program Definition complete [ Morphism (A -> B) (eqA ==> eqB) m ] +Program Definition complete `{Proper (A -> B) (eqA ==> eqB) m} hunk ./Lattice.v 372 -Class [ la : Lattice A ] => CompleteLattice := +Class CompleteLattice `(la : Lattice A) := hunk ./Lattice.v 375 -Class [ la : InfLattice A (join:=join) ] => CompleteInfLattice := +Class CompleteInfLattice `(la : InfLattice A (join:=join)) := hunk ./Lattice.v 380 - Context [ js : InfJoinSemiLattice A eqA ordA join ]. + Context `{js : InfJoinSemiLattice A eqA ordA join}. hunk ./Lattice.v 415 - Context [ cla : CompleteInfLattice A eqA ordA meet join ]. + Context `{cla : CompleteInfLattice A eqA ordA meet join}. hunk ./Lattice.v 431 - Instance Inhabited A. + Instance: Inhabited A. hunk ./Lattice.v 451 -Instance [ po : PartialOrder A eqA ] => - Morphism (subset_equality ==> eqA ==> iff) least_upper_bound. +Instance lub_mor `(po : PartialOrder A eqA) : + Proper (subset_equality ==> eqA ==> iff) least_upper_bound. hunk ./Lattice.v 496 - Context [ po : PartialOrder A eqA ordA ]. + Context `{po : PartialOrder A eqA ordA}. hunk ./Lattice.v 555 - full_finite : Finite A full_subset. + full_finite : Finite_sets.Finite A full_subset. hunk ./Lattice.v 557 -Lemma finite_subsets [ Finite A ] : forall (s : subset A), Finite_sets.Finite A s. +Lemma finite_subsets `{Finite A} : forall (s : subset A), Finite_sets.Finite A s. hunk ./Lattice.v 564 -Class [ la : InfLattice A ] => FiniteLattice := +Class FiniteLattice `(la : InfLattice A) := hunk ./Lattice.v 566 + hunk ./Order.v 49 -Tactic Notation "class_apply_once" ident(c) := - match goal with - | [ _ : @applied _ ?T |- _ ] => match T with c => fail 2 | _ => fail 1 end - | _ => let H := fresh "applied" in assert(H:=@is_applied _ c) ; class_apply c - end. +Tactic Notation "class_apply_once" ident(c) := class_apply c ; trivial. + (* match goal with *) + (* | [ _ : @applied _ ?T |- _ ] => match T with c => fail 2 | _ => fail 1 end *) + (* | _ => let H := fresh "applied" in assert(H:=@is_applied _ c) ; class_apply c *) + (* end. *) hunk ./Order.v 170 -Hint Extern 2 (StrictOrder _) => class_apply_once strict_order_dual : typeclass_instances. +Hint Extern 2 (StrictOrder _) => solve [ class_apply @strict_order_dual ] : typeclass_instances. hunk ./Order.v 204 -Next Obligation. -Proof. destruct (compare x y) ; intuition. Qed. - + Next Obligation. + Proof. destruct (compare x y) ; intuition. Qed. + hunk ./Order.v 417 -Print Hint PreOrder. -Typeclasses eauto := debug. - -Ltac show_goal := match goal with [ |- ?T ] => idtac T end. - -Ltac show_hyp id := - match goal with - | [ H := ?b : ?T |- _ ] => - match H with - | id => idtac id ":=" b ":" T - end - | [ H : ?T |- _ ] => - match H with - | id => idtac id ":" T - end - end. - -Ltac show_hyps := - try match reverse goal with - | [ H : ?T |- _ ] => show_hyp H ; fail - end. - - -Hint Extern 2 (PartialOrder _ _) => show_hyps ; rapply @partial_order_dual : typeclass_instances. hunk ./Order.v 418 - -Lemma flip_restriction : forall `(po : PartialOrder A eqA ord) (x y : A), True. - intros. - Check (flip (partial_order_restriction ord) x y). Check (partial_order_restriction (flip ord)). +Lemma flip_restriction : forall `(po : PartialOrder A eqA ord) (x y : A), + flip (partial_order_restriction ord) x y === partial_order_restriction (flip ord) x y. hunk ./Order.v 479 + +About partial_order_restriction_strict. hunk ./Order.v 488 -Hint Extern 2 (StrictOrder _) => class_apply_once @partial_order_restriction_strict : +Hint Extern 2 (StrictOrder _) => class_apply_once partial_order_restriction_strict : hunk ./Order.v 523 -Hint Extern 3 (PreOrder _) => class_apply_once @strict_order_extension_preorder : typeclass_instances. +Hint Extern 3 (PreOrder _) => class_apply_once strict_order_extension_preorder : typeclass_instances. hunk ./Order.v 532 - class_apply_once @strict_order_extension_partial_order : typeclass_instances. + class_apply_once strict_order_extension_partial_order : typeclass_instances.