(** * Post Correspondence Problem *)

Require Export Reductions Problems.PCP.

Lemma stack_discrete :
  discrete (stack bool).
Proof.
(* Goal: discrete (stack bool) *)
  eapply discrete_iff; econstructor. intros ? ?. hnf. repeat decide equality.
Qed.

Lemma stack_enum :
  enumerable__T (stack bool).
Proof.
  apply enumerable__T_list, enumerable__T_prod;
  apply enumerable__T_list, count_bool.
Qed.

(** ** Enumerability *)

Fixpoint L_PCP n : list (BSRS * (string bool * string bool)) :=
  match n with
  | 0 => []
  | S n => L_PCP n
              ++ [ (C, (x, y)) | (C, x, y) ∈ (L_T BSRS n × L_T (string bool) n × L_T (string bool) n), (x/y) el C ]
              ++ [ (C, (x ++ u, y ++ v)) | ( (C, (u,v)), x, y) ∈ (L_PCP n × L_T (string bool) n × L_T (string bool) n), (x,y) el C ]
  end.

Lemma enum_PCP' :
  enum (fun '(C, (u, v)) => @derivable bool C u v) L_PCP.
Proof.
(* Goal: iff (@derivable bool C u v) (@ex nat (fun m : nat => @In (prod (stack bool) (prod (string bool) (string bool))) (@pair (stack bool) (prod (string bool) (string bool)) C (@pair (string bool) (string bool) u v)) (L_PCP m))) *)
  split.
  - eauto.
(* Goal: iff (@derivable bool C u v) (@ex nat (fun m : nat => @In (prod (stack bool) (prod (string bool) (string bool))) (@pair (stack bool) (prod (string bool) (string bool)) C (@pair (string bool) (string bool) u v)) (L_PCP m))) *)
  - intros ( C & u & v ). split.
    + induction 1.
      * destruct (el_T C) as [m1], (el_T x) as [m2], (el_T y) as [m3].
        exists (1 + m1 + m2 + m3). cbn. in_app 2.
(* Goal: @In (prod (list (prod (string bool) (string bool))) (prod (string bool) (string bool))) (@pair (stack bool) (prod (string bool) (string bool)) C (@pair (string bool) (string bool) x y)) (@map (prod (prod (list (prod (string bool) (string bool))) (string bool)) (string bool)) (prod (list (prod (string bool) (string bool))) (prod (string bool) (string bool))) (fun '(pair (pair C x as y0) y) => @pair (list (prod (string bool) (string bool))) (prod (string bool) (string bool)) C (@pair (string bool) (string bool) x y)) (@filter (prod (prod (list (prod (string bool) (string bool))) (string bool)) (string bool)) (fun '(pair (pair C x as y0) y) => @dec2bool (@In (prod (string bool) (string bool)) (@pair (string bool) (string bool) x y) C) (@Dec (@In (prod (string bool) (string bool)) (@pair (string bool) (string bool) x y) C) (@list_in_dec (prod (string bool) (string bool)) (@pair (string bool) (string bool) x y) C (@prod_eq_dec (string bool) (string bool) (@list_eq_dec bool bool_eq_dec) (@list_eq_dec bool bool_eq_dec))))) (@list_prod (prod BSRS (string bool)) (string bool) (@list_prod BSRS (string bool) (@L_T BSRS (@enumerable_list (card bool) (@prod_enumerable (string bool) (string bool) (@enumerable_list bool enum_bool) (@enumerable_list bool enum_bool))) (Init.Nat.add (Init.Nat.add m1 m2) m3)) (@L_T (string bool) (@enumerable_list bool enum_bool) (Init.Nat.add (Init.Nat.add m1 m2) m3))) (@L_T (string bool) (@enumerable_list bool enum_bool) (Init.Nat.add (Init.Nat.add m1 m2) m3))))) *)
        in_collect (C, x, y); eapply cum_ge'; eauto; omega.
      * destruct IHderivable as [m1], (el_T x) as [m2], (el_T y) as [m3]. 
        exists (1 + m1 + m2 + m3). cbn. in_app 3.
(* Goal: @In (prod (list (prod (string bool) (string bool))) (prod (string bool) (string bool))) (@pair (stack bool) (prod (string bool) (string bool)) C (@pair (string bool) (string bool) (@app bool x u) (@app bool y v))) (@map (prod (prod (prod (list (prod (string bool) (string bool))) (prod (list bool) (list bool))) (list bool)) (list bool)) (prod (list (prod (string bool) (string bool))) (prod (list bool) (list bool))) (fun '(pair (pair (pair C (pair u v as y2) as y1) x as y0) y) => @pair (list (prod (string bool) (string bool))) (prod (list bool) (list bool)) C (@pair (list bool) (list bool) (@app bool x u) (@app bool y v))) (@filter (prod (prod (prod (list (prod (string bool) (string bool))) (prod (string bool) (string bool))) (string bool)) (string bool)) (fun '(pair (pair (pair C (pair u v as y2) as y1) x as y0) y) => @dec2bool (@In (prod (string bool) (string bool)) (@pair (string bool) (string bool) x y) C) (@Dec (@In (prod (string bool) (string bool)) (@pair (string bool) (string bool) x y) C) (@list_in_dec (prod (string bool) (string bool)) (@pair (string bool) (string bool) x y) C (@prod_eq_dec (string bool) (string bool) (@list_eq_dec bool bool_eq_dec) (@list_eq_dec bool bool_eq_dec))))) (@list_prod (prod (prod BSRS (prod (string bool) (string bool))) (string bool)) (string bool) (@list_prod (prod BSRS (prod (string bool) (string bool))) (string bool) (L_PCP (Init.Nat.add (Init.Nat.add m1 m2) m3)) (@L_T (string bool) (@enumerable_list bool enum_bool) (Init.Nat.add (Init.Nat.add m1 m2) m3))) (@L_T (string bool) (@enumerable_list bool enum_bool) (Init.Nat.add (Init.Nat.add m1 m2) m3))))) *)
        in_collect ( (C, (u, v), x, y)); eapply cum_ge'; eauto; try omega.
    + intros [m]. revert C u v H. induction m; intros.
      * inv H.
      * cbn in H. inv_collect; inv H; eauto using derivable.
Qed.

Lemma enumerable_derivable : enumerable (fun '(C, (u, v)) => @derivable bool C u v).
Proof.
(* Goal: sumbool (@eq (stack bool) x y) (not (@eq (stack bool) x y)) *)
  eapply enum_count. intros; repeat decide equality. eapply enum_PCP'.
Qed.

Lemma enumerable_PCP : enumerable BPCP'.
Proof.
(* Goal: @enumerable (stack bool) BPCP' *)
  pose proof enumerable_derivable. 
  assert (enumerable (X := (stack bool * (string bool * string bool))) (fun '(C, (s, t)) => s = t)). {
(* Goal: @enumerable (prod (stack bool) (prod (string bool) (string bool))) (fun '(pair C (pair s t as p)) => @eq (string bool) s t) *)
    eapply dec_count_enum.
    - eapply decidable_iff. econstructor. intros (? & ? & ?). exact _.
    - eapply enum_enumT. econstructor. exact _.
  }
(* Goal: @enumerable (stack bool) BPCP' *)
  unshelve epose proof (enumerable_conj _ H H0).
  - eapply discrete_iff. econstructor. exact _.
  - eapply projection in H1 as [f]. exists f.
    intros. rewrite <- H1. intuition.
(* Goal: @derivable bool x v v *)
    + destruct H2 as [u]. exists (u,u). eauto.
    + destruct H2 as [[u v] [? ->]]. exists v. eauto.
Qed.
