Require Import List Lia.

From Undecidability.FOL Require Import FullSyntax.
From Undecidability.FOL.Arithmetics Require Import Robinson NatModel.
Import Vector.VectorNotations.
From Undecidability Require Import Synthetic.Undecidability.

Notation "I ⊨= phi" := ( rho, sat I ) (at level 20).
Notation "I ⊨=T T" := ( psi, T I ⊨= ) (at level 20).
Notation "I ⊫= Gamma" := ( rho psi, In sat I ) (at level 20).

Section Signature.


  Context {Σ_funcs : funcs_signature}.
  Context {Σ_preds : preds_signature}.

  Inductive new_preds : Type :=
    Q_ : new_preds
  | old_preds (P : Σ_preds) : new_preds.

  Definition new_preds_ar (P : new_preds) :=
    match P with
    | Q_ 0
    | old_preds P ar_preds P
    end.

  Existing Instance Σ_funcs.
  Instance extended_preds : preds_signature :=
    {| preds := new_preds ; ar_preds := new_preds_ar |}.

  Definition extend_interp {D} :
    @interp Σ_funcs Σ_preds D Prop interp D.
  Proof.
    intros I Q. split.
    - exact (@i_func _ _ _ I).
    - intros P. destruct P as [|] eqn:?.
      + intros _. exact Q.
      + exact (@i_atom _ _ _ I ).
  Defined.


  Definition Q := (@atom Σ_funcs extended_preds _ falsity_off Q_ ([])).
  Definition dn {ff} F phi : @form Σ_funcs extended_preds _ ff :=
    ( F) F.

  Fixpoint cast {ff} (phi : @form Σ_funcs Σ_preds _ ff) : @form Σ_funcs extended_preds _ falsity_off :=
    match with
    | falsity Q
    | atom P v (@atom _ _ _ falsity_off (old_preds P) v)
    | bin b bin b (cast ) (cast )
    | quant q quant q (cast )
    end.

  Fixpoint Fr {ff} (phi : @form Σ_funcs Σ_preds _ ff) : @form Σ_funcs extended_preds _ falsity_off :=
    match with
    | falsity Q
    | atom P v dn Q (@atom _ _ _ falsity_off (old_preds P) v)
    | bin Impl (Fr ) (Fr )
    | bin Conj (Fr ) (Fr )
    | bin Disj dn Q ((Fr ) (Fr ))
    | quant All (Fr )
    | quant Ex dn Q ( (Fr ))
    end.

  Definition Fr_ {ff} Gamma := map (@Fr ff) .

  Fact subst_Fr {ff} (phi : @form Σ_funcs Σ_preds _ ff) sigma:
    subst_form (Fr ) = Fr (subst_form ).
  Proof.
    revert .
    induction ; cbn.
    - reflexivity.
    - now unfold dn.
    - destruct ; cbn; unfold dn, Q; congruence.
    - destruct q; cbn; intros ; unfold dn, Q; congruence.
  Qed.


  Fact subst_Fr_ {ff} L sigma :
    map (subst_form ) (map (@Fr ff) L) = map Fr (map (subst_form ) L).
  Proof.
    induction L.
    - reflexivity.
    - cbn. now rewrite IHL, subst_Fr.
  Qed.


  Lemma double_dn Gamma F phi :
     M dn F (dn F ) dn F .
  Proof.
    apply II, II. eapply IE with (:= _ _). { apply Ctx; firstorder. }
    apply II. apply IE with (:= F). all: apply Ctx; cbv;eauto.
  Qed.


  Lemma rm_dn Gamma F alpha beta :
    ( :: ) M (dn F :: ) I dn F .
  Proof.
    intros H.
    apply II. eapply IE with (:= _ _). { apply Ctx; firstorder. }
    apply II. eapply IE with (:= ). {apply Ctx; cbv;eauto. }
    eapply Weak. 1:eassumption. apply ListAutomation.incl_shift, incl_tl, incl_tl, incl_refl.
  Qed.


  Lemma form_up_var0_invar {ff} (phi : @form _ _ _ ff) :
    [up ][$0..] = .
  Proof.
    asimpl. reflexivity.
  Qed.


  Lemma dn_forall {F} Gamma phi :
    F[] = F M dn F ( ) dn F .
  Proof.
    intros HF.
    apply II. constructor. apply II. cbn.
    change (( [up ])) with (( )[]).
    rewrite !HF.
    eapply IE with (:= _ _). { apply Ctx; auto. right. left. easy. }
    apply II. eapply IE with (:= ). { apply Ctx; auto. right. left. easy. }
    cbn. rewrite form_up_var0_invar.
    apply AllE, Ctx; auto. left. easy.
  Qed.


  Lemma exist_dn phi Gamma:
     M (( (dn Q )) dn Q ( )).
  Proof.
    apply II, II. eapply ExE. {apply Ctx; auto. right. now left. }
    cbn; fold Q. apply IE with (:= Q).
    {apply Ctx; auto. now left. }
    apply II. eapply IE with (:= _).
    {apply Ctx; auto. do 2 right. now left. }
    eapply ExI. rewrite form_up_var0_invar.
    apply Ctx; auto. now left.
  Qed.


  Ltac try_lr := let rec H f := match f with S ?n (try now left); right; H n | _ idtac end in H 100.

  Lemma DNE_Fr {ff} :
     phi Gamma, M dn Q (Fr ) @Fr ff .
  Proof.
    refine (@size_ind _ size _ _). intros sRec.
    destruct ; intros ; unfold dn.
    - apply II. eapply IE; cbn. { apply Ctx; auto. now left. }
      apply II, Ctx; auto. now left.
    - apply double_dn.
    - destruct ; cbn.
      + apply II, CI.
        * eapply IE. apply sRec; cbn. 1: .
          apply rm_dn. eapply CE1, Ctx; auto. now left.
        * eapply IE. apply sRec; cbn. 1: .
          apply rm_dn. eapply CE2, Ctx; auto. now left.
      + apply double_dn.
      + apply II, II. eapply IE. apply sRec; cbn. 1: .
        apply II. eapply IE with (:= _ _). { apply Ctx; auto. try_lr. }
        apply II. eapply IE with (:= Fr ). { apply Ctx; auto. try_lr. }
        eapply IE with (:= Fr ); apply Ctx; auto. all: try_lr.
    - destruct q.
      + cbn. apply II. apply IE with (:= dn Q (Fr )).
        { apply II. constructor. cbn; fold Q.
          eapply IE. apply sRec; auto.
          rewrite form_up_var0_invar.
          apply AllE, Ctx; auto. try_lr. }
        constructor.
        cbn; fold Q. rewrite form_up_var0_invar.
        apply AllE. cbn; fold Q.
        now apply imps, dn_forall.
      + apply double_dn.
  Qed.


  Lemma Peirce_Fr {ff} Gamma phi psi : M @Fr ff ((( ) ) ).
  Proof.
    eapply IE. apply DNE_Fr. cbn.
    apply II. eapply IE. { apply Ctx; auto. try_lr. }
    apply II. eapply IE. { apply Ctx; auto. try_lr. }
    apply II. eapply IE. apply DNE_Fr. cbn; fold Q.
    apply II. eapply IE with (:= _ _). {apply Ctx; auto. try_lr. }
    apply II, Ctx; auto. try_lr.
  Qed.



  Theorem Fr_cl_to_min {ff} Gamma phi :
     C (@Fr_ ff ) M Fr .
  Proof.
    induction 1; unfold Fr_ in *; cbn in *.
    - now constructor.
    - econstructor; eassumption.
    - constructor. now rewrite subst_Fr_.
    - eapply AllE with (t:=t) in IHprv.
      now rewrite subst_Fr in IHprv.
    - apply II.
      eapply IE.
      + apply Ctx. firstorder.
      + apply Weak with (A := map Fr A); [|apply incl_tl, incl_refl].
        apply ExI with (t:=t). now rewrite subst_Fr.
    - eapply IE. apply DNE_Fr. unfold dn in *; cbn.
      apply II. eapply IE.
      { eapply Weak; [apply |auto]. apply incl_tl,incl_refl. }
      apply II. eapply IE. { apply Ctx; auto. try_lr. }
      rewrite subst_Fr, subst_Fr_ in .
      eapply ExE. { apply Ctx; auto. try_lr. }
      cbn. eapply Weak; [apply |auto]. apply ListAutomation.incl_shift, incl_tl, incl_tl, incl_refl.
    - specialize (DNE_Fr (map Fr A)) as H'.
      eapply IE; [eassumption|].
      cbn; apply II. eapply Weak; eauto. apply incl_tl, incl_refl.
    - now apply Ctx, in_map.
    - now apply CI.
    - eapply CE1; eauto.
    - eapply CE2; eauto.
    - apply II. eapply IE.
      + apply Ctx. auto. try_lr.
      + apply DI1. eapply Weak; eauto. apply incl_tl, incl_refl.
    - apply II. eapply IE.
      + apply Ctx; auto. try_lr.
      + apply DI2. eapply Weak; eauto. apply incl_tl, incl_refl.
    - eapply IE. apply DNE_Fr.
      apply II. eapply IE.
      { eapply Weak; [apply |auto]. apply incl_tl, incl_refl. }
      apply II. eapply IE. { apply Ctx; auto. try_lr. }
      apply imps in . apply imps in .
      eapply DE.
      1 : apply Ctx; firstorder.
      1,2 : apply imps; eapply Weak; [eassumption|auto]; apply incl_tl, incl_tl, incl_refl.
    - apply Peirce_Fr.
  Qed.


  Lemma bounded_Fr {ff : falsity_flag} N ϕ :
    bounded N ϕ bounded N (Fr ϕ).
  Proof.
    induction 1; cbn; solve_bounds; auto.
    - econstructor. apply H.
    - destruct binop; now solve_bounds.
    - destruct quantop; now solve_bounds.
  Qed.

End Signature.

Section Arithmetic.

  Existing Instance PA_preds_signature.
  Existing Instance PA_funcs_signature.

  Lemma nat_sat_Fr_Q P :
    (extend_interp interp_nat P) ⊫= Fr_ Qeq.
  Proof.
    intros ρ a Qa.
    repeat (destruct Qa as [|Qa]).
    all: cbn -[FAeq]; try refine ( A let F := A _ in _); intuition.
    - apply H. intros . apply . intros . auto.
    - now apply H.
    - destruct d; eauto.
    - destruct Qa.
  Qed.


End Arithmetic.