Require Import Undecidability.Synthetic.Definitions Undecidability.Synthetic.Undecidability.
From Undecidability.FOL.Util Require Import Syntax Syntax_facts FullTarski FullTarski_facts FullDeduction_facts FullDeduction FA_facts.
Require Import Undecidability.FOL.PA.
From Undecidability.H10 Require Import H10p.
Require Import List Lia.

Fixpoint embed_poly p : term :=
    match p with
    | dp_nat_pfree n num n
    | dp_var_pfree k $k
    | dp_comp_pfree do_add_pfree a b (embed_poly a) (embed_poly b)
    | dp_comp_pfree do_mul_pfree a b (embed_poly a) (embed_poly b)
    end.


Definition embed_problem (E : H10p_PROBLEM) : form :=
  let (a, b) := E in embed_poly a == embed_poly b.

Definition H10p_sem E sigma := dp_eval_pfree (fst E) = dp_eval_pfree (snd E).

Definition poly_bound p := proj1_sig (find_bounded_t (embed_poly p)).
Definition problem_bound (E : H10p_PROBLEM) :=
  let (a, b) := E in proj1_sig (find_bounded (embed_poly a == embed_poly b) ).

Definition embed E := exist_times (problem_bound E) (embed_problem E).

Lemma exists_close_form N phi : bounded 0 (exist_times N ) bounded N .
Proof.
  induction N in |- *.
  - reflexivity.
  - cbn. rewrite iter_switch.
    change (iter _ _ _) with (exist_times N ( )).
    setoid_rewrite IHN. symmetry.
    now apply bounded_S_exists.
Qed.


Lemma embed_is_closed E : bounded 0 (embed E).
Proof.
  unfold embed. rewrite exists_close_form.
  unfold problem_bound. destruct E as [a b]; cbn.
  apply (proj2_sig (find_bounded _)).
Qed.


Fact numeral_subst_invariance n rho : subst_term (num n) = num n.
Proof.
  induction n.
  - reflexivity.
  - cbn. now rewrite IHn.
Qed.


Lemma prv_poly {p : peirce} sigma q Gamma :
  incl FAeq ( (embed_poly q)`[ >> num] == num (dp_eval_pfree q) ).
Proof.
  intros H.
  induction q; cbn.
  - change ((num n)`[ >> num]) with (subst_term ( >> num) (num n)).
    rewrite numeral_subst_invariance.
    now apply reflexivity.
  - now apply reflexivity.
  - destruct d; cbn.
    + eapply transitivity. assumption.
      apply (eq_add _ _ H ).
      now apply num_add_homomorphism.
    + eapply transitivity. assumption.
      apply (eq_mult _ _ H ).
      now apply num_mult_homomorphism.
Qed.


Lemma problem_to_prv {p : peirce} :
   E sigma, H10p_sem E FAeq (embed_problem E)[ >> num].
Proof.
  intros [a b] HE. cbn -[FAeq].
  eapply transitivity; firstorder.
  apply prv_poly; firstorder.
  apply symmetry; firstorder.
  unfold H10p_sem in *. cbn in HE. rewrite HE.
  apply prv_poly; firstorder.
Qed.


Theorem H10p_to_FA_prv' {p : peirce} E :
  H10p E FAeq embed E.
Proof.
  intros [ HE].
  eapply subst_exist_prv.
  apply problem_to_prv, HE.
  rewrite exists_close_form; apply embed_is_closed.
Qed.


Section FA_ext_Model.

  Context {D : Type}.
  Context {I : interp D}.

  Hypothesis ext_model : extensional I.
  Hypothesis FA_model : ax rho, In ax FA ax.

  Notation "'iO'" := (i_func (f:=Zero) (Vector.nil D)) (at level 2) : PA_Notation.

  Fact eval_poly sigma p : eval ( >> ) (embed_poly p) = (dp_eval_pfree p).
    Proof.
      induction p; cbn.
      - now rewrite eval_num.
      - reflexivity.
      - destruct d; cbn.
        + now rewrite , , add_hom.
        + now rewrite , , mult_hom.
    Qed.


    Lemma problem_to_ext_model : E sigma, H10p_sem E ( >> ) embed_problem E.
    Proof.
      intros [a b] Hs. cbn -[sat].
      unfold H10p_sem in *. cbn -[FA] in *.
      apply ext_model. rewrite !eval_poly. congruence.
    Qed.


    Theorem H10p_to_FA_ext_model' E rho : H10p E embed E.
    Proof.
      intros [ HE].
      eapply subst_exist_sat.
      apply problem_to_ext_model.
      - apply HE.
      - rewrite exists_close_form; apply embed_is_closed.
    Qed.


End FA_ext_Model.

Section FA_Model.


  Context {D : Type}.
  Context {I : interp D}.

  Hypothesis FA_model : rho ax, In ax FAeq ax.

  Notation "'iO'" := (i_func (f:=Zero) (Vector.nil D)) (at level 2) : PA_Notation.

  Lemma problem_to_model E sigma : H10p_sem E ( >> ) embed_problem E.
  Proof.
    eintros HE%problem_to_prv%soundness.
    specialize (HE D I).
    setoid_rewrite sat_comp in HE.
    eapply sat_ext. 2: apply HE.
    intros x. unfold ">>". now rewrite eval_num.
    intros. instantiate (1 := ( _ iO)).
    now apply FA_model.
  Qed.


  Definition standard :=
    extensional I f : D , ( d, (f d) = d) ( n, f ( n) = n).

  Fact standard_embed_poly rho p f :
    extensional I ( d, (f d) = d) eval (embed_poly p) = (dp_eval_pfree ( >> f) p).
  Proof.
    intros HI Hf. induction p; try destruct d; cbn.
    - apply eval_num.
    - unfold funcomp. now rewrite Hf.
    - rewrite , . rewrite add_hom; trivial. firstorder.
    - rewrite , . rewrite mult_hom; trivial. firstorder.
  Qed.


  Lemma standard_embed_problem' E rho f :
    extensional I ( d, (f d) = d) ( n, f ( n) = n) embed_problem E H10p_sem E ( >> f).
  Proof.
    intros HI H. destruct E as [p q]. apply HI in H.
    unfold H10p_sem. cbn. rewrite at 1. setoid_rewrite at 3.
    f_equal. now rewrite !standard_embed_poly.
  Qed.


  Lemma standard_embed_problem E :
    standard ( rho, embed_problem E) H10p E.
  Proof.
    intros (HI & f & & ) [ Hr]. exists ( >> f). now apply standard_embed_problem'.
  Qed.


  Lemma standard_embed E rho :
    standard (embed E) H10p E.
  Proof.
    intros HS H. apply standard_embed_problem; trivial. eapply subst_exist_sat2, H.
  Qed.


End FA_Model.

Arguments standard _ _ : clear implicits.

Lemma nat_standard :
  standard interp_nat.
Proof.
  split; try reflexivity. exists ( n n).
  setoid_rewrite (eval_num _ _ ( n n)).
  setoid_rewrite nat_eval_num.
  split; reflexivity.
Qed.


Fact nat_eval_poly (sigma : env ) p :
  @eval _ _ _ interp_nat (embed_poly p) = dp_eval_pfree p.
Proof.
  induction p; cbn.
  - now rewrite nat_eval_num.
  - reflexivity.
  - destruct d; cbn.
    + now rewrite , .
    + now rewrite , .
Qed.


Lemma nat_H10 E :
  ( rho, sat interp_nat (embed E)) H10p E.
Proof.
  destruct E as [a b]. unfold embed in *.
  intros H. specialize (H ( _ 0)).
  apply subst_exist_sat2 in H as [ H].
  exists . unfold H10p.H10p_sem. cbn.
  rewrite !nat_eval_poly. apply H.
Qed.


Lemma nat_sat :
   E rho, sat interp_nat (embed_problem E) H10p_sem E .
Proof.
  intros E . split.
  - destruct E as [a b]. unfold H10p_sem. cbn.
    now rewrite !nat_eval_poly.
  - intros. eapply (@sat_ext _ _ _ _ _ ( >> @ interp_nat)).
    intros x. change (( >> ) x) with (@ interp_nat ( x)).
    induction ( x). reflexivity. cbn. now rewrite IHn.
    eapply problem_to_model.
    apply nat_is_FA_model.
    assumption.
Qed.


Lemma nat_sat' E :
  ( sigma, sat interp_nat (embed_problem E)) H10p E.
Proof.
  split; intros [ ]; exists ; now apply nat_sat.
Qed.


Theorem H10p_to_FA_ext_sat E :
  H10p E ext_entailment_PA (embed E).
Proof.
  split.
  - intros [ HE].
    intros D I Hext H.
    eapply subst_exist_sat.
    apply problem_to_ext_model.
    + apply Hext.
    + intros. apply H. now constructor.
    + apply HE.
    + rewrite exists_close_form; apply embed_is_closed.
  - intros H.
    specialize (H interp_nat id nat_extensional).
    unfold embed in *. apply subst_exist_sat2 in H.
    now apply nat_sat'.
    apply nat_is_PA_model.
Qed.


Theorem H10p_to_FA_sat E :
  H10p E valid_ctx FAeq (embed E).
Proof.
  split.
  - intros [ HE].
    intros D I H.
    eapply subst_exist_sat.
    apply problem_to_model.
    + intros ρ' ax Hax. eapply sat_closed.
      2: now apply H.
      repeat (destruct Hax as [ | Hax]; cbn; repeat solve_bounds; auto).
    + apply HE.
    + rewrite exists_close_form; apply embed_is_closed.
  - intros H.
    specialize (H interp_nat id (nat_is_FA_model id)).
    unfold embed in *. apply subst_exist_sat2 in H.
    now apply nat_sat'.
Qed.


Theorem H10p_to_Q_sat E :
  H10p E valid_ctx Qeq (embed E).
Proof.
  split.
  - intros [ HE].
    intros D I H.
    eapply subst_exist_sat.
    apply problem_to_model.
    + intros ρ' ax Hax. eapply sat_closed.
      2: apply H.
      repeat (destruct Hax as [ | Hax]; cbn; repeat solve_bounds; auto).
      firstorder.
    + apply HE.
    + rewrite exists_close_form; apply embed_is_closed.
  - intros H.
    specialize (H interp_nat id (nat_is_Q_model id)).
    unfold embed in *. apply subst_exist_sat2 in H.
    now apply nat_sat'.
Qed.


Theorem H10p_to_PA_sat E :
  H10p E D (I : interp D) rho, ( psi rho, PAeq ) (embed E).
Proof.
  split.
  - intros [ HE].
    intros D I H.
    eapply subst_exist_sat.
    apply problem_to_model.
    + intros ρ' ax Hax. apply (sat_closed ).
      repeat (destruct Hax as [ | Hax]; cbn; repeat solve_bounds; auto).
      apply H. now constructor.
    + apply HE.
    + rewrite exists_close_form; apply embed_is_closed.
  - intros H.
    specialize (H interp_nat id nat_is_PAeq_model).
    unfold embed in *. apply subst_exist_sat2 in H.
    now apply nat_sat'.
Qed.


Theorem H10p_to_FA_prv E :
  H10p E FAeq I embed E.
Proof.
  split.
  - intros [ HE].
    eapply subst_exist_prv.
    apply problem_to_prv, HE.
    rewrite exists_close_form; apply embed_is_closed.
  - intros H%soundness.
    now apply H10p_to_FA_sat.
Qed.


Theorem H10p_to_Q_prv E :
  H10p E Qeq I embed E.
Proof.
  split.
  - intros.
    apply Weak with FAeq.
    now apply H10p_to_FA_prv.
    firstorder.
  - intros H%soundness.
    now apply H10p_to_Q_sat.
Qed.


Theorem H10p_to_PA_prv E :
  H10p E PAeq TI embed E.
Proof.
  split.
  - intros [ HE].
    exists FAeq. split. intros. now constructor.
    apply H10p_to_FA_prv.
    now exists .
  - intros H. apply nat_sat'.
    eapply subst_exist_sat2.
    apply (tsoundness H interp_nat id).
    intros. now apply nat_is_PAeq_model.
Qed.



Theorem H10_to_ext_entailment_PA :
  H10p ext_entailment_PA.
Proof.
  exists embed. intros E. apply H10p_to_FA_ext_sat.
Qed.



Theorem H10_to_entailment_FA :
  H10p entailment_FA.
Proof.
  exists embed; intros E. apply H10p_to_FA_sat.
Qed.


Corollary H10_to_entailment_Q :
  H10p entailment_Q.
Proof.
  exists embed; intros E. apply H10p_to_Q_sat.
Qed.


Corollary H10_to_entailment_PA :
  H10p entailment_PA.
Proof.
  exists embed; intros E. apply H10p_to_PA_sat.
Qed.


Theorem H10_to_deduction_FA :
  H10p deduction_FA.
Proof.
  exists embed; intros E. apply H10p_to_FA_prv.
Qed.


Theorem H10_to_deduction_Q :
  H10p deduction_Q.
Proof.
  exists embed; intros E. apply H10p_to_Q_prv.
Qed.


Corollary H10_to_deduction_PA :
  H10p deduction_PA.
Proof.
  exists embed; intros E. apply H10p_to_PA_prv.
Qed.