Require Import Undecidability.StringRewriting.SR.
Require Import Undecidability.StringRewriting.Util.Definitions.
Require Import List.
Import ListNotations.
Require Import Undecidability.Synthetic.Definitions.

Require Import Undecidability.Shared.ListAutomation.
Import ListAutomationNotations.

Import RuleNotation.

Set Default Proof Using "Type".


Section SRH_SR.

  Local Notation "A <<= B" := (incl A B) (at level 70).
  Local Notation symbol := .
  Local Notation string := (string ).
  Local Notation SRS := (SRS ).
  Variables (R : SRS) ( : string) ( : symbol).
  Notation Sigma := ( :: sym R).

  Definition P :=
    R map ( a [a; ] / []) Sigma map ( a [; a] / []) Sigma.

  Lemma sym_P :
    sym P Sigma.
  Proof.
    unfold P. rewrite !sym_app. eapply incl_app; [ | eapply incl_app].
    - eauto.
    - eapply sym_map. cbn. intros ? [ | [ | ] % in_app_iff] ? [ | [ | ]]; subst; eauto.
      inv H. eauto. inv . inv . eauto. eauto. inv . eauto. inv .
    - eapply sym_map. cbn. intros ? [ | [ | ] % in_app_iff] ? [ | [ | ]]; subst; eauto.
      inv H. eauto. inv . inv . eauto. eauto. inv . eauto. inv .
  Qed.


  Lemma rewt_a0_L x :
    x Sigma rewt P ( :: x) [].
  Proof.
    intros. induction x.
    - reflexivity.
    - econstructor.
      replace ( :: a :: x) with ([] [;a] x) by now simpl_list. econstructor.
      unfold P. rewrite !in_app_iff, !in_map_iff. eauto 9. firstorder.
  Qed.


  Lemma rewt_a0_R x :
    x Sigma rewt P (x []) [].
  Proof.
    induction x using rev_ind.
    - econstructor.
    - econstructor. replace (( [x]) []) with ( ([x] []) []). econstructor.
      cbn. unfold P. rewrite !in_app_iff, !in_map_iff. eauto 9. now simpl_list.
      rewrite app_nil_r. firstorder.
  Qed.


  Lemma cons_incl X (a : X) (A B : list X) : a :: A B A B.
  Proof. intros ? ? ?. eapply H. firstorder. Qed.

  Lemma app_incl_l X (A B C : list X) : A B C A C.
  Proof. firstorder eauto. Qed.

  Lemma app_incl_R X (A B C : list X) : A B C B C.
  Proof. firstorder eauto. Qed.

  Lemma x_rewt_a0 x :
     x x Sigma rewt P x [].
  Proof.
    intros (y & z & ) % in_split ?.
    transitivity (y []).
    eapply rewt_app_L, rewt_a0_L. eapply cons_incl. eapply app_incl_R. eassumption.
    eapply rewt_a0_R. eapply app_incl_l. eassumption.
  Qed.


  Lemma SR_SRH x :
    x Sigma
    rewt P x [] y, rewt R x y y.
  Proof.
    intros. pattern x; refine (rewt_induct _ _ ).
    + exists []. split. reflexivity. eauto.
    + clear H . intros. inv H. destruct as [y []].
      unfold P in . eapply in_app_iff in as [ | [ (? & ? & ?) % in_map_iff | (? & ? & ?) % in_map_iff ] % in_app_iff].
      * exists y. eauto using rewS, rewB, rewR.
      * inv . eauto 9 using rewS, rewB, rewR.
      * inv . eauto 9 using rewS, rewB, rewR.
  Qed.


  Lemma equi :
    SRH (R, , ) SR (P, , []).
  Proof.
    split.
    - intros (y & H & Hi).
      unfold SR. transitivity y. eapply (rewt_subset H). unfold P. eapply incl_appl. eapply incl_refl.
      eapply x_rewt_a0. firstorder. eapply rewt_sym with (x := ); eauto.
    - intros H. unfold SRH, SR in *.
      eapply SR_SRH in H; eauto.
  Qed.


End SRH_SR.

Theorem reduction :
  SRH SR.
Proof.
  exists ( '(R, x, a) (P R x a, x, [a])). intros [[R ] ].
  now eapply equi.
Qed.