From Undecidability.FOL
     Require Import Semantics.Tarski.FullFacts Syntax.Facts Deduction.FullNDFacts.

From Undecidability.FOL.Sets
     Require Import ZF minZF.

From Undecidability.FOL.Undecidability.Reductions
     Require Import PCPb_to_ZF PCPb_to_minZF PCPb_to_ZFD.

From Undecidability Require Import Shared.ListAutomation.
Import ListAutomationNotations.
Local Set Implicit Arguments.
Local Unset Strict Implicit.

Open Scope syn.

Local Hint Constructors prv : core.


Lemma elem_iff { p : peirce } A x y :
  minZFeq' <<= A -> A ⊢ ∃ $0 ≡' $(S x) ∧ (∃ $0 ≡' $(S (S y)) ∧ $1 ∈' $0) <-> A ⊢ $x ∈' $y.
Proof.
  intros HA. split; intros H.
  - use_exists' H x'. clear H. assert1 H. apply CE in H as [_ H].
    use_exists' H y'. eapply minZF_elem; auto. 1,2: eapply CE1; eauto. eapply CE2; auto.
  - apply ExI with $x. cbn. apply CI; try apply minZF_refl; auto.
    apply ExI with $y. cbn. apply CI; try apply minZF_refl; auto.
Qed.

Lemma equal_iff { p : peirce } A x y :
  minZFeq' <<= A -> A ⊢ ∃ $0 ≡' $(S x) ∧ (∃ $0 ≡' $(S (S y)) ∧ $1 ≡' $0) <-> A ⊢ $x ≡' $y.
Proof.
  intros HA. split; intros H.
  - use_exists' H x'. clear H. assert1 H. apply CE in H as [_ H].
    use_exists' H y'. eapply minZF_trans; auto. 2: eapply CE1; auto.
      apply minZF_sym; auto. eapply minZF_trans; auto. 2: eapply CE1; auto.
      apply minZF_sym; auto. eapply CE2; auto.
  - apply ExI with $x. cbn. apply CI; try apply minZF_refl; auto.
    apply ExI with $y. cbn. apply CI; try apply minZF_refl; auto.
Qed.

Lemma loop_deductive { p : peirce } phi :
  minZFeq' ⊢ phi ↔ rm_const_fm (embed phi).
Proof.
  induction phi using form_ind_subst; cbn.
  - apply CI; apply II; auto.
  - rewrite (vec_inv2 t). cbn.
    destruct Vector.hd as [x|[]], (Vector.hd (Vector.tl t)) as [y|[]]. cbn.
    destruct P0; cbn in *; apply CI; apply II.
    + apply elem_iff; auto.
    + apply elem_iff; auto.
    + apply equal_iff; auto.
    + apply equal_iff; auto.
  - destruct b0; cbn in *; apply CI; apply II.
    + apply CE1 in IHphi1. apply CE1 in IHphi2. apply CI; eapply IE.
      1,3: eapply Weak; eauto. eapply CE1; auto. eapply CE2; auto.
    + apply CE2 in IHphi1. apply CE2 in IHphi2. apply CI; eapply IE.
      1,3: eapply Weak; eauto. eapply CE1; auto. eapply CE2; auto.
    + apply CE1 in IHphi1. apply CE1 in IHphi2. eapply DE; try now apply Ctx.
      * apply DI1. eapply IE; try now apply Ctx. eapply Weak; try apply IHphi1. auto.
      * apply DI2. eapply IE; try now apply Ctx. eapply Weak; try apply IHphi2. auto.
    + apply CE2 in IHphi1. apply CE2 in IHphi2. eapply DE; try now apply Ctx.
      * apply DI1. eapply IE; try now apply Ctx. eapply Weak; try apply IHphi1. auto.
      * apply DI2. eapply IE; try now apply Ctx. eapply Weak; try apply IHphi2. auto.
    + apply CE2 in IHphi1. apply CE1 in IHphi2. apply II. eapply IE.
      eapply Weak; eauto. eapply IE. auto. eapply IE; try now apply Ctx. eapply Weak; eauto.
    + apply CE1 in IHphi1. apply CE2 in IHphi2. apply II. eapply IE.
      eapply Weak; eauto. eapply IE. auto. eapply IE; try now apply Ctx. eapply Weak; eauto.
  - destruct q; cbn in *; apply CI; apply II.
    + prv_all' x. rewrite rm_const_fm_subst, <- embed_subst. eapply IE.
      * eapply Weak; try eapply CE1, H. auto.
      * apply AllE. auto.
    + prv_all' x. eapply IE.
      * eapply Weak; try eapply CE2, H. auto.
      * rewrite embed_subst, <- rm_const_fm_subst. apply AllE. auto.
    + assert1 H'. use_exists' H' x. apply ExI with x.
      rewrite rm_const_fm_subst, <- embed_subst. eapply IE; try now apply Ctx.
      eapply Weak; try eapply CE1, H. auto.
    + assert1 H'. use_exists' H' x. apply ExI with x.
      rewrite rm_const_fm_subst, <- embed_subst. eapply IE; try now apply Ctx.
      eapply Weak; try eapply CE2, H. auto.
Qed.

Lemma loop_deductive' { p : peirce } phi A :
  minZFeq' <<= A -> A ⊢ rm_const_fm (embed phi) -> A ⊢ phi.
Proof.
  intros H1 H2. eapply IE; try apply H2. eapply CE2.
  eapply Weak; try apply H1. apply loop_deductive.
Qed.

Theorem conservativity_ZF' { p : peirce } phi :
  ZFeq' ⊢ embed phi -> minZFeq' ⊢ phi.
Proof.
  intros H. apply (@rm_const_prv _ nil) in H. cbn in H. now apply loop_deductive'.
Qed.

Lemma Z_decomp { p : peirce } phi :
  Zeq ⊢T phi -> exists A, (map ax_sep A ++ ZFeq') ⊢ phi.
Proof.
  intros [A [H1 H2]]. induction A in phi, H1, H2 |- *.
  - exists nil. cbn. eapply Weak; eauto.
  - rewrite <- imps in H2. apply IHA in H2 as [B H]; auto.
    rewrite imps in H. destruct (H1 a); auto.
    + exists B. eapply Weak; try apply H. auto.
    + exists (phi0 :: B). cbn. apply H.
Qed.

Lemma minZF_sep { p : peirce } A phi :
  minZFeq' <<= A -> A ⊢ ax_sep' (rm_const_fm phi) → rm_const_fm (ax_sep phi).
Proof.
  intros HA. apply II. assert1 H. cbn in *.
  eapply all_equiv. 2: apply Ctx; now left. intros [x|[]]. cbn.
  apply ex_equiv. intros B [y|[]] HB. cbn.
  apply all_equiv. intros [z|[]]. cbn.
  apply iff_equiv; intros C HC.
  2: apply and_equiv. 1,2: apply elem_iff; intros psi; auto.
  rewrite !rm_const_fm_subst. cbn; subsimpl; rewrite !subst_comp.
  erewrite subst_ext; try reflexivity. now intros [|n].
Qed.

Theorem conservativity_Z { p : peirce } phi :
  Zeq ⊢T embed phi -> minZeq ⊢T phi.
Proof.
  intros [A HA] % Z_decomp. apply rm_const_prv in HA.
  rewrite map_map in HA. apply loop_deductive' in HA; auto.
  exists ([ax_sep' (rm_const_fm psi) | psi ∈ A] ++ minZFeq'). split.
  - intros psi [H|H] % in_app_iff; try now constructor.
    apply in_map_iff in H as [psi'[<- H]]. constructor 2.
  - apply (prv_cut HA). intros psi [[psi' [<- H]] % in_map_iff|H] % in_app_iff; auto.
    eapply IE; try apply minZF_sep; auto. apply Ctx, in_app_iff. left. refine (in_map _ _ _ H).
Qed.

Lemma ZF_decomp { p : peirce } phi :
  ZFeq ⊢T phi -> exists A B, ((map ax_sep A ++ map ax_rep B) ++ ZFeq') ⊢ phi.
Proof.
  intros [C [H1 H2]]. induction C in phi, H1, H2 |- *.
  - exists nil, nil. cbn. eapply Weak; eauto.
  - rewrite <- imps in H2. apply IHC in H2 as [A[B HAB]]; auto.
    rewrite imps in HAB. destruct (H1 a); auto.
    + exists A, B. eapply Weak; try apply HAB. auto.
    + exists (phi0 :: A), B. cbn. apply HAB.
    + exists A, (phi0 :: B). cbn. eapply Weak; try apply HAB.
      intros psi [->|[[H|H] % in_app_iff|H] % in_app_iff]; auto.
      apply in_app_iff. left. apply in_app_iff. right. now right.
Qed.

Lemma minZF_rep { p : peirce } A phi :
  minZFeq' <<= A -> A ⊢ ax_rep' (rm_const_fm phi) → rm_const_fm (ax_rep phi).
Proof.
  intros HA. apply II. assert1 H. cbn in *. eapply impl_equiv. 3: apply Ctx; now left.
  - intros B HB. apply all_equiv. intros [x|[]]. cbn. apply all_equiv. intros [y|[]]. cbn.
    apply all_equiv. intros [z|[]]. cbn. apply impl_equiv; intros C HC.
    + rewrite !rm_const_fm_subst, !subst_comp.
      erewrite subst_ext; try reflexivity. now intros [|[|n]].
    + apply impl_equiv; intros D HD. 2: eapply equal_iff; intros psi HP; apply HD; auto.
      rewrite !rm_const_fm_subst, !subst_comp.
      erewrite subst_ext; try reflexivity. now intros [|[|n]].
  - intros B HB. apply all_equiv. intros [x|[]]. cbn.
    apply ex_equiv. intros C [y|[]] HC. cbn.
    apply all_equiv. intros [z|[]]. cbn.
    apply iff_equiv; intros D HD. 1: apply elem_iff; intros psi HP; apply HD; auto.
    apply ex_equiv. intros E [u|[]] HE. cbn.
    apply and_equiv. 1: apply elem_iff; intros psi HP; apply HE, HD; auto.
    rewrite !rm_const_fm_subst. cbn; subsimpl; rewrite !subst_comp.
    erewrite subst_ext; try reflexivity. now intros [|[|n]].
Qed.

Theorem conservativity_ZF { p : peirce } phi :
  ZFeq ⊢T embed phi -> minZFeq ⊢T phi.
Proof.
  intros [A [B HAB]] % ZF_decomp. apply rm_const_prv, loop_deductive' in HAB; auto.
  exists ([ax_sep' (rm_const_fm psi) | psi ∈ A] ++ [ax_rep' (rm_const_fm psi) | psi ∈ B] ++ minZFeq'). split.
  - intros psi [|[H|H] % in_app_iff] % in_app_iff; try now constructor.
    all: apply in_map_iff in H as [psi'[<- H]]. constructor 2. constructor 3.
  - apply (prv_cut HAB). intros psi [[psi' [<- H]] % in_map_iff|H] % in_app_iff.
    + apply in_app_iff in H as [[phi' [<- H]] % in_map_iff|[phi' [<- H]] % in_map_iff].
      * eapply IE; try apply minZF_sep; auto. apply Ctx, in_app_iff. left. refine (in_map _ _ _ H).
      * eapply IE; try apply minZF_rep; auto. apply Ctx, in_app_iff. right.
        apply in_app_iff. left. refine (in_map _ _ _ H).
    + auto. apply Ctx. auto.
Qed.


Lemma prv_embed { p : peirce } A phi :
  A ⊢ phi -> (map embed A) ⊢ embed phi.
Proof.
  intros H. pattern p, A, phi. revert p A phi H.
  apply prv_ind_full; cbn; intros; subst; auto. 1,6-9: eauto.
  - apply AllI. apply (Weak H0).
    rewrite !map_map. intros psi' [psi [<- HP]] % in_map_iff.
    apply in_map_iff. eexists. split; try apply HP.
    rewrite embed_subst. apply subst_ext. reflexivity.
  - apply (AllE (embed_t t)) in H0. rewrite embed_subst.
    erewrite subst_ext; try apply H0. now intros [|n].
  - apply (ExI (embed_t t)). rewrite embed_subst in H0.
    erewrite subst_ext; try apply H0. now intros [|n].
  - eapply ExE; try apply H0. rewrite embed_subst in H2.
    erewrite subst_ext; try apply (Weak H2); try now intros [|n].
    rewrite !map_map. intros theta' [<-|[theta [<- HP]] % in_map_iff]; auto.
    right. apply in_map_iff. eexists. split; try apply HP.
    rewrite embed_subst. apply subst_ext. reflexivity.
Qed.

Lemma ZF_eset { p : peirce } :
  ZFeq' ⊢ ∀ ¬ $0 ∈ ∅.
Proof.
  assert (H : ZFeq' ⊢ ax_eset) by (apply Ctx; unfold ZFeq', ZF'; eauto 6).
  prv_all x. apply (AllE x H).
Qed.

Lemma ZF_inductive_embed { p : peirce } t :
  ZFeq' ⊢ inductive t ↔ (embed (is_inductive $0))[t..].
Proof.
  cbn. apply CI; apply II; apply CI.
  - apply (ExI ∅). cbn. subsimpl. apply CI; try apply (Weak ZF_eset); auto.
    eapply CE1. apply Ctx. left. reflexivity.
  - prv_all x. apply II. apply (ExI (σ x)). cbn. subsimpl. apply CI.
    + prv_all y. apply CI. 1: apply bunion_use; auto. eapply II, DE; try now apply Ctx.
      * apply ZF_bunion_el1; auto.
      * apply ZF_bunion_el2; auto. apply ZF_pair_el'; auto.
    + eapply IE; try now apply Ctx. assert2 H.
      apply CE2, (AllE x) in H. cbn in H. now subsimpl_in H.
  - assert1 H. apply CE1 in H. use_exists H x. clear H. eapply ZF_eq_elem; auto.
    2: apply ZF_refl'; auto. 2: eapply CE2; eauto. apply ZF_ext'; auto.
    + prv_all y. apply II. apply Exp. assert2 H. apply CE1 in H. apply (AllE y) in H.
      cbn in H. subsimpl_in H. apply (IE H). auto.
    + prv_all y. apply II. apply Exp. eapply IE; try now apply Ctx. apply ZF_eset'. auto.
  - prv_all x. assert1 H. apply CE2 in H. apply (AllE x) in H. cbn in H. subsimpl_in H.
    rewrite imps in *. use_exists H y. clear H. eapply ZF_eq_elem with y t; auto.
    + assert1 H. apply CE1 in H. apply ZF_ext'; auto.
      * prv_all a. apply (AllE a) in H. cbn in H. subsimpl_in H. apply CE1 in H.
        rewrite imps in *. apply (DE H). apply ZF_bunion_el1; auto 6.
        apply ZF_bunion_el2; auto 6. apply ZF_pair_el'; auto 6.
      * prv_all a. apply (AllE a) in H. cbn in H. subsimpl_in H. apply CE2 in H. apply II.
        eapply IE; try apply (Weak H); auto. rewrite <- imps. apply bunion_use; auto.
    + apply ZF_refl'. auto.
    + eapply CE2. auto.
Qed.

Lemma embed_ZF' { p : peirce } phi :
  phi el minZFeq' -> ZFeq' ⊢ embed phi.
Proof.
  intros [<-|[<-|[<-|[<-|[<-|[<-|[<-|[<-|[<-|[<-|[]]]]]]]]]]].
  1-5: cbn; apply Ctx; unfold ZFeq', ZF'; eauto.
  - cbn. apply (ExI ∅). cbn. apply ZF_eset.
  - assert (H : ZFeq' ⊢ ax_pair) by (apply Ctx; unfold ZFeq', ZF'; eauto 7).
    cbn. prv_all x. prv_all y. apply (ExI ({x; y})). cbn. subsimpl.
    apply (AllE y) in H. cbn in H. apply (AllE x) in H. cbn in H. now subsimpl_in H.
  - assert (H : ZFeq' ⊢ ax_union) by (apply Ctx; unfold ZFeq', ZF'; eauto 8).
    cbn. prv_all x. apply (ExI (⋃ x)). cbn. subsimpl. apply (AllE x H).
  - assert (H : ZFeq' ⊢ ax_power) by (apply Ctx; unfold ZFeq', ZF'; eauto 9).
    cbn. prv_all x. apply (ExI (PP x)). cbn. subsimpl. apply (AllE x H).
  - cbn. apply (ExI ω). cbn. apply CI.
    + assert (H : ZFeq' ⊢ ax_om1) by (apply Ctx; unfold ZFeq', ZF'; eauto 10).
      unfold ax_om1 in H. apply (IE (CE1 (ZF_inductive_embed ω))) in H. apply H.
    + assert (H : ZFeq' ⊢ ax_om2) by (apply Ctx; unfold ZFeq', ZF'; eauto 11).
      prv_all x. apply II. apply (AllE x) in H. cbn in H. eapply IE; try apply (Weak H); auto.
      specialize (CE2 (ZF_inductive_embed x)). intros H'. eapply IE; try apply (Weak H'); auto.
Qed.

Theorem conservativity_back_ZF' { p : peirce } phi :
  minZFeq' ⊢ phi -> ZFeq' ⊢ embed phi.
Proof.
  intros HP. apply prv_embed in HP. apply (prv_cut HP).
  intros psi' [psi[<- H]] % in_map_iff. now apply embed_ZF'.
Qed.

Lemma minZ_decomp { p : peirce } phi :
  minZeq ⊢T phi -> exists A, (map ax_sep' A ++ minZFeq') ⊢ phi.
Proof.
  intros [A [H1 H2]]. induction A in phi, H1, H2 |- *.
  - exists nil. cbn. eapply Weak; eauto.
  - rewrite <- imps in H2. apply IHA in H2 as [B H]; auto.
    rewrite imps in H. destruct (H1 a); auto.
    + exists B. eapply Weak; try apply H. auto.
    + exists (phi0 :: B). cbn. apply H.
Qed.

Theorem conservativity_back_Z { p : peirce } phi :
  minZeq ⊢T phi -> Zeq ⊢T embed phi.
Proof.
  intros [A HA] % minZ_decomp. apply prv_embed in HA.
  exists ([ax_sep (embed psi) | psi ∈ A] ++ ZFeq'). split.
  - intros psi [H|H] % in_app_iff; try now constructor.
    apply in_map_iff in H as [psi'[<- H]]. constructor 2.
  - apply (prv_cut HA). intros psi' [psi [<- [H|H] % in_app_iff]] % in_map_iff.
    + apply in_map_iff in H as [theta [<- H]]. apply Ctx. apply in_app_iff. left.
      apply in_map_iff. exists theta. split; trivial. cbn. unfold ax_sep.
      rewrite embed_subst. erewrite subst_ext; try reflexivity. now intros [|n].
    + eapply Weak; try apply embed_ZF'; auto.
Qed.

Lemma minZF_decomp { p : peirce } phi :
  minZFeq ⊢T phi -> exists A B, ((map ax_sep' A ++ map ax_rep' B) ++ minZFeq') ⊢ phi.
Proof.
  intros [C [H1 H2]]. induction C in phi, H1, H2 |- *.
  - exists nil, nil. cbn. eapply Weak; eauto.
  - rewrite <- imps in H2. apply IHC in H2 as [A[B HAB]]; auto.
    rewrite imps in HAB. destruct (H1 a); auto.
    + exists A, B. eapply Weak; try apply HAB. auto.
    + exists (phi0 :: A), B. cbn. apply HAB.
    + exists A, (phi0 :: B). cbn. eapply Weak; try apply HAB.
      intros psi [->|[[H|H] % in_app_iff|H] % in_app_iff]; auto.
      apply in_app_iff. left. apply in_app_iff. right. now right.
Qed.

Theorem conservativity_back_ZF { p : peirce } phi :
  minZFeq ⊢T phi -> ZFeq ⊢T embed phi.
Proof.
  intros [A[B HAB]] % minZF_decomp. apply prv_embed in HAB.
  exists ([ax_sep (embed psi) | psi ∈ A] ++ [ax_rep (embed psi) | psi ∈ B] ++ ZFeq'). split.
  - intros psi [H|[H|H] % in_app_iff] % in_app_iff; try now constructor.
    + apply in_map_iff in H as [psi'[<- H]]. constructor 2.
    + apply in_map_iff in H as [psi'[<- H]]. constructor 3.
  - apply (prv_cut HAB). intros psi' [psi [<- [[H|H] % in_app_iff|H] % in_app_iff]] % in_map_iff.
    + apply in_map_iff in H as [theta [<- H]]. apply Ctx. apply in_app_iff. left.
      apply in_map_iff. exists theta. split; trivial. cbn. unfold ax_sep.
      rewrite embed_subst. erewrite subst_ext; try reflexivity. now intros [|n].
    + apply in_map_iff in H as [theta [<- H]]. apply Ctx. apply in_app_iff. right.
      apply in_app_iff. left. apply in_map_iff. exists theta. split; trivial. cbn. unfold ax_rep, fun_rel.
      rewrite !embed_subst. setoid_rewrite subst_ext at 1. setoid_rewrite subst_ext at 2.
      setoid_rewrite subst_ext at 3. setoid_rewrite subst_ext at 4. reflexivity.
      all: now intros [|[|n]].
    + eapply Weak; try apply embed_ZF'; auto.
Qed.