Require Import Prelim PCP Reductions.

Section MPCP_PCP_Reduction.

  (* Definition of PCP Types *)
  Variable sig' : Type.
  Inductive sig := hash | dollar | sigma (s: sig').

  Definition trans_sig'_sig: sig' -> sig := fun (s: sig') => sigma s.
  Definition trans_lsig'_lsig : list sig' -> list sig := fun S => map trans_sig'_sig S.
  Definition trans_pair_sig'_sig : (list sig' * list sig') -> (list sig * list sig) :=
  fun p => let (a,b) := p in (trans_lsig'_lsig a, trans_lsig'_lsig b).

  Notation "#" := hash.
  Notation "$" := dollar.

  Definition del_empty_dominos (X:Type) : list (list X * list X) -> list (list X * list X):=
    List.filter (fun p => match p with |([],[]) => false | _=> true end).

  Implicit Types (d: list sig' * list sig') (M: mpcp sig').

  Definition hash_right : list sig' -> list sig := fun A => flat_map (fun (a: sig') => [(sigma a);#]) A.
  Definition hash_left : list sig' -> list sig := fun A => flat_map (fun (a: sig') => [#;(sigma a)]) A.

  Definition hash_list := map (fun A => (hash_left (fst A), hash_right (snd A))).

  Definition mpcp_to_pcp d (P: pcp sig') : (pcp sig) :=
    ($::hash_left (fst d), ($::#::hash_right (snd d)))::(hash_list (del_empty_dominos P))
                                                      ++[([#;$], [$])].

  Definition mpcp_to_pcp_instance M :=
    let (fcard, L) := M in
    mpcp_to_pcp fcard (fcard::L).

  Lemma solution_subset d P R:
    (d::P) <<= (d::R) -> mpcp_to_pcp d P <<= mpcp_to_pcp d (d::R).
  Proof.
    unfold mpcp_to_pcp.
    intros HS e EL. destruct EL as [<-|[EL|EL]%in_app_iff]; try auto.
    right. apply in_app_iff. left. unfold hash_list in *. rewrite in_map_iff in EL.
    destruct EL as [x [HX HQ]]. apply in_map_iff. exists x. split; auto.
    unfold del_empty_dominos in *. rewrite filter_In in *. destruct HQ. split.
    apply HS. now right. assumption.
  Qed.

  Lemma hash_equal_hash (A:list sig') :
    (hash_left A)++[#] = #::(hash_right A).
  Proof.
    induction A. auto. simpl. now rewrite <- IHA.
  Qed.

  Lemma hash_hash_right A B:
    hash_right (A++B) = hash_right A ++ hash_right B.
  Proof.
    unfold hash_right. rewrite !flat_map_concat_map. now rewrite map_app, concat_app.
  Qed.

  Lemma hash_hash_left A B:
    hash_left (A++B) = hash_left A ++ hash_left B.
  Proof.
    unfold hash_left. rewrite !flat_map_concat_map. now rewrite map_app, concat_app.
  Qed.

  Lemma concat_hash_left Q :
    concat (map fst (hash_list Q)) = hash_left (concat (map fst Q)).
  Proof.
    induction Q. auto. simpl. now rewrite IHQ, hash_hash_left.
  Qed.

  Lemma concat_hash_right Q :
    concat (map snd (hash_list Q)) = hash_right (concat (map snd Q)).
  Proof.
    induction Q. auto. simpl. now rewrite IHQ, hash_hash_right.
  Qed.

  Lemma concat_del_dominos_fst (X:Type) (A: list (list X * list X)) :
    concat (List.map fst (del_empty_dominos A)) = concat (List.map fst A).
  Proof.
    induction A.
    - reflexivity.
    - simpl. destruct a eqn: HA. destruct l, l0; cbn; now rewrite IHA.
  Qed.

  Lemma concat_del_dominos_snd (X:Type) (A: list (list X * list X)) :
    concat (List.map snd (del_empty_dominos A)) = concat (List.map snd A).
  Proof.
    induction A.
    - reflexivity.
    - simpl. destruct a eqn: HA. destruct l, l0; cbn; now rewrite IHA.
  Qed.

  Lemma pcp_mpcp_solution (S: pcp sig') d:
    solution (d::S) -> solution (mpcp_to_pcp d S).
  Proof.
    unfold solution, mpcp_to_pcp. destruct d as (a,b).
    cbn[List.map concat fst snd]. intros H.
    rewrite !List.map_app, !concat_app, concat_hash_left, concat_hash_right.
    cbn. rewrite !app_assoc, <- !hash_hash_right, <- !hash_hash_left.
    rewrite concat_del_dominos_fst, concat_del_dominos_snd.
    rewrite H. setoid_rewrite app_comm_cons at 2.
    now rewrite <- hash_equal_hash, <- app_assoc.
  Qed.

  Theorem mpcp_pcp:
    forall (M:mpcp sig'), MPCP M -> PCP (mpcp_to_pcp_instance M).
  Proof.
    intros (d, P). intros [S [_ [sub fsol]]].
    exists (mpcp_to_pcp d S). repeat split.
    - intros Hnil%symmetry. apply (nil_cons Hnil).
    - unfold mpcp_to_pcp_instance. now apply solution_subset.
    - now apply pcp_mpcp_solution.
  Qed.

  Definition lsig_lsig' (A: list sig): list sig' -> list sig' :=
    fold_left (fun (B: list sig') (s: sig) => match s with |sigma s' => (B++[s']) |_ => B end) A.

  Definition trans_pcp_pcp': (pcp sig) -> (pcp sig') :=
    map (fun (p: list sig * list sig) => (lsig_lsig' (fst p) [], (lsig_lsig' (snd p) []))).

  Lemma hash_trans_right_inv (l: list sig'):
     lsig_lsig' (hash_right l) [] = l.
  Proof.
    enough (forall B, lsig_lsig' (hash_right l) B = B++l).
    specialize (H nil). now rewrite app_nil_l in H. induction l; intros A; simpl.
    - now rewrite app_nil_r.
    - specialize (IHl (A++[a])). change (A ++ a :: l) with (A++[a]++l).
      now rewrite app_assoc.
  Qed.

  Lemma hash_trans_left_inv (l: list sig'):
   lsig_lsig' (hash_left l) [] = l.
  Proof.
    enough (forall B, lsig_lsig' (hash_left l) B = B++l).
    specialize (H nil). now rewrite app_nil_l in H. induction l; intros A; simpl.
    - now rewrite app_nil_r.
    - specialize (IHl (A++[a])). change (A ++ a :: l) with (A++[a]++l).
      now rewrite app_assoc.
  Qed.

  Lemma sigma_no_solution S d P s L:
    S <<= mpcp_to_pcp_instance (d,P) ->
    ((concat (map fst S) = sigma s :: # :: L ++ concat (map snd S))
     \/ (#::sigma s::L ++ concat (map fst S) = concat (map snd S))) -> False.
  Proof.
    revert L. induction S; intros L sub.
    - intros [H|H]; now inv H.
    - destruct (sub a (or_introl (eq_refl))) as [<-|[H1|H1%in_sing]%in_app_iff].
      + intros [H|H]; inv H.
      + unfold hash_list, del_empty_dominos in H1.
        apply in_map_iff in H1 as [(u,v) [M1 [M2 M3]%filter_In]].
        subst. intros [H|H].
        * destruct u. inv H. apply (@IHS (L++hash_right v)). intros e HE. apply sub.
          now right. left. now rewrite <- app_assoc. inv H.
        * destruct v. inv H. apply (@IHS (L++hash_left u)). intros e HE. apply sub.
          now right. right. now rewrite <- app_assoc. inv H.
      + subst. intros [H|H];inv H.
  Qed.

  Lemma hd_modified_pcp S M:
    pcp_solution (mpcp_to_pcp_instance M) S ->
    exists C, S = [($::hash_left (fst (fst M)), ($::#::(hash_right (snd (fst M)))))]++C.
  Proof. intros [HN [sub sol]]. destruct M as ((d1,d2),P). destruct S. contradiction.
         cbn[fst snd]. clear HN. assert (sub1:=sub).
         unfold mpcp_to_pcp_instance, mpcp_to_pcp in sub.
         destruct (sub p (or_introl eq_refl)) as [<-|[I2|I2%in_sing]%in_app_iff].
         - exists S. now cbn.
         - exfalso. unfold hash_list, del_empty_dominos in I2.
           apply in_map_iff in I2 as [x [M1 [M2 M3]%filter_In]]. subst. destruct x as (u,v).
           cbn. unfold solution in sol. destruct u,v; try now inv sol.
           cbn in sol. apply (@sigma_no_solution S (d1,d2) P s (flat_map (fun a => [sigma a; #]) v)).
           intros e HE. apply sub. now right. now left.
           cbn in sol. apply (@sigma_no_solution S (d1,d2) P s (flat_map (fun a => [#;sigma a]) u)).
           intros e HE. apply sub. now right. now right.
         - subst. inv sol.
  Qed.

  Lemma shift_list_trans_lsig (A: list sig) B:
    lsig_lsig' A B = B++(lsig_lsig' A nil).
  Proof.
    revert B. induction A; intros B; simpl.
    - now rewrite app_nil_r.
    - destruct a; try (now apply IHA).
      now rewrite (IHA (B++[s])), (IHA ([s])), <- app_assoc.
  Qed.

  Lemma shift_trans_lsig'_lists (l m: list sig) A:
    lsig_lsig' l A ++ lsig_lsig' m nil = lsig_lsig' (l++m) A.
  Proof.
    revert m A. induction l; intros m A; simpl.
    - now rewrite <- shift_list_trans_lsig.
    - destruct a; now apply IHl.
  Qed.

  Definition get_mpcp_solution (P: pcp sig): pcp sig' :=
    del_empty_dominos (trans_pcp_pcp' P).

  Lemma concat_pcp_lsig_fst S:
    concat (map fst (trans_pcp_pcp' S)) = lsig_lsig' (concat (map fst S)) nil.
  Proof.
    induction S. auto. destruct a. simpl. rewrite IHS. unfold lsig_lsig'.
      now rewrite shift_trans_lsig'_lists.
  Qed.

  Lemma concat_pcp_lsig_snd S:
    concat (map snd (trans_pcp_pcp' S)) = lsig_lsig' (concat (map snd S)) nil.
  Proof.
    induction S. auto. destruct a. simpl. rewrite IHS. unfold lsig_lsig'.
      now rewrite shift_trans_lsig'_lists.
  Qed.

  Lemma solution_trans_pcp S:
    solution S -> solution (trans_pcp_pcp' S).
  Proof.
    unfold solution. unfold trans_pcp_pcp'.
    rewrite concat_pcp_lsig_fst, concat_pcp_lsig_snd. intros <-. reflexivity.
  Qed.

  Lemma mpcp_solution_subset (S: pcp sig) d P:
    S <<= mpcp_to_pcp_instance (d,P) -> get_mpcp_solution S <<= (d::P).
  Proof.
    intros sub. unfold get_mpcp_solution, del_empty_dominos, trans_pcp_pcp'.
    intros e [[x [H1 H3]]%in_map_iff H2]%filter_In. subst.
    unfold mpcp_to_pcp_instance, mpcp_to_pcp in sub.
    destruct (sub x H3) as [<-|[H4|H4%in_sing]%in_app_iff].
    - left. simpl. rewrite hash_trans_left_inv, hash_trans_right_inv. now destruct d.
    - unfold hash_list in H4. apply in_map_iff in H4 as [y [H5 H6]].
      subst. unfold del_empty_dominos in H6. apply filter_In in H6 as [[H7|H7] _].
      subst. left. cbn. rewrite hash_trans_left_inv, hash_trans_right_inv.
      now destruct y. right. cbn. rewrite hash_trans_left_inv, hash_trans_right_inv.
      destruct y; assumption.
    - subst. discriminate H2.
  Qed.

  Theorem pcp_mpcp:
    forall (M: mpcp sig'), PCP (mpcp_to_pcp_instance M) -> MPCP M.
  Proof.
    intros (d,P) [S PS]. destruct (hd_modified_pcp PS) as [C HCS].
    exists (get_mpcp_solution C). destruct PS as [H1 [H2 H3]]. repeat split.
    - inversion 1.
    - simpl. intros e [<-|HE]. now left. unfold get_mpcp_solution in HE.
      assert (C <<= mpcp_to_pcp_instance (d,P)).
      { intros c HC. apply H2. rewrite HCS. apply in_app_iff. now right. }
      apply (@mpcp_solution_subset C d P H). assumption.
    - unfold get_mpcp_solution, solution. destruct d as (d1,d2). simpl.
      rewrite concat_del_dominos_fst, concat_del_dominos_snd.
      apply solution_trans_pcp in H3. rewrite HCS in H3.
      unfold solution in H3; simpl in H3.
      now rewrite hash_trans_left_inv, hash_trans_right_inv in H3.
  Qed.

End MPCP_PCP_Reduction.

Theorem reduction_mpcp_pcp : red MPCPD PCPD.
Proof. unfold red.
       exists (fun S => existT (fun X => pcp X) (sig (projT1 S)) (mpcp_to_pcp_instance (projT2 S))).
       intros [gam M]. unfold MPCPD, PCPD. cbn. split. apply mpcp_pcp. apply pcp_mpcp.
Qed.