Require Export TLC.LibLN Nat.
Require Import TLC.LibEpsilon TLC.LibLogic TLC.LibList TLC.LibVar TLC.LibNat TLC.LibEpsilon TLC.LibRelation.

Notation Rincl := LibRelation.rel_incl.

Definition comp_rel {A:Type} (R S :binary A) x y := ∃ z, R x z ∧ S z y.

Notation "R ° S" := (@comp_rel _ R S) (at level 42, right associativity).

Lemma comp_trans{A}: ∀ (R S:binary A), inverse (R°S) = (inverse S ° inverse R).
Proof.
  intros. apply binary_ext.
    split; intros H; destruct H as [ z [ H1 H2 ]]; eexists; eauto.
Qed.

Lemma comp_assoc {A} : ∀ (R S T:binary A), R ° S ° T = (R ° S) ° T.
Proof.
  intros. apply binary_ext. intros.
    split; introv H; inverts H as [H1 H2].
    inverts H2; repeat (eexists; intuition eauto).
    inverts H1; repeat (eexists; intuition eauto).
Qed.

Ltac destruct_hyps :=
  repeat match goal with H: ?T |- _ ⇒
    match T with
    | _ ∧ _ ⇒ destruct H
    | ∃ a, _ ⇒ destruct H
    end
  end.

Ltac destruct_comp :=
  repeat match goal with
    | H: (_ ° _) _ _ |- _ ⇒ unfold comp_rel in H; destruct_hyps
  end.

Hint Rewrite in_remove in_singleton union_remove union_empty_l in_union in_empty
        notin_singleton notin_union:fs.

Hint Resolve subset_empty_l:fs.
Hint Unfold subset:fs.

Ltac autofs :=
    repeat (try (apply fset_extens); auto with fs; autorewrite with fs in *; intros_all; substs;
    try (match goal with
    | H1 : ?A \c _, H2 : _ \in ?A |- _ ⇒ apply H1 in H2
    end); destruct_hyps; intuition auto).


Lemma remove_singleton: ∀ A (x:A), \{ x} \- \{x} = \{}.
Proof.
  autofs.
Qed.

Lemma remove_singleton_neq: ∀ A (x v:A), x ≠ v → \{ v} \- \{x} = \{v}.
Proof.
  autofs.
Qed.

Hint Rewrite remove_singleton:fs.

Lemma subset_trans {A} : ∀ (E F G: fset A), E \c F → F \c G → E \c G.
Proof.
  autofs.
Qed.

Hint Extern 1 (?A \c ?B) ⇒ match goal with
  | H1 : A \c ?C, H2 : ?C \c B |- _ ⇒ apply subset_trans
  end.

Lemma fset_extens_rev {A:Type} : ∀ (E F:fset A), E = F → E \c F ∧ F \c E.
Proof.
  autofs.
Qed.

Lemma remove_subset_union {A:Type}: ∀ (E F G: fset A), E \- F = G → E \c G \u F.
Proof.
  intros_all. apply fset_extens_rev in H. intuition. autofs. destruct× (classic (x \in F)).
  left. apply H1. autofs.
Qed.

Definition to_list (E:fset nat) : list nat.
  assert (Inhab (list nat)). apply Inhab_list.
  remember (fun L ⇒ E = from_list L) as f.
  exact (epsilon f).
Defined.

Lemma from_list_to_list : ∀ E, from_list (to_list E) = E.
Proof.
  intros. unfold to_list. symmetry. apply pred_epsilon'. apply fset_finite.
Qed.

Lemma to_list_empty: to_list (\{}:fset nat) = nil.
Proof.
  unfold to_list. apply pred_epsilon_of_val_weaken with nil. unfold from_list. simpl. auto.
  intros. unfold from_list in H. destruct x; simpl; auto. rewrite fold_right_cons in H.
  false. assert (\{ n} \u fold_right (fun (x : nat) (acc : fset nat) ⇒ \{ x} \u acc) \{} x \c \{}).
  rewrite H at 2; apply subset_refl. forwards: H0 n; autofs.
Qed.

Definition map_fset (f:nat → nat)(E:fset nat):= from_list (map f (to_list E)).

Lemma mem_map_rev {A B:Type} : ∀ (f:A → B) l x, mem x (map f l) →
  ∃ y, x = f y ∧ mem y l.
Proof.
  induction l; intros; simpl.
  - rewrite map_nil in H. false. rewrite mem_nil_eq in H; auto.
  - rewrite map_cons in H. rewrite mem_cons_eq in H. destruct H.
    + ∃ a; intuition.
    + destruct (IHl x H). ∃ x0; intuition.
Qed.

Lemma from_list_spec : ∀ x (L:list nat),
  x \in from_list L = mem x L.
 Proof using.
   unfold from_list. induction L; rew_listx.
   rewrite in_empty. auto.
   rewrite in_union, in_singleton. congruence.
Qed.

Lemma map_fset_spec : ∀ E f x, x \in map_fset f E ↔ ∃ y, f y = x ∧ y \in E.
Proof.
  split; intros.
  - unfold map_fset in H. Locate from_list_spec. rewrite from_list_spec in H.
    apply mem_map_rev in H; destruct H. ∃ x0; intuition. rewrite <- from_list_spec in H1.
    rewrite from_list_to_list in H1; auto.
  - unfold map_fset. rewrite from_list_spec.
    destruct H as [ y [ H1 H2 ]]. rewrite <- H1. apply mem_map. rewrite <- from_list_spec.
    rewrite from_list_to_list; auto.
Qed.

Hint Rewrite map_fset_spec:fs.

Lemma map_fset_empty : ∀ f, map_fset f \{} = \{}.
Proof.
  autofs.
Qed.

Lemma map_union : ∀ E F f, map_fset f (E \u F) = map_fset f E \u map_fset f F.
Proof.
  intros; autofs.
  - left. ∃ x0. intuition.
  - right. ∃ x0. intuition.
  - ∃ x0; autofs.
  - ∃ x0; autofs.
Qed.

Lemma map_singleton : ∀ f x, map_fset f (\{ x }) = \{ f x}.
Proof.
  intros; autofs.
    ∃ x; autofs.
Qed.

Definition filter_fset (P:nat → Prop)(E:fset nat):= from_list (filter P (to_list E)).

Lemma filter_fset_spec : ∀ E P x, x \in filter_fset P E ↔ P x ∧ x \in E.
Proof.
  split; intros.
  - unfold filter_fset in H. rewrite from_list_spec in H.
    apply mem_filter_inv in H; destruct H. rewrite <- from_list_spec in H.
    rewrite from_list_to_list in H; intuition.
  - unfold filter_fset. rewrite from_list_spec.
    destruct H. apply mem_filter; auto. rewrite <- from_list_spec.
    rewrite from_list_to_list; auto.
Qed.

Hint Rewrite filter_fset_spec:fs.

Lemma fresh_single_notin_rev: ∀ (xs : list var) (x : var), fresh \{} (length xs) xs
    → x \notin from_list xs → fresh \{ x} (length xs) xs.
Proof.
  induction xs; intros; try solve [simpl; auto].
   rewrite length_cons in ×. simpl in ×. rewrite from_list_cons in H0. autofs.
Qed.

Lemma fresh_sub : ∀ l L L', fresh L' (length l) l → L \c L' → fresh L (length l) l.
Proof.
  induction l; intros; try solve [simpl; auto].
  rewrite length_cons in ×. simpl in ×. intuition. intros_all. apply H0 in H.
  auto. eapply IHl; eauto. autofs.
Qed.