From Undecidability.PCP Require Import PCP Util.PCP_facts.
From Undecidability.FOL Require Import Deduction.FragmentNDFacts Semantics.Tarski.FragmentFacts Semantics.Tarski.FragmentSoundness Syntax.Core Syntax.Facts.
From Undecidability.FOL.Undecidability Require Import FOL.
From Undecidability.Synthetic Require Import Definitions DecidabilityFacts EnumerabilityFacts ReducibilityFacts.
Require Import Undecidability.FOL.Undecidability.Reductions.PCPb_to_FOL.
Require Import Undecidability.PCP.Reductions.PCPb_iff_dPCPb.
Require Import List.
Require Import Undecidability.Shared.ListAutomation.
Import ListNotations.

Set Default Proof Using "Type".


Implicit Type b : falsity_flag.

Definition cprv := @prv _ _ falsity_on class.

#[global]
Instance iUnit (P : Prop) : interp unit.
Proof.
  split; intros [] v.
  - exact tt.
  - exact tt.
  - exact True.
  - exact P.
Defined.

Local Hint Constructors prv : core.

Fixpoint cast {b} (phi : form b) : form falsity_on :=
  match phi with
  | atom P v => atom P v
  | falsity => falsity
  | bin Impl phi psi => bin (b := falsity_on) Impl (cast phi) (cast psi)
  | quant All phi => quant (b := falsity_on) All (cast phi)
  end.

Lemma subst_cast {b} sigma phi :
  cast (subst_form sigma phi) = subst_form sigma (cast phi).
Proof.
  induction phi in sigma |- *; cbn in *; trivial.
  - destruct b0. cbn. congruence.
  - destruct q. cbn. congruence.
Qed.

Lemma MND_CND A (phi : form falsity_off) :
  A ⊢M phi -> map cast A ⊢C cast phi.
Proof.
  revert A phi. remember falsity_off as b. intros.
  induction H; cbn in *; subst; try congruence.
  - eapply II; eauto.
  - eapply IE; try now apply IHprv1. now apply IHprv2.
  - eapply AllI. rewrite map_map. rewrite map_map in IHprv.
    erewrite map_ext; try now apply IHprv. intros psi. cbn. now rewrite subst_cast.
  - setoid_rewrite subst_cast. eapply AllE; eauto.
  - eapply Ctx, in_map_iff; eauto.
  - apply Pc.
Qed.

Lemma DN A phi :
  A ⊢C (¬¬phi) -> A ⊢C phi.
Proof.
  intros H. eapply IE with ((phi → falsity) → phi); try apply Pc.
  apply II, Exp. eapply IE. apply (Weak H); auto. now apply Ctx.
Qed.

Lemma cnd_XM:
  (forall (phi : form falsity_on), cprv nil phi -> valid phi) ->
  forall P, ~~ P -> P.
Proof.
  intros H P. specialize (H ((¬¬Q) → Q)).
  refine (H _ unit (iUnit P) (fun _ => tt)).
  eapply II. eapply DN. eauto.
Qed.

Definition dnQ {b} (phi : form b) : form b := (phi → Q) → Q.

Fixpoint trans {b} (phi : form b) : form b :=
  match phi with
  | bin Impl phi1 phi2 => bin Impl (trans phi1) (trans phi2)
  | quant All phi => quant All (trans phi)
  | atom sPr v => dnQ (atom sPr v)
  | atom _ _ => atom sQ (Vector.nil _)
  | falsity => @atom _ _ _ falsity_on sQ (Vector.nil _)
  end.

Lemma trans_subst b sigma (phi : form b) :
  trans (subst_form sigma phi) = subst_form sigma (trans phi).
Proof.
  induction phi in sigma |- *; cbn; trivial.
  - now destruct P.
  - destruct b0. cbn. congruence.
  - destruct q. cbn. congruence.
Qed.

Lemma appCtx b psi1 psi2 A :
  In (psi1 → psi2) A -> A ⊢I psi1 -> A ⊢I psi2.
Proof.
  intros. eapply (IE (phi := psi1) (psi := psi2)); eauto using Ctx.
Qed.

Lemma app1 b psi1 psi2 A :
  (psi1 → psi2 :: A) ⊢I psi1 -> (psi1 → psi2 :: A) ⊢I psi2.
Proof.
  intros. eapply appCtx; eauto.
Qed.

Lemma app2 b psi1 psi2 A phi :
  (phi :: psi1 → psi2 :: A) ⊢I psi1 -> (phi :: psi1 → psi2 :: A) ⊢I psi2.
Proof.
  intros. eapply appCtx; eauto.
Qed.

Lemma app3 b psi1 psi2 A phi phi2 :
  (phi :: phi2 :: psi1 → psi2 :: A) ⊢I psi1 -> (phi :: phi2 :: psi1 → psi2 :: A) ⊢I psi2.
Proof.
  intros. eapply appCtx; eauto.
Qed.

Lemma trans_trans' b (phi : form b) A sigma tau :
  (map (subst_form tau) A) ⊢I ((dnQ (trans phi[sigma])) → trans phi[sigma]).
Proof.
  revert A sigma tau. induction phi; cbn; intros; try destruct P; try destruct b0; try destruct q.
  - cbn. eapply II. eapply app1. eapply II. eapply Ctx. eauto.
  - eapply II. eapply II. eapply app2. eapply II.
    eapply app1. eapply Ctx. eauto.
  - eapply II. eapply app1. eapply II. eapply Ctx. eauto.
  - eapply II. eapply II. apply IE with (dnQ (trans phi2[sigma])). specialize (IHphi2 A sigma tau). apply (Weak IHphi2). auto.
    eapply II. eapply app3. eapply II. eapply app2. eapply app1. eapply Ctx. eauto.
  - apply II, AllI. apply IE with (dnQ (trans phi[up sigma])).
    + apply IHphi.
    + apply II. eapply IE. { apply Ctx. right. left. cbn. reflexivity. }
      apply II. eapply IE. { apply Ctx. right. left. reflexivity. }
      replace (trans phi[up sigma]) with (((trans (phi[up sigma]))[up ↑])[($0)..]) at 4.
      * apply AllE. apply Ctx. now left.
      * setoid_rewrite trans_subst. cbn. repeat setoid_rewrite subst_comp.
        apply subst_ext. intros n. unfold funcomp. cbn.
        apply subst_term_id. now intros [].
Qed.

Lemma trans_trans b (phi : form b) A :
  A ⊢I ((dnQ (trans phi)) → trans phi).
Proof.
  specialize (trans_trans' phi A var var).
  rewrite subst_var. intros H. apply (Weak H).
  clear H. induction A; cbn; trivial. setoid_rewrite subst_var. auto.
Qed.

Goal (forall X, ~ ~ X -> X) -> (forall (X Y : Prop), ((X -> Y) -> X) -> X).
Proof.
  intros H X Y. apply H. intros H'. clear H.
  apply H'. intros f. apply f. intros x. exfalso.
  apply H'. intros _. exact x.
Qed.

Lemma Double' b A (phi : form b) :
  A ⊢C phi -> map trans A ⊢I trans phi.
Proof.
  remember class as s; induction 1; subst.
  - cbn. eapply II. eauto.
  - eapply IE; eauto.
  - cbn. apply AllI. rewrite map_map. rewrite map_map in IHprv.
    erewrite map_ext; try now apply IHprv. intros psi. cbn. now rewrite trans_subst.
  - setoid_rewrite trans_subst. eapply AllE; eauto.
  - specialize (IHprv eq_refl). eapply IE; try apply trans_trans.
    apply II. apply (Weak IHprv). auto.
  - eapply Ctx. now eapply in_map.
  - eapply IE; try apply trans_trans.
    apply II. eapply IE; try now apply Ctx.
    cbn. apply II. eapply IE; try now apply Ctx.
    apply II. eapply IE; try apply trans_trans.
    apply II. eapply IE.
    + apply Ctx. right. right. right. now left.
    + apply II. apply Ctx. auto.
Qed.

Lemma Double b (phi : form b) :
  [] ⊢C phi -> [] ⊢I (trans phi).
Proof.
  eapply Double'.
Qed.


Section BPCP_CND.
  Local Definition BSRS := list (card bool).
  Variable R : BSRS.
  Context {ff : falsity_flag}.

  Lemma BPCP_to_CND :
    PCPb R -> [] ⊢C (F R).
  Proof.
    intros H. rewrite PCPb_iff_dPCPb in *. now apply BPCP_prv'.
  Qed.

  Lemma impl_trans A phi :
    trans (A ==> phi) = (map trans A) ==> trans phi.
  Proof.
    induction A; cbn; congruence.
  Qed.

  Lemma CND_BPCP :
    [] ⊢C (F R) -> PCPb R.
  Proof.
    intros H % Double % soundness.
    specialize (H _ (IB R) (fun _ => nil)).
    unfold F, F1, F2 in H. rewrite !impl_trans, !map_map, !impl_sat in H. cbn in H.
    eapply PCPb_iff_dPCPb. eapply H; try tauto.
    - intros ? [(x,y) [<- ?] ] % in_map_iff ?. cbn in *. eapply H1.
      left. now rewrite !IB_enc.
    - intros ? [(x,y) [<- ?] ] % in_map_iff ? ? ? ?. cbn in *. eapply H1. intros.
      eapply H2. rewrite !IB_prep. cbn. econstructor 2; trivial.
    - intros. eapply H0. intros. unfold dPCPb, dPCP. eauto.
  Qed.

  Lemma BPCP_CND :
    PCPb R <-> [] ⊢C (F R).
  Proof.
    split. eapply BPCP_to_CND. intros ? % CND_BPCP. eauto.
  Qed.

End BPCP_CND.

Theorem cprv_red :
  PCPb ⪯ FOL_prv_class.
Proof.
  exists (fun R => F R). intros R. apply (BPCP_CND R).
Qed.


Corollary cprv_undec :
  UA -> ~ decidable (cprv nil).
Proof.
  intros H. now apply (not_decidable cprv_red).
Qed.

Corollary cprv_unenum :
  UA -> ~ enumerable (complement (@cprv nil)).
Proof.
  intros H. apply (not_coenumerable cprv_red); trivial.
Qed.