Require Export Separation.

Fixpoint step G G' :=
  match G' with
    [] ⇒ []
  | R A [] :: Gr ⇒ R A [] :: step G Gr
  | R A [s0] :: Gr ⇒ R A [s0] :: step G Gr
  | R A [s0 ; s1] :: Gr ⇒ R A [s0 ; s1] :: step G Gr
  | R A (s0 :: ur) :: Gr ⇒
    let (B, H) := pickFresh G
    in R A [s0 ; Vs B] :: R B ur :: Gr
  end.

Definition step' G := step G G.

Fixpoint count_bin G :=
  match G with
    [] ⇒ 0
  | R A u :: Gr ⇒ if decision ((|u|) ≤ 2) then count_bin Gr else |u| + count_bin Gr
  end.

Definition bin G := it step' (count_bin G) G.

Definition binary G := ∀ A u, R A u el G → (|u|) ≤ 2.

Lemma count_decr G G' :
  step G' G ≠ G → count_bin G > count_bin (step G' G).
Proof.
  intros H.
  induction G as [| [A u] G IHG] ; simpl in × ; [tauto | ].
  destruct u as [| s0 [| s1 [| s2 u]]] ; try now (simpl ; apply IHG ; intros H0 ; apply H ; f_equal).
  simpl. decide (S (S (| u |)) ≤ 2) as [D | D] ; omega.
Qed.

Lemma fp_bin G :
  FP step' (bin G).
Proof.
  apply it_fp. intros n.
  remember (it step' n G) as G'.
  decide (step' G' = G') as [D | D].
  - left. auto.
  - right. simpl. rewrite <- HeqG'.
    apply count_decr in D. unfold step'. omega.
Qed.

Lemma fp_binary G :
  FP step' G → binary G.
Proof.
  intros Ss A u Ru.
  unfold FP, step' in Ss.
  remember G as G'.
  do 2 rewrite HeqG' in Ss at 2.
  rewrite HeqG' in Ru. clear HeqG'.
  induction G as [| [B v] Gr IHGr] ; simpl in × ; [tauto |].
  destruct Ru as [Ru | Ru].
  - inv Ru. destruct u as [| s0 [| s1 [| s2 u]]] ; simpl ; auto. inv Ss.
  - destruct v as [| s0 [| s1 [| s2 v]]] ; try now (simpl in Ss ; inversion Ss ; apply IHGr ; auto).
Qed.

 Lemma bin_binary G :
   binary (bin G).
 Proof.
   apply fp_binary, fp_bin.
 Qed.

Lemma step_or G G' :
  step G' G = G ∨ ∃ A Gr B u s, G === R A (s :: u) :: Gr ∧ step G' G === R A [s ; Vs B] :: R B u :: Gr ∧ ¬ Vs B el symbs G'.
Proof.
  induction G as [| [A u] G IHG].
  - simpl. now left.
  - destruct u as [| s0 [| s1 [| s2 u]]] ; unfold step.
    + destruct IHG as [H | [A' [Gr [B' [u' [s [H0 [H1 H2]]]]]]]] ; try now (left ; f_equal).
      right. ∃ A', (R A [] :: Gr), B', u', s. repeat split ; try rewrite H0 ; auto using Base.equi_swap ; rewrite H1 ; auto 7 using Base.equi_swap.
    + simpl ; destruct IHG as [H | [A' [Gr [B' [u' [s [H0 [H1 H2]]]]]]]] ; try now (left ; f_equal).
      right. ∃ A', (R A [s0] :: Gr), B', u', s. repeat split ; try rewrite H0 ; auto using Base.equi_swap ; rewrite H1 ; auto 7 using Base.equi_swap.
    + simpl ; destruct IHG as [H | [A' [Gr [B' [u' [s [H0 [H1 H2]]]]]]]] ; try now (left ; f_equal).
      right. ∃ A', (R A [s0 ; s1] :: Gr), B', u', s. repeat split ; try rewrite H0 ; auto using Base.equi_swap ; rewrite H1 ; auto 7 using Base.equi_swap.
    + destruct (pickFresh G') as [B N].
      right. ∃ A, G, B, (s1 :: s2 :: u), s0. repeat split ; auto.
      intros H. specialize (N (Vs B) H). unfold sless' in N. omega.
Qed.

Lemma step_der_equiv G A u :
  terminal u → (Vs A) el dom G → (der G A u ↔ der (step G G) A u).
Proof.
  intros T Do.
  destruct (step_or G G) as [Ss | Ss].
  - rewrite <- Ss at 1. split ; auto.
  - destruct Ss as [A' [Gr [B [v [s [H0 [H1 H2]]]]]]].
    assert (RL : substG (R A' [s; Vs B] :: Gr) (Vs B) v = R A' (s :: v) :: Gr). {
      simpl. decide (s = Vs B).
      + exfalso. rewrite e in H0.
        apply H2. apply symbs_inv. ∃ A', (Vs B :: v). rewrite H0. split ; auto.
      + decide (Vs B = Vs B) ; try tauto. rewrite app_nil_r. f_equal.
        apply substG_skip. intros H. apply H2.
        apply symbs_subset with (G := Gr) ; auto. rewrite H0. auto. }
    rewrite der_equiv_G with (G1 := step G G) (G2 := R B v :: R A' [s; Vs B] :: Gr) by (rewrite Base.equi_swap ; auto).
    rewrite der_equiv_G with (G2 := R A' (s :: v) :: Gr) ; auto.
    rewrite <- RL. symmetry. apply der_substG_G_equiv.
    + intros H. apply symbs_dom in Do. inv H. tauto.
    + simpl. intros [H | H].
      { inv H. apply H2. apply symbs_inv. ∃ B, (s :: v). rewrite H0. split ; auto. }
      { apply symbs_dom in H. apply H2.
        apply symbs_subset with (G := Gr) ; auto. rewrite H0. auto. }
    + intros H. apply H2. apply symbs_inv. ∃ A', (s :: v). rewrite H0. split ; auto.
    + intros H. destruct (T (Vs B) H) as [t T']. inv T'.
Qed.

Lemma step_dom G G' :
  dom G <<= dom (step G' G).
Proof.
  revert G'.
  induction G as [| [A u] G IHG] ; intros G' ; try destruct u as [| s0 [| s1 [| s2 u]]] ; simpl ; auto.
Qed.

Lemma bin_der_equiv G A u :
  terminal u → (Vs A) el dom G → (der G A u ↔ der (bin G) A u).
Proof.
  unfold bin. remember (count_bin G) as n. clear Heqn.
  intros T. revert G.
  induction n as [| n IHn] ; intros G Do ; simpl.
  - split ; auto.
  - rewrite (IHn G Do).
    apply step_der_equiv ; auto.
    apply it_ind ; auto.
    intros r H0. now apply step_dom.
Qed.

Lemma bin_language G A u :
  Vs A el dom G → (language G A u ↔ language (bin G) A u).
Proof.
  intros D.
  split ; intros [L0 L1] ; split ; auto ; [rewrite <- bin_der_equiv | rewrite bin_der_equiv] ; auto.
Qed.