# 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
end
end.
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).

## cardinal

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).

## folding

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
end.

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.

## instances

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
end.
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.

option

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
end.
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.

unit

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
end.
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.