Require Import Undecidability.PCP.Definitions.

(** * SRH to SR *)

Section SRH_SR.

  Variables (R : SRS) (x0 : string) (a0 : symbol).
  Notation Sigma :=  (a0 :: x0 ++ sym R).

  Definition P :=
    R ++ map (fun a => [a; a0] / [a0]) Sigma ++ map (fun a => [a0; a] / [a0]) Sigma.
  
  Lemma sym_P :
    sym P <<= Sigma.
  Proof.
(* Goal: @incl (PCP.card nat) R P *)
(* Goal: rewt P y (@cons symbol a0 (@nil symbol)) *)
    unfold P. rewrite !sym_app. eapply incl_app; [ | eapply incl_app].
    - eauto.
    - eapply sym_map. cbn. intros ? [-> | [ | ] % in_app_iff] ? [ | [ | ]]; subst; eauto.
(* Goal: @incl (PCP.card nat) R (@app (PCP.card nat) R (@app (prod (list symbol) (list symbol)) (@map symbol (prod (list symbol) (list symbol)) (fun a : symbol => @pair (list symbol) (list symbol) (@cons symbol a (@cons symbol a0 (@nil symbol))) (@cons symbol a0 (@nil symbol))) (@cons symbol a0 (@app nat x0 (sym R)))) (@map symbol (prod (list symbol) (list symbol)) (fun a : symbol => @pair (list symbol) (list symbol) (@cons symbol a0 (@cons symbol a (@nil symbol))) (@cons symbol a0 (@nil symbol))) (@cons symbol a0 (@app nat x0 (sym R)))))) *)
(* Goal: rewt P y (@cons symbol a0 (@nil symbol)) *)
      inv H. eauto. inv H0. inv H0. eauto. eauto. inv H0. eauto. inv H1.
    - eapply sym_map. cbn. intros ? [-> | [ | ] % in_app_iff] ? [ | [ | ]]; subst; eauto.
(* Goal: @incl (PCP.card nat) R (@app (PCP.card nat) R (@app (prod (list symbol) (list symbol)) (@map symbol (prod (list symbol) (list symbol)) (fun a : symbol => @pair (list symbol) (list symbol) (@cons symbol a (@cons symbol a0 (@nil symbol))) (@cons symbol a0 (@nil symbol))) (@cons symbol a0 (@app nat x0 (sym R)))) (@map symbol (prod (list symbol) (list symbol)) (fun a : symbol => @pair (list symbol) (list symbol) (@cons symbol a0 (@cons symbol a (@nil symbol))) (@cons symbol a0 (@nil symbol))) (@cons symbol a0 (@app nat x0 (sym R)))))) *)
(* Goal: rewt P y (@cons symbol a0 (@nil symbol)) *)
      inv H. eauto. inv H0. inv H0. eauto. eauto. inv H0. eauto. inv H1.
  Qed.

  Lemma rewt_a0_L x :
    x <<= Sigma -> rewt P (a0 :: x) [a0].
  Proof.
(* Goal: forall (x y : string) (_ : rew P x y) (_ : rewt P y (@cons symbol a0 (@nil symbol))) (_ : @ex string (fun y0 : string => and (rewt R y y0) (@In symbol a0 y0))), @ex string (fun y0 : string => and (rewt R x y0) (@In symbol a0 y0)) *)
    intros. induction x.
    - reflexivity.
    - econstructor.
      replace (a0 :: a :: x) with ([] ++ [a0;a] ++ x) by now simpl_list. econstructor.
(* Goal: @incl (PCP.card nat) R P *)
(* Goal: rewt P y (@cons symbol a0 (@nil symbol)) *)
      unfold P. rewrite !in_app_iff, !in_map_iff. eauto 9. firstorder.
  Qed.

  Lemma rewt_a0_R x :
    x <<= Sigma -> rewt P (x ++ [a0]) [a0].
  Proof.
    induction x using rev_ind.
    - econstructor.
    - econstructor. replace ((x1 ++ [x]) ++ [a0]) with (x1 ++ ([x] ++ [a0]) ++ []). econstructor.
(* Goal: @incl (PCP.card nat) R P *)
(* Goal: rewt P y (@cons symbol a0 (@nil symbol)) *)
      cbn. unfold P. rewrite !in_app_iff, !in_map_iff. eauto 9. now simpl_list.
(* Goal: @In symbol a0 y *)
(* Goal: @incl symbol y (@cons symbol a0 (@app nat x0 (sym R))) *)
      rewrite app_nil_r. firstorder.
  Qed.

  Lemma x_rewt_a0 x :
    a0 el x -> x <<= Sigma -> rewt P x [a0].
  Proof.
    intros (y & z & ->) % in_split ?.
(* Goal: rewt P (@app symbol y (@app symbol (@cons symbol a0 (@nil symbol)) z)) (@cons symbol a0 (@nil symbol)) *)
    transitivity (y ++ [a0]).
(* Goal: @incl (PCP.card nat) R (@app (PCP.card nat) R (@app (prod (list symbol) (list symbol)) (@map symbol (prod (list symbol) (list symbol)) (fun a : symbol => @pair (list symbol) (list symbol) (@cons symbol a (@cons symbol a0 (@nil symbol))) (@cons symbol a0 (@nil symbol))) (@cons symbol a0 (@app nat x0 (sym R)))) (@map symbol (prod (list symbol) (list symbol)) (fun a : symbol => @pair (list symbol) (list symbol) (@cons symbol a0 (@cons symbol a (@nil symbol))) (@cons symbol a0 (@nil symbol))) (@cons symbol a0 (@app nat x0 (sym R)))))) *)
(* Goal: rewt P y (@cons symbol a0 (@nil symbol)) *)
    eapply rewt_app_L, rewt_a0_L. eauto.
(* Goal: @incl (PCP.card nat) R (@app (PCP.card nat) R (@app (prod (list symbol) (list symbol)) (@map symbol (prod (list symbol) (list symbol)) (fun a : symbol => @pair (list symbol) (list symbol) (@cons symbol a (@cons symbol a0 (@nil symbol))) (@cons symbol a0 (@nil symbol))) (@cons symbol a0 (@app nat x0 (sym R)))) (@map symbol (prod (list symbol) (list symbol)) (fun a : symbol => @pair (list symbol) (list symbol) (@cons symbol a0 (@cons symbol a (@nil symbol))) (@cons symbol a0 (@nil symbol))) (@cons symbol a0 (@app nat x0 (sym R)))))) *)
(* Goal: rewt P y (@cons symbol a0 (@nil symbol)) *)
    eapply rewt_a0_R. eauto.
  Qed.
  
  Lemma SR_SRH x :
    x <<= Sigma ->
    rewt P x [a0] -> exists y, rewt R x y /\ a0 el y.
  Proof.
(* Goal: forall (x y : string) (_ : rew P x y) (_ : rewt P y (@cons symbol a0 (@nil symbol))) (_ : @ex string (fun y0 : string => and (rewt R y y0) (@In symbol a0 y0))), @ex string (fun y0 : string => and (rewt R x y0) (@In symbol a0 y0)) *)
    intros. pattern x; refine (rewt_induct _ _ H0).
(* Goal: @incl (PCP.card nat) R (@app (PCP.card nat) R (@app (prod (list symbol) (list symbol)) (@map symbol (prod (list symbol) (list symbol)) (fun a : symbol => @pair (list symbol) (list symbol) (@cons symbol a (@cons symbol a0 (@nil symbol))) (@cons symbol a0 (@nil symbol))) (@cons symbol a0 (@app nat x0 (sym R)))) (@map symbol (prod (list symbol) (list symbol)) (fun a : symbol => @pair (list symbol) (list symbol) (@cons symbol a0 (@cons symbol a (@nil symbol))) (@cons symbol a0 (@nil symbol))) (@cons symbol a0 (@app nat x0 (sym R)))))) *)
(* Goal: rewt P y (@cons symbol a0 (@nil symbol)) *)
    + exists [a0]. split. reflexivity. eauto.
(* Goal: @ex string (fun y : string => and (rewt R x1 y) (@In symbol a0 y)) *)
    + clear H H0. intros. inv H. destruct H1 as [y []].
(* Goal: @ex string (fun y : string => and (rewt R (@app nat x2 (@app nat u y0)) y) (@In symbol a0 y)) *)
      unfold P in H2. eapply in_app_iff in H2 as [ | [ (? & ? & ?) % in_map_iff | (? & ? & ?) % in_map_iff ] % in_app_iff].
      * exists y. eauto using rewt, rew.
      * inv H2. eauto 9 using rewt.
      * inv H2. eauto 9 using rewt.
  Qed.

  Lemma equi :
    SRH (R, x0, a0) <-> SR (P, x0, [a0]).
  Proof.
(* Goal: iff (SRH (@pair (prod SRS string) symbol (@pair SRS string R x0) a0)) (SR (@pair (prod (list (PCP.card nat)) string) (list symbol) (@pair (list (PCP.card nat)) string P x0) (@cons symbol a0 (@nil symbol)))) *)
    split.
    - intros (y & H & Hi).
(* Goal: @incl (PCP.card nat) R P *)
(* Goal: rewt P y (@cons symbol a0 (@nil symbol)) *)
      unfold SR. transitivity y. eapply (rewt_subset H). unfold P. eauto.
(* Goal: @incl (PCP.card nat) R (@app (PCP.card nat) R (@app (prod (list symbol) (list symbol)) (@map symbol (prod (list symbol) (list symbol)) (fun a : symbol => @pair (list symbol) (list symbol) (@cons symbol a (@cons symbol a0 (@nil symbol))) (@cons symbol a0 (@nil symbol))) (@cons symbol a0 (@app nat x0 (sym R)))) (@map symbol (prod (list symbol) (list symbol)) (fun a : symbol => @pair (list symbol) (list symbol) (@cons symbol a0 (@cons symbol a (@nil symbol))) (@cons symbol a0 (@nil symbol))) (@cons symbol a0 (@app nat x0 (sym R)))))) *)
(* Goal: rewt P y (@cons symbol a0 (@nil symbol)) *)
      eapply x_rewt_a0. firstorder. eapply rewt_sym with (x := x0); eauto.
    - intros H. unfold SRH, SR in *.
(* Goal: @incl (PCP.card nat) R (@app (PCP.card nat) R (@app (prod (list symbol) (list symbol)) (@map symbol (prod (list symbol) (list symbol)) (fun a : symbol => @pair (list symbol) (list symbol) (@cons symbol a (@cons symbol a0 (@nil symbol))) (@cons symbol a0 (@nil symbol))) (@cons symbol a0 (@app nat x0 (sym R)))) (@map symbol (prod (list symbol) (list symbol)) (fun a : symbol => @pair (list symbol) (list symbol) (@cons symbol a0 (@cons symbol a (@nil symbol))) (@cons symbol a0 (@nil symbol))) (@cons symbol a0 (@app nat x0 (sym R)))))) *)
(* Goal: rewt P y (@cons symbol a0 (@nil symbol)) *)
      eapply SR_SRH in H; eauto.
  Qed.
          
End SRH_SR.

Theorem reduction :
  SRH ⪯ SR.
Proof.
(* Goal: @reduces (prod (prod SRS string) nat) (prod (prod SRS string) string) SRH SR *)
  exists (fun '(R, x, a) => (P R x a, x, [a])). intros [[R x0] a0].
(* Goal: iff (SRH (@pair (prod SRS string) nat (@pair SRS string R x0) a0)) (SR (@pair (prod (list (PCP.card nat)) string) (list symbol) (@pair (list (PCP.card nat)) string (P R x0 a0) x0) (@cons symbol a0 (@nil symbol)))) *)
  now eapply equi.
Qed.
