# Various utilities

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

## 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).
Proof. destruct a; simpl; intuition discriminate. Qed.

Lemma lex_eq a b: lex a b=Eq <-> (a=Eq /\ b=Eq).
Proof. destruct a; simpl; intuition discriminate. Qed.

Lemma lex_sym a b: lex a b=CompOpp(lex (CompOpp a) (CompOpp b)).
Proof. destruct a; trivial; destruct b; trivial. Qed.

## 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.
Proof.
constructor; intros.
apply nat_compare_eq_iff.
symmetry. case nat_compare_spec; intro; simpl; symmetry.
rewrite nat_compare_eq_iff; auto.
apply nat_compare_gt; auto.
apply nat_compare_lt; auto.
rewrite <- nat_compare_lt in *. eauto with arith.
Qed.

Lemma cmp_refl `{Cmp}: forall x, cmp x x = Eq.
Proof. intro. rewrite cmp_eq. reflexivity. Qed.

Lemma cmp_irrefl `{Cmp}: forall x y, cmp x y = Lt -> x<>y.
Proof. intros x y XY <-. rewrite cmp_refl in XY. discriminate. Qed.

# 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).
Proof.
induction q as [|z q IH]; simpl.
reflexivity.
case_eq (cmp x z); intro Hxz; simpl.
apply cmp_eq in Hxz; subst. tauto.
reflexivity.
rewrite IH. simpl. tauto.
Qed.
Lemma In_sort y l: In y (sort l) <-> In y l.
Proof.
induction l; simpl.
reflexivity.
rewrite In_insert. simpl. rewrite IHl. reflexivity.
Qed.
Lemma s_insert x q: sorted q -> sorted (insert x q).
Proof.
induction 1 as [|y q Hy Hq IH]; simpl.
constructor.
simpl. tauto.
constructor.
case_eq (cmp x y); intro Hxy; constructor; simpl; auto.
intros z [<-|Hz]; eauto using cmp_trans.
constructor; auto.
intros z Hz. rewrite In_insert in Hz. simpl in Hz. destruct Hz as [->|Hz]; auto.
generalize (cmp_sym y z). rewrite Hxy. trivial.
Qed.
Lemma sorted_sort l: sorted (sort l).
Proof.
induction l; simpl.
constructor.
apply s_insert; trivial.
Qed.
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).
Proof.
intros Hh Hk Hhk. induction Hh as [|x q Hx Hq IH]; simpl; auto.
constructor.
intro. rewrite in_app_iff. intros [Hy|Hy]; auto. apply Hhk; simpl; auto.
apply IH. intros ? ?. apply Hhk. right. trivial.
Qed.
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).
Proof.
intros Hl H. induction Hl as [|x q Hx Hq IH]; simpl; constructor; auto.
intros fy Hy. apply in_map_iff in Hy as (y&<-&Hy). rewrite H. auto.
Qed.

# 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).
Proof.
apply iff_reflect. rewrite <- cmp_eq. unfold eqc.
case cmp; simpl; intuition discriminate.
Qed.

Lemma eqc_refl {X: FSet} (x: X): (x?=x) = true.
Proof. unfold eqc. rewrite cmp_refl. reflexivity. Qed.

Lemma eqc_comm {X: FSet} (x y: X): (x?=y) = (y?=x).
Proof. case eq_spec; case eq_spec; congruence. Qed.

## 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.
Proof.
induction l; simpl. intuition discriminate.
rewrite IHl. rewrite (reflect_iff _ _ (eq_spec _ _)). rewrite orb_true_iff. reflexivity.
Qed.

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).
Proof. intro H. unfold fold. induction elements; simpl; auto. Qed.

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).
Proof.
intros Hf a Ha. unfold fold.
induction sorted_elements as [|x q Hq Hs IHs]; simpl.
apply Ha.
apply Hf; auto. intro H. apply Hq in H.
rewrite (proj2 (cmp_eq x x)) in H. discriminate. trivial.
Qed.

Lemma fold_compat: Proper (pointwise_relation X (pointwise_relation A eq) ==> eq ==> eq) fold.
Proof.
unfold fold. intros f g H ? ? <-.
induction elements; simpl; trivial. rewrite IHl. apply H.
Qed.

## 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.
Proof. unfold set; case eq_spec; intuition congruence. Qed.

Lemma set_neq a x y f: x<>y -> set x a f y = f y.
Proof. unfold set. case eq_spec; congruence. Qed.

Lemma set_idem a x f: set x a f x = a.
Proof. unfold set. case eq_spec; congruence. Qed.

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.
Proof. unfold set. case eq_spec; case eq_spec; trivial. Qed.

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.
Proof. unfold set. case eq_spec; case eq_spec; congruence. Qed.

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.
Proof.
unfold exists_. split.
apply fold_wspec.
intros ? [|]; eauto.
discriminate.
intros [x Hx]. fold_spec (fun done l => done x -> l=true).
intros y done a Ha Hy. rewrite orb_true_iff. intros [->|H]; auto.
Qed.

Lemma exists_spec (p: X -> bool): reflect (exists x, p x = true) (exists_ p).
Proof.
apply iff_reflect. symmetry. apply exists_iff.
Qed.

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.
Proof.
unfold cmp_prod. constructor.
intros [? ?]; intros [? ?]; simpl; rewrite lex_eq, 2cmp_eq. intuition congruence.
intros [? ?]; intros [? ?]; simpl; trivial. rewrite lex_sym. setoid_rewrite <- cmp_sym. reflexivity.
intros [? ?]; intros [? ?]; intros [? ?]; simpl; trivial.
rewrite 3lex_lt, 3cmp_eq. intuition try congruence.
left. eauto using @cmp_trans.
right. split. congruence. eauto using @cmp_trans.
Qed.
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
|}.
Next Obligation.
unfold elements_prod, fold.
induction sorted_elements as [|x q Hx Hq IH]; simpl.
constructor.
apply sorted_app.
apply (sorted_map _ sorted_elements). intros. unfold cmp_prod. rewrite cmp_refl. reflexivity.
apply IH.
intros [x' y'] H. apply in_map_iff in H as (y&E&Hxy). injection E. intros <- <-. clear E.
intros [x' y'] H'. cut (In x' q).
intro Hx'. apply Hx in Hx'. unfold cmp_prod. simpl. rewrite Hx'. reflexivity.
revert H'. clear. induction q as [|y q IH]; simpl; trivial.
rewrite in_app_iff. intros [Hy|Hy]; auto.
apply in_map_iff in Hy as (?&?&?). left. congruence.
Qed.
Next Obligation.
rename c into x, c0 into y. unfold elements_prod.
fold_spec (fun done l => done x -> In (x,y) l).
intros x' xdone xl Hxl Hx'. rewrite in_app_iff, in_map_iff. intros [->|Hx]; auto.
eauto using @all_elements.
Qed.
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.
Proof.
constructor.
intros [?|?]; intros [?|?]; simpl; rewrite ?cmp_eq; intuition congruence.
intros [?|?]; intros [?|?]; simpl; trivial; apply cmp_sym.
intros [?|?]; intros [?|?]; intros [?|?]; simpl; trivial; discriminate || apply cmp_trans.
Qed.
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
|}.
Next Obligation.
apply sorted_app.
apply (sorted_map _ sorted_elements). simpl. reflexivity.
apply (sorted_map _ sorted_elements). simpl. reflexivity.
intros x Hx y Hy. apply in_map_iff in Hx as (?&<-&?). apply in_map_iff in Hy as (?&<-&?).
reflexivity.
Qed.
Next Obligation.
apply in_or_app. rewrite 2in_map_iff. destruct x; eauto using @all_elements.
Qed.
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.
Proof.
constructor.
intros [?|]; intros [?|]; simpl; rewrite ?cmp_eq; intuition congruence.
intros [?|]; intros [?|]; simpl; trivial; apply cmp_sym.
intros [?|]; intros [?|]; intros [?|]; simpl; trivial; discriminate || apply cmp_trans.
Qed.
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
|}.
Next Obligation.
apply sorted_app.
apply (sorted_map _ sorted_elements). simpl. reflexivity.
constructor. intros ? []. constructor.
intros x Hx y [<-|[]]. apply in_map_iff in Hx as (?&<-&?). reflexivity.
Qed.
Next Obligation.
apply in_or_app. rewrite in_map_iff. simpl.
destruct x; eauto using @all_elements.
Qed.
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
|}.
Next Obligation.
constructor.
destruct x; destruct y; simpl; tauto.
destruct x; destruct y; simpl; tauto.
destruct x; destruct y; destruct z; simpl; tauto.
Qed.
Next Obligation.
constructor. intros ? []. constructor.
Qed.
Next Obligation.
destruct x; auto.
Qed.
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.
Proof.
intros x y Hxy n. simpl.
fold_spec (fun done m => done x -> xrank n x < m).
intros z done m Hm _ [->|Hx].
rewrite Hxy. apply max_case_strong; auto with arith.
case r; auto. apply max_case_strong; auto with arith.
intro. eapply lt_le_trans; eauto.
Qed.

## 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.
Proof.
induction n; simpl; intro y.
exists nil. split. constructor. reflexivity.
apply fold_wspec.
intros x m (l&Hly&Hlm).
case_eq (r x y); intro Hxy.
apply max_case. eauto. destruct (IHn x) as (q&Hq&Hq').
exists (x::q). split. constructor; trivial. simpl. f_equal. trivial.
eauto.
exists nil. split. constructor. reflexivity.
Qed.

Lemma points_to_trans: forall y l, points_to l y -> forall x, In x l -> clos_trans_n1 _ r' x y.
Proof.
induction 1 as [|x y q Hxy Hq IH]; simpl.
intros _ [].
intros z [<-|Hzq].
constructor. assumption.
econstructor 2; eauto.
Qed.

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)).
Proof.
induction l; simpl.
intros [].
case eq_spec. trivial. simpl. intuition congruence.
Qed.
Lemma in_rem x y l: x<>y -> In x l -> In x (rem y l).
Proof.
intros D Hx. induction l; simpl in *.
destruct Hx.
case eq_spec; simpl; intuition congruence.
Qed.

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.
Proof.
intros y l H1 H2. generalize (points_to_trans H1 _ H2).
clear - Hwf. rewrite <- clos_trans_tn1_iff.
induction y using (well_founded_induction (wf_clos_trans _ _ Hwf)). eauto.
Qed.

Lemma points_to_cardinal: forall y l, points_to l y -> length l < cardinal X.
Proof.
cut (forall y l, points_to l y -> forall e, (forall x, In x (y::l) -> In x e) -> length l < length e).
intros. eapply H; eauto using all_elements.
induction 1 as [|x y q Hx Hq IH]; simpl; intros e He.
destruct e. destruct (He y); auto. simpl. auto with arith.
assert (Hy: ~In y (x::q)). apply points_to_notin. constructor; assumption.
rewrite (length_rem y e) by auto. apply lt_n_S, IH.
intros z Hz. apply in_rem; auto. congruence.
Qed.

Lemma points_to_rank: forall l y, points_to l y -> length l <= rank y.
Proof.
cut (forall l y, points_to l y -> forall e, (forall x, In x (y::l) -> In x e) -> length l <= xrank (length e) y).
intro H. intros. apply H; auto using all_elements.
induction 1 as [|x y q Hx Hq IH]; simpl; intros e He.
auto with arith.
assert (Hy: ~In y (x::q)). apply points_to_notin. constructor; assumption.
rewrite (length_rem y e) by auto.
eapply le_lt_trans. 2: apply xrank_spec, Hx.
apply IH. intros z Hz. apply in_rem; auto. congruence.
Qed.

## 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.
Proof.
intros x. unfold rank. destruct (xrank_points_to (cardinal X) x) as (l&?&<-).
eapply points_to_cardinal. eassumption.
Qed.

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.
Proof.
unfold rank at 1. intros x y Hxy.
destruct (xrank_points_to (cardinal X) x) as (l&Hl&<-).
assert (length (x::l) <= rank y). apply points_to_rank. constructor; assumption.
simpl in H. eauto with arith.
Qed.

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.
Proof.
intros Hs H x. induction x as [x IH] using (well_founded_induction Hs).
constructor. intros; auto.
Qed.