InqLog.FO.Semantics
Referent of a term
Fixpoint referent `{Model} (t : term) : World -> assignment -> Individual :=
match t with
| Var v =>
fun _ a =>
a v
| Func f args =>
fun w a =>
FInterpretation w f
(fun arg => referent (args arg) w a)
end.
Instance referent_Proper `{Model} :
Proper (term_eq ==> equiv ==> ext_eq ==> eq)
referent.
Proof.
intros t1.
induction t1 as [x1|f1 args1 IH].
all: intros [x2|f2 args2] H1 w1 w2 H2 a1 a2 H3.
all: try contradiction.
-
simpl in *.
congruence.
-
simpl in *.
destruct (f1 == f2) as [H4|H4]; try contradiction.
simpl in H4.
subst f2.
assert (H5 : FInterpretation w1 = FInterpretation w2).
{
rewrite H2.
reflexivity.
}
rewrite H5.
f_equiv.
intros arg.
apply IH.
+
apply H1.
+
exact H2.
+
exact H3.
Qed.
Lemma rigidity_referent `{Model} :
forall t w w' a,
term_rigid t ->
referent t w a =
referent t w' a.
Proof.
induction t as [x|f args IH].
all: intros w w' a H1.
-
reflexivity.
-
destruct H1 as [H1 H2].
simpl.
rewrite rigidity with (w' := w'); try assumption.
f_equiv.
intros arg.
apply IH.
apply H2.
Qed.
Lemma referent_subst `{Model} :
forall t w a sigma,
referent t.[sigma] w a =
referent t w (fun x => referent (sigma x) w a).
Proof.
induction t as [x|f args IH].
-
autosubst.
-
intros a w sigma.
asimpl.
f_equiv.
intros arg.
apply IH.
Qed.
Corollary referent_subst_var `{Model} :
forall t w a sigma,
referent t.[ren sigma] w a = referent t w (sigma >>> a).
Proof.
intros t w a sigma.
rewrite referent_subst.
reflexivity.
Qed.
Lemma unnamed_helper_Support_24 `{Model} :
forall w a i sigma,
(fun x => referent (up sigma x) w (i .: a)) ==
i .: (fun x => referent (sigma x) w a).
Proof.
intros * x.
revert w a i sigma.
induction x as [|x' IH].
all: intros w a i sigma.
-
reflexivity.
-
simpl.
assert (H1 : up sigma (S x') == (sigma x').[ren (+1)])
by apply rename_subst'.
rewrite H1.
apply referent_subst_var.
Qed.
Support satisfaction
Module Support (S : State_Spec).
Module SP := State_Properties S.
Import S SP.
Fixpoint support `{Model} (phi : form) :
state -> assignment -> Prop :=
match phi with
| Pred p args =>
fun s a =>
forall (w : World),
contains s w ->
PInterpretation w p
(fun arg => referent (args arg) w a)
| Bot _ =>
fun s a =>
forall (w : World),
~ contains s w
| Impl phi1 phi2 =>
fun s a =>
forall (t : state),
substate t s ->
support phi1 t a ->
support phi2 t a
| Conj phi1 phi2 =>
fun s a =>
support phi1 s a /\
support phi2 s a
| Idisj phi1 phi2 =>
fun s a =>
support phi1 s a \/
support phi2 s a
| Forall phi1 =>
fun s a =>
forall (i : Individual),
support phi1 s (i .: a)
| Iexists phi1 =>
fun s a =>
exists (i : Individual),
support phi1 s (i .: a)
end.
Again, we introduce some notation.
Notation "M , s , a |= phi" := (@support _ M phi s a)
(at level 95)
: form_scope.
Notation "s , a |= phi" := (support phi s a)
(at level 95)
: form_scope.
In order to make future proofs more readable, we restate the defining cases of support as various Facts.
They can be used for the rewrite-tactic.
Fact support_Pred `{Model} :
forall p args s a,
s, a |= <{Pred p args}> <->
forall w,
contains s w ->
PInterpretation w p
(fun arg => referent (args arg) w a).
Proof.
reflexivity.
Qed.
Fact support_Bot `{Model} :
forall x s a,
s, a |= <{Bot x}> <->
forall w,
~ contains s w.
Proof.
reflexivity.
Qed.
Fact support_Impl `{Model} :
forall phi1 phi2 s a,
s, a |= <{phi1 -> phi2}> <->
forall t,
substate t s ->
t, a |= phi1 ->
t, a |= phi2.
Proof.
reflexivity.
Qed.
Fact support_Conj `{Model} :
forall phi1 phi2 s a,
s, a |= <{phi1 /\ phi2}> <->
(s, a |= phi1) /\
(s, a |= phi2).
Proof.
reflexivity.
Qed.
Fact support_Idisj `{Model} :
forall phi1 phi2 s a,
s, a |= <{phi1 \\/ phi2}> <->
(s, a |= phi1) \/
(s, a |= phi2).
Proof.
reflexivity.
Qed.
Fact support_Forall `{Model} :
forall phi1 s a,
s, a |= <{forall phi1}> <->
forall i,
s, i.: a |= phi1.
Proof.
reflexivity.
Qed.
Fact support_Iexists `{Model} :
forall phi1 s a,
s, a |= <{iexists phi1}> <->
exists i,
s, i .: a |= phi1.
Proof.
reflexivity.
Qed.
Instance support_Proper `{M : Model} :
Proper (equiv ==> equiv ==> equiv ==> equiv)
support.
Proof with (try contradiction).
intros phi1.
induction phi1 as
[p1 args1
|?
|phi1 IH1 phi2 IH2
|phi1 IH1 phi2 IH2
|phi1 IH1 phi2 IH2
|phi1 IH1
|phi1 IH1].
all: intros psi H1 s1 s2 H2 a1 a2 H3.
all: destruct psi as
[p2 args2
|?
|psi1 psi2
|psi1 psi2
|psi1 psi2
|psi1
|psi1]...
all: simpl in H1.
-
destruct (p1 == p2) as [H4|H4]; try contradiction.
simpl in H4.
subst p2.
split.
all: intros H4 w H5.
all: rewrite H2 in H5 + rewrite <- H2 in H5.
all: apply H4 in H5.
all: simpl in H1.
all: eapply PInterpretation_Proper_inner.
all: try exact H5.
all: intros arg.
all: f_equiv.
all: try easy.
-
simpl.
firstorder.
all: now rewrite H2 + rewrite <- H2.
-
destruct H1 as [H11 H12].
do 2 rewrite support_Impl.
split.
all: intros H4 s3 H5 H6.
all: eapply IH2.
all: try eassumption + reflexivity.
all: try apply H4.
all: try (rewrite H2 + rewrite <- H2; exact H5).
all: eapply IH1.
all: eassumption + reflexivity.
-
destruct H1 as [H11 H12].
split.
all: intros [H4 H5].
all: split.
all: eapply IH1 + eapply IH2; eassumption + reflexivity.
-
destruct H1 as [H11 H12].
split.
all: intros [H4|H4]; [left|right].
all: eapply IH1 + eapply IH2; eassumption + reflexivity.
-
split.
all: intros H4 i.
all: rewrite support_Forall in H4.
all: specialize (H4 i).
all: eapply IH1.
all: try eassumption.
all: simpl. (* TODO annoying *)
all: f_equiv.
all: exact H3.
-
split.
all: intros [i H4].
all: exists i.
all: eapply IH1.
all: try eassumption.
all: simpl. (* TODO annoying *)
all: f_equiv.
all: exact H3.
Qed.
Therefore, we can see support as a morphism.
Program Definition support_Morph `{Model} (s : state) (a : assignment) : Morph form Prop :=
{|
morph phi := s,a |= phi
|}.
Next Obligation.
intros phi1 phi2 H1.
now rewrite H1.
Qed.
Proposition persistency `{Model} :
forall s t a phi,
s, a |= phi ->
substate t s ->
t, a |= phi.
Proof.
intros s t a phi.
revert a.
induction phi as
[p args
|?
|phi1 IH1 phi2 IH2
|phi1 IH1 phi2 IH2
|phi1 IH1 phi2 IH2
|phi1 IH1
|phi1 IH1].
all: intros a H1 H2.
-
firstorder.
-
intros w H3.
rewrite H2 in H3.
eapply H1.
exact H3.
-
firstorder.
-
firstorder.
-
firstorder.
-
firstorder.
-
destruct H1 as [i H1].
exists i.
eauto.
Qed.
Instance support_Proper_substate `{Model} :
Proper (form_eq ==> substate --> ext_eq ==> impl) support.
Proof.
intros phi1 phi2 H1 s1 s2 H2 a1 a2 H3 H4.
eapply persistency.
-
rewrite H1,H3 in H4.
exact H4.
-
exact H2.
Qed.
Proposition empty_state_property `{Model} :
forall (a : assignment) (phi : form),
empty_state, a |= phi.
Proof.
intros a phi.
revert a.
induction phi as
[p args
|?
|phi1 IH1 phi2 IH2
|phi1 IH1 phi2 IH2
|phi1 IH1 phi2 IH2
|phi1 IH1
|phi1 IH1].
all: intros a.
-
intros w H1.
now apply contains_empty_state_E in H1.
-
rewrite support_Bot.
intros w H1.
now apply contains_empty_state_E in H1.
-
intros t H1 H2.
rewrite H1.
apply IH2.
-
firstorder.
-
firstorder.
-
firstorder.
-
firstorder.
exact Individual_inh.
Qed.
Definition ruling_out `{Model} (s : state) (phi : form) (a : assignment) :=
~ exists t,
consistent t /\
substate t s /\
(t, a |= phi).
Notation "M , s , a _||_ phi" := (@ruling_out _ M s phi a)
(at level 95)
: form_scope.
Notation "s , a _||_ phi" := (ruling_out s phi a)
(at level 95)
: form_scope.
Lemma support_Neg `{Model} :
forall phi s a,
s, a |= <{~ phi}> <->
(s, a _||_ phi).
Proof.
intros phi s a.
unfold Neg.
rewrite support_Impl.
split.
-
intros H1 [t [[w H2] [H3 H4]]].
specialize (H1 t H3 H4).
rewrite support_Bot in H1.
firstorder.
-
intros H1 t H2 H3 w H4.
apply H1.
exists t.
repeat split.
all: firstorder.
Qed.
Lemma support_Top `{Model} :
forall s a,
s, a |= <{Top}>.
Proof.
intros s a.
unfold Top.
rewrite support_Neg.
intros [t [[w H1] [H2 H3]]].
specialize (H3 w).
congruence.
Qed.
Lemma support_Disj `{Model} :
forall phi1 phi2 s a,
s, a |= <{phi1 \/ phi2}> <->
~ exists t,
consistent t /\
substate t s /\
(t, a _||_ phi1) /\
(t, a _||_ phi2).
Proof.
intros phi1 phi2 s a.
unfold Disj.
rewrite support_Neg.
split.
-
intros H1.
intros [t [H2 [H3 [H4 H5]]]].
apply H1.
exists t.
rewrite support_Conj.
do 2 rewrite support_Neg.
auto.
-
intros H1.
intros [t [H2 [H3 [H4 H5]]]].
apply H1.
exists t.
rewrite support_Neg in H4,H5.
auto.
Qed.
Lemma support_Iff `{Model} :
forall phi1 phi2 s a,
s, a |= <{phi1 <-> phi2}> <->
forall t,
substate t s ->
t,a |= phi1 <->
(t,a |= phi2).
Proof.
firstorder.
Qed.
Lemma support_hsubst `{Model} :
forall phi s a sigma w,
(forall x, term_rigid (sigma x)) ->
(s, (fun x => referent (sigma x) w a) |= phi) <->
(s, a |= phi.|[sigma]).
Proof.
induction phi as
[p args
|?
|phi1 IH1 phi2 IH2
|phi1 IH1 phi2 IH2
|phi1 IH1 phi2 IH2
|phi1 IH1
|phi1 IH1].
all: intros s a sigma w H1.
-
split.
all: intros H2 w' H3.
all: specialize (H2 w' H3).
all: eapply PInterpretation_Proper_inner; try exact H2.
all: intros arg.
+
etransitivity.
*
apply referent_subst.
*
f_equiv.
intros x.
apply rigidity_referent.
exact (H1 x).
+
symmetry.
etransitivity.
*
apply referent_subst.
*
f_equiv.
intros x.
apply rigidity_referent.
exact (H1 x).
-
reflexivity.
-
split.
all: intros H2 t H3 H4.
all: eapply IH2; try eassumption.
all: simpl in H2.
all: apply H2; try assumption.
all: eapply IH1; eassumption.
-
split.
all: intros [H2 H3].
all: split.
all: try eapply IH1.
all: try eapply IH2.
all: eassumption.
-
split.
all: intros [H2|H2].
all: try eapply IH1 in H2.
all: try eapply IH2 in H2.
all: try assumption.
all: try (left; eassumption).
all: try (right; eassumption).
-
split.
all: intros H2 i.
all: simpl in H2.
all: specialize (H2 i).
+
eapply IH1.
*
apply unnamed_helper_Syntax_3.
exact H1.
*
rewrite unnamed_helper_Support_24.
exact H2.
+
eapply IH1 in H2.
*
rewrite <- unnamed_helper_Support_24.
exact H2.
*
apply unnamed_helper_Syntax_3.
exact H1.
-
split.
all: intros [i H2].
all: exists i.
+
eapply IH1.
*
apply unnamed_helper_Syntax_3.
exact H1.
*
rewrite unnamed_helper_Support_24.
exact H2.
+
eapply IH1 in H2.
*
rewrite <- unnamed_helper_Support_24.
exact H2.
*
apply unnamed_helper_Syntax_3.
exact H1.
Qed.
Corollary support_hsubst_var `{Model} :
forall phi s a sigma,
(s, (sigma >>> a) |= phi) <->
(s, a |= phi.|[ren sigma]).
Proof.
intros phi s a sigma.
destruct (classic (consistent s)) as [[w H1]|H1].
-
pose proof support_hsubst as H2.
specialize H2 with
(phi := phi)
(s := s)
(a := a)
(w := w).
specialize (H2 (ren sigma)).
apply H2.
intros x.
exact I.
-
apply state_eq_empty_state_iff_not_consistent in H1.
rewrite H1.
firstorder using empty_state_property.
Qed.
Definition support_mult
`{Model}
(s : state)
(a : assignment) :
list form -> Prop :=
mult (support_Morph s a).
Lemma support_mult_hsubst_var `{Model} :
forall Phi s a sigma,
support_mult s (sigma >>> a) Phi <->
support_mult s a (map (fun phi => phi.|[ren sigma]) Phi).
Proof.
induction Phi as [|phi Phi' IH].
all: intros s a sigma.
-
split.
all: intro.
all: apply mult_nil_I.
-
split.
all: intros H1.
all: apply mult_cons_E_tl in H1 as H2.
all: apply mult_cons_E_hd in H1.
+
simpl.
apply mult_cons_I.
*
apply support_hsubst_var in H1.
exact H1.
*
apply IH.
exact H2.
+
apply mult_cons_I.
*
apply support_hsubst_var.
exact H1.
*
apply IH.
exact H2.
Qed.
Proposition persistency_support_mult `{Model} :
forall s t a Phi,
support_mult s a Phi ->
substate t s ->
support_mult t a Phi.
Proof.
induction Phi as [|phi Phi' IH].
-
intros H1 H2.
apply mult_nil_I.
-
intros H1 H2.
apply mult_cons_E_hd in H1 as H3.
apply mult_cons_E_tl in H1 as H4.
apply mult_cons_I.
+
simpl.
rewrite H2.
exact H3.
+
eapply IH; eassumption.
Qed.
Definition support_some
`{Model}
(s : state)
(a : assignment) :
list form -> Prop :=
some (support_Morph s a).
Lemma support_some_hsubst_var `{Model} :
forall Phi s a sigma,
support_some s (sigma >>> a) Phi <->
support_some s a (map (fun phi => phi.|[ren sigma]) Phi).
Proof.
induction Phi as [|phi Phi' IH].
all: intros s a sigma.
-
split.
all: intros H1.
all: now apply some_nil_E in H1.
-
split.
all: simpl.
all: intros H1.
all: apply some_cons_E in H1 as [H1|H1].
+
apply some_cons_I_hd.
apply support_hsubst_var in H1.
exact H1.
+
apply some_cons_I_tl.
apply IH.
exact H1.
+
apply some_cons_I_hd.
apply support_hsubst_var.
exact H1.
+
apply some_cons_I_tl.
apply IH.
exact H1.
Qed.
Proposition persistency_support_some `{Model} :
forall s t a Phi,
support_some s a Phi ->
substate t s ->
support_some t a Phi.
Proof.
induction Phi as [|phi Phi' IH].
all: intros H1 H2.
-
now apply some_nil_E in H1.
-
apply some_cons_E in H1 as [H1|H1].
+
apply some_cons_I_hd.
simpl.
rewrite H2.
exact H1.
+
apply some_cons_I_tl.
apply IH; assumption.
Qed.
Definition support_valid `{S : Signature} (phi : form) :=
forall `(M : @Model S) s a,
s, a |= phi.
End Support.
Module Support_PropState := Support PropState_Impl.
Module Support_BoolState := Support BoolState_Impl.
Module Locality.
Export BoolState Support_BoolState.
Lemma restricted_referent `{M : Model} :
forall s t w a,
@referent _ (restricted_Model s) t w a =
@referent _ M t (proj1_sig w) a.
Proof.
intros s.
induction t as [x|f args IH].
all: intros w a.
-
reflexivity.
-
simpl.
apply FInterpretation_Proper_inner.
intros arg.
apply IH.
Qed.
Proposition locality `{M : Model} :
forall phi s a t,
substate t s ->
support phi t a <->
support phi (@restricted_state _ M s t) a.
Proof.
induction phi as
[p args
|?
|phi1 IH1 phi2 IH2
|phi1 IH1 phi2 IH2
|phi1 IH1 phi2 IH2
|phi1 IH1
|phi1 IH1].
all: intros s1 a s2 H1.
-
split.
+
intros H2 w H3.
apply andb_true_iff in H3 as [_ H3].
apply H2 in H3.
simpl.
eapply PInterpretation_Proper_inner; try exact H3.
intros arg.
apply restricted_referent.
+
intros H2 w H3.
apply H1 in H3 as H4.
specialize (H2 (exist _ _ H4)).
eapply PInterpretation_Proper_inner; try apply H2.
*
intros arg.
rewrite restricted_referent.
reflexivity.
*
apply andb_true_iff; split; assumption.
-
split.
+
intros H2 w H3.
apply andb_true_iff in H3 as [H3 H4].
eapply H2.
exact H4.
+
intros H2 w H3.
apply H1 in H3 as H4.
apply H2 with (w := exist _ w H4).
apply andb_true_iff.
split.
*
exact H4.
*
exact H3.
-
split.
all: intros H2 s3 H3 H4.
all: rewrite support_Impl in H2.
+
apply unrestricted_substate in H3 as H5.
rewrite (state_eq_restricted_state_unrestricted_state s1 s3) in *.
eapply IH2.
{
etransitivity; eassumption.
}
apply H2; try eassumption.
eapply IH1; try etransitivity; eassumption.
+
eapply IH2.
{
etransitivity; eassumption.
}
apply H2.
*
intros w H5.
apply andb_true_iff in H5 as [H5 H6].
apply andb_true_iff.
split.
--
exact H5.
--
apply H3.
exact H6.
*
apply IH1.
{
etransitivity; eassumption.
}
exact H4.
-
split.
all: intros [H2 H3].
all: split.
all: eapply IH1 + eapply IH2.
all: eassumption.
-
split.
all: intros [H2|H2].
all: eapply IH1 in H2 + eapply IH2 in H2.
all: try (left + right); eassumption.
-
split.
all: intros H2 i.
all: rewrite support_Forall in H2.
+
eapply IH1; auto.
+
eapply IH1; eauto.
-
split.
all: intros [i H2].
+
exists i.
eapply IH1; auto.
+
exists i.
eapply IH1; eauto.
Qed.
End Locality.
Module Truth (S : State_Spec).
Module SP := State_Properties S.
Module SSup := Support S.
Import S SP SSup.
Definition truth `{Model} (phi : form) (w : World) (a : assignment) : Prop :=
(singleton w), a |= phi.
Lemma truth_Pred `{Model} :
forall p args w a,
truth <{Pred p args}> w a <->
PInterpretation w p (fun arg => referent (args arg) w a).
Proof.
intros p args w a.
split.
-
intros H1.
apply H1.
apply contains_singleton_refl.
-
intros H1 w' H2.
apply contains_singleton_iff in H2.
erewrite PInterpretation_Proper_outer; try exact H2.
eapply PInterpretation_Proper_inner; try exact H1.
intros arg.
rewrite H2.
reflexivity.
Qed.
Lemma truth_Bot `{Model} :
forall v w a,
(truth <{Bot v}> w a) <-> False.
Proof.
intros ? w a.
split.
-
intros H1.
specialize (H1 w).
apply H1.
apply contains_singleton_refl.
-
contradiction.
Qed.
Lemma truth_Impl `{Model} :
forall phi1 phi2 w a,
truth <{phi1 -> phi2}> w a <->
(truth phi1 w a -> truth phi2 w a).
Proof.
intros phi1 phi2 w a.
split.
-
firstorder.
-
intros H1 t H2 H3.
apply substate_singleton_E in H2 as [H2|H2].
+
rewrite H2.
apply empty_state_property.
+
rewrite H2 in *.
apply H1.
exact H3.
Qed.
Lemma truth_Conj `{Model} :
forall phi1 phi2 w a,
truth <{phi1 /\ phi2}> w a <->
truth phi1 w a /\ truth phi2 w a.
Proof.
firstorder.
Qed.
Lemma truth_Idisj `{Model} :
forall phi1 phi2 w a,
truth <{phi1 \\/ phi2}> w a <->
truth phi1 w a \/ truth phi2 w a.
Proof.
firstorder.
Qed.
Lemma truth_Forall `{Model} :
forall phi w a,
truth <{forall phi}> w a <->
forall i,
truth phi w (i .: a).
Proof.
firstorder.
Qed.
Lemma truth_Iexists `{Model} :
forall phi w a,
truth <{iexists phi}> w a <->
exists i,
truth phi w (i .: a).
Proof.
firstorder.
Qed.
Instance truth_Proper `{M : Model} :
Proper (form_eq ==> equiv ==> ext_eq ==> iff) truth.
Proof.
intros phi1 phi2 H1 w1 w2 H2 a1 a2 H3.
unfold truth.
now rewrite H1,H2,H3.
Qed.
Program Definition truth_Morph `{M : Model} (w : World) (a : assignment) : Morph form Prop :=
{|
morph phi := truth phi w a
|}.
Next Obligation.
intros phi1 phi2 H1.
now rewrite H1.
Qed.
Lemma truth_Neg `{Model} :
forall phi w a,
truth <{~ phi}> w a <->
~ truth phi w a.
Proof.
intros phi w a.
unfold Neg.
rewrite truth_Impl.
rewrite truth_Bot.
reflexivity.
Qed.
Lemma truth_Top `{Model} :
forall w a,
truth Top w a <-> True.
Proof.
intros w a.
unfold Top.
rewrite truth_Neg.
rewrite truth_Bot.
easy.
Qed.
Lemma truth_Disj `{Model} :
forall phi1 phi2 w a,
truth <{phi1 \/ phi2}> w a <->
truth phi1 w a \/ truth phi2 w a.
Proof.
intros phi1 phi2 w a.
unfold Disj.
rewrite truth_Neg.
rewrite truth_Conj.
do 2 rewrite truth_Neg.
apply NNPP.
firstorder.
Qed.
Lemma truth_Iff `{Model} :
forall phi1 phi2 w a,
truth <{phi1 <-> phi2}> w a <->
(truth phi1 w a <-> truth phi2 w a).
Proof.
intros phi1 phi2 w a.
unfold Iff.
rewrite truth_Conj.
do 2 rewrite truth_Impl.
reflexivity.
Qed.
Lemma truth_Exists `{Model} :
forall phi w a,
truth <{exists phi}> w a <->
exists i,
truth phi w (i .: a).
Proof.
intros phi w a.
unfold Exists.
rewrite truth_Neg.
rewrite truth_Forall.
split.
-
intros H1.
apply NNPP.
intros H2.
apply H1.
intros i.
rewrite truth_Neg.
firstorder.
-
intros [i H1] H2.
specialize (H2 i).
rewrite truth_Neg in H2.
contradiction.
Qed.
Lemma truth_Iquest `{Model} :
forall phi w a,
truth <{? phi}> w a <-> True.
Proof.
intros phi w a.
unfold Iquest.
rewrite truth_Idisj.
rewrite truth_Neg.
apply NNPP.
firstorder.
Qed.
Proposition truth_classical_variant `{Model} :
forall phi w a,
truth (classical_variant phi) w a <->
truth phi w a.
Proof.
induction phi as
[p args
|?
|phi1 IH1 phi2 IH2
|phi1 IH1 phi2 IH2
|phi1 IH1 phi2 IH2
|phi1 IH1
|phi1 IH1].
all: intros w a.
all: simpl.
all: try reflexivity.
-
specialize (IH1 w a).
specialize (IH2 w a).
do 2 rewrite truth_Impl.
firstorder.
-
specialize (IH1 w a).
specialize (IH2 w a).
firstorder.
-
rewrite truth_Idisj.
rewrite truth_Disj.
rewrite IH1, IH2.
reflexivity.
-
do 2 rewrite truth_Forall.
split.
all: intros H1 i.
all: apply IH1.
all: exact (H1 i).
-
rewrite truth_Iexists.
rewrite truth_Exists.
split.
all: intros [i H1].
all: exists i.
all: apply IH1.
all: exact H1.
Qed.
Print Assumptions truth_classical_variant.
Definition truth_mult
`{Model}
(w : World)
(a : assignment) :
list form -> Prop :=
mult (truth_Morph w a).
Remark truth_mult_support_mult `{Model} :
forall Phi w a,
truth_mult w a Phi <->
support_mult (singleton w) a Phi.
Proof.
intros Phi w a.
firstorder.
Qed.
Definition truth_some
`{Model}
(w : World)
(a : assignment) :
list form -> Prop :=
some (truth_Morph w a).
Remark truth_some_support_some `{Model} :
forall Phi w a,
truth_some w a Phi <->
support_some (singleton w) a Phi.
Proof.
firstorder.
Qed.
Definition truth_conditional `{S : Signature} (phi : form) : Prop :=
forall `(M : @Model S) (s : state) (a : assignment),
(forall w, contains s w -> truth phi w a) ->
s, a |= phi.
Remark truth_conditional_other_direction `{S : Signature} :
forall phi `(M : @Model S) s a,
s, a |= phi ->
forall w,
contains s w ->
truth phi w a.
Proof.
intros phi M s a H1 w H2.
red.
eapply persistency; try eassumption.
apply singleton_substate_iff.
exact H2.
Qed.
Lemma truth_conditional_Pred `{Signature} :
forall p args,
truth_conditional (Pred p args).
Proof.
intros p args M s a.
intros H1 w1 H2.
apply truth_Pred.
auto using truth_Pred.
Qed.
Lemma truth_conditional_Bot `{Signature} :
forall x,
truth_conditional (Bot x).
Proof.
intros x M s a H1 w H2.
specialize (H1 w).
rewrite truth_Bot in H1.
auto.
Qed.
Lemma truth_conditional_Impl `{Signature} :
forall phi psi,
truth_conditional psi ->
truth_conditional <{phi -> psi}>.
Proof.
intros phi psi H1 M s a H2 t H3 H4.
apply H1.
intros w H5.
specialize (H2 w).
rewrite truth_Impl in H2.
eauto using truth_conditional_other_direction.
Qed.
Lemma truth_conditional_Conj `{Signature} :
forall phi psi,
truth_conditional phi ->
truth_conditional psi ->
truth_conditional <{phi /\ psi}>.
Proof.
intros phi psi H1 H2 M s a H3.
split.
-
apply H1.
intros w H4.
apply H3.
exact H4.
-
apply H2.
intros w H4.
apply H3.
exact H4.
Qed.
Lemma truth_conditional_Forall `{Signature} :
forall phi,
truth_conditional phi ->
truth_conditional <{forall phi}>.
Proof.
intros phi H1 M s a H2 i.
apply H1.
intros w H3.
apply H2.
exact H3.
Qed.
Lemma truth_conditional_Neg `{Signature} :
forall phi,
truth_conditional <{~ phi}>.
Proof.
intros phi M s a H1.
unfold Neg.
apply truth_conditional_Impl.
-
apply truth_conditional_Bot.
-
exact H1.
Qed.
Lemma truth_conditional_Disj `{Signature} :
forall phi psi,
truth_conditional <{phi \/ psi}>.
Proof.
intros phi psi.
unfold Disj.
apply truth_conditional_Neg.
Qed.
Lemma truth_conditional_Iff `{Signature} :
forall phi psi,
truth_conditional phi ->
truth_conditional psi ->
truth_conditional <{phi <-> psi}>.
Proof.
intros phi psi H1 H2.
unfold Iff.
apply truth_conditional_Conj.
all: apply truth_conditional_Impl.
all: assumption.
Qed.
Lemma truth_conditional_Exists `{Signature} :
forall phi,
truth_conditional <{exists phi}>.
Proof.
intros phi.
unfold Exists.
apply truth_conditional_Neg.
Qed.
Proposition classical_truth_conditional `{S : Signature} :
forall phi,
classical phi = true ->
truth_conditional phi.
Proof.
induction phi as
[p args
|?
|phi1 IH1 phi2 IH2
|phi1 IH1 phi2 IH2
|phi1 IH1 phi2 IH2
|phi1 IH1
|phi1 IH1].
all: intros H1.
-
apply truth_conditional_Pred.
-
apply truth_conditional_Bot.
-
simpl in H1.
apply andb_true_iff in H1 as [_ H1].
auto using truth_conditional_Impl.
-
simpl in H1.
apply andb_true_iff in H1 as [H1 H2].
auto using truth_conditional_Conj.
-
discriminate.
-
auto using truth_conditional_Forall.
-
discriminate.
Qed.
Print Assumptions classical_truth_conditional. (* Closed under the global context *)
Lemma truth_hsubst `{Model} :
forall phi w a sigma,
truth phi w (fun x => referent (sigma x) w a) <->
truth phi.|[sigma] w a.
Proof.
induction phi as
[p args
|?
|phi1 IH1 phi2 IH2
|phi1 IH1 phi2 IH2
|phi1 IH1 phi2 IH2
|phi1 IH1
|phi1 IH1].
all: intros w a sigma.
-
split.
all: intros H1.
all: apply truth_Pred.
all: apply truth_Pred in H1.
all: eapply PInterpretation_Proper_inner; try exact H1.
all: intros arg.
+
apply referent_subst.
+
symmetry.
apply referent_subst.
-
reflexivity.
-
split.
all: intros H1.
all: apply truth_Impl.
all: intros H2.
all: apply IH2.
all: simpl hsubst in H1.
all: rewrite truth_Impl in H1.
all: apply H1.
all: apply IH1.
all: exact H2.
-
simpl hsubst.
do 2 rewrite truth_Conj.
rewrite IH1, IH2.
reflexivity.
-
simpl hsubst.
do 2 rewrite truth_Idisj.
rewrite IH1, IH2.
reflexivity.
-
simpl hsubst.
do 2 rewrite truth_Forall.
split.
all: intros H1 i.
all: specialize (H1 i).
+
apply IH1.
red.
rewrite unnamed_helper_Support_24.
exact H1.
+
apply IH1 in H1.
red.
rewrite <- unnamed_helper_Support_24.
exact H1.
-
simpl hsubst.
do 2 rewrite truth_Iexists.
split.
all: intros [i H1].
all: exists i.
+
apply IH1.
red.
rewrite unnamed_helper_Support_24.
exact H1.
+
apply IH1 in H1.
red.
rewrite <- unnamed_helper_Support_24.
exact H1.
Qed.
End Truth.
Module Truth_PropState := Truth PropState_Impl.
Module Truth_BoolState := Truth BoolState_Impl.
Export BoolState Support_BoolState Truth_BoolState.