Library Signatures
Require Export Wf.
Require Export Relation_Operators.
Require Export ZArith.
Require Export OrderedType_def.
Module Type Poset.
Parameter t : Set.
Parameter eq : t -> t -> Prop.
Parameter eq_refl : forall x : t, eq x x.
Parameter eq_sym : forall x y : t, eq x y -> eq y x.
Parameter eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
Parameter eq_dec : forall x y : t, {eq x y}+{~ eq x y}.
Parameter order : t -> t -> Prop.
Parameter order_refl : forall x y : t, eq x y -> order x y.
Parameter order_antisym : forall x y : t, order x y -> order y x -> eq x y.
Parameter order_trans : forall x y z : t, order x y -> order y z -> order x z.
Parameter order_dec : forall x y : t, {order x y}+{~ order x y}.
Hint Resolve eq_refl eq_sym eq_trans order_refl order_antisym order_trans.
End Poset.
Module Type PosetBottom.
Parameter t : Set.
Parameter eq : t -> t -> Prop.
Parameter eq_refl : forall x : t, eq x x.
Parameter eq_sym : forall x y : t, eq x y -> eq y x.
Parameter eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
Parameter eq_dec : forall x y : t, {eq x y}+{~ eq x y}.
Parameter order : t -> t -> Prop.
Parameter order_refl : forall x y : t, eq x y -> order x y.
Parameter order_antisym : forall x y : t, order x y -> order y x -> eq x y.
Parameter order_trans : forall x y z : t, order x y -> order y z -> order x z.
Parameter order_dec : forall x y : t, {order x y}+{~ order x y}.
Parameter bottom : t.
Parameter bottom_is_bottom : forall x : t, order bottom x.
Hint Resolve eq_refl eq_sym eq_trans order_refl order_antisym order_trans bottom bottom_is_bottom.
End PosetBottom.
Module Type PosetWf.
Parameter t : Set.
Parameter eq : t -> t -> Prop.
Parameter eq_refl : forall x : t, eq x x.
Parameter eq_sym : forall x y : t, eq x y -> eq y x.
Parameter eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
Parameter eq_dec : forall x y : t, {eq x y}+{~ eq x y}.
Parameter order : t -> t -> Prop.
Parameter order_refl : forall x y : t, eq x y -> order x y.
Parameter order_antisym : forall x y : t, order x y -> order y x -> eq x y.
Parameter order_trans : forall x y z : t, order x y -> order y z -> order x z.
Parameter order_dec : forall x y : t, {order x y}+{~ order x y}.
Parameter ascending_chain_condition :
well_founded (fun x y => ~ eq y x /\ order y x).
Hint Resolve eq_refl eq_sym eq_trans order_refl order_antisym order_trans.
End PosetWf.
Module Type Lattice.
Parameter t : Set.
Parameter eq : t -> t -> Prop.
Parameter eq_refl : forall x : t, eq x x.
Parameter eq_sym : forall x y : t, eq x y -> eq y x.
Parameter eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
Parameter eq_dec : forall x y : t, {eq x y}+{~ eq x y}.
Parameter order : t -> t -> Prop.
Parameter order_refl : forall x y : t, eq x y -> order x y.
Parameter order_antisym : forall x y : t, order x y -> order y x -> eq x y.
Parameter order_trans : forall x y z : t, order x y -> order y z -> order x z.
Parameter order_dec : forall x y : t, {order x y}+{~ order x y}.
Parameter join : t -> t -> t.
Parameter join_bound1 : forall x y : t, order x (join x y).
Parameter join_bound2 : forall x y : t, order y (join x y).
Parameter join_least_upper_bound : forall x y z : t, order x z -> order y z -> order (join x y) z.
Parameter meet : t -> t -> t.
Parameter meet_bound1 : forall x y : t, order (meet x y) x.
Parameter meet_bound2 : forall x y : t, order (meet x y) y.
Parameter meet_greatest_lower_bound : forall x y z : t, order z x -> order z y -> order z (meet x y).
Parameter bottom : t.
Parameter bottom_is_bottom : forall x : t, order bottom x.
Hint Resolve eq_refl eq_sym eq_trans
order_refl order_antisym order_trans
join_bound1 join_bound2 join_least_upper_bound
meet_bound1 meet_bound2 meet_greatest_lower_bound
bottom_is_bottom.
End Lattice.
Module Type LatticeWf.
Parameter t : Set.
Parameter eq : t -> t -> Prop.
Parameter eq_refl : forall x : t, eq x x.
Parameter eq_sym : forall x y : t, eq x y -> eq y x.
Parameter eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
Parameter eq_dec : forall x y : t, {eq x y}+{~ eq x y}.
Parameter order : t -> t -> Prop.
Parameter order_refl : forall x y : t, eq x y -> order x y.
Parameter order_antisym : forall x y : t, order x y -> order y x -> eq x y.
Parameter order_trans : forall x y z : t, order x y -> order y z -> order x z.
Parameter order_dec : forall x y : t, {order x y}+{~ order x y}.
Parameter join : t -> t -> t.
Parameter join_bound1 : forall x y : t, order x (join x y).
Parameter join_bound2 : forall x y : t, order y (join x y).
Parameter join_least_upper_bound : forall x y z : t, order x z -> order y z -> order (join x y) z.
Parameter meet : t -> t -> t.
Parameter meet_bound1 : forall x y : t, order (meet x y) x.
Parameter meet_bound2 : forall x y : t, order (meet x y) y.
Parameter meet_greatest_lower_bound : forall x y z : t, order z x -> order z y -> order z (meet x y).
Parameter bottom : t.
Parameter bottom_is_bottom : forall x : t, order bottom x.
Hint Resolve eq_refl eq_sym eq_trans
order_refl order_antisym order_trans
join_bound1 join_bound2 join_least_upper_bound
meet_bound1 meet_bound2 meet_greatest_lower_bound
bottom_is_bottom.
Parameter ascending_chain_condition :
well_founded (fun x y => ~ eq y x /\ order y x).
End LatticeWf.
Module Type PosetWiden.
Parameter t : Set.
Parameter eq : t -> t -> Prop.
Parameter eq_refl : forall x : t, eq x x.
Parameter eq_sym : forall x y : t, eq x y -> eq y x.
Parameter eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
Parameter eq_dec : forall x y : t, {eq x y}+{~ eq x y}.
Parameter order : t -> t -> Prop.
Parameter order_refl : forall x y : t, eq x y -> order x y.
Parameter order_antisym : forall x y : t, order x y -> order y x -> eq x y.
Parameter order_trans : forall x y z : t, order x y -> order y z -> order x z.
Parameter order_dec : forall x y : t, {order x y}+{~ order x y}.
Parameter widen : t -> t -> t.
Definition widen_rel : (t*t) -> (t*t) -> Prop := fun x y =>
order (fst y) (fst x) /\
eq (snd x) (widen (snd y) (fst x)) /\
~ eq (snd y) (snd x).
Parameter widen_bound1 : forall x y : t, order x (widen x y).
Parameter widen_bound2 : forall x y : t, order y (widen x y).
Parameter widen_eq1 : forall x y z: t,
eq x y -> eq (widen x z) (widen y z).
Parameter widen_eq2 : forall x y z: t,
eq x y -> eq (widen z x) (widen z y).
Parameter widen_acc_property : forall x:t, Acc widen_rel (x,x).
Hint Resolve eq_refl eq_sym eq_trans order_refl order_antisym order_trans widen_bound1 widen_bound2 widen_eq1 widen_eq2.
End PosetWiden.
Module option.
Section A.
Variable A : Set.
Inductive eq (P : A -> A -> Prop) : option A -> option A -> Prop :=
eq_none : eq P None None
| eq_some : forall x y : A, P x y -> eq P (Some x) (Some y).
Inductive order (P : A -> A -> Prop) : A -> option A -> Prop :=
order_none : forall x : A, order P x None
| order_some : forall x y : A, P x y -> order P x (Some y).
End A.
Implicit Arguments eq [A].
Implicit Arguments order [A].
End option.
Module Type PosetPartialWiden.
Parameter t : Set.
Parameter eq : t -> t -> Prop.
Parameter eq_refl : forall x : t, eq x x.
Parameter eq_sym : forall x y : t, eq x y -> eq y x.
Parameter eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
Parameter eq_dec : forall x y : t, {eq x y}+{~ eq x y}.
Parameter order : t -> t -> Prop.
Parameter order_refl : forall x y : t, eq x y -> order x y.
Parameter order_antisym : forall x y : t, order x y -> order y x -> eq x y.
Parameter order_trans : forall x y z : t, order x y -> order y z -> order x z.
Parameter order_dec : forall x y : t, {order x y}+{~ order x y}.
Parameter widen : t -> t -> option t.
Parameter widen_bound1 : forall x y : t,
option.order order x (widen x y).
Parameter widen_bound2 : forall x y : t,
option.order order y (widen x y).
Parameter widen_eq1 : forall x y z: t,
eq x y -> option.eq eq (widen x z) (widen y z).
Parameter widen_eq2 : forall x y z: t,
eq x y -> option.eq eq (widen z x) (widen z y).
Definition widen_rel : (t*t) -> (t*t) -> Prop := fun x y =>
order (fst y) (fst x) /\
option.eq eq (Some (snd x)) (widen (snd y) (fst x)) /\
~ eq (snd y) (snd x).
Parameter widen_acc_property : forall x:t, Acc widen_rel (x,x).
Hint Resolve eq_refl eq_sym eq_trans order_refl order_antisym order_trans widen_bound1 widen_bound2 widen_eq1.
End PosetPartialWiden.
Module Type PosetWidenBottom.
Parameter t : Set.
Parameter eq : t -> t -> Prop.
Parameter eq_refl : forall x : t, eq x x.
Parameter eq_sym : forall x y : t, eq x y -> eq y x.
Parameter eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
Parameter eq_dec : forall x y : t, {eq x y}+{~ eq x y}.
Parameter order : t -> t -> Prop.
Parameter order_refl : forall x y : t, eq x y -> order x y.
Parameter order_antisym : forall x y : t, order x y -> order y x -> eq x y.
Parameter order_trans : forall x y z : t, order x y -> order y z -> order x z.
Parameter order_dec : forall x y : t, {order x y}+{~ order x y}.
Parameter bottom : t.
Parameter bottom_is_bottom : forall x : t, order bottom x.
Parameter widen : t -> t -> t.
Definition widen_rel : (t*t) -> (t*t) -> Prop := fun x y =>
order (fst y) (fst x) /\
eq (snd x) (widen (snd y) (fst x)) /\
~ eq (snd y) (snd x).
Parameter widen_bound1 : forall x y : t, order x (widen x y).
Parameter widen_bound2 : forall x y : t, order y (widen x y).
Parameter widen_eq1 : forall x y z: t,
eq x y -> eq (widen x z) (widen y z).
Parameter widen_eq2 : forall x y z: t,
eq x y -> eq (widen z x) (widen z y).
Parameter widen_bottom1 : forall x : t, eq x (widen x bottom).
Parameter widen_bottom2 : forall x : t, eq x (widen bottom x).
Parameter widen_acc_property : forall x:t, Acc widen_rel (x,x).
Hint Resolve eq_refl eq_sym eq_trans order_refl order_antisym order_trans bottom_is_bottom widen_bound1 widen_bound2 widen_eq1 widen_eq2 widen_bottom1 widen_bottom2.
End PosetWidenBottom.
Module Type LatticeWiden.
Parameter t : Set.
Parameter eq : t -> t -> Prop.
Parameter eq_refl : forall x : t, eq x x.
Parameter eq_sym : forall x y : t, eq x y -> eq y x.
Parameter eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
Parameter eq_dec : forall x y : t, {eq x y}+{~ eq x y}.
Parameter order : t -> t -> Prop.
Parameter order_refl : forall x y : t, eq x y -> order x y.
Parameter order_antisym : forall x y : t, order x y -> order y x -> eq x y.
Parameter order_trans : forall x y z : t, order x y -> order y z -> order x z.
Parameter order_dec : forall x y : t, {order x y}+{~ order x y}.
Parameter join : t -> t -> t.
Parameter join_bound1 : forall x y : t, order x (join x y).
Parameter join_bound2 : forall x y : t, order y (join x y).
Parameter join_least_upper_bound : forall x y z : t, order x z -> order y z -> order (join x y) z.
Parameter meet : t -> t -> t.
Parameter meet_bound1 : forall x y : t, order (meet x y) x.
Parameter meet_bound2 : forall x y : t, order (meet x y) y.
Parameter meet_greatest_lower_bound : forall x y z : t, order z x -> order z y -> order z (meet x y).
Parameter bottom : t.
Parameter bottom_is_bottom : forall x : t, order bottom x.
Parameter widen : t -> t -> t.
Definition widen_rel : (t*t) -> (t*t) -> Prop := fun x y =>
order (fst y) (fst x) /\
eq (snd x) (widen (snd y) (fst x)) /\
~ eq (snd y) (snd x).
Parameter widen_bound1 : forall x y : t, order x (widen x y).
Parameter widen_bound2 : forall x y : t, order y (widen x y).
Parameter widen_eq1 : forall x y z: t,
eq x y -> eq (widen x z) (widen y z).
Parameter widen_eq2 : forall x y z: t,
eq x y -> eq (widen z x) (widen z y).
Parameter widen_bottom1 : forall x : t, eq x (widen x bottom).
Parameter widen_bottom2 : forall x : t, eq x (widen bottom x).
Parameter widen_acc_property : forall x:t, Acc widen_rel (x,x).
Hint Resolve eq_refl eq_sym eq_trans order_refl order_antisym order_trans widen_bound1 widen_bound2 widen_eq1 widen_eq2
join_bound1 join_bound2 join_least_upper_bound
meet_bound1 meet_bound2 meet_greatest_lower_bound
bottom bottom_is_bottom.
End LatticeWiden.
Open Scope Z_scope.
Module Type SetSign.
Parameter t : Set.
Parameter eq : t -> t -> Prop.
Parameter eq_refl : forall x : t, eq x x.
Parameter eq_sym : forall x y : t, eq x y -> eq y x.
Parameter eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
Parameter eq_dec : forall x y : t, {eq x y}+{~ eq x y}.
Hint Resolve eq_refl eq_sym eq_trans.
End SetSign.
Module Type FiniteSet.
Parameter t : Set.
Parameter eq : t -> t -> Prop.
Parameter eq_refl : forall x : t, eq x x.
Parameter eq_sym : forall x y : t, eq x y -> eq y x.
Parameter eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
Parameter eq_dec : forall x y : t, {eq x y}+{~ eq x y}.
Parameter cardinal : Z.
Parameter cardinal_positive : cardinal > 0.
Parameter inject : t -> Z.
Parameter nat2t : Z -> t.
Parameter inject_bounded : forall x : t, 0 <= (inject x) < cardinal.
Parameter inject_nat2t : forall n : Z,
0 <= n < cardinal -> inject (nat2t n) = n.
Parameter inject_injective : forall x y : t, inject x = inject y -> eq x y.
Parameter inject_comp_eq : forall x y : t, eq x y -> inject x = inject y.
Hint Resolve eq_refl eq_sym eq_trans cardinal_positive.
End FiniteSet.
Module Type FiniteSetOT.
Parameter t : Set.
Parameter eq : t -> t -> Prop.
Parameter eq_refl : forall x : t, eq x x.
Parameter eq_sym : forall x y : t, eq x y -> eq y x.
Parameter eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
Parameter eq_dec : forall x y : t, {eq x y}+{~ eq x y}.
Parameter cardinal : Z.
Parameter cardinal_positive : cardinal > 0.
Parameter inject : t -> Z.
Parameter nat2t : Z -> t.
Parameter inject_bounded : forall x : t, 0 <= (inject x) < cardinal.
Parameter inject_nat2t : forall n : Z,
0 <= n < cardinal -> inject (nat2t n) = n.
Parameter inject_injective : forall x y : t, inject x = inject y -> eq x y.
Parameter inject_comp_eq : forall x y : t, eq x y -> inject x = inject y.
Hint Resolve eq_refl eq_sym eq_trans cardinal_positive.
Declare Module OT : OrderedType
with Definition t := t
with Definition eq := eq.
End FiniteSetOT.
Index
This page has been generated by coqdoc