Require Import List Lia.
From Undecidability.FOL Require Import FragmentSyntax.
Import Vector.VectorNotations.
From Undecidability Require Import Synthetic.Undecidability.
Notation "I ⊨= phi" := (forall rho, sat I rho phi) (at level 20).
Notation "I ⊨=T T" := (forall psi, T psi -> I ⊨= psi) (at level 20).
Notation "I ⊫= Gamma" := (forall rho psi, In psi Gamma -> sat I rho psi) (at level 20).
Section Signature.
Import FragmentSyntax.
Existing Instance frag_operators | 0.
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 [|P0] eqn:?.
+ intros _. exact Q.
+ exact (@i_atom _ _ _ I P0).
Defined.
Definition Q := (@atom Σ_funcs extended_preds _ falsity_off Q_ ([])).
Definition dn {ff} F phi : @form Σ_funcs extended_preds _ ff :=
(phi → F) → F.
Fixpoint cast {ff} (phi : @form Σ_funcs Σ_preds _ ff) : @form Σ_funcs extended_preds _ falsity_off :=
match phi with
| falsity => Q
| atom P v => (@atom _ _ _ falsity_off (old_preds P) v)
| bin b phi psi => bin b (cast phi) (cast psi)
| quant q phi => quant q (cast phi)
end.
Fixpoint Fr {ff} (phi : @form Σ_funcs Σ_preds _ ff) : @form Σ_funcs extended_preds _ falsity_off :=
match phi with
| falsity => Q
| atom P v => dn Q (@atom _ _ _ falsity_off (old_preds P) v)
| bin Impl phi psi => (Fr phi) → (Fr psi)
| quant All phi => ∀ (Fr phi)
end.
Definition Fr_ {ff} Gamma := map (@Fr ff) Gamma.
Fact subst_Fr {ff} (phi : @form Σ_funcs Σ_preds _ ff) sigma:
subst_form sigma (Fr phi) = Fr (subst_form sigma phi).
Proof.
revert sigma.
induction phi; cbn.
- reflexivity.
- now unfold dn.
- destruct b0; cbn; unfold dn, Q; congruence.
- destruct q; cbn; intros sigma; unfold dn, Q; congruence.
Qed.
Fact subst_Fr_ {ff} L sigma :
map (subst_form sigma) (map (@Fr ff) L) = map Fr (map (subst_form sigma) L).
Proof.
induction L.
- reflexivity.
- cbn. now rewrite IHL, subst_Fr.
Qed.
Lemma double_dn Gamma F phi :
Gamma ⊢M (dn F (dn F phi) → dn F phi).
Proof.
apply II, II. eapply IE with (phi:= _ → _). { apply Ctx; firstorder. }
apply II. apply IE with (phi:= phi → F). all: apply Ctx; cbv;eauto.
Qed.
Lemma rm_dn Gamma F alpha beta :
(alpha :: Gamma) ⊢M beta -> (dn F alpha :: Gamma) ⊢I dn F beta.
Proof.
intros H.
apply II. eapply IE with (phi:= _ → _). { apply Ctx; firstorder. }
apply II. eapply IE with (phi:= beta). {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) :
phi[up ↑][$0..] = phi.
Proof.
asimpl. reflexivity.
Qed.
Lemma dn_forall {F} Gamma phi :
F[↑] = F -> Gamma ⊢M (dn F (∀ phi) → ∀ dn F phi).
Proof.
intros HF.
apply II. constructor. apply II. cbn.
change ((∀ phi[up ↑])) with ((∀ phi)[↑]).
rewrite !HF.
eapply IE with (phi:= _ → _). { apply Ctx; auto. right. left. easy. }
apply II. eapply IE with (phi:= phi). { apply Ctx; auto. right. left. easy. }
cbn. rewrite <-form_up_var0_invar.
apply AllE, Ctx; auto. left. easy.
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} :
forall phi Gamma, Gamma ⊢M (dn Q (Fr phi) → @Fr ff phi).
Proof.
refine (@size_ind _ size _ _). intros phi sRec.
destruct phi; intros Gamma; unfold dn.
- apply II. eapply IE; cbn. { apply Ctx; auto. now left. }
apply II, Ctx; auto. now left.
- apply double_dn.
- destruct b0; cbn.
+ apply II, II. eapply IE. apply sRec; cbn. 1: lia.
apply II. eapply IE with (phi:= _ → _). { apply Ctx; auto. try_lr. }
apply II. eapply IE with (phi:= Fr phi2). { apply Ctx; auto. try_lr. }
eapply IE with (phi:= Fr phi1); apply Ctx; auto. all: try_lr.
- destruct q.
+ cbn. apply II. apply IE with (phi:= ∀ dn Q (Fr phi)).
{ 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.
Qed.
Lemma Peirce_Fr {ff} Gamma phi psi : Gamma ⊢M @Fr ff (((phi → psi) → phi) → phi).
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 (phi:= _ → _). {apply Ctx; auto. try_lr. }
apply II, Ctx; auto. try_lr.
Qed.
Theorem Fr_cl_to_min {ff} Gamma phi :
Gamma ⊢C phi -> (@Fr_ ff Gamma) ⊢M Fr phi.
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.
- specialize (DNE_Fr phi (map Fr A)) as H'.
eapply IE; [eassumption|].
cbn; apply II. eapply Weak; eauto. apply incl_tl, incl_refl.
- now apply Ctx, in_map.
- 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.