Require Import GraphTC.
Require Import Quotient.

Definition NSet := quot graph_num graph_index.

Definition nIn (M N : NSet) :=
  elem (repr M) (repr N).

Definition g_to_nset := norm graph_num_corr graph_index_corr.

Lemma repr_nset_bisim g : bisim g (repr (g_to_nset g)).
Proof.
  unfold g_to_nset. apply norm_corr.
Qed.

Lemma g_to_nset_bisim_eq (g1 g2 : Graph) : bisim g1 g2 <-> g_to_nset g1 = g_to_nset g2.
Proof with eauto using bisimSym, bisimTrans.
  unfold g_to_nset. apply R_repr_iff...
Qed.

Lemma repr_bisim_eq (M N : NSet) : M = N <-> bisim (repr M) (repr N).
Proof with eauto using bisimRefl, bisimSym, bisimTrans, graph_index_corr, graph_num_corr.
  symmetry. apply quot_R_eq...
Qed.

Lemma g_to_nset_repr_id (M : NSet) : M = g_to_nset (repr M).
Proof.
  assert (bisim (repr M) (repr (g_to_nset (repr M)))).
  { apply repr_nset_bisim. }
  now apply repr_bisim_eq in H.
Qed.

Lemma repr_g_to_nset_bisim_eq (M : NSet) (g : Graph) : M = g_to_nset g <-> bisim (repr M) g.
Proof.
  split; intros. 
  - rewrite repr_nset_bisim. apply g_to_nset_bisim_eq. rewrite H. now repeat rewrite <- g_to_nset_repr_id.
  - rewrite repr_nset_bisim in H. apply g_to_nset_bisim_eq in H. rewrite <- H.
    now repeat rewrite <- g_to_nset_repr_id.
Qed.

Instance nInDec (M N : NSet) : dec (nIn M N).
Proof. 
  unfold nIn. auto.
Qed.

Instance NSet_eq_dec (M N : NSet) : dec (M = N).
Proof. 
  decide (bisim (repr M) (repr N)); [left|right]; now rewrite repr_bisim_eq.
Qed.

Definition subset (M N : NSet) := forall N', nIn N' M -> nIn N' N.

Lemma double_incl (M N : NSet) : subset M N -> subset N M -> N = M.
Proof with eauto using repr_nset_bisim, bisimSym.
   unfold subset; unfold nIn; intros. apply repr_bisim_eq. 
   apply Ext. split. 
   - unfold g_incl. intros. specialize (H0 (g_to_nset g3)). 
     assert (bisim g3 (repr (g_to_nset g3)))... eapply elem_bisim_inv_l; [|symmetry; eapply H2].
     apply H0. eapply elem_bisim_inv_l...
   - unfold g_incl; intros. specialize (H (g_to_nset g3)). 
     assert (bisim g3 (repr (g_to_nset g3)))... apply elem_bisim_inv_l with (g1 := repr (g_to_nset g3))...
     apply H. apply elem_bisim_inv_l with (g1 := g3)...
Qed.

Lemma subset_refl (M : NSet) : subset M M.
Proof.
  unfold subset; intros; auto.
Qed.

Lemma Extensionality (M N : NSet) : N = M <-> subset M N /\ subset N M.
Proof. 
  split; intros.
  - subst; split; apply subset_refl.
  - destruct H as [A B]; now apply double_incl.
Qed.

Lemma g_elem_repr_NIn (g : Graph) (M : NSet) : nIn M (g_to_nset g) <-> elem (repr M) g.
Proof.
  split; intros; unfold nIn in *; eapply elem_bisim_inv_r; eauto; [symmetry|]; apply repr_nset_bisim.
Qed.

Lemma g_elem_repr_NIn' (g : Graph) (M : NSet) : nIn (g_to_nset g) M <-> elem g (repr M).
Proof.
  split; intros; unfold nIn in *; eapply elem_bisim_inv_l; eauto; [symmetry|]; apply repr_nset_bisim.
Qed.

Lemma nIn_repr_elem (M N : NSet) : nIn M N <-> elem (repr M) (repr N).
Proof.
  split; intros; unfold nIn in *; auto.
Qed.

Definition empty : NSet := g_to_nset empty.

Lemma Empty : forall M, ~ nIn M empty.
Proof with eauto using repr_nset_bisim, bisimSym.
   intros M C. unfold nIn, empty in C. apply elem_bisim_inv_r with (g3 := GraphAxioms.empty) in C...
   now apply Empty in C.
Qed.

Definition adjoin (M N : NSet) := g_to_nset (adj (repr M) (repr N)).

Lemma Adjunction (M N x : NSet) : nIn x (adjoin M N) <-> x = M \/ nIn x N.
Proof with eauto using repr_nset_bisim, bisimRefl, repr_bisim_eq.
  split; intros; unfold nIn in *; unfold adjoin in *.
  - apply elem_bisim_inv_r with (g3 := adj (repr M) (repr N)) in H.
    + apply Adj in H as [H|H]; [left|right]... 
      now apply repr_bisim_eq in H.
    + symmetry; apply repr_nset_bisim.
  - destruct H; subst; apply elem_bisim_inv_r with (g2 := adj (repr M) (repr N)); try apply Adj...
Qed.
     
Definition union (M : NSet) := g_to_nset (union (repr M)).

Lemma Union (M N : NSet) : nIn M (union N) <-> exists x, nIn x N /\ nIn M x.
Proof with eauto using repr_nset_bisim, bisimSym.
  split; intros.
  - rewrite nIn_repr_elem in H. unfold union in H. 
    apply elem_bisim_inv_r with (g3 := GraphAxioms.union (repr N)) in H...
    rewrite Union in H. destruct H as [x [A B]]. exists (g_to_nset x).
    rewrite <- g_elem_repr_NIn' in A. rewrite <- g_elem_repr_NIn in B. intuition.
  - apply nIn_repr_elem. unfold union. apply elem_bisim_inv_r with (g2 := GraphAxioms.union (repr N))...
    apply GraphAxioms.Union. destruct H as [x [A B]]. rewrite nIn_repr_elem in A. rewrite nIn_repr_elem in B.
    exists (repr x); intuition.
Qed. 

Definition lift_p (p : NSet -> Prop) := fun g => p (g_to_nset g).

Instance list_dec (p : NSet -> Prop) {p_dec : forall M, dec (p M)} : forall g, dec (lift_p p g).
Proof.
  intros; unfold lift_p; auto.
Qed.

Definition sep (M : NSet) (p : NSet -> Prop) {p_dec : forall N, dec (p N)} :=
  g_to_nset (sep (repr M) (lift_p p)).

Arguments sep M p {p_dec}.

Lemma lift_ext_bisim p : ext_bisim (lift_p p).
Proof.
  hnf. unfold lift_p. intros. apply g_to_nset_bisim_eq in H. split; congruence.
Qed.

Lemma Sep (M N : NSet) (p : NSet -> Prop) {p_dec : forall M, dec (p M)} : 
      nIn M (sep N p) <-> nIn M N /\ p M.
Proof with eauto using repr_nset_bisim, bisimSym, bisimTrans.
  assert (p_ext : ext_bisim (lift_p p)) by apply lift_ext_bisim. 
  split; intros; unfold nIn, sep in *.
  - apply elem_bisim_inv_r with (g3 := (GraphAxioms.sep (repr N) (lift_p p))) in H... 
    apply Sep in H as [x [A [B C]]]; auto. split.
    + eapply elem_bisim_inv_l...
    + unfold lift_p in B. assert (bisim (repr M) (repr (g_to_nset x)))...
      apply repr_bisim_eq in H. congruence.
  - apply elem_bisim_inv_r with (g2 := GraphAxioms.sep (repr N) (lift_p p))... apply Sep...
    destruct H as [A B]. exists (repr M); repeat split... unfold lift_p. rewrite <- g_to_nset_repr_id...
Qed. 
  
Definition lift_f (f : NSet -> NSet) := fun g => repr (f (g_to_nset g)).

Definition rep (M : NSet) (f : NSet -> NSet) := g_to_nset (rep (repr M) (lift_f f)).


Lemma lift_f_ext f : forall g g', bisim g g' -> bisim (lift_f f g) (lift_f f g').
Proof.
  unfold lift_f. intros. 
  apply g_to_nset_bisim_eq in H. rewrite H. reflexivity. 
Qed.


Lemma Rep (M N : NSet) (f : NSet -> NSet) : nIn N (rep M f) <-> exists M', nIn M' M /\ N = f M'.
Proof with eauto using repr_nset_bisim, bisimSym.
  pose (ext := lift_f_ext f).
  unfold rep; unfold nIn; split; intros.
  - apply elem_bisim_inv_r with (g3 := GraphAxioms.rep (repr M) (lift_f f)) in H...
    apply Rep in H as [x [A B]]... exists (g_to_nset x). split.
    + apply elem_bisim_inv_l with (g3 := repr (g_to_nset x)) in A...
    + unfold lift_f in *. now apply repr_bisim_eq in B.
  - apply elem_bisim_inv_r with (g2 := GraphAxioms.rep (repr M) (lift_f f))...
    destruct H as [x [A B]]. apply Rep... 
    exists (repr x). split... unfold lift_f... apply repr_bisim_eq. now rewrite <- g_to_nset_repr_id.
Qed.

Definition power (M : NSet) := g_to_nset (pow (repr M)).


Lemma Power (M N : NSet) : nIn N (power M) <-> subset N M.
Proof with eauto using repr_nset_bisim, bisimSym. 
  unfold power, subset, nIn. split; intros. 
  - apply elem_bisim_inv_r with (g3 := pow (repr M)) in H...
    apply Pow in H. unfold g_incl in H...
  - apply elem_bisim_inv_r with (g2 := pow (repr M))...
    apply Pow. unfold g_incl; intros. apply elem_bisim_inv_l with (g1 := repr (g_to_nset g3))...
    apply elem_bisim_inv_l with (g3 := repr (g_to_nset g3)) in H0...
Qed.

Definition choice (M : NSet) := 
  match child_nodes (repr M) with
    | [] => empty
    | (x :: _) => g_to_nset (subgraph x)
  end.

Lemma choice_elem (M : NSet) : M <> empty -> nIn (choice M) M.
Proof.
  unfold nIn, empty. simpl; intros. 
  destruct (child_nodes (repr M)) eqn:E; simpl.
  - cut (bisim (repr M) GraphAxioms.empty). 
    { intros. contradict H. now apply repr_g_to_nset_bisim_eq. }
    assert (forall g, ~ elem g (repr M)). 
    { intros g [x [A B]]. apply in_children_iff in A as [y [A C]]. now rewrite E in A. }
    apply bisim_empty_iff; auto.
  - unfold choice. rewrite E. unfold elem. exists (subgraph t). split; auto.
    + apply in_children_iff. exists t; split; auto. rewrite E; auto.
    + symmetry. apply repr_nset_bisim.
Qed.
