Library Common

Various utilities

Require Export Bool List Setoid Morphisms Compare_dec.
Require Import Relations Wellfounded.
Require Import Arith MinMax.

currying uncurrying

Definition curry A B C (f: A -> B -> C): A*B -> C := fun xy => let (x,y) := xy in f x y.
Definition uncurry A B C (f: A * B -> C): A -> B -> C := fun x y => f (x,y).

lexicographic ordering

Definition lex a b := (match a with Eq => b | r => r end).

Lemma lex_lt a b: lex a b = Lt <-> a=Lt \/ (a=Eq /\ b=Lt).

Lemma lex_eq a b: lex a b=Eq <-> (a=Eq /\ b=Eq).

Lemma lex_sym a b: lex a b=CompOpp(lex (CompOpp a) (CompOpp b)).

comparison functions

Class Cmp X (cmp: X -> X -> comparison) := {
 cmp_eq: forall x y, cmp x y = Eq <-> x=y;
 cmp_sym: forall x y, cmp x y = CompOpp (cmp y x);
 cmp_trans: forall x y z, cmp x y = Lt -> cmp y z = Lt -> cmp x z = Lt

Instance Cmp_nat_compare: Cmp nat_compare.

Lemma cmp_refl `{Cmp}: forall x, cmp x x = Eq.

Lemma cmp_irrefl `{Cmp}: forall x y, cmp x y = Lt -> x<>y.

List sorting

Section sort.
 Variable X: Set.
 Variable cmp: X -> X -> comparison.
 Context {H: Cmp cmp}.
 Fixpoint insert x l :=
   match l with
     | nil => x::nil
     | y::q =>
       match cmp x y with
         | Eq => l
         | Lt => x::l
         | Gt => y::insert x q
 Definition sort := fold_right insert nil.
 Inductive sorted: list X -> Prop :=
 | s_nil: sorted nil
 | s_cons: forall x q, (forall y, In y q -> cmp x y = Lt) -> sorted q -> sorted (x::q).
 Lemma In_insert x y q: In y (insert x q) <-> In y (x::q).
 Lemma In_sort y l: In y (sort l) <-> In y l.
 Lemma s_insert x q: sorted q -> sorted (insert x q).
 Lemma sorted_sort l: sorted (sort l).
 Lemma sorted_app h k: sorted h -> sorted k ->
   (forall x, In x h -> forall y, In y k -> cmp x y = Lt) -> sorted (h++k).
End sort.
Implicit Arguments sorted_sort [[X] [cmp] [H]].
Implicit Arguments In_sort [[X] [cmp] [H]].

Lemma sorted_map (X: Set) xcmp {Cx: @Cmp X xcmp} (Y: Set) ycmp {Cy: @Cmp Y ycmp} (f: X -> Y) l:
  sorted xcmp l -> (forall x y, ycmp (f x) (f y) = xcmp x y) -> sorted ycmp (map f l).

Finite/ordered/foldable sets

Class FSet := mk_fset {
  carr: Set;
  cmp: carr -> carr -> comparison;
  elements: list carr;
  cmp_spec:> Cmp cmp;
  sorted_elements: sorted cmp elements;
  all_elements: forall x, In x elements
Coercion carr: FSet >-> Sortclass.
Coercion elements: FSet >-> list.

Definition cmp_bool c := match c with Eq => true | _ => false end.
Definition eqc {X: FSet} x y := cmp_bool (cmp x y).
Infix "?=" := eqc (at level 70).

Lemma eq_spec {X: FSet} x y: reflect (x=y) (eqc x y).

Lemma eqc_refl {X: FSet} (x: X): (x?=x) = true.

Lemma eqc_comm {X: FSet} (x y: X): (x?=y) = (y?=x).


Definition cardinal (X: FSet) := length elements.

Section fs.
 Context {X: FSet} {A: Type}.

list membership

 Fixpoint mem (x: X) l := match l with nil => false | y::q => (y?=x) || mem x q end.
 Lemma mem_in: forall x l, In x l <-> mem x l = true.

 Definition mem_spec x l := iff_reflect _ _ (mem_in x l).


 Definition fold f (a: A) := fold_right f a elements.

weak, non dependent, specification

 Lemma fold_wspec (P: A -> Prop) f:
   (forall x a, P a -> P (f x a)) ->
   forall a, P a -> P (fold f a).

dependent specification

 Lemma fold_spec (P: (carr -> Prop) -> A -> Prop) f:
   (forall x done a, P done a -> ~done x -> P (fun y => x=y \/ done y) (f x a)) ->
   forall a, P (fun _ => False) a -> P (fun x => In x elements) (fold f a).

 Lemma fold_compat: Proper (pointwise_relation X (pointwise_relation A eq) ==> eq ==> eq) fold.

finite maps

 Definition set (x: X) (a: A) (f: X -> A): X -> A := fun y => if x ?= y then a else f y.

 Lemma set_spec x a f y: x=y /\ set x a f y = a \/ x<>y /\ set x a f y = f y.

 Lemma set_neq a x y f: x<>y -> set x a f y = f y.

 Lemma set_idem a x f: set x a f x = a.

 Lemma set_same_commute a x y z f: set x a (set y a f) z = set y a (set x a f) z.

 Lemma set_neq_commute a b x y z f: x<>y -> set x a (set y b f) z = set y b (set x a f) z.

End fs.

Ltac set_case :=
  match goal with
   | |- context[set ?x ?a ?f ?x'] =>
      let H := fresh "H" in
        destruct (set_spec x a f x') as [[? H]|[? H]];
          try subst; try rewrite H in *; trivial; try congruence

Ltac fold_spec P := apply (fold_spec P); [|tauto|apply all_elements].

Section e.
 Context {X: FSet} {A: Type}.

existential quantification

 Definition exists_ (p: X -> bool) := fold (fun x acc => acc || p x) false.

 Lemma exists_iff (p: X -> bool): exists_ p = true <-> exists x, p x = true.

 Lemma exists_spec (p: X -> bool): reflect (exists x, p x = true) (exists_ p).

End e.


cartesian product

Section c.
 Context {X} {xcmp} {Cx: @Cmp X xcmp} {Y} {ycmp} {Cy: @Cmp Y ycmp}.
 Definition cmp_prod (a b: X*Y) := lex (xcmp (fst a) (fst b)) (ycmp (snd a) (snd b)).
 Global Instance Cmp_prod: Cmp cmp_prod.
End c.
Definition elements_prod {X Y: FSet}: list (X*Y) :=
  fold (fun x a => map (fun y => (x,y)) elements ++ a) nil.
Program Definition fset_prod {X Y: FSet}: FSet := {|
  carr := X*Y;
  cmp := @cmp_prod _ cmp _ cmp;
  elements := elements_prod
Canonical Structure fset_prod.

disjoint union

Section u.
 Context {X} {xcmp} {Cx: @Cmp X xcmp} {Y} {ycmp} {Cy: @Cmp Y ycmp}.
 Definition cmp_sum (a b: X+Y) :=
   match a,b with
     | inl x,inl x' => xcmp x x'
     | inr y, inr y' => ycmp y y'
     | inl _, inr _ => Lt
     | inr _, inl _ => Gt
 Global Instance Cmp_sum: Cmp cmp_sum.
End u.
Definition elements_sum {X Y: FSet} := map (@inl X Y) elements ++ map (@inr X Y) elements.
Program Definition fset_sum {X Y: FSet}: FSet := {|
  carr := X+Y;
  cmp := @cmp_sum _ cmp _ cmp;
  elements := elements_sum
Canonical Structure fset_sum.


Section o.
 Context {X} {xcmp} {Cx: @Cmp X xcmp}.
 Definition cmp_option (a b: option X) :=
   match a,b with
     | Some x,Some x' => xcmp x x'
     | None, None => Eq
     | Some _, None => Lt
     | None, Some _ => Gt
 Global Instance Cmp_option: Cmp cmp_option.
End o.
Definition elements_option {X: FSet} := map (@Some X) elements ++ None::nil.
Program Definition fset_option {X: FSet}: FSet := {|
  carr := option X;
  cmp := @cmp_option _ cmp;
  elements := elements_option
Canonical Structure fset_option.


Definition cmp_unit (_ _: unit) := Eq.
Definition elements_unit := tt::nil.
Program Definition fset_unit: FSet := {|
  carr := unit;
  cmp := cmp_unit;
  elements := elements_unit
Canonical Structure fset_unit.

Topological sorting on acyclic relations on finite sets

Section a.
 Context {X: FSet}.
 Variable r: X -> X -> bool.

 Notation r' := (fun x y => r x y = true).

we define acyclicity as being well-founded

 Definition acyclic := well_founded r'.

ranking function:

  • y has rank 0 if it has no antecedent by r,
  • y has rank S i if its antecedent of maximal rank has rank i.

 Fixpoint xrank n y :=
   match n with O => O | S n =>
   fold (fun x k => if r x y then max k (S (xrank n x)) else k) O
 Definition rank := xrank (cardinal X).

 Lemma xrank_spec: forall x y, r x y = true -> forall n, xrank n x < xrank (S n) y.

utilities to establish the required properties of this ranking function

points_to l y holds if l is a list l_0,...,l_n such that
  • forall i, r l_(i+1) l_i holds,
  • and r l_0 y if l is not empty.

 Inductive points_to: list X -> X -> Prop :=
 | pt_nil: forall y, points_to nil y
 | pt_app: forall x y q, r x y = true -> points_to q x -> points_to (x::q) y.

 Lemma xrank_points_to n: forall y, exists l, points_to l y /\ length l = xrank n y.

 Lemma points_to_trans: forall y l, points_to l y -> forall x, In x l -> clos_trans_n1 _ r' x y.

removing elements from a list

 Fixpoint rem x l := match l with nil => nil | y::q => if x?=y then q else y::rem x q end.
 Lemma length_rem: forall x l, In x l -> length l = S (length (rem x l)).
 Lemma in_rem x y l: x<>y -> In x l -> In x (rem y l).

from now on, we suppose that r is acyclic

 Hypothesis Hwf: acyclic.

 Lemma points_to_notin: forall y l, points_to l y -> ~In y l.

 Lemma points_to_cardinal: forall y l, points_to l y -> length l < cardinal X.

 Lemma points_to_rank: forall l y, points_to l y -> length l <= rank y.

key properties of the rank function on acyclic graphs

the rank is always strictly less than the cardinal of the set X

 Theorem rank_cardinal: forall x, rank x < cardinal X.

the ranking function is a morphism from the graph to the strict ordering of natural numbers

 Theorem rank_spec: forall x y, r x y = true -> rank x < rank y.

End a.

additional lemma: any subrelation of an acyclic relation is acyclic

Lemma subrelation_acyclic {X: FSet} (r s: X -> X -> bool):
  acyclic s -> (forall x y, r x y = true -> s x y = true) -> acyclic r.

This page has been generated by coqdoc