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

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

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.

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.

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.

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.

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

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

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

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

 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.

 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.

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

 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.

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.

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.

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.

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.

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

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

 Definition acyclic := well_founded r'.

 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.

 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.

 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.

 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.

 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.

 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.

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.