From Loeb Require Import Definitions.
From Loeb.util Require Import Util.
From Loeb.internal_provability Require Import PA_Lists_Signature QEqLiFull Prov_Definition.
From Loeb.hilbert_system Require Import Hilbert_System Hilbert_System_Deduction_Facts.

From Undecidability.FOL Require Import Syntax.Core Arithmetics.Signature Arithmetics.FA.
From FOL.Proofmode Require Import Theories ProofMode.
Require Import String.

Open Scope string_scope.

Existing Instance falsity_on.
Existing Instance PA_li_funcs_signature.
Existing Instance PA_preds_signature.
Existing Instance full_operators.

Section MP.

    Context {p: peirce}.

    Context {göd: goedelisation}.

    Variables ax: form.
    Variables ax_bound: bounded 1 ax.
    Variables Hax: forall φ, (QEqLiFull φ \/ exists n ψ, hilAx p ψ /\ φ = forall_times n ψ) <-> QEqLi ⊢ ax[(num' ((göd.(g)) φ))..].

    Lemma box_distr_Gödel_numeral φ ψ:
    QEqLiFull ⊩ ((prov ax)[(num' (g φ))..] → (prov ax)[(num' (g (φ → ψ)))..] → (prov ax)[(num' (g ψ))..]).
    Proof.
      Opaque prov.
      exists ((ax_impl φ ψ)::AxiomList)%list. split.
      - intros τ. intros [Heq | Helem].
        + rewrite <- Heq. apply QEqImpl.
        + now apply AxiomList_in_QEqLi_Axioms.
      - specialize (box_distr ax_bound p (num'_bound' (g φ) 0) (num'_bound' (g ψ) 0)) as Hdistr.
        fstart. fintros "Hφ" "Himpl". fapply Hdistr.
        + fapply "Hφ".
        + feapply QEqLi_leibniz; last fapply "Himpl". fapply 2.       Transparent prov.
    Qed.

End MP.

Section nec.

    Context {p: peirce}.

    Context {göd: goedelisation}.

    Variables ax: form.
    Variables ax_bound: bounded 1 ax.
    Variables Hax: forall φ, (QEqLiFull φ \/ exists n ψ, hilAx p ψ /\ φ = forall_times n ψ) <-> QEqLi ⊢ ax[(num' ((göd.(g)) φ))..].

    Lemma necessitation φ:
        QEqLiFull ⊩ φ -> QEqLiFull ⊩ (prov ax)[(num' (g φ))..].
    Proof.
        intros [L [Hincl HL]]. apply Hil_ND_agree in HL.
        induction HL as [φ ψ p' _ IH1 _ IH2 | φ n Hφ | φ].
        - specialize (IH1 Hax). specialize (IH2 Hax). fstart.
          specialize (box_distr_Gödel_numeral ax_bound φ ψ) as HMP.           eapply T_IE; last eapply IH2. now eapply T_IE.
        - apply (axioms_are_provable ax_bound). apply Hax. right.
          now exists n, φ.
        - apply (axioms_are_provable ax_bound). apply Hax. firstorder.
    Qed.

End nec.