Require Import Undecidability.FOL.Util.Syntax.
Require Import Undecidability.FOL.Util.FullTarski_facts.
Require Import Undecidability.FOL.ZF.
Require Import Undecidability.FOL.Reductions.PCPb_to_ZF.
Require Import Lia.

From Undecidability.PCP Require Import PCP Util.PCP_facts Reductions.PCPb_iff_dPCPb.

From Undecidability Require Import Shared.ListAutomation.
Import ListAutomationNotations.

Local Set Implicit Arguments.
Local Unset Strict Implicit.

Require Import Morphisms.


Section ZF.

  Context { V : Type }.
  Context { M : interp V }.

  Hypothesis M_ZF : forall rho, rho ⊫ ZFeq'.

  Definition set_equiv x y :=
    x ≡ y.

  Notation "x ≡' y" := (set_equiv x y) (at level 35).

  Definition set_elem x y :=
    x ∈ y.

  Notation "x ∈' y" := (set_elem x y) (at level 35).

  Definition set_sub x y :=
    forall z, z ∈' x -> z ∈' y.

  Notation "x ⊆' y" := (set_sub x y) (at level 35).

  Instance set_equiv_equiv :
    Equivalence set_equiv.
  Proof.
    split.
    - apply (@M_ZF (fun _ => ∅) ax_refl). cbn; tauto.
    - apply (@M_ZF (fun _ => ∅) ax_sym). cbn; tauto.
    - apply (@M_ZF (fun _ => ∅) ax_trans). cbn; tauto.
  Qed.

  Instance set_equiv_elem :
    Proper (set_equiv ==> set_equiv ==> iff) set_elem.
  Proof.
    intros x x' Hx y y' Hy. split.
    - apply (@M_ZF (fun _ => ∅) ax_eq_elem); cbn; tauto.
    - symmetry in Hx, Hy. apply (@M_ZF (fun _ => ∅) ax_eq_elem); cbn; tauto.
  Qed.

  Instance set_equiv_sub :
    Proper (set_equiv ==> set_equiv ==> iff) set_sub.
  Proof.
    intros x x' Hx y y' Hy. unfold set_sub.
    setoid_rewrite Hx. setoid_rewrite Hy. tauto.
  Qed.

  Lemma set_equiv_refl' x :
    x ≡' x.
  Proof.
    apply set_equiv_equiv.
  Qed.

  Lemma set_equiv_refl x :
    x ≡ x.
  Proof.
    apply set_equiv_equiv.
  Qed.

  Hint Resolve set_equiv_refl set_equiv_refl' : core.

  Lemma M_ext x y :
    x ⊆' y -> y ⊆' x -> x ≡' y.
  Proof.
    apply (@M_ZF (fun _ => ∅) ax_ext). cbn; tauto.
  Qed.

  Lemma M_eset x :
    ~ x ∈' ∅.
  Proof.
    refine (@M_ZF (fun _ => ∅) ax_eset _ x). cbn; tauto.
  Qed.

  Lemma M_pair x y z :
    x ∈' {y; z} <-> x ≡' y \/ x ≡' z.
  Proof.
    apply (@M_ZF (fun _ => ∅) ax_pair). cbn; tauto.
  Qed.

  Definition pair x y :=
    {x; y}.

  Instance set_equiv_pair :
    Proper (set_equiv ==> set_equiv ==> set_equiv) pair.
  Proof.
    intros x x' Hx y y' Hy. unfold pair.
    apply M_ext; unfold set_sub.
    all: setoid_rewrite M_pair.
    all: setoid_rewrite Hx; setoid_rewrite Hy; tauto.
  Qed.

  Instance set_equiv_opair :
    Proper (set_equiv ==> set_equiv ==> set_equiv) M_opair.
  Proof.
    intros x x' Hx y y' Hy. unfold M_opair.
    change ({pair x x; pair x y} ≡' {pair x' x'; pair x' y'}).
    apply M_ext; unfold set_sub.
    all: setoid_rewrite M_pair.
    all: setoid_rewrite Hx; setoid_rewrite Hy; tauto.
  Qed.

  Lemma M_union x y :
    x ∈' ⋃ y <-> exists z, z ∈' y /\ x ∈' z.
  Proof.
    apply (@M_ZF (fun _ => ∅) ax_union). cbn; tauto.
  Qed.

  Definition union x :=
    ⋃ x.

  Instance equiv_union :
    Proper (set_equiv ==> set_equiv) union.
  Proof.
    intros x x' Hx. unfold union.
    apply M_ext; unfold set_sub.
    all: setoid_rewrite M_union.
    all: setoid_rewrite Hx; tauto.
  Qed.

  Lemma M_power x y :
    x ∈' PP y <-> x ⊆' y.
  Proof.
    apply (@M_ZF (fun _ => ∅) ax_power). cbn; tauto.
  Qed.

  Definition power x :=
    PP x.

  Instance equiv_power :
    Proper (set_equiv ==> set_equiv) power.
  Proof.
    intros x x' Hx. unfold power.
    apply M_ext; unfold set_sub.
    all: setoid_rewrite M_power.
    all: setoid_rewrite Hx; tauto.
  Qed.

  Lemma M_om1 :
    M_inductive ω.
  Proof.
    apply (@M_ZF (fun _ => ∅) ax_om1). cbn; tauto.
  Qed.

  Lemma M_om2 x :
    M_inductive x -> ω ⊆ x.
  Proof.
    apply (@M_ZF (fun _ => ∅) ax_om2). cbn; tauto.
  Qed.


  Definition M_binunion x y :=
    ⋃ {x; y}.

  Notation "x ∪' y" := (M_binunion x y) (at level 32).

  Lemma binunion_el x y z :
    x ∈' y ∪ z <-> x ∈' y \/ x ∈' z.
  Proof.
    split.
    - intros [u [H1 H2]] % M_union.
      apply M_pair in H1 as [<-| <-]; auto.
    - intros [H|H].
      + apply M_union. exists y. rewrite M_pair. auto.
      + apply M_union. exists z. rewrite M_pair. auto.
  Qed.

  Instance equiv_bunion :
    Proper (set_equiv ==> set_equiv ==> set_equiv) M_binunion.
  Proof.
    intros x x' Hx y y' Hy. unfold M_binunion.
    apply M_ext; unfold set_sub.
    all: setoid_rewrite binunion_el.
    all: setoid_rewrite Hx; setoid_rewrite Hy; tauto.
  Qed.

  Lemma sing_el x y :
    x ∈' M_sing y <-> x ≡' y.
  Proof.
    split.
    - now intros [H|H] % M_pair.
    - intros ->. apply M_pair. now left.
  Qed.

  Lemma M_pair1 x y :
    x ∈' {x; y}.
  Proof.
    apply M_pair. now left.
  Qed.

  Lemma M_pair2 x y :
    y ∈' {x; y}.
  Proof.
    apply M_pair. now right.
  Qed.

  Lemma sing_pair x y z :
    {x; x} ≡' {y; z} -> x ≡' y /\ x ≡' z.
  Proof.
    intros He. split.
    - assert (H : y ∈' {y; z}) by apply M_pair1.
      rewrite <- He in H. apply M_pair in H. intuition.
    - assert (H : z ∈' {y; z}) by apply M_pair2.
      rewrite <- He in H. apply M_pair in H. intuition.
  Qed.

  Lemma opair_inj1 x x' y y' :
    M_opair x y ≡' M_opair x' y' -> x ≡' x'.
  Proof.
    intros He. assert (H : {x; x} ∈' M_opair x y) by apply M_pair1.
    rewrite He in H. apply M_pair in H as [H|H]; apply (sing_pair H).
  Qed.

  Lemma opair_inj2 x x' y y' :
    M_opair x y ≡' M_opair x' y' -> y ≡' y'.
  Proof.
    intros He. assert (y ≡' x' \/ y ≡' y') as [Hy | Hy]; trivial.
    - assert (H : {x; y} ∈' M_opair x y) by apply M_pair2.
      rewrite He in H. apply M_pair in H as [H|H].
      + symmetry in H. apply sing_pair in H. intuition.
      + assert (H' : y ∈' {x; y}) by apply M_pair2.
        rewrite H in H'. now apply M_pair in H'.
    - assert (Hx : x ≡' x') by now apply opair_inj1 in He.
      rewrite Hx, Hy in He. rewrite Hy.
      assert (H : {x'; y'} ∈' M_opair x' y') by apply M_pair2.
      rewrite <- He in H. apply M_pair in H as [H|H]; symmetry in H; now apply sing_pair in H.
  Qed.

  Lemma opair_inj x x' y y' :
    M_opair x y ≡' M_opair x' y' -> x ≡' x' /\ y ≡' y'.
  Proof.
    intros H. split.
    - eapply opair_inj1; eassumption.
    - eapply opair_inj2; eassumption.
  Qed.

  Lemma sigma_el x y :
    x ∈' σ y <-> x ∈' y \/ x ≡' y.
  Proof.
    split.
    - intros [H|H] % binunion_el; auto.
      apply sing_el in H. now right.
    - intros [H| ->]; apply binunion_el; auto.
      right. now apply sing_el.
  Qed.

  Lemma binunion_eset x :
    x ≡' ∅ ∪ x.
  Proof.
    apply M_ext.
    - intros y H. apply binunion_el. now right.
    - intros y [H|H] % binunion_el.
      + now apply M_eset in H.
      + assumption.
  Qed.

  Lemma pair_com x y :
    {x; y} ≡' {y; x}.
  Proof.
    apply M_ext; intros z; rewrite !M_pair; tauto.
  Qed.

  Lemma binunion_com x y :
    x ∪' y ≡' y ∪' x.
  Proof.
    apply equiv_union, pair_com.
  Qed.

  Lemma binunionl a x y :
    a ∈' x -> a ∈' x ∪' y.
  Proof.
    intros H. apply binunion_el. now left.
  Qed.

  Lemma binunionr a x y :
    a ∈' y -> a ∈' x ∪' y.
  Proof.
    intros H. apply binunion_el. now right.
  Qed.

  Hint Resolve binunionl binunionr : core.

  Lemma binunion_assoc x y z :
    (x ∪' y) ∪' z ≡' x ∪' (y ∪' z).
  Proof.
    apply M_ext; intros a [H|H] % binunion_el; eauto.
    - apply binunion_el in H as [H|H]; eauto.
    - apply binunion_el in H as [H|H]; eauto.
  Qed.

  Lemma numeral_lt k l :
    k < l -> numeral k ∈ numeral l.
  Proof.
    induction 1; cbn; apply sigma_el; auto.
  Qed.


  Lemma enc_bool_inj b c :
    M_enc_bool b ≡' M_enc_bool c -> b = c.
  Proof.
    destruct b, c; trivial; cbn.
    - intros H. contradiction (@M_eset ∅).
      rewrite <- H at 2. apply M_pair; auto.
    - intros H. contradiction (@M_eset ∅).
      rewrite H at 2. apply M_pair; auto.
  Qed.

  Lemma enc_string_inj s t :
    M_enc_string s ≡' M_enc_string t -> s = t.
  Proof.
    induction s in t|-*; destruct t as [|b t]; cbn; trivial.
    - intros H. contradiction (M_eset (x:=M_sing (M_enc_bool b))).
      rewrite H. apply M_pair. now left.
    - intros H. contradiction (M_eset (x:=M_sing (M_enc_bool a))).
      rewrite <- H. apply M_pair. now left.
    - intros [H1 H2] % opair_inj. apply IHs in H2 as ->.
      apply enc_bool_inj in H1 as ->. reflexivity.
  Qed.

  Instance equiv_prep :
    Proper (eq ==> set_equiv ==> set_equiv) M_prep_string.
  Proof.
    intros s s' <- x x' Hx.
    induction s; cbn; trivial.
    now rewrite IHs.
  Qed.

  Lemma M_enc_stack_app A B :
    M_enc_stack (A ++ B) ≡' M_enc_stack A ∪' M_enc_stack B.
  Proof.
    induction A as [|[s t] A IH]; cbn.
    - apply binunion_eset.
    - change (M_enc_stack (A ++ B) ∪' M_sing (M_enc_card s t)
                          ≡' (M_enc_stack A ∪' M_sing (M_enc_card s t)) ∪' M_enc_stack B).
      rewrite IH. rewrite !binunion_assoc.
      now rewrite (binunion_com (M_enc_stack B) (M_sing (M_enc_card s t))).
  Qed.

  Lemma enc_stack_el' x A :
    x ∈ M_enc_stack A -> exists s t, (s, t) el A /\ x ≡' M_enc_card s t.
  Proof.
    induction A as [|[s t] A IH]; cbn.
    - now intros H % M_eset.
    - intros [H|H] % binunion_el.
      + destruct (IH H) as (u&v&H1&H2). exists u, v. intuition.
      + apply sing_el in H. exists s, t. intuition.
  Qed.

  Lemma enc_stack_el B s t :
    (s, t) el B -> M_enc_card s t ∈ M_enc_stack B.
  Proof.
    induction B as [|[u b] B IH]; cbn; auto.
    intros [H|H]; apply binunion_el.
    - right. apply sing_el. injection H. now intros -> ->.
    - left. apply IH, H.
  Qed.



  Definition M_comb_rel s t :=
    fun u v => exists u1 u2, u ≡' M_opair u1 u2 /\ v ≡' M_opair (M_prep_string s u1) (M_prep_string t u2).

  Fixpoint M_combinations B x y :=
    match B with
    | nil => y = ∅
    | (s,t)::B => exists y1 y2, y ≡' y2 ∪ y1 /\ M_combinations B x y1 /\ M_is_rep (M_comb_rel s t) x y2
    end.

  Lemma M_combinations_spec B rho x y a b :
    M_combinations B x y -> eval rho a = x -> eval rho b = y -> rho ⊨ combinations B a b.
  Proof.
    induction B in y,a,b,rho|-*; cbn.
    - now intros -> _ ->.
    - destruct a0 as [s t]. intros (y1&y2&H1&H2&H3) Ha Hb. exists y1, y2. repeat split.
      + cbn. erewrite !eval_comp. unfold funcomp. cbn.
        change (eval rho b ≡' y2 ∪ y1). now rewrite Hb, H1.
      + eapply (IHB _ y1); trivial. erewrite !eval_comp. unfold funcomp. cbn.
        change (eval (fun x => rho x) a) with (eval rho a). now rewrite Ha.
      + intros (u & Hu & c & d' & H) % H3. exists u. split.
        * cbn. erewrite !eval_comp. erewrite eval_ext, Ha; trivial.
        * exists d', c. cbn. rewrite !eval_prep_string. apply H.
      + intros (u & Hu & c & d' & H). apply H3. exists u. split.
        * cbn in Hu. erewrite !eval_comp in Hu. rewrite <- Ha. apply Hu.
        * exists d', c. cbn in H. rewrite !eval_prep_string in H. apply H.
  Qed.

  Definition M_solutions B f n :=
    M_opair ∅ (M_enc_stack B) ∈' f /\ forall k x y, k ∈' n -> M_opair k x ∈' f -> M_combinations B x y -> M_opair (σ k) y ∈' f.

  Instance equiv_solutions :
    Proper (eq ==> eq ==> set_equiv ==> iff) M_solutions.
  Proof.
    intros B B' <- f f' <- x x' Hx. unfold M_solutions. setoid_rewrite Hx. tauto.
  Qed.

  Lemma comb_rel_rep C s t :
    M_is_rep (M_comb_rel s t) (M_enc_stack C) (M_enc_stack (append_all C (s, t))).
  Proof.
    intros y. split.
    - intros (u&v&H&H') % enc_stack_el'.
      unfold append_all in H. apply in_map_iff in H as [[a b][H1 H2]]. cbn in H1.
      exists (M_enc_card a b). split; try now apply enc_stack_el.
      exists (M_enc_string a), (M_enc_string b). split; trivial.
      assert (u = s++a) as -> by congruence. assert (v = t++b) as -> by congruence.
      now rewrite !M_prep_enc.
    - intros (u&H&a&b&H3&H4). apply enc_stack_el' in H as [u'[v[H1 H2]]]. rewrite H3 in H2.
      apply opair_inj in H2 as [H2 H2']. change (y ∈' M_enc_stack (append_all C (s, t))).
      rewrite H4, H2, H2', !M_prep_enc. apply enc_stack_el.
      apply in_map_iff. now exists (u', v).
  Qed.

  Lemma M_combinations_step B C :
    M_combinations B (M_enc_stack C) (M_enc_stack (derivation_step B C)).
  Proof.
    induction B as [|[s t] B IH]; cbn; trivial.
    exists (M_enc_stack (derivation_step B C)), (M_enc_stack (append_all C (s, t))).
    rewrite M_enc_stack_app. split; trivial. split; trivial.
    apply comb_rel_rep.
  Qed.

  Lemma solutions_derivations B f n k :
    M_solutions B f (numeral n) -> k <= n -> M_opair (numeral k) (M_enc_stack (derivations B k)) ∈ f.
  Proof.
    intros H Hk; induction k; cbn.
    - apply H.
    - assert (Hk' : k <= n) by lia. specialize (IHk Hk').
      destruct H as [_ H]. eapply H in IHk; eauto.
      + now apply numeral_lt.
      + apply M_combinations_step.
  Qed.

  Definition M_function f :=
    forall x y y', M_opair x y ∈ f -> M_opair x y' ∈ f -> y ≡' y'.

  Lemma M_solutions_el B f k X p :
    standard M -> k ∈ ω -> M_function f -> M_solutions B f k -> M_opair k X ∈' f
    -> p ∈' X -> exists u v, p ≡' M_enc_card u v /\ derivable B u v.
  Proof.
    intros HS HO Hf Hk HX Hp. destruct (HS k HO) as [n Hn].
    change (k ≡' numeral n) in Hn. rewrite Hn in Hk. rewrite Hn in HX.
    pose proof (H := solutions_derivations Hk (le_n n)).
    rewrite (Hf _ _ _ HX H) in Hp. apply enc_stack_el' in Hp as (s&t&H'&Hp).
    exists s, t. split; trivial. eapply derivations_derivable; eauto.
  Qed.

  Theorem PCP_ZF2 B rho :
    standard M -> rho ⊨ solvable B -> exists s, derivable B s s.
  Proof.
    intros VIN (n & f & s & X & [[[[H1 H2] H3] H4] H5]).
    assert (H1' : n ∈ ω) by apply H1. clear H1.
    assert (H4' : M_opair n X ∈ f) by apply H4. clear H4.
    assert (H5' : M_opair s s ∈ X) by apply H5. clear H5.
    assert (H2' : M_function f).
    { intros x y y' H H'. eapply H2. apply H. apply H'. } clear H2.
    assert (H3' : M_opair ∅ (M_enc_stack B) ∈ f).
    { erewrite <- eval_enc_stack. apply H3. } destruct H3 as [_ H3].
    assert (H3'' : forall k x y, k ∈ n -> M_opair k x ∈ f -> M_combinations B x y -> M_opair (σ k) y ∈ f).
    { intros k x y Hn Hk Hy. apply (H3 k x y); auto. fold sat. eapply M_combinations_spec; eauto. } clear H3.
    destruct (@M_solutions_el B f n X (M_opair s s)) as (u&v&H1&H2); trivial.
    now split. exists u. apply opair_inj in H1 as [H H1]. rewrite H1 in H.
    apply enc_string_inj in H as ->. apply H2.
  Qed.

  Theorem PCP_ZFeq B rho :
    standard M -> rho ⊨ solvable B -> PCPb B.
  Proof.
    intros H1 H2. apply PCPb_iff_dPCPb. eapply PCP_ZF2; eauto.
  Qed.

End ZF.


Theorem PCP_ZFeq' B :
  (exists V (M : interp V), standard M /\ forall rho, rho ⊫ ZFeq')
  -> entailment_ZFeq' (solvable B) -> PCPb B.
Proof.
  intros (M & H1 & H2 & H3) H. rewrite PCPb_iff_dPCPb.
  specialize (H M H1 (fun _ => @i_func _ _ _ _ eset Vector.nil) H3).
  apply PCP_ZF2 in H as [s Hs]; trivial. now exists s.
Qed.