Require Import Definitions Prelim.

Hint Rewrite concat_app map_app map_map : list.
Hint Rewrite <- map_rev : list.

Lemma nil_app_nil X (A : list X) :
  A = [] ++ A ++ [].
Proof.
  now autorewrite with list.
Qed.

Section CFGs.

  Notation sig := nat.
  Definition rule : Type := sig * list sig.
  Definition cfg : Type := sig * list rule.

  Definition rules (G : cfg) := snd G.
  Definition startsym (G : cfg) := fst G.

  Inductive rew_cfg : cfg -> list sig -> list sig -> Prop:=
  |rewR R x a y v : (a,v) el rules R -> rew_cfg R (x++[a]++y) (x++v++y).
  Hint Constructors rew_cfg.

  Lemma rewrite_sing R a x :
    (a, x) el rules R -> rew_cfg R [a] x.
  Proof.
    intros. rewrite nil_app_nil, (nil_app_nil [a]). now econstructor.
  Qed.

  Inductive rewt (S: cfg) (x: list sig) : list sig -> Prop :=
  |rewtRefl : rewt S x x
  |rewtRule y z : rewt S x y -> rew_cfg S y z -> rewt S x z.
  Hint Constructors rewt.

  Global Instance rewtTrans R :
    PreOrder (rewt R).
  Proof.
    split.
    - hnf. econstructor.
    - induction 2; eauto.
  Qed.

  Global Instance rewrite_proper R :
    Proper (rewt R ==> rewt R ==> rewt R) (@app sig).
  Proof.
    intros x1 y1 H1 x2 y2 H2.
    induction H1.
    - induction H2.
      + reflexivity.
      + rewrite IHrewt. inv H. eapply rewtRule.
        replace (x1 ++ x ++ [a] ++ y0) with ( (x1 ++ x) ++ [a] ++ y0) by now autorewrite with list.
        eauto. replace (x1 ++ x ++ v ++ y0) with ( (x1 ++ x) ++ v ++ y0) by now autorewrite with list. eauto.
    - rewrite IHrewt. inv H. autorewrite with list. eauto.
  Qed.

  Global Instance subrel R :
    subrelation (rew_cfg R) (rewt R).
  Proof.
    intros x y H. econstructor. reflexivity. eassumption.
  Qed.

  Definition terminal G x := ~ exists y, rew_cfg G x y.

  Lemma terminal_iff G x :
    terminal G x <-> forall s y, s el x -> ~ (s, y) el rules G.
  Proof.
    split.
    - intros H s y A B. apply H. destruct (@in_split _ _ _ A) as (l1 & l2 & ->).
      exists (l1 ++ y ++ l2). change (s :: l2) with ([s] ++ l2). now econstructor.
    - intros H1 [y H2]. inv H2. eapply (H1 _ v); eauto.
  Qed.

  Definition L (G : cfg) x := rewt G [startsym G] x /\ terminal G x.

  Definition sym_G (G : cfg) :=
    startsym G :: flat_map (fun '(a, x) => a :: x) (rules G).

  Lemma sym_G_rewt x G y :
    x <<= sym_G G -> rewt G x y -> y <<= sym_G G.
  Proof.
    intros. induction H0.
    - eauto.
    - destruct H1. destruct R. cbn in *.
      eapply incl_app; eauto. eapply incl_app; eauto.
      unfold sym_G. intros ? ?.
      right. eapply in_flat_map. exists (a / v). eauto.
  Qed.

End CFGs.

Definition CFP' (G : cfg) := exists x, L G x /\ x = List.rev x.

Definition CFI' '(G1, G2) :=
  exists x, L G1 x /\ L G2 x.

Section Post_CFG.

  Variable R : SRS.
  Variable a : symbol.

  Definition Sigma := sym R ++ [a].
  Definition S : symbol := fresh Sigma.

  Definition G := (S, (S,[S]) :: map (fun '(u / v) => (S, u ++ [S] ++ v)) R ++ map (fun '(u / v) => (S, u ++ [a] ++ v)) R).

  Lemma terminal_iff_G y :
    terminal G y <-> ~ S el y.
  Proof.
    unfold terminal.
    enough ((exists y0, rew_cfg G y y0) <-> S el y). firstorder. split.
    - intros [y0 ?]. inv H. cbn in H0.
      destruct H0 as [ | [ [[] []] % in_map_iff | [[] []] % in_map_iff ] % in_app_iff]; inv H; eauto.
    - intros (u' & v' & ?) % List.in_split.
      subst. exists (u' ++ [S] ++ v'). econstructor. cbn. eauto.
  Qed.

  Lemma rewt_count x :
    rewt G [S] x -> count x S <= 1.
  Proof.
    induction 1.
    - cbn. now rewrite Nat.eqb_refl.
    - inv H0. destruct H1 as [ | [ [[] []] % in_map_iff | [[] []] % in_map_iff ] % in_app_iff]; inv H0.
      + eauto.
      + unfold Sigma. simpl_list. rewrite <- !countSplit in *. cbn in *.
        rewrite Nat.eqb_refl in *.
        enough (count l S = 0) as ->. enough (count l0 S = 0) as ->. omega.
        * eapply notInZero. intros D.
          edestruct (fresh_spec) with (l := Sigma); try reflexivity.
          eapply sym_word_R in H1. unfold Sigma. eauto.
        * eapply notInZero. intros D.
          edestruct (fresh_spec) with (l := Sigma); try reflexivity.
          eapply sym_word_l in H1. unfold Sigma. eauto.
      + unfold Sigma. simpl_list. rewrite <- !countSplit in *. cbn in *.
        rewrite Nat.eqb_refl in *.
        assert (S =? a = false) as ->. eapply Nat.eqb_neq. intros D.
        edestruct fresh_spec with (l := Sigma); try reflexivity.
        unfold S in *. rewrite D. unfold Sigma; eauto.
        enough (count l S = 0) as ->. enough (count l0 S = 0) as ->. omega.
        * eapply notInZero. intros D.
          edestruct (fresh_spec) with (l := Sigma); try reflexivity.
          eapply sym_word_R in H1. unfold Sigma. eauto.
        * eapply notInZero. intros D.
          edestruct (fresh_spec) with (l := Sigma); try reflexivity.
          eapply sym_word_l in H1. unfold Sigma. eauto.
  Qed.

  Lemma Post_CFG_1' A :
    A <<= R -> A = [] \/ rewt G [S] (sigma a A).
  Proof.
    induction A.
    - cbn. eauto.
    - intros. assert (A <<= R) by eauto. eapply IHA in H0.
      destruct a0 as [u v]. destruct H0.
      + subst. right. erewrite rewrite_sing with (x := u ++ [a] ++ v). reflexivity.
        right. eapply in_app_iff. right. eapply in_map_iff. exists (u,v); eauto.
      + right. erewrite rewrite_sing with (x := u ++ [S] ++ v).
        now rewrite H0. right. eapply in_app_iff. left. eapply in_map_iff. exists (u,v); eauto.
  Qed.

  Definition gamma (A : SRS) := map (fun '(x,y) => (x, rev y)) A.

  Lemma sigma_eq s A :
    sigma s A = tau1 A ++ [s] ++ rev (tau2 (gamma A)).
  Proof.
    induction A.
    - reflexivity.
    - destruct a0 as [u v]. cbn. rewrite IHA.
      now simpl_list.
  Qed.

  Lemma tau2_gamma s A :
    s el rev (tau2 (gamma A)) <-> s el tau2 A.
  Proof.
    induction A as [ | [u v] ]; cbn.
    - reflexivity.
    - simpl_list. rewrite !in_app_iff, IHA. firstorder.
  Qed.

  Lemma sigma_inv A s1 s x y :
    sigma s1 A = x ++ [s] ++ y -> ~ s el x -> ~ s el y -> ~ s el sym A ->
    s1 = s.
  Proof.
    rewrite sigma_eq. intros.
    cbn in H. assert (s el tau1 A ++ s1 :: rev (tau2 (gamma A))) by (rewrite H; eauto).
    eapply in_app_iff in H3 as [ | [ | ? % tau2_gamma]]; try firstorder using tau1_sym, tau2_sym.
  Qed.

  Lemma sigma_snoc A x y u v s s' :
    sigma s A = x ++ [s] ++ y -> ~ s el x -> ~ s el y ->
    sigma s' (A ++ [u/v]) = x ++ u ++ s' ++ v ++ y.
  Proof.
    rewrite !sigma_eq. unfold gamma. cbn. simpl_list. cbn. simpl_list. cbn.
    intros. eapply list_prefix_inv in H as [-> <-]; eauto.
    eapply notInZero.
    eapply (f_equal (fun a => count a s)) in H. rewrite <- !countSplit in H. cbn in H.
    rewrite !Nat.eqb_refl in H. eapply notInZero in H0. eapply notInZero in H1.
    rewrite H0, H1 in *. omega.
  Qed.

  Lemma Post_CFG_2 x :
    rewt G [S] x ->
    exists A m, A <<= R /\ sigma m A = x /\ (m = S \/ m = a /\ A <> []).
  Proof.
    intros. induction H.
    - cbn. exists [], S. eauto.
    - inv H0. destruct H1 as [ | [(? & ? & ?) % in_map_iff | (? & ? & ?) % in_map_iff] % in_app_iff]; inv H0.
      + eassumption.
      + destruct x0 as [u' v']. inv H3.
        destruct IHrewt as (A & m & HA & IHA & Hm).
        exists (A ++ [u'/v']), S. repeat split.
        * eauto.
        * simpl_list. cbn.
          enough (~ S el x). enough (~ S el y0).
          eapply sigma_snoc with (s := S); eauto.
          -- assert (IH2 := IHA).
          eapply sigma_inv in IHA; eauto. subst. eauto.
          intros D.
          edestruct fresh_spec with (l := sym R ++ [a]); try reflexivity.
          eapply in_app_iff. left. eapply sym_mono. eauto. eauto.
          -- eapply rewt_count in H. rewrite <- !countSplit in H. cbn in H.
             rewrite Nat.eqb_refl in H. eapply notInZero. omega.
          -- eapply rewt_count in H. rewrite <- !countSplit in H. cbn in H.
             rewrite Nat.eqb_refl in H. eapply notInZero. omega.
        * eauto.
      + destruct x0 as [u' v']. inv H3.
        destruct IHrewt as (A & m & HA & IHA & Hm).
        exists (A ++ [u'/v']), a. repeat split.
        * eauto.
        * simpl_list. cbn.
          enough (~ S el x). enough (~ S el y0).
          eapply sigma_snoc with (s := S); eauto.
          -- assert (IH2 := IHA).
          eapply sigma_inv in IHA; eauto. subst. eauto.
          intros D.
          edestruct fresh_spec with (l := sym R ++ [a]); try reflexivity.
          eapply in_app_iff. left. eapply sym_mono. eauto. eauto.
          -- eapply rewt_count in H. rewrite <- !countSplit in H. cbn in H.
             rewrite Nat.eqb_refl in H. eapply notInZero. omega.
          -- eapply rewt_count in H. rewrite <- !countSplit in H. cbn in H.
             rewrite Nat.eqb_refl in H. eapply notInZero. omega.
        * destruct A; firstorder.
  Qed.

  Lemma reduction_full x :
    (exists A, A <<= R /\ A <> [] /\ sigma a A = x) <-> L G x.
  Proof.
    split.
    - intros (A & ? & ? & ?). subst. destruct Post_CFG_1' with (A := A); intuition.
      split.
      + eassumption.
      + eapply terminal_iff_G. rewrite sigma_eq. intros E.
        edestruct fresh_spec with (l := sym R ++ [a]); try reflexivity.
        eapply in_app_iff in E as [ | [ | ? % tau2_gamma ] % in_app_iff].
        * eapply in_app_iff. left. eapply sym_mono; eauto. now eapply tau1_sym.
        * eapply in_app_iff. right. eauto.
        * eapply in_app_iff. left. eapply sym_mono; eauto. now eapply tau2_sym.
    - intros [(A & m & HA & HE & Hm) % Post_CFG_2 ?].
      subst. destruct Hm as [-> | [-> ?]].
      + eapply terminal_iff_G in H. exfalso. rewrite sigma_eq in H.
        eapply H. eauto.
      + exists A. eauto.
  Qed.

End Post_CFG.

Definition Post_G '(R, a, x) := exists A, A <<= R /\ A <> [] /\ sigma a A = x.
Definition CFG '(G, x) := L G x.

Lemma reduce_grammars :
  Post_G ⪯ CFG.
Proof.
  exists (fun '(R, a, x) => (G R a, x)). intros ((? & ?) & ?). cbn. eapply reduction_full.
Qed.

Lemma reduce_CFP :
  CFP ⪯ CFP'.
Proof.
  exists (fun '(R, a) => (G R a)). intros [R a].
  intuition; cbn in *.
  - destruct H as (A & HR & HA & H).
    exists (sigma a A). split. eapply reduction_full; eauto.
    eauto.
  - destruct H as (x & Hx & H).
    eapply reduction_full in Hx as (A & HR & HA & H1).
    exists A. subst; eauto.
Qed.

Lemma reduce_CFI :
  CFI ⪯ CFI'.
Proof.
  exists (fun '(R1, R2, a) => (G R1 a, G R2 a)). intros [[R1 R2] a].
  intuition; cbn in *.
  - destruct H as (A1 & A2 & HR1 & HR2 & HA1 & HA2 & H).
    exists (sigma a A1). split; eapply reduction_full; eauto.
  - destruct H as (x & HR1 & HR2).
    eapply reduction_full in HR1 as (A1 & HR1 & HA1 & H1).
    eapply reduction_full in HR2 as (A2 & HR2 & HA2 & H2).
    exists A1, A2. subst; eauto.
Qed.