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 sigma (fst E) = dp_eval_pfree sigma (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 phi) <-> bounded N phi.
Proof.
induction N in phi |- *.
- reflexivity.
- cbn. rewrite iter_switch.
change (iter _ _ _) with (exist_times N (∃ phi)).
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 rho (num n) = num n.
Proof.
induction n.
- reflexivity.
- cbn. now rewrite IHn.
Qed.
Lemma prv_poly {p : peirce} sigma q Gamma :
incl FAeq Gamma -> Gamma ⊢ ( (embed_poly q)`[sigma >> num] == num (dp_eval_pfree sigma q) ).
Proof.
intros H.
induction q; cbn.
- change ((num n)`[sigma >> num]) with (subst_term (sigma >> num) (num n)).
rewrite numeral_subst_invariance.
now apply reflexivity.
- now apply reflexivity.
- destruct d; cbn.
+ eapply transitivity. assumption.
apply (eq_add _ _ H IHq1 IHq2).
now apply num_add_homomorphism.
+ eapply transitivity. assumption.
apply (eq_mult _ _ H IHq1 IHq2).
now apply num_mult_homomorphism.
Qed.
Lemma problem_to_prv {p : peirce} :
forall E sigma, H10p_sem E sigma -> FAeq ⊢ (embed_problem E)[sigma >> num].
Proof.
intros [a b] sigma 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 [sigma 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 : forall ax rho, In ax FA -> rho ⊨ ax.
Notation "'iO'" := (i_func (f:=Zero) (Vector.nil D)) (at level 2) : PA_Notation.
Fact eval_poly sigma p : eval (sigma >> iμ) (embed_poly p) = iμ (dp_eval_pfree sigma p).
Proof.
induction p; cbn.
- now rewrite eval_num.
- reflexivity.
- destruct d; cbn.
+ now rewrite IHp1, IHp2, add_hom.
+ now rewrite IHp1, IHp2, mult_hom.
Qed.
Lemma problem_to_ext_model : forall E sigma, H10p_sem E sigma -> (sigma >> iμ) ⊨ embed_problem E.
Proof.
intros [a b] sigma 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 -> rho ⊨ embed E.
Proof.
intros [sigma 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 : forall rho ax, In ax FAeq -> rho ⊨ ax.
Notation "'iO'" := (i_func (f:=Zero) (Vector.nil D)) (at level 2) : PA_Notation.
Lemma problem_to_model E sigma : H10p_sem E sigma -> (sigma >> iμ) ⊨ 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 := (fun _ => iO)).
now apply FA_model.
Qed.
Definition standard :=
extensional I /\ exists f : D -> nat, (forall d, iμ (f d) = d) /\ (forall n, f (iμ n) = n).
Fact standard_embed_poly rho p f :
extensional I -> (forall d, iμ (f d) = d) -> eval rho (embed_poly p) = iμ (dp_eval_pfree (rho >> f) p).
Proof.
intros HI Hf. induction p; try destruct d; cbn.
- apply eval_num.
- unfold funcomp. now rewrite Hf.
- rewrite IHp1, IHp2. rewrite add_hom; trivial. firstorder.
- rewrite IHp1, IHp2. rewrite mult_hom; trivial. firstorder.
Qed.
Lemma standard_embed_problem' E rho f :
extensional I -> (forall d, iμ (f d) = d) -> (forall n, f (iμ n) = n) -> rho ⊨ embed_problem E -> H10p_sem E (rho >> f).
Proof.
intros HI Hf1 Hf2 H. destruct E as [p q]. apply HI in H.
unfold H10p_sem. cbn. rewrite <- Hf2 at 1. setoid_rewrite <- Hf2 at 3.
f_equal. now rewrite <- !standard_embed_poly.
Qed.
Lemma standard_embed_problem E :
standard -> (exists rho, rho ⊨ embed_problem E) -> H10p E.
Proof.
intros (HI & f & Hf1 & Hf2) [rho Hr]. exists (rho >> f). now apply standard_embed_problem'.
Qed.
Lemma standard_embed E rho :
standard -> rho ⊨ (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 nat interp_nat.
Proof.
split; try reflexivity. exists (fun n => n).
setoid_rewrite <- (eval_num _ _ (fun n => n)).
setoid_rewrite nat_eval_num.
split; reflexivity.
Qed.
Fact nat_eval_poly (sigma : env nat) p :
@eval _ _ _ interp_nat sigma (embed_poly p) = dp_eval_pfree sigma p.
Proof.
induction p; cbn.
- now rewrite nat_eval_num.
- reflexivity.
- destruct d; cbn.
+ now rewrite IHp1, IHp2.
+ now rewrite IHp1, IHp2.
Qed.
Lemma nat_H10 E :
(forall rho, sat interp_nat rho (embed E)) -> H10p E.
Proof.
destruct E as [a b]. unfold embed in *.
intros H. specialize (H (fun _ => 0)).
apply subst_exist_sat2 in H as [sigma H].
exists sigma. unfold H10p.H10p_sem. cbn.
rewrite <- !nat_eval_poly. apply H.
Qed.
Lemma nat_sat :
forall E rho, sat interp_nat rho (embed_problem E) <-> H10p_sem E rho.
Proof.
intros E rho. split.
- destruct E as [a b]. unfold H10p_sem. cbn.
now rewrite !nat_eval_poly.
- intros. eapply (@sat_ext _ _ _ _ _ (rho >> @iμ nat interp_nat)).
intros x. change ((rho >> iμ) x) with (@iμ nat interp_nat (rho x)).
induction (rho x). reflexivity. cbn. now rewrite IHn.
eapply problem_to_model.
apply nat_is_FA_model.
assumption.
Qed.
Lemma nat_sat' E :
(exists sigma, sat interp_nat sigma (embed_problem E)) <-> H10p E.
Proof.
split; intros [sigma ]; exists sigma; now apply nat_sat.
Qed.
Theorem H10p_to_FA_ext_sat E :
H10p E <-> ext_entailment_PA (embed E).
Proof.
split.
- intros [sigma HE].
intros D I rho 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 nat 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 [sigma HE].
intros D I rho 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 nat 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 [sigma HE].
intros D I rho 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 nat 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 <-> forall D (I : interp D) rho, (forall psi rho, PAeq psi -> rho ⊨ psi) -> rho ⊨ (embed E).
Proof.
split.
- intros [sigma HE].
intros D I rho H.
eapply subst_exist_sat.
apply problem_to_model.
+ intros ρ' ax Hax. apply (sat_closed rho).
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 nat 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 [sigma 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 [sigma HE].
exists FAeq. split. intros. now constructor.
apply H10p_to_FA_prv.
now exists sigma.
- 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.