Require Import Undecidability.FOL.Syntax.Facts Undecidability.FOL.Syntax.Theories.
Require Export Undecidability.FOL.Semantics.Tarski.FragmentCore.
From Undecidability Require Import Shared.ListAutomation.
Import ListAutomationNotations.
Require Import Vector Lia.
Local Set Implicit Arguments.
Local Unset Strict Implicit.
Local Notation vec := Vector.t.
Section Tarski.
Context {Σ_funcs : funcs_signature}.
Context {Σ_preds : preds_signature}.
Section Substs.
Variable D : Type.
Variable I : interp D.
Lemma eval_ext rho xi t :
(forall x, rho x = xi x) -> eval rho t = eval xi t.
Proof.
intros H. induction t; cbn.
- now apply H.
- f_equal. apply map_ext_in. now apply IH.
Qed.
Lemma eval_comp rho xi t :
eval rho (subst_term xi t) = eval (xi >> eval rho) t.
Proof.
induction t; cbn.
- reflexivity.
- f_equal. rewrite map_map. apply map_ext_in, IH.
Qed.
Lemma sat_ext {ff : falsity_flag} rho xi phi :
(forall x, rho x = xi x) -> rho ⊨ phi <-> xi ⊨ phi.
Proof.
induction phi as [ | b P v | | ] in rho, xi |- *; cbn; intros H.
- reflexivity.
- erewrite map_ext; try reflexivity. intros t. now apply eval_ext.
- specialize (IHphi1 rho xi). specialize (IHphi2 rho xi). destruct b0; intuition.
- destruct q.
+ split; intros H' d; eapply IHphi; try apply (H' d). 1,2: intros []; cbn; intuition.
Qed.
Lemma sat_ext' {ff : falsity_flag} rho xi phi :
(forall x, rho x = xi x) -> rho ⊨ phi -> xi ⊨ phi.
Proof.
intros Hext H. rewrite sat_ext. exact H.
intros x. now rewrite (Hext x).
Qed.
Lemma sat_comp {ff : falsity_flag} rho xi phi :
rho ⊨ (subst_form xi phi) <-> (xi >> eval rho) ⊨ phi.
Proof.
induction phi as [ | b P v | | ] in rho, xi |- *; cbn.
- reflexivity.
- erewrite map_map, map_ext; try reflexivity. intros t. apply eval_comp.
- specialize (IHphi1 rho xi). specialize (IHphi2 rho xi). destruct b0; intuition.
- destruct q.
+ setoid_rewrite IHphi. split; intros H d; eapply sat_ext. 2, 4: apply (H d).
all: intros []; cbn; trivial; now setoid_rewrite eval_comp.
Qed.
Lemma sat_subst {ff : falsity_flag} rho sigma phi :
(forall x, eval rho (sigma x) = rho x) -> rho ⊨ phi <-> rho ⊨ (subst_form sigma phi).
Proof.
intros H. rewrite sat_comp. apply sat_ext. intros x. now rewrite <- H.
Qed.
Lemma sat_single {ff : falsity_flag} (rho : nat -> D) (Phi : form) (t : term) :
(eval rho t .: rho) ⊨ Phi <-> rho ⊨ subst_form (t..) Phi.
Proof.
rewrite sat_comp. apply sat_ext. now intros [].
Qed.
Lemma impl_sat {ff : falsity_flag} A rho phi :
sat rho (A ==> phi) <-> ((forall psi, psi el A -> sat rho psi) -> sat rho phi).
Proof.
induction A; cbn; firstorder congruence.
Qed.
Lemma impl_sat' {ff : falsity_flag} A rho phi :
sat rho (A ==> phi) -> ((forall psi, psi el A -> sat rho psi) -> sat rho phi).
Proof.
eapply impl_sat.
Qed.
Lemma bounded_eval_t n t sigma tau :
(forall k, n > k -> sigma k = tau k) -> bounded_t n t -> eval sigma t = eval tau t.
Proof.
intros H. induction 1; cbn; auto.
f_equal. now apply Vector.map_ext_in.
Qed.
Lemma bound_ext {ff : falsity_flag} N phi rho sigma :
bounded N phi -> (forall n, n < N -> rho n = sigma n) -> (rho ⊨ phi <-> sigma ⊨ phi).
Proof.
induction 1 in sigma, rho |- *; cbn; intros HN; try tauto.
- enough (map (eval rho) v = map (eval sigma) v) as E. now setoid_rewrite E.
apply Vector.map_ext_in. intros t Ht.
eapply bounded_eval_t; try apply HN. now apply H.
- destruct binop; now rewrite (IHbounded1 rho sigma), (IHbounded2 rho sigma).
- destruct quantop.
+ split; intros Hd d; eapply IHbounded.
all : try apply (Hd d); intros [] Hk; cbn; auto.
symmetry. all: apply HN; lia.
Qed.
Corollary sat_closed {ff : falsity_flag} rho sigma phi :
bounded 0 phi -> rho ⊨ phi <-> sigma ⊨ phi.
Proof.
intros H. eapply bound_ext. apply H. lia.
Qed.
Lemma bounded_S_forall {ff : falsity_flag} N phi :
bounded (S N) phi <-> bounded N (∀ phi).
Proof.
split; intros H.
- now constructor.
- inversion H. apply Eqdep_dec.inj_pair2_eq_dec in H4 as ->; trivial.
unfold Dec.dec. decide equality.
Qed.
Definition forall_times {ff : falsity_flag} n (phi : form) := iter (fun psi => ∀ psi) n phi.
End Substs.
End Tarski.
Section TM.
Context {Σ_funcs : funcs_signature}.
Context {Σ_preds : preds_signature}.
Instance TM : interp unit :=
{| i_func := fun _ _ => tt; i_atom := fun _ _ => True; |}.
Fact TM_sat (rho : nat -> unit) (phi : form falsity_off) :
rho ⊨ phi.
Proof.
revert rho. remember falsity_off as ff. induction phi; cbn; trivial.
- discriminate.
- destruct b0; auto.
- destruct q; firstorder.
Qed.
Fact TM_sat_decidable {ff} (rho : nat -> unit) (phi : form ff) :
rho ⊨ phi \/ ~(rho ⊨ phi).
Proof.
revert rho. induction phi; cbn; intros rho; eauto.
- destruct b0. destruct (IHphi1 rho), (IHphi2 rho); tauto.
- destruct q. destruct (IHphi (tt .: rho)).
+ left; now intros [].
+ right; intros Hcc. apply H, Hcc.
Qed.
End TM.
Section FlagsTransport.
Context {Σ_funcs : funcs_signature}.
Context {Σ_preds : preds_signature}.
Context {ff1 : falsity_flag}.
Section Bottom.
Variable D : Type.
Variable I : interp D.
Context (default : @form _ _ _ ff1).
Lemma sat_to_falsity_compat {ff2} rho (phi : @form _ _ _ ff2) :
(sat rho default -> False)
-> sat rho phi <-> sat rho (phi[default /⊥]).
Proof.
induction phi as [|t1 t2|ff [] phi IHphi psi IHpsi|ff [] phi IHphi] in rho,default|-*; intros Hdefault; split.
- intros [].
- apply Hdefault.
- intros H; apply H.
- intros H; apply H.
- intros H H1. cbn in H. apply IHpsi. 1:easy. apply H. now eapply IHphi, H1.
- intros H H1. cbn in H. apply IHpsi with default. 1:easy. apply H. now apply IHphi.
- intros H d. apply IHphi. 2: apply H. intros Hd. apply Hdefault.
eapply sat_comp in Hd. eapply sat_ext in Hd. 1: apply Hd.
now intros [|x].
- intros H d. apply IHphi with (default [↑]). 2: apply H. intros Hd. apply Hdefault.
eapply sat_comp in Hd. eapply sat_ext in Hd. 1: apply Hd.
now intros [|x].
Qed.
End Bottom.
Section Atoms.
Context {Σ_preds2 : preds_signature}.
Context (s : forall (P : Σ_preds), Vector.t (@term Σ_funcs) (ar_preds P) -> (@form Σ_funcs Σ_preds2 _ _)).
Context (Hresp : atom_subst_respects s).
Definition rho_from_vec {A} n (v : Vector.t A n) d : env A := fun m => match Compare_dec.lt_dec m n with
left Hl => Vector.nth v (Fin.of_nat_lt Hl)
| right _ => d end.
Lemma rho_from_vec_map {A B} {n} (f : B -> A) (t : Vector.t B n) (d2 : A) (d:B):
f d = d2 ->
forall k, rho_from_vec (map f t) d2 k = f (rho_from_vec t d k).
Proof.
intros H k. unfold rho_from_vec. destruct (Compare_dec.lt_dec k n) as [Hl|Hr].
- erewrite nth_map. 2:reflexivity. easy.
- easy.
Qed.
Fixpoint tabulate_vars n : Vector.t term n := match n with
0 => Vector.nil _
| S n => Vector.cons _ ($0) _ (map (subst_term (S >> var)) (tabulate_vars n)) end.
Lemma tabulate_vars_nth n (x : Fin.t n) : Vector.nth (tabulate_vars n) x = $(proj1_sig (Fin.to_nat x)).
Proof.
induction n in x|-*. 1: exfalso; revert x; apply Fin.case0.
induction x. try easy.
cbn. destruct (Fin.to_nat x) as [i P]. cbn in *. erewrite nth_map. 2:easy.
rewrite IHx. easy.
Qed.
Lemma semantic_lifting_correct n t tt :
map (subst_term (rho_from_vec t tt)) (tabulate_vars n) = t.
Proof.
apply eq_nth_iff. intros i ? <-.
erewrite nth_map. 2:reflexivity.
rewrite tabulate_vars_nth. cbn.
unfold rho_from_vec. destruct (Fin.to_nat i) as [i2 P2] eqn:Heq; cbn.
destruct Compare_dec.lt_dec; try lia.
f_equal. erewrite <- Fin.of_nat_to_nat_inv. rewrite Heq. cbn. apply Fin.of_nat_ext.
Qed.
Section ConstructInterp.
Variable D : Type.
Variable I : @interp Σ_funcs Σ_preds2 D.
Definition lift_s_semantically (d:D) (P : Σ_preds) (v : Vector.t D (ar_preds P)) : Prop
:= sat (rho_from_vec v d) (s (tabulate_vars (ar_preds P))).
Definition interp_s (d:D) : @interp Σ_funcs Σ_preds D := {|
i_func := @i_func _ _ D I;
i_atom := lift_s_semantically d
|}.
Lemma sat_atom_subst_compat rho phi n :
sat rho (phi [s/atom]) <-> @sat _ _ _ (interp_s (rho n)) _ rho phi.
Proof using Hresp.
unfold interp_s, lift_s_semantically. revert rho n.
induction phi as [|t1 t2|ff [] phi IHphi psi IHpsi|ff [] phi IHphi]; split.
- intros H; apply H.
- intros H; apply H.
- cbn; intros H.
eapply sat_ext with (((rho_from_vec t $n) >> eval rho)).
1: intros x; unfold funcomp. now apply rho_from_vec_map.
rewrite <- sat_comp. rewrite Hresp. now rewrite semantic_lifting_correct.
- cbn; intros H.
eapply (@sat_ext _ _ _ _ _ (((rho_from_vec t $n) >> eval rho))) in H.
2: intros x; unfold funcomp; symmetry; now apply rho_from_vec_map.
rewrite <- sat_comp in H. rewrite Hresp in H. now rewrite semantic_lifting_correct in H.
- cbn; intros H1 Hphi. apply IHpsi. 1:easy. apply H1. apply IHphi with n. 1:easy. apply Hphi.
- cbn; intros H1 Hphi. apply IHpsi with n. 1:easy. apply H1, IHphi. 1:easy. apply Hphi.
- cbn; intros H1 d. apply (IHphi s Hresp (d.:rho) (S n)). apply H1.
- cbn; intros H1 d. apply (IHphi s Hresp (d.:rho) (S n)). apply H1.
Qed.
End ConstructInterp.
Lemma valid_atom_subst_compat phi :
valid phi -> valid phi [s/atom].
Proof using Hresp.
intros H D I rho. unshelve apply <- sat_atom_subst_compat. 1:exact 0. apply H.
Qed.
Lemma satis_atom_subst_compat phi :
satis phi[s/atom] -> satis phi .
Proof using Hresp.
intros (D&I&rho&H). unshelve eapply sat_atom_subst_compat in H. 1:exact 0. do 3 eexists. apply H.
Qed.
End Atoms.
End FlagsTransport.
Section Bottom.
Context {Σ_funcs : funcs_signature}.
Context {Σ_preds : preds_signature}.
Variable D : Type.
Variable I : interp D.
Definition interp_bot (F_P : Prop) (i : @interp Σ_funcs Σ_preds D) : @interp Σ_funcs (@Σ_preds_bot Σ_preds) D := {|
i_func := @i_func _ _ D i;
i_atom := fun (P : (@preds (@Σ_preds_bot Σ_preds))) => match P with inl _ => fun v => F_P | inr P => fun v => @i_atom _ _ D i P v end
|}.
Definition sat_bot {ff : falsity_flag} (F_P : Prop) (rho : env D) (phi : form) : Prop
:= @sat _ Σ_preds_bot D (interp_bot F_P I) falsity_off rho (falsity_to_pred phi).
Lemma sat_bot_False {ff:falsity_flag} rho phi : sat_bot False rho phi <-> sat rho phi.
Proof.
induction phi in rho|-*.
- easy.
- easy.
- destruct b0. unfold sat_bot, falsity_to_pred in *. cbn.
split; intros H H1 %IHphi1; apply IHphi2; apply H, H1.
- destruct q. unfold sat_bot, falsity_to_pred in *. cbn.
split; intros H d; apply IHphi, H.
Qed.
End Bottom.
Arguments sat_bot {_} {_} {_} {_} {_} _ _ _.
Section BottomDef.
Context {Σ_funcs : funcs_signature}.
Context {Σ_preds : preds_signature}.
Context {ff : falsity_flag}.
Definition exploding D (M : interp D) (F_P:Prop) := forall rho phi, sat_bot F_P rho (⊥ → phi).
Arguments exploding _ _ _ : clear implicits.
Definition valid_exploding_ctx A phi :=
forall D (M : interp D) F_P rho, exploding D M F_P -> (forall psi, psi el A -> sat_bot F_P rho psi) -> sat_bot F_P rho phi.
Definition valid_exploding_theory (T:theory) phi :=
forall D (M : interp D) F_P rho, exploding D M F_P -> (forall psi, T psi -> sat_bot F_P rho psi) -> sat_bot F_P rho phi.
Definition valid_exploding phi :=
forall D (M : interp D) F_P rho, exploding D M F_P -> sat_bot F_P rho phi.
Definition satis_exploding phi :=
exists D (M : interp D) F_P rho, exploding D M F_P /\ sat_bot F_P rho phi.
End BottomDef.
Require Export Undecidability.FOL.Semantics.Tarski.FragmentCore.
From Undecidability Require Import Shared.ListAutomation.
Import ListAutomationNotations.
Require Import Vector Lia.
Local Set Implicit Arguments.
Local Unset Strict Implicit.
Local Notation vec := Vector.t.
Section Tarski.
Context {Σ_funcs : funcs_signature}.
Context {Σ_preds : preds_signature}.
Section Substs.
Variable D : Type.
Variable I : interp D.
Lemma eval_ext rho xi t :
(forall x, rho x = xi x) -> eval rho t = eval xi t.
Proof.
intros H. induction t; cbn.
- now apply H.
- f_equal. apply map_ext_in. now apply IH.
Qed.
Lemma eval_comp rho xi t :
eval rho (subst_term xi t) = eval (xi >> eval rho) t.
Proof.
induction t; cbn.
- reflexivity.
- f_equal. rewrite map_map. apply map_ext_in, IH.
Qed.
Lemma sat_ext {ff : falsity_flag} rho xi phi :
(forall x, rho x = xi x) -> rho ⊨ phi <-> xi ⊨ phi.
Proof.
induction phi as [ | b P v | | ] in rho, xi |- *; cbn; intros H.
- reflexivity.
- erewrite map_ext; try reflexivity. intros t. now apply eval_ext.
- specialize (IHphi1 rho xi). specialize (IHphi2 rho xi). destruct b0; intuition.
- destruct q.
+ split; intros H' d; eapply IHphi; try apply (H' d). 1,2: intros []; cbn; intuition.
Qed.
Lemma sat_ext' {ff : falsity_flag} rho xi phi :
(forall x, rho x = xi x) -> rho ⊨ phi -> xi ⊨ phi.
Proof.
intros Hext H. rewrite sat_ext. exact H.
intros x. now rewrite (Hext x).
Qed.
Lemma sat_comp {ff : falsity_flag} rho xi phi :
rho ⊨ (subst_form xi phi) <-> (xi >> eval rho) ⊨ phi.
Proof.
induction phi as [ | b P v | | ] in rho, xi |- *; cbn.
- reflexivity.
- erewrite map_map, map_ext; try reflexivity. intros t. apply eval_comp.
- specialize (IHphi1 rho xi). specialize (IHphi2 rho xi). destruct b0; intuition.
- destruct q.
+ setoid_rewrite IHphi. split; intros H d; eapply sat_ext. 2, 4: apply (H d).
all: intros []; cbn; trivial; now setoid_rewrite eval_comp.
Qed.
Lemma sat_subst {ff : falsity_flag} rho sigma phi :
(forall x, eval rho (sigma x) = rho x) -> rho ⊨ phi <-> rho ⊨ (subst_form sigma phi).
Proof.
intros H. rewrite sat_comp. apply sat_ext. intros x. now rewrite <- H.
Qed.
Lemma sat_single {ff : falsity_flag} (rho : nat -> D) (Phi : form) (t : term) :
(eval rho t .: rho) ⊨ Phi <-> rho ⊨ subst_form (t..) Phi.
Proof.
rewrite sat_comp. apply sat_ext. now intros [].
Qed.
Lemma impl_sat {ff : falsity_flag} A rho phi :
sat rho (A ==> phi) <-> ((forall psi, psi el A -> sat rho psi) -> sat rho phi).
Proof.
induction A; cbn; firstorder congruence.
Qed.
Lemma impl_sat' {ff : falsity_flag} A rho phi :
sat rho (A ==> phi) -> ((forall psi, psi el A -> sat rho psi) -> sat rho phi).
Proof.
eapply impl_sat.
Qed.
Lemma bounded_eval_t n t sigma tau :
(forall k, n > k -> sigma k = tau k) -> bounded_t n t -> eval sigma t = eval tau t.
Proof.
intros H. induction 1; cbn; auto.
f_equal. now apply Vector.map_ext_in.
Qed.
Lemma bound_ext {ff : falsity_flag} N phi rho sigma :
bounded N phi -> (forall n, n < N -> rho n = sigma n) -> (rho ⊨ phi <-> sigma ⊨ phi).
Proof.
induction 1 in sigma, rho |- *; cbn; intros HN; try tauto.
- enough (map (eval rho) v = map (eval sigma) v) as E. now setoid_rewrite E.
apply Vector.map_ext_in. intros t Ht.
eapply bounded_eval_t; try apply HN. now apply H.
- destruct binop; now rewrite (IHbounded1 rho sigma), (IHbounded2 rho sigma).
- destruct quantop.
+ split; intros Hd d; eapply IHbounded.
all : try apply (Hd d); intros [] Hk; cbn; auto.
symmetry. all: apply HN; lia.
Qed.
Corollary sat_closed {ff : falsity_flag} rho sigma phi :
bounded 0 phi -> rho ⊨ phi <-> sigma ⊨ phi.
Proof.
intros H. eapply bound_ext. apply H. lia.
Qed.
Lemma bounded_S_forall {ff : falsity_flag} N phi :
bounded (S N) phi <-> bounded N (∀ phi).
Proof.
split; intros H.
- now constructor.
- inversion H. apply Eqdep_dec.inj_pair2_eq_dec in H4 as ->; trivial.
unfold Dec.dec. decide equality.
Qed.
Definition forall_times {ff : falsity_flag} n (phi : form) := iter (fun psi => ∀ psi) n phi.
End Substs.
End Tarski.
Section TM.
Context {Σ_funcs : funcs_signature}.
Context {Σ_preds : preds_signature}.
Instance TM : interp unit :=
{| i_func := fun _ _ => tt; i_atom := fun _ _ => True; |}.
Fact TM_sat (rho : nat -> unit) (phi : form falsity_off) :
rho ⊨ phi.
Proof.
revert rho. remember falsity_off as ff. induction phi; cbn; trivial.
- discriminate.
- destruct b0; auto.
- destruct q; firstorder.
Qed.
Fact TM_sat_decidable {ff} (rho : nat -> unit) (phi : form ff) :
rho ⊨ phi \/ ~(rho ⊨ phi).
Proof.
revert rho. induction phi; cbn; intros rho; eauto.
- destruct b0. destruct (IHphi1 rho), (IHphi2 rho); tauto.
- destruct q. destruct (IHphi (tt .: rho)).
+ left; now intros [].
+ right; intros Hcc. apply H, Hcc.
Qed.
End TM.
Section FlagsTransport.
Context {Σ_funcs : funcs_signature}.
Context {Σ_preds : preds_signature}.
Context {ff1 : falsity_flag}.
Section Bottom.
Variable D : Type.
Variable I : interp D.
Context (default : @form _ _ _ ff1).
Lemma sat_to_falsity_compat {ff2} rho (phi : @form _ _ _ ff2) :
(sat rho default -> False)
-> sat rho phi <-> sat rho (phi[default /⊥]).
Proof.
induction phi as [|t1 t2|ff [] phi IHphi psi IHpsi|ff [] phi IHphi] in rho,default|-*; intros Hdefault; split.
- intros [].
- apply Hdefault.
- intros H; apply H.
- intros H; apply H.
- intros H H1. cbn in H. apply IHpsi. 1:easy. apply H. now eapply IHphi, H1.
- intros H H1. cbn in H. apply IHpsi with default. 1:easy. apply H. now apply IHphi.
- intros H d. apply IHphi. 2: apply H. intros Hd. apply Hdefault.
eapply sat_comp in Hd. eapply sat_ext in Hd. 1: apply Hd.
now intros [|x].
- intros H d. apply IHphi with (default [↑]). 2: apply H. intros Hd. apply Hdefault.
eapply sat_comp in Hd. eapply sat_ext in Hd. 1: apply Hd.
now intros [|x].
Qed.
End Bottom.
Section Atoms.
Context {Σ_preds2 : preds_signature}.
Context (s : forall (P : Σ_preds), Vector.t (@term Σ_funcs) (ar_preds P) -> (@form Σ_funcs Σ_preds2 _ _)).
Context (Hresp : atom_subst_respects s).
Definition rho_from_vec {A} n (v : Vector.t A n) d : env A := fun m => match Compare_dec.lt_dec m n with
left Hl => Vector.nth v (Fin.of_nat_lt Hl)
| right _ => d end.
Lemma rho_from_vec_map {A B} {n} (f : B -> A) (t : Vector.t B n) (d2 : A) (d:B):
f d = d2 ->
forall k, rho_from_vec (map f t) d2 k = f (rho_from_vec t d k).
Proof.
intros H k. unfold rho_from_vec. destruct (Compare_dec.lt_dec k n) as [Hl|Hr].
- erewrite nth_map. 2:reflexivity. easy.
- easy.
Qed.
Fixpoint tabulate_vars n : Vector.t term n := match n with
0 => Vector.nil _
| S n => Vector.cons _ ($0) _ (map (subst_term (S >> var)) (tabulate_vars n)) end.
Lemma tabulate_vars_nth n (x : Fin.t n) : Vector.nth (tabulate_vars n) x = $(proj1_sig (Fin.to_nat x)).
Proof.
induction n in x|-*. 1: exfalso; revert x; apply Fin.case0.
induction x. try easy.
cbn. destruct (Fin.to_nat x) as [i P]. cbn in *. erewrite nth_map. 2:easy.
rewrite IHx. easy.
Qed.
Lemma semantic_lifting_correct n t tt :
map (subst_term (rho_from_vec t tt)) (tabulate_vars n) = t.
Proof.
apply eq_nth_iff. intros i ? <-.
erewrite nth_map. 2:reflexivity.
rewrite tabulate_vars_nth. cbn.
unfold rho_from_vec. destruct (Fin.to_nat i) as [i2 P2] eqn:Heq; cbn.
destruct Compare_dec.lt_dec; try lia.
f_equal. erewrite <- Fin.of_nat_to_nat_inv. rewrite Heq. cbn. apply Fin.of_nat_ext.
Qed.
Section ConstructInterp.
Variable D : Type.
Variable I : @interp Σ_funcs Σ_preds2 D.
Definition lift_s_semantically (d:D) (P : Σ_preds) (v : Vector.t D (ar_preds P)) : Prop
:= sat (rho_from_vec v d) (s (tabulate_vars (ar_preds P))).
Definition interp_s (d:D) : @interp Σ_funcs Σ_preds D := {|
i_func := @i_func _ _ D I;
i_atom := lift_s_semantically d
|}.
Lemma sat_atom_subst_compat rho phi n :
sat rho (phi [s/atom]) <-> @sat _ _ _ (interp_s (rho n)) _ rho phi.
Proof using Hresp.
unfold interp_s, lift_s_semantically. revert rho n.
induction phi as [|t1 t2|ff [] phi IHphi psi IHpsi|ff [] phi IHphi]; split.
- intros H; apply H.
- intros H; apply H.
- cbn; intros H.
eapply sat_ext with (((rho_from_vec t $n) >> eval rho)).
1: intros x; unfold funcomp. now apply rho_from_vec_map.
rewrite <- sat_comp. rewrite Hresp. now rewrite semantic_lifting_correct.
- cbn; intros H.
eapply (@sat_ext _ _ _ _ _ (((rho_from_vec t $n) >> eval rho))) in H.
2: intros x; unfold funcomp; symmetry; now apply rho_from_vec_map.
rewrite <- sat_comp in H. rewrite Hresp in H. now rewrite semantic_lifting_correct in H.
- cbn; intros H1 Hphi. apply IHpsi. 1:easy. apply H1. apply IHphi with n. 1:easy. apply Hphi.
- cbn; intros H1 Hphi. apply IHpsi with n. 1:easy. apply H1, IHphi. 1:easy. apply Hphi.
- cbn; intros H1 d. apply (IHphi s Hresp (d.:rho) (S n)). apply H1.
- cbn; intros H1 d. apply (IHphi s Hresp (d.:rho) (S n)). apply H1.
Qed.
End ConstructInterp.
Lemma valid_atom_subst_compat phi :
valid phi -> valid phi [s/atom].
Proof using Hresp.
intros H D I rho. unshelve apply <- sat_atom_subst_compat. 1:exact 0. apply H.
Qed.
Lemma satis_atom_subst_compat phi :
satis phi[s/atom] -> satis phi .
Proof using Hresp.
intros (D&I&rho&H). unshelve eapply sat_atom_subst_compat in H. 1:exact 0. do 3 eexists. apply H.
Qed.
End Atoms.
End FlagsTransport.
Section Bottom.
Context {Σ_funcs : funcs_signature}.
Context {Σ_preds : preds_signature}.
Variable D : Type.
Variable I : interp D.
Definition interp_bot (F_P : Prop) (i : @interp Σ_funcs Σ_preds D) : @interp Σ_funcs (@Σ_preds_bot Σ_preds) D := {|
i_func := @i_func _ _ D i;
i_atom := fun (P : (@preds (@Σ_preds_bot Σ_preds))) => match P with inl _ => fun v => F_P | inr P => fun v => @i_atom _ _ D i P v end
|}.
Definition sat_bot {ff : falsity_flag} (F_P : Prop) (rho : env D) (phi : form) : Prop
:= @sat _ Σ_preds_bot D (interp_bot F_P I) falsity_off rho (falsity_to_pred phi).
Lemma sat_bot_False {ff:falsity_flag} rho phi : sat_bot False rho phi <-> sat rho phi.
Proof.
induction phi in rho|-*.
- easy.
- easy.
- destruct b0. unfold sat_bot, falsity_to_pred in *. cbn.
split; intros H H1 %IHphi1; apply IHphi2; apply H, H1.
- destruct q. unfold sat_bot, falsity_to_pred in *. cbn.
split; intros H d; apply IHphi, H.
Qed.
End Bottom.
Arguments sat_bot {_} {_} {_} {_} {_} _ _ _.
Section BottomDef.
Context {Σ_funcs : funcs_signature}.
Context {Σ_preds : preds_signature}.
Context {ff : falsity_flag}.
Definition exploding D (M : interp D) (F_P:Prop) := forall rho phi, sat_bot F_P rho (⊥ → phi).
Arguments exploding _ _ _ : clear implicits.
Definition valid_exploding_ctx A phi :=
forall D (M : interp D) F_P rho, exploding D M F_P -> (forall psi, psi el A -> sat_bot F_P rho psi) -> sat_bot F_P rho phi.
Definition valid_exploding_theory (T:theory) phi :=
forall D (M : interp D) F_P rho, exploding D M F_P -> (forall psi, T psi -> sat_bot F_P rho psi) -> sat_bot F_P rho phi.
Definition valid_exploding phi :=
forall D (M : interp D) F_P rho, exploding D M F_P -> sat_bot F_P rho phi.
Definition satis_exploding phi :=
exists D (M : interp D) F_P rho, exploding D M F_P /\ sat_bot F_P rho phi.
End BottomDef.