File ModelExtension
Require Import Logic.Classical_Prop.
From MatchingLogic.Theories Require Export Sorts_Semantics.
From MatchingLogic Require Export monotonic.
Import Definedness_Syntax.Notations.
Import Sorts_Syntax.Notations.
Import Logic.Notations.
Section with_syntax.
Context
{Σ : Signature}
(* TODO: maybe remove and use the imported one from Sorts_Syntax? *)
{ds : Definedness_Syntax.Syntax}
{ss : Sorts_Syntax.Syntax}
(HSortImptDef : imported_definedness = ds)
(HDefNeqInh : Definedness_Syntax.sym_inj def_sym ≠ Sorts_Syntax.sym_inj sym_inh)
.
Open Scope ml_scope.
Definition is_core_symbol (s : symbols) : Prop
:= s = Definedness_Syntax.sym_inj def_sym ∨ s = Sorts_Syntax.sym_inj sym_inh.
Instance is_core_symbol_dec (s : symbols) : Decision (is_core_symbol s).
Definition is_not_core_symbol (s : symbols) : Prop
:= ¬ is_core_symbol s.
Instance is_not_core_symbol_dec (s : symbols) : Decision (is_not_core_symbol s).
Inductive is_SPredicate
: Pattern → Prop :=
| spred_bott
: is_SPredicate patt_bott
| spred_def (ϕ : Pattern)
: is_SData ϕ → is_SPredicate (patt_defined ϕ)
(* note that we have to add equality and subseteq manually,
since they are usually defined using totality,
and we do not have totality in the fragment!
*)
| spred_eq (ϕ₁ ϕ₂ : Pattern)
: is_SData ϕ₁ → is_SData ϕ₂ → is_SPredicate (patt_equal ϕ₁ ϕ₂)
| spred_subseteq (ϕ₁ ϕ₂ : Pattern)
: is_SData ϕ₁ → is_SData ϕ₂ → is_SPredicate (patt_subseteq ϕ₁ ϕ₂)
| spred_imp (ϕ₁ ϕ₂ : Pattern)
: is_SPredicate ϕ₁ → is_SPredicate ϕ₂ → is_SPredicate (patt_imp ϕ₁ ϕ₂)
| spred_ex (ϕ : Pattern) (s : symbols)
: is_SPredicate ϕ → is_not_core_symbol s → is_SPredicate (ex (patt_sym s) , ϕ)
| spred_all (ϕ : Pattern) (s : symbols)
: is_SPredicate ϕ → is_not_core_symbol s → is_SPredicate (all (patt_sym s), ϕ)
with is_SData
: Pattern → Prop :=
| sdata_bott
: is_SData patt_bott
| sdata_fevar (x : evar)
: is_SData (patt_free_evar x)
| sdata_fsvar (X : svar)
: is_SData (patt_free_svar X)
| sdata_bevar (dbi : db_index)
: is_SData (patt_bound_evar dbi)
| sdata_bsvar (dbi : db_index)
: is_SData (patt_bound_svar dbi)
| sdata_sym (s : symbols)
: is_not_core_symbol s → is_SData (patt_sym s)
| sdata_inh (s : symbols)
: is_not_core_symbol s → is_SData (patt_inhabitant_set (patt_sym s))
| sdata_sneg (ϕ : Pattern) (s : symbols)
: is_SData ϕ → is_not_core_symbol s → is_SData (patt_sorted_neg (patt_sym s) ϕ)
| sdata_app (ϕ₁ ϕ₂ : Pattern)
: is_SData ϕ₁ → is_SData ϕ₂ → is_SData (patt_app ϕ₁ ϕ₂)
| sdata_or (ϕ₁ ϕ₂ : Pattern)
: is_SData ϕ₁ → is_SData ϕ₂ → is_SData (patt_or ϕ₁ ϕ₂)
| sdata_filter (ϕ ψ : Pattern)
: is_SData ϕ → is_SPredicate ψ → is_SData (patt_and ϕ ψ)
| sdata_ex (ϕ : Pattern) (s : symbols)
: is_SData ϕ → is_not_core_symbol s → is_SData (ex (patt_sym s) , ϕ)
(* This is disabled, because if the sort is empty, then the forall evaluates to full set,
and that does not get lifted to full set in the extended model.
*)
(*
| sdata_all (ϕ : Pattern) (s : symbols)
: is_SData ϕ -> is_not_core_symbol s -> is_SData (patt_sorted_forall (patt_sym s) ϕ)
*)
| sdata_mu (ϕ : Pattern)
: is_SData ϕ → is_SData (patt_mu ϕ)
.
Lemma is_SData_bevar_subst ϕ₁ ϕ₂ dbi:
is_SData ϕ₁ →
is_SData ϕ₂ →
is_SData (ϕ₁^[evar: dbi ↦ ϕ₂])
with is_SPredicate_bevar_subst ψ ϕ₂ dbi:
is_SPredicate ψ →
is_SData ϕ₂ →
is_SPredicate (ψ^[evar: dbi ↦ ϕ₂])
.
Lemma is_SData_evar_open x ϕ:
is_SData ϕ →
is_SData (ϕ^{evar: 0 ↦ x}).
Lemma is_SPredicate_evar_open x ϕ:
is_SPredicate ϕ →
is_SPredicate (ϕ^{evar: 0 ↦ x}).
Lemma is_SData_bsvar_subst ϕ₁ ϕ₂ dbi:
is_SData ϕ₁ →
is_SData ϕ₂ →
is_SData (ϕ₁^[svar: dbi ↦ ϕ₂])
with is_SPredicate_bsvar_subst ψ ϕ₂ dbi:
is_SPredicate ψ →
is_SData ϕ₂ →
is_SPredicate (ψ^[svar: dbi ↦ ϕ₂])
.
Lemma is_SData_svar_open x ϕ:
is_SData ϕ →
is_SData (ϕ^{svar: 0 ↦ x}).
Lemma is_SPredicate_svar_open x ϕ:
is_SPredicate ϕ →
is_SPredicate (ϕ^{svar: 0 ↦ x}).
Lemma is_SPredicate_patt_not (ϕ : Pattern) :
is_SPredicate ϕ →
is_SPredicate (patt_not ϕ).
Section ext.
Context
(M : Model)
(indec : ∀ (s : symbols),
is_not_core_symbol s →
∀ (m : Domain M) ρ,
Decision (m ∈ Minterp_inhabitant (patt_sym s) ρ))
(R : Type)
(fRM : R → (Domain M) → propset (Domain M + R)%type)
(fMR : (Domain M) → R → propset (Domain M + R)%type)
(fRR : R → R → propset (Domain M + R)%type)
(finh : R → propset (Domain M + R)%type)
.
Inductive Carrier := cdef | cinh | cel (el: (Domain M + R)%type).
Instance Carrier_inhabited : Inhabited Carrier := populate cdef.
Definition new_app_interp (x y : Carrier) : propset Carrier :=
match x with
| cdef ⇒
⊤
| cinh ⇒
match y with
| cdef ⇒ ∅
| cinh ⇒ ∅
| cel el ⇒
match el with
| inl m ⇒
cel <$> (@fmap propset _ _ _ inl (@app_ext _ M (sym_interp M (Sorts_Syntax.sym_inj sym_inh)) {[m]}))
| inr r ⇒
cel <$> finh r
end
end
| cel elx ⇒
match y with
| cdef ⇒ ∅
| cinh ⇒ ∅
| cel ely ⇒
match elx,ely with
| (inl mx),(inl my) ⇒
cel <$> (@fmap propset _ _ _ inl (@app_interp _ M mx my))
| (inl mx),(inr ry) ⇒
cel <$> (fMR mx ry)
| (inr rx),(inl my) ⇒
cel <$> (fRM rx my)
| (inr rx),(inr ry) ⇒
cel <$> (fRR rx ry)
end
end
end.
Definition new_sym_interp (s : symbols) : propset Carrier :=
match (decide (s = Definedness_Syntax.sym_inj def_sym)) with
| left _ ⇒ {[ cdef ]}
| right _ ⇒
match (decide (s = Sorts_Syntax.sym_inj sym_inh)) with
| left _ ⇒ {[ cinh ]}
| right _ ⇒ cel <$> (@fmap propset _ _ _ inl (@sym_interp _ M s))
end
end.
(* TODO: why was this poliorphic? *)
Definition Mext : Model :=
{|
Domain := Carrier ;
Domain_inhabited := Carrier_inhabited ;
app_interp := new_app_interp ;
sym_interp := new_sym_interp ;
|}.
Lemma Mext_satisfies_definedness : Mext ⊨ᵀ Definedness_Syntax.theory.
Definition lift_value (x : Domain M) : (Domain Mext)
:= cel (inl x).
Definition lift_set (xs : propset (Domain M)) : (propset (Domain Mext))
:= cel <$> (@fmap propset _ _ _ inl xs).
(* Valuations lifted from the original model to the extended model. *)
Definition lift_val (ρ : @Valuation Σ M) :
(@Valuation Σ Mext)
:= {|
evar_valuation := λ (x : evar), lift_value (evar_valuation ρ x);
svar_valuation := λ (X : svar), lift_set (svar_valuation ρ X)
|}.
Lemma lift_set_mono (xs ys : propset (Domain M)) :
xs ⊆ ys ↔
lift_set xs ⊆ lift_set ys.
Lemma lift_set_injective (xs ys : propset (Domain M)) :
xs = ys ↔ lift_set xs = lift_set ys.
Lemma Mext_indec :
∀ (s : symbols),
is_not_core_symbol s →
∀ (m : Domain Mext) ρ,
Decision (m ∈ @Minterp_inhabitant Σ _ Mext (patt_sym s) (lift_val ρ)).
Section semantic_preservation.
Context
(M_def : M ⊨ᵀ Definedness_Syntax.theory)
.
Lemma SPred_is_pre_predicate
(ψ : Pattern)
:
is_SPredicate ψ →
M_pre_predicate M ψ.
Lemma SPred_is_predicate
(ψ : Pattern)
:
well_formed_closed_ex_aux ψ 0 →
is_SPredicate ψ →
M_predicate M ψ.
Lemma semantics_preservation_sym (s : symbols)
(ρ : @Valuation _ M)
ρ0
:
is_not_core_symbol s →
@eval Σ Mext ρ0 (patt_sym s) =
lift_set (@eval Σ M ρ (patt_sym s)).
Lemma semantics_preservation_inhabitant_set (s : symbols)
(ρ : @Valuation _ M)
ρ0
:
is_not_core_symbol s →
@eval Σ Mext ρ0 (patt_inhabitant_set (patt_sym s))
= lift_set (@eval Σ M ρ (patt_inhabitant_set (patt_sym s))).
Lemma update_evar_val_lift_val_comm
(ρ : @Valuation _ M)
(x : evar)
(d : Domain M)
:
(@update_evar_val Σ Mext x (cel (inl d)) (lift_val ρ))
= lift_val (@update_evar_val Σ M x d ρ).
Lemma update_svar_val_lift_set_comm
(ρ : @Valuation _ M)
(X : svar)
(D : propset (Domain M))
:
(@update_svar_val Σ Mext X (lift_set D) (lift_val ρ))
= lift_val (@update_svar_val Σ M X D ρ).
Lemma lift_set_fa_union (C : Type) (f : C → propset (Domain M)) :
lift_set (stdpp_ext.propset_fa_union f) = stdpp_ext.propset_fa_union (λ k, lift_set (f k)).
Lemma lift_set_fa_intersection (C : Type) {_ : Inhabited C} (f : C → propset (Domain M)) :
lift_set (stdpp_ext.propset_fa_intersection f) = stdpp_ext.propset_fa_intersection (λ k, lift_set (f k)).
Lemma semantics_preservation
(sz : nat)
:
(
∀ (ϕ : Pattern) (ρ : @Valuation _ M),
pat_size ϕ < sz →
is_SData ϕ →
well_formed ϕ →
@eval Σ Mext (lift_val ρ) ϕ
= lift_set (@eval Σ M ρ ϕ)
)
∧
(
∀ (ψ : Pattern) (ρ : @Valuation _ M),
pat_size ψ < sz →
is_SPredicate ψ →
well_formed ψ →
(@eval Σ Mext (lift_val ρ) ψ = ∅
↔ @eval Σ M ρ ψ = ∅)
∧
(@eval Σ Mext (lift_val ρ) ψ = ⊤
↔ @eval Σ M ρ ψ = ⊤)
).
End semantic_preservation.
End ext.
End with_syntax.
From MatchingLogic.Theories Require Export Sorts_Semantics.
From MatchingLogic Require Export monotonic.
Import Definedness_Syntax.Notations.
Import Sorts_Syntax.Notations.
Import Logic.Notations.
Section with_syntax.
Context
{Σ : Signature}
(* TODO: maybe remove and use the imported one from Sorts_Syntax? *)
{ds : Definedness_Syntax.Syntax}
{ss : Sorts_Syntax.Syntax}
(HSortImptDef : imported_definedness = ds)
(HDefNeqInh : Definedness_Syntax.sym_inj def_sym ≠ Sorts_Syntax.sym_inj sym_inh)
.
Open Scope ml_scope.
Definition is_core_symbol (s : symbols) : Prop
:= s = Definedness_Syntax.sym_inj def_sym ∨ s = Sorts_Syntax.sym_inj sym_inh.
Instance is_core_symbol_dec (s : symbols) : Decision (is_core_symbol s).
Definition is_not_core_symbol (s : symbols) : Prop
:= ¬ is_core_symbol s.
Instance is_not_core_symbol_dec (s : symbols) : Decision (is_not_core_symbol s).
Inductive is_SPredicate
: Pattern → Prop :=
| spred_bott
: is_SPredicate patt_bott
| spred_def (ϕ : Pattern)
: is_SData ϕ → is_SPredicate (patt_defined ϕ)
(* note that we have to add equality and subseteq manually,
since they are usually defined using totality,
and we do not have totality in the fragment!
*)
| spred_eq (ϕ₁ ϕ₂ : Pattern)
: is_SData ϕ₁ → is_SData ϕ₂ → is_SPredicate (patt_equal ϕ₁ ϕ₂)
| spred_subseteq (ϕ₁ ϕ₂ : Pattern)
: is_SData ϕ₁ → is_SData ϕ₂ → is_SPredicate (patt_subseteq ϕ₁ ϕ₂)
| spred_imp (ϕ₁ ϕ₂ : Pattern)
: is_SPredicate ϕ₁ → is_SPredicate ϕ₂ → is_SPredicate (patt_imp ϕ₁ ϕ₂)
| spred_ex (ϕ : Pattern) (s : symbols)
: is_SPredicate ϕ → is_not_core_symbol s → is_SPredicate (ex (patt_sym s) , ϕ)
| spred_all (ϕ : Pattern) (s : symbols)
: is_SPredicate ϕ → is_not_core_symbol s → is_SPredicate (all (patt_sym s), ϕ)
with is_SData
: Pattern → Prop :=
| sdata_bott
: is_SData patt_bott
| sdata_fevar (x : evar)
: is_SData (patt_free_evar x)
| sdata_fsvar (X : svar)
: is_SData (patt_free_svar X)
| sdata_bevar (dbi : db_index)
: is_SData (patt_bound_evar dbi)
| sdata_bsvar (dbi : db_index)
: is_SData (patt_bound_svar dbi)
| sdata_sym (s : symbols)
: is_not_core_symbol s → is_SData (patt_sym s)
| sdata_inh (s : symbols)
: is_not_core_symbol s → is_SData (patt_inhabitant_set (patt_sym s))
| sdata_sneg (ϕ : Pattern) (s : symbols)
: is_SData ϕ → is_not_core_symbol s → is_SData (patt_sorted_neg (patt_sym s) ϕ)
| sdata_app (ϕ₁ ϕ₂ : Pattern)
: is_SData ϕ₁ → is_SData ϕ₂ → is_SData (patt_app ϕ₁ ϕ₂)
| sdata_or (ϕ₁ ϕ₂ : Pattern)
: is_SData ϕ₁ → is_SData ϕ₂ → is_SData (patt_or ϕ₁ ϕ₂)
| sdata_filter (ϕ ψ : Pattern)
: is_SData ϕ → is_SPredicate ψ → is_SData (patt_and ϕ ψ)
| sdata_ex (ϕ : Pattern) (s : symbols)
: is_SData ϕ → is_not_core_symbol s → is_SData (ex (patt_sym s) , ϕ)
(* This is disabled, because if the sort is empty, then the forall evaluates to full set,
and that does not get lifted to full set in the extended model.
*)
(*
| sdata_all (ϕ : Pattern) (s : symbols)
: is_SData ϕ -> is_not_core_symbol s -> is_SData (patt_sorted_forall (patt_sym s) ϕ)
*)
| sdata_mu (ϕ : Pattern)
: is_SData ϕ → is_SData (patt_mu ϕ)
.
Lemma is_SData_bevar_subst ϕ₁ ϕ₂ dbi:
is_SData ϕ₁ →
is_SData ϕ₂ →
is_SData (ϕ₁^[evar: dbi ↦ ϕ₂])
with is_SPredicate_bevar_subst ψ ϕ₂ dbi:
is_SPredicate ψ →
is_SData ϕ₂ →
is_SPredicate (ψ^[evar: dbi ↦ ϕ₂])
.
Lemma is_SData_evar_open x ϕ:
is_SData ϕ →
is_SData (ϕ^{evar: 0 ↦ x}).
Lemma is_SPredicate_evar_open x ϕ:
is_SPredicate ϕ →
is_SPredicate (ϕ^{evar: 0 ↦ x}).
Lemma is_SData_bsvar_subst ϕ₁ ϕ₂ dbi:
is_SData ϕ₁ →
is_SData ϕ₂ →
is_SData (ϕ₁^[svar: dbi ↦ ϕ₂])
with is_SPredicate_bsvar_subst ψ ϕ₂ dbi:
is_SPredicate ψ →
is_SData ϕ₂ →
is_SPredicate (ψ^[svar: dbi ↦ ϕ₂])
.
Lemma is_SData_svar_open x ϕ:
is_SData ϕ →
is_SData (ϕ^{svar: 0 ↦ x}).
Lemma is_SPredicate_svar_open x ϕ:
is_SPredicate ϕ →
is_SPredicate (ϕ^{svar: 0 ↦ x}).
Lemma is_SPredicate_patt_not (ϕ : Pattern) :
is_SPredicate ϕ →
is_SPredicate (patt_not ϕ).
Section ext.
Context
(M : Model)
(indec : ∀ (s : symbols),
is_not_core_symbol s →
∀ (m : Domain M) ρ,
Decision (m ∈ Minterp_inhabitant (patt_sym s) ρ))
(R : Type)
(fRM : R → (Domain M) → propset (Domain M + R)%type)
(fMR : (Domain M) → R → propset (Domain M + R)%type)
(fRR : R → R → propset (Domain M + R)%type)
(finh : R → propset (Domain M + R)%type)
.
Inductive Carrier := cdef | cinh | cel (el: (Domain M + R)%type).
Instance Carrier_inhabited : Inhabited Carrier := populate cdef.
Definition new_app_interp (x y : Carrier) : propset Carrier :=
match x with
| cdef ⇒
⊤
| cinh ⇒
match y with
| cdef ⇒ ∅
| cinh ⇒ ∅
| cel el ⇒
match el with
| inl m ⇒
cel <$> (@fmap propset _ _ _ inl (@app_ext _ M (sym_interp M (Sorts_Syntax.sym_inj sym_inh)) {[m]}))
| inr r ⇒
cel <$> finh r
end
end
| cel elx ⇒
match y with
| cdef ⇒ ∅
| cinh ⇒ ∅
| cel ely ⇒
match elx,ely with
| (inl mx),(inl my) ⇒
cel <$> (@fmap propset _ _ _ inl (@app_interp _ M mx my))
| (inl mx),(inr ry) ⇒
cel <$> (fMR mx ry)
| (inr rx),(inl my) ⇒
cel <$> (fRM rx my)
| (inr rx),(inr ry) ⇒
cel <$> (fRR rx ry)
end
end
end.
Definition new_sym_interp (s : symbols) : propset Carrier :=
match (decide (s = Definedness_Syntax.sym_inj def_sym)) with
| left _ ⇒ {[ cdef ]}
| right _ ⇒
match (decide (s = Sorts_Syntax.sym_inj sym_inh)) with
| left _ ⇒ {[ cinh ]}
| right _ ⇒ cel <$> (@fmap propset _ _ _ inl (@sym_interp _ M s))
end
end.
(* TODO: why was this poliorphic? *)
Definition Mext : Model :=
{|
Domain := Carrier ;
Domain_inhabited := Carrier_inhabited ;
app_interp := new_app_interp ;
sym_interp := new_sym_interp ;
|}.
Lemma Mext_satisfies_definedness : Mext ⊨ᵀ Definedness_Syntax.theory.
Definition lift_value (x : Domain M) : (Domain Mext)
:= cel (inl x).
Definition lift_set (xs : propset (Domain M)) : (propset (Domain Mext))
:= cel <$> (@fmap propset _ _ _ inl xs).
(* Valuations lifted from the original model to the extended model. *)
Definition lift_val (ρ : @Valuation Σ M) :
(@Valuation Σ Mext)
:= {|
evar_valuation := λ (x : evar), lift_value (evar_valuation ρ x);
svar_valuation := λ (X : svar), lift_set (svar_valuation ρ X)
|}.
Lemma lift_set_mono (xs ys : propset (Domain M)) :
xs ⊆ ys ↔
lift_set xs ⊆ lift_set ys.
Lemma lift_set_injective (xs ys : propset (Domain M)) :
xs = ys ↔ lift_set xs = lift_set ys.
Lemma Mext_indec :
∀ (s : symbols),
is_not_core_symbol s →
∀ (m : Domain Mext) ρ,
Decision (m ∈ @Minterp_inhabitant Σ _ Mext (patt_sym s) (lift_val ρ)).
Section semantic_preservation.
Context
(M_def : M ⊨ᵀ Definedness_Syntax.theory)
.
Lemma SPred_is_pre_predicate
(ψ : Pattern)
:
is_SPredicate ψ →
M_pre_predicate M ψ.
Lemma SPred_is_predicate
(ψ : Pattern)
:
well_formed_closed_ex_aux ψ 0 →
is_SPredicate ψ →
M_predicate M ψ.
Lemma semantics_preservation_sym (s : symbols)
(ρ : @Valuation _ M)
ρ0
:
is_not_core_symbol s →
@eval Σ Mext ρ0 (patt_sym s) =
lift_set (@eval Σ M ρ (patt_sym s)).
Lemma semantics_preservation_inhabitant_set (s : symbols)
(ρ : @Valuation _ M)
ρ0
:
is_not_core_symbol s →
@eval Σ Mext ρ0 (patt_inhabitant_set (patt_sym s))
= lift_set (@eval Σ M ρ (patt_inhabitant_set (patt_sym s))).
Lemma update_evar_val_lift_val_comm
(ρ : @Valuation _ M)
(x : evar)
(d : Domain M)
:
(@update_evar_val Σ Mext x (cel (inl d)) (lift_val ρ))
= lift_val (@update_evar_val Σ M x d ρ).
Lemma update_svar_val_lift_set_comm
(ρ : @Valuation _ M)
(X : svar)
(D : propset (Domain M))
:
(@update_svar_val Σ Mext X (lift_set D) (lift_val ρ))
= lift_val (@update_svar_val Σ M X D ρ).
Lemma lift_set_fa_union (C : Type) (f : C → propset (Domain M)) :
lift_set (stdpp_ext.propset_fa_union f) = stdpp_ext.propset_fa_union (λ k, lift_set (f k)).
Lemma lift_set_fa_intersection (C : Type) {_ : Inhabited C} (f : C → propset (Domain M)) :
lift_set (stdpp_ext.propset_fa_intersection f) = stdpp_ext.propset_fa_intersection (λ k, lift_set (f k)).
Lemma semantics_preservation
(sz : nat)
:
(
∀ (ϕ : Pattern) (ρ : @Valuation _ M),
pat_size ϕ < sz →
is_SData ϕ →
well_formed ϕ →
@eval Σ Mext (lift_val ρ) ϕ
= lift_set (@eval Σ M ρ ϕ)
)
∧
(
∀ (ψ : Pattern) (ρ : @Valuation _ M),
pat_size ψ < sz →
is_SPredicate ψ →
well_formed ψ →
(@eval Σ Mext (lift_val ρ) ψ = ∅
↔ @eval Σ M ρ ψ = ∅)
∧
(@eval Σ Mext (lift_val ρ) ψ = ⊤
↔ @eval Σ M ρ ψ = ⊤)
).
End semantic_preservation.
End ext.
End with_syntax.
This page has been generated by coqdoc