From Coq Require Import List.
From PCF2.Autosubst Require Import pcf_2.
From PCF2 Require Import preliminaries pcf_2_system pcf_2_utils CE CE_facts PS PS_facts RPS RPS_facts.
From PCF2.external Require Import SR.
From PCF2.external.Synthetic Require Import Definitions ReducibilityFacts.
Set Default Goal Selector "!".

Lemma restrict_sys (sys: ps_system) (T: ty) (sys_wf: forall p, In p sys -> (cons T nil) ⊢ (fst p): Base /\ nil ⊢ (snd p): Base):
    sig (fun rsys: rps_system => rps_system_well_formed rsys T /\ (forall sol, nil ⊢ sol : T -> solves_rps_system rsys sol <-> solves_ps_system sys sol)).
Proof.
    induction sys.
    - exists nil. split.
    + apply Forall_nil.
    + intros sol. split.
        all: intros _; apply Forall_nil.
    - assert (H1: In a (a::sys)) by firstorder. destruct (sys_wf a H1) as [pfst psnd].
    assert (H2: forall p, In p sys -> (cons T nil) ⊢ (fst p): Base /\ nil ⊢ (snd p): Base) by firstorder.
    specialize (IHsys H2). destruct IHsys as [sys' [Hsys'_wf Hsys'_char]].
    destruct (weak_normalisation_comp (snd a) psnd) as [v [eval_v val_v]]. destruct v; try easy.
    + exists (cons (fst a, true) sys'). split.
        1: rewrite riq_sys_wf_cons_char; split; eauto.
        intros sol typed_sol. split.
        * intro H. rewrite iq_sys_val_cons_char. rewrite res_ineq_sys_val_cons_char in H. destruct H as [Hsys H].
        split.
        -- now rewrite <- Hsys'_char.
        -- cbn in H. specialize (base_preord_tt_le _ H). intros H'. eapply norm_comp. {split. 1: exact eval_v. easy. } split; eauto.
        * intro H. rewrite iq_sys_val_cons_char in H. rewrite res_ineq_sys_val_cons_char.
        destruct H as [Hsys H].
        split.
        -- now rewrite Hsys'_char.
        -- cbn. inv H.
            ++ exfalso. enough (bot = tt) by easy. eapply evaluates_to_same; split; eauto.
            ++ enough (z = tt).
                ** subst. eapply norm_comp; eauto.
                ** now eapply (evaluates_to_same (snd a)).
    + exists (cons (fst a, false) sys'). split.
    1: rewrite riq_sys_wf_cons_char; split; eauto.
    intros sol typed_sol. split.
    * intro H. rewrite iq_sys_val_cons_char. rewrite res_ineq_sys_val_cons_char in H. destruct H as [Hsys H].
        split.
        -- now rewrite <- Hsys'_char.
        -- cbn in H. specialize (base_preord_ff_le _ H). intros H'. eapply norm_comp; eauto. {split. 1: exact eval_v. easy. } split; eauto.
    * intro H. rewrite iq_sys_val_cons_char in H. rewrite res_ineq_sys_val_cons_char.
        destruct H as [Hsys H].
        split.
        -- now rewrite Hsys'_char.
        -- cbn. inv H.
            ++ exfalso. enough (bot = ff) by easy. eapply evaluates_to_same; split; eauto.
            ++ enough (z = ff).
            ** subst. eapply norm_comp; eauto.
            ** now eapply (evaluates_to_same (snd a)).
    + exists sys'. split; eauto.
        intros sol typed_sol. split.
        * intro H. rewrite iq_sys_val_cons_char. split.
        1: now rewrite <- Hsys'_char.
        now constructor.
        * intro H. rewrite iq_sys_val_cons_char in H. destruct H as [H _].
        now rewrite Hsys'_char.
Qed.

Lemma well_formed_forall (sys: wf_ps_system):
    forall p, In p (fst (proj1_sig sys)) -> (cons (snd (proj1_sig sys)) nil) ⊢ (fst p): Base /\ nil ⊢ (snd p): Base.
Proof.
    destruct sys as [[sys T] H]. cbn. induction H.
    1: firstorder.
    intros p [H1 | H1].
    1: now subst.
    now apply IHForall.
Qed.

Lemma reduces_PS_RPS:
    reduces PS RPS.
Proof.
    exists (fun sys => let H := restrict_sys (fst (proj1_sig sys)) (snd (proj1_sig sys)) (well_formed_forall sys) in
            let sys'_wf := match proj2_sig H with | conj wf _ => wf end in
            exist _ (proj1_sig H, snd (proj1_sig sys)) (sys'_wf)); cbn.
    intro sys.
    destruct (restrict_sys (fst (proj1_sig sys)) (snd (proj1_sig sys)) (well_formed_forall sys)) as [sys' [sys'_wf sys'_char]]; cbn.
    split.
    all: intros [sol Hsol]; exists sol; firstorder.
Qed.

Lemma reduces_co_PS_co_RPS:
    reduces (complement PS) (complement RPS).
Proof.
    apply reduces_complement. apply reduces_PS_RPS.
Qed.