NB: This Coq documentation contains a revised version of the Coq implementation of these papers [1], [2], [3], [4], and is also the support for ongoing research. A partial archive (14/01/2001) is available at here. Drop us a line if you are interested in a complete, up-to-date archive.

Library ordset

Require Import ProofIrrelevance.
Require Import eqtype ssrbool seq ssreflect ssrfun.
Require Import Arith_ext seq_ext.
Require Import order.



this files provides:
  • a section that defines ordered sequences
  • a module type for finite sets (equality is the Coq equality)
  • a functor to instantiate finite sets of ordered types

Module OrderedSequence.


Section ordered_sequence.

Variable A : eqType.
Variable ltA : A -> A -> bool.
Notation "x < y" := (ltA x y) : section_ordered_sequence.
Open Local Scope section_ordered_sequence.
Variable ltA_trans : forall n m p, m < n -> n < p -> m < p.
Variable ltA_total : forall m n, (m != n) = (m < n) || (n < m).
Variable ltA_irr : forall a, a < a = false.


strict lower bound of an sequence
Fixpoint lb n (lst : seq A) :=
  match lst with
    | [::] => true
    | h :: t => (n < h) && lb n t
  end.

Lemma lt_lb : forall l m, (forall n, n \in l -> m < n) -> lb m l.

Lemma lb_trans : forall l n m, lb n l -> m < n -> lb m l.

Lemma mem_lt_lb : forall l x, lb x l -> forall y, y \in l -> x < y.

Lemma lb_incl : forall l n, lb n l -> forall f, lb n (filter f l).

Lemma mem_lb : forall l x, lb x l -> ~~ (x \in l).

strict upper bound of an sequence
Definition ub a (k : seq A) : Prop := forall m, m \in k -> m < a.

Lemma mem_ub : forall k a, ub a k -> a \notin k.

Inductive ordered : seq A -> Prop :=
| ord_nil : ordered [::]
| ord_cons : forall lst, ordered lst -> forall a, lb a lst -> ordered (a :: lst).

Lemma ordered_inv : forall h t, ordered (h :: t) -> ordered t /\ lb h t.

Lemma ordered_app_inv : forall (a b : seq A), ordered (a ++ b) ->
  forall x y, x \in a -> y \in b -> ltA x y.

Lemma ordered_singleton : forall x, ordered [:: x].

Lemma ordered_uniq : forall k, ordered k -> uniq k.

Lemma ordered_filter : forall l, ordered l -> forall f, ordered (filter f l).

Lemma ordered_ext : forall (l1 l2 : seq_eqType A),
  ordered l1 -> ordered l2 ->
  (forall x, has (pred1 x) l1 = has (pred1 x) l2) ->
  l1 = l2.

Fixpoint ordered_fix l :=
  match l with
    | [::] => true
    | [:: _] => true
    | h :: t => if lb h t then ordered_fix t else false
  end.

Lemma ordered_fix_inv : forall x l, ordered_fix (x :: l) -> ordered_fix l /\ lb x l.

Lemma ordered_fix_lb : forall l, ordered_fix l -> forall x, lb x l -> ordered_fix (x :: l).

Lemma ordered_fix_ordered : forall l, ordered l <-> ordered_fix l.

Inductive ord_seq : Type := mk_ord_seq : forall l, ordered l -> ord_seq.

Definition ord2seq (v : ord_seq) : seq A := let: mk_ord_seq l _ := v in l.

Lemma mk_ord_seq_pi : forall l l', l = l' ->
  forall (H : ordered l) (H' : ordered l'), mk_ord_seq H = mk_ord_seq H'.

Definition ord_seq_size (s : ord_seq) := size (ord2seq s).

Definition mk_ord_seq_singleton (x : A) := mk_ord_seq (ordered_singleton x).

addition of an element to an ordered sequence (element not added if already present)

Fixpoint add_ord_seq x (lst : seq A) :=
  match lst with
    | [::] => [:: x]
    | h :: t =>
      if x < h then x :: h :: t else
        if x == h then h :: t
          else h :: add_ord_seq x t
  end.

Lemma add_ord_seq_reg : forall (l1 l2:seq A) x,
  ~ x \in l1 -> ~ x \in l2 ->
  add_ord_seq x l1 = add_ord_seq x l2 ->
  l1 = l2.

Lemma add_ord_seq_lb : forall s y, lb y s -> forall x, y < x -> lb y (add_ord_seq x s).

Lemma add_ord_seq_ordered : forall l, ordered l -> forall x, ordered (add_ord_seq x l).

Lemma add_ord_seq_cat : forall l x, lb x l -> add_ord_seq x l = x :: l.

Lemma mem_add_ord_seq : forall l x, x \in (add_ord_seq x l).

Lemma add_ord_seq_add_ord_seq'': forall l n, add_ord_seq n (add_ord_seq n l) = add_ord_seq n l.

Lemma add_ord_seq_add_ord_seq': forall l n n' , n < n' ->
  add_ord_seq n (add_ord_seq n' l) = add_ord_seq n' (add_ord_seq n l).

Lemma add_ord_seq_add_ord_seq: forall l n n' , n <> n' ->
  add_ord_seq n (add_ord_seq n' l) = add_ord_seq n' (add_ord_seq n l).

Lemma add_ord_seq_In: forall k x a, x \in (add_ord_seq a k) -> x = a \/ x \in k.

Definition add : forall (x : A) (l : ord_seq), ord_seq.

the union of two ordered sequences

Fixpoint app_ord_seq (l1 l2 : seq A) { struct l1 } :=
  match l1 with
    | [::] => l2
    | h :: t => add_ord_seq h (app_ord_seq t l2)
  end.

Lemma app_ord_seq_nil : forall l, ordered l -> app_ord_seq l [::] = l.

Lemma app_ord_seq_com : forall l, ordered l -> forall l', ordered l' ->
  app_ord_seq l l' = app_ord_seq l' l.

Lemma app_ord_seq_ordered : forall l1, ordered l1 -> forall l2, ordered l2 -> ordered (app_ord_seq l1 l2).

Definition app : forall (l1 l2 : ord_seq), ord_seq.

Lemma app_com : forall l l', app l l' = app l' l.

disjointness

Definition dis_ord_seq (l1 l2 : ord_seq) := dis (ord2seq l1) (ord2seq l2).

Lemma dis_ord_seq_com : forall l1 l2, dis_ord_seq l1 l2 = dis_ord_seq l2 l1.

element removal

Definition dels_seq (x k : seq A) : seq A := filter (fun y => ~~ (y \in x)) k.

Lemma dels_seq_ordered : forall l, ordered l -> forall x, ordered (dels_seq x l).

Definition dels : forall (x l : ord_seq), ord_seq.

inclusion

Definition inc_ord (l1 l2 : ord_seq) := inc (ord2seq l1) (ord2seq l2).
End ordered_sequence.


Implicit Arguments lb [A].
Implicit Arguments ub [A].
Implicit Arguments mem_lt_lb [A].
Implicit Arguments ordered [A].

End OrderedSequence.

Lemmas only for NatOrder

Lemma lb_seq : forall k n m, NatOrder.ltA n m ->
  OrderedSequence.lb NatOrder.ltA n (l2s (List.seq m k)).

Lemma ordered_seq : forall k n,
  OrderedSequence.ordered NatOrder.ltA (l2s (List.seq n k)).

Section seq_addendum2.
Variable A : eqType.
Variable ltA : A -> A -> bool.
Fixpoint ord_seq_flat (l : seq (seq_eqType (seq_eqType A))) {struct l} : seq (seq_eqType A) :=
  if l is h :: t then OrderedSequence.app_ord_seq _ (lex _ ltA) h (ord_seq_flat t) else [::].
End seq_addendum2.

Module Type ORDSET.
Parameter elt : eqType.
Parameter t : Type.
Parameter singleton : elt -> t.
Parameter add : elt -> t -> t.
Parameter dels : t -> t -> t.
Parameter incl : t -> t -> bool.
Notation "k [<=] m" := (incl k m) (at level 69) : ordset_scope.
Open Local Scope ordset_scope.
Parameter union : t -> t -> t.
Notation "k [U] m" := (union k m) (at level 69) : ordset_scope.
Open Local Scope ordset_scope.
Parameter union_com : forall s s', s [U] s' = s' [U] s.
End ORDSET.

Module OrdSet (O : ORDER) : ORDSET.
Definition elt := O.A.

Import OrderedSequence.

Definition t := ord_seq O.A O.ltA.
Definition singleton (e:elt) := mk_ord_seq_singleton O.A O.ltA e.
Definition add := add O.ltA_trans O.ltA_total.
Definition dels : t -> t -> t := @dels O.A O.ltA.
Definition incl := @inc_ord O.A O.ltA.
Notation "k [<=] m" := (incl k m) (at level 69) : ordset_scope.
Open Local Scope ordset_scope.
Definition union := app O.ltA_trans O.ltA_total.
Notation "k [U] m" := (union k m) (at level 69) : ordset_scope.
Open Local Scope ordset_scope.
Lemma union_com : forall s s', s [U] s' = s' [U] s.
End OrdSet.

Module ordset_of_nat := OrdSet NatOrder.

Module ordset_of_pairs_of_nat := OrdSet pair_nat_order.