File Semantics
From Coq Require Import Classical_Prop.
From Coq Require Export Program.Wf
PropExtensionality
FunctionalExtensionality.
From Equations Require Export -(notations) Equations.
From MatchingLogic Require Export Lattice
NamedAxioms
Syntax.
Import MatchingLogic.Syntax.Notations.
Import MatchingLogic.Substitution.Notations.
From Coq Require Export Program.Wf
PropExtensionality
FunctionalExtensionality.
From Equations Require Export -(notations) Equations.
From MatchingLogic Require Export Lattice
NamedAxioms
Syntax.
Import MatchingLogic.Syntax.Notations.
Import MatchingLogic.Substitution.Notations.
Section semantics.
Context {signature : Signature}.
Open Scope ml_scope.
(* Model of AML ref. snapshot: Definition 2 *)
Section with_model.
Context {M : Model}.
Definition Empty : propset (Domain M) := @empty (propset (Domain M)) _.
Definition Full : propset (Domain M) := @top (propset (Domain M)) _.
(* full set and empty set are distinct *)
Lemma empty_impl_not_full : ∀ (S : propset (Domain M)),
S = Empty → S ≠ Full.
Lemma full_impl_not_empty : ∀ (S : propset (Domain M)),
S = Full → S ≠ Empty.
(* element and set variable valuations *)
Polymorphic Record Valuation : Type := mkValuation
{ evar_valuation : evar → Domain M ;
svar_valuation : svar → propset (Domain M) ;
}.
Definition update_evar_val
(ev : evar) (x : Domain M) (val : Valuation) : Valuation :=
{|
evar_valuation := fun ev' : evar ⇒
if decide (ev = ev') is left _ then x else evar_valuation val ev' ;
svar_valuation := (svar_valuation val)
|}.
Definition update_svar_val
(sv : svar) (X : propset (Domain M)) (val : Valuation) : Valuation :=
{|
evar_valuation := (evar_valuation val);
svar_valuation := fun sv' : svar ⇒
if decide (sv = sv') is left _ then X else svar_valuation val sv' ;
|}.
Lemma update_evar_val_svar_val_comm
(ev : evar) (x : Domain M)
(sv : svar) (X : propset (Domain M))
(ρ : Valuation) :
update_evar_val ev x (update_svar_val sv X ρ)
= update_svar_val sv X (update_evar_val ev x ρ).
Lemma update_svar_val_comm :
∀ (X1 X2 : svar) (S1 S2 : propset (Domain M)) (ρ : Valuation),
X1 ≠ X2 →
update_svar_val X1 S1 (update_svar_val X2 S2 ρ)
= update_svar_val X2 S2 (update_svar_val X1 S1 ρ).
Lemma update_svar_val_shadow : ∀ (X : svar)
(S1 S2 : propset (Domain M))
(ρ : Valuation),
update_svar_val X S1 (update_svar_val X S2 ρ) = update_svar_val X S1 ρ.
Lemma update_svar_val_neq (ρ : Valuation) X1 S X2 :
X1 ≠ X2 → svar_valuation (update_svar_val X1 S ρ) X2 = svar_valuation ρ X2.
Lemma update_evar_val_comm :
∀ (x1 x2 : evar) (m1 m2 : Domain M) (ρ : Valuation),
x1 ≠ x2 →
update_evar_val x1 m1 (update_evar_val x2 m2 ρ)
= update_evar_val x2 m2 (update_evar_val x1 m1 ρ).
Lemma update_evar_val_shadow : ∀ (x : evar)
(m1 m2 : Domain M)
(ρ : Valuation),
update_evar_val x m1 (update_evar_val x m2 ρ) = update_evar_val x m1 ρ.
Lemma update_evar_val_same x m ρ :
evar_valuation (update_evar_val x m ρ) x = m.
Lemma update_evar_val_neq (ρ : Valuation) x1 e x2 :
x1 ≠ x2 → evar_valuation (update_evar_val x1 e ρ) x2 = evar_valuation ρ x2.
Lemma update_evar_val_same_2 x ρ :
update_evar_val x (evar_valuation ρ x) ρ = ρ.
Lemma update_svar_val_same X S ρ :
svar_valuation (update_svar_val X S ρ) X = S.
Lemma update_svar_val_same_2 x ρ :
update_svar_val x (svar_valuation ρ x) ρ = ρ.
(* We use propositional extensionality here. *)
#[export]
Instance propset_leibniz_equiv : LeibnizEquiv (propset (Domain M)).
(* extending pointwise application *)
Lemma app_ext_bot_r :
∀ S : propset (Domain M),
app_ext S ∅ = ∅.
Theorem app_ext_singleton : ∀ (x y : M),
app_ext {[x]} {[y]} = app_interp _ x y.
Lemma app_ext_bot_l :
∀ S : propset (Domain M),
app_ext ∅ S = ∅.
Lemma app_ext_monotonic_l :
∀ (S1 S2 S : propset (Domain M)),
S1 ⊆ S2 → (app_ext S1 S) ⊆ (app_ext S2 S).
Lemma app_ext_monotonic_r :
∀ (S S1 S2 : propset (Domain M)),
S1 ⊆ S2 → (app_ext S S1) ⊆ (app_ext S S2).
(* Semantics of AML ref. snapshot: Definition 3 *)
Let OS := PropsetOrderedSet (Domain M).
Let L := PowersetLattice (Domain M).
Equations? eval (ρ : Valuation) (ϕ : Pattern)
: propset (@Domain M) by wf (pat_size ϕ) :=
eval ρ (patt_free_evar x) := {[ evar_valuation ρ x ]} ;
eval ρ (patt_free_svar X) := svar_valuation ρ X ;
eval ρ (patt_bound_evar n) := ∅ ;
eval ρ (patt_bound_svar n) := ∅ ;
eval ρ (patt_sym s) := @sym_interp M s ;
eval ρ (patt_app ϕ₁ ϕ₂) := app_ext (eval ρ ϕ₁) (eval ρ ϕ₂) ;
eval ρ (patt_bott) := ∅ ;
eval ρ (patt_imp ϕ₁ ϕ₂) := (difference ⊤ (eval ρ ϕ₁)) ∪ (eval ρ ϕ₂) ;
eval ρ (patt_exists ϕ') := let x := fresh_evar ϕ' in
propset_fa_union
(fun e ⇒
let ρ' := (update_evar_val x e ρ) in
eval ρ' (ϕ'^{evar: 0 ↦ x})
) ;
eval ρ (patt_mu ϕ') := let X := fresh_svar ϕ' in
@LeastFixpointOf _ OS L
(fun S ⇒
let ρ' := (update_svar_val X S ρ) in
eval ρ' (ϕ'^{svar: 0 ↦ X})
) .
Definition Fassoc ρ ϕ X :=
λ S, eval (update_svar_val X S ρ) ϕ.
Lemma eval_free_evar_simpl
(ρ : Valuation)
(x : evar) :
eval ρ (patt_free_evar x) = {[ evar_valuation ρ x ]}.
Lemma eval_free_svar_simpl
(ρ : Valuation)
(X : svar) :
eval ρ (patt_free_svar X) = svar_valuation ρ X.
Lemma eval_bound_evar_simpl
(ρ : Valuation)
(x : db_index) :
eval ρ (patt_bound_evar x) = ∅.
Lemma eval_bound_svar_simpl
(ρ : Valuation)
(X : db_index) :
eval ρ (patt_bound_svar X) = ∅.
Lemma eval_sym_simpl
(ρ : Valuation)
(s : symbols) :
eval ρ (patt_sym s) = @sym_interp M s.
Lemma eval_app_simpl
(ρ : Valuation)
(ϕ₁ ϕ₂ : Pattern) :
eval ρ (patt_app ϕ₁ ϕ₂) = app_ext (eval ρ ϕ₁) (eval ρ ϕ₂).
Lemma eval_bott_simpl
(ρ : Valuation) :
eval ρ patt_bott = ∅.
Lemma eval_imp_simpl
(ρ : Valuation)
(ϕ₁ ϕ₂ : Pattern) :
eval ρ (patt_imp ϕ₁ ϕ₂) = (difference ⊤ (eval ρ ϕ₁)) ∪ (eval ρ ϕ₂).
Lemma eval_ex_simpl
(ρ : Valuation)
(ϕ' : Pattern) :
eval ρ (patt_exists ϕ') =
let x := fresh_evar ϕ' in
propset_fa_union
(fun e ⇒
let ρ' := (update_evar_val x e ρ) in
eval ρ' (ϕ'^{evar: 0 ↦ x})
).
Lemma eval_mu_simpl
(ρ : Valuation)
(ϕ' : Pattern) :
eval ρ (patt_mu ϕ') =
let X := fresh_svar ϕ' in
@LeastFixpointOf _ OS L
(fun S ⇒
let ρ' := (update_svar_val X S ρ) in
eval ρ' (ϕ'^{svar: 0 ↦ X})
).
(* TODO extend with derived constructs using typeclasses *)
Definition eval_simpl :=
( eval_free_evar_simpl,
eval_free_svar_simpl,
eval_bound_evar_simpl,
eval_bound_svar_simpl,
eval_sym_simpl,
eval_app_simpl,
eval_bott_simpl,
eval_imp_simpl,
eval_ex_simpl,
eval_mu_simpl
).
End with_model.
Section with_explicit_model.
Context (M : Model).
(* Model predicate. Useful mainly if the pattern is well-formed. *)
Definition M_predicate (ϕ : Pattern) : Prop := ∀ ρ,
@eval M ρ ϕ = ⊤ ∨ eval ρ ϕ = ∅.
Lemma M_predicate_impl ϕ₁ ϕ₂ : M_predicate ϕ₁ → M_predicate ϕ₂ → M_predicate (patt_imp ϕ₁ ϕ₂).
Hint Resolve M_predicate_impl : core.
Lemma M_predicate_bott : M_predicate patt_bott.
Hint Resolve M_predicate_bott : core.
Lemma M_predicate_exists ϕ :
let x := evar_fresh (elements (free_evars ϕ)) in
M_predicate (ϕ^{evar: 0 ↦ x}) → M_predicate (patt_exists ϕ).
Hint Resolve M_predicate_exists : core.
Lemma predicate_not_empty_iff_full ϕ ρ :
M_predicate ϕ →
@eval M ρ ϕ ≠ ∅ ↔
eval ρ ϕ = ⊤.
Lemma predicate_not_full_iff_empty ϕ ρ :
M_predicate ϕ →
@eval M ρ ϕ ≠ ⊤ ↔
eval ρ ϕ = ∅.
Lemma eval_impl_MP ϕ₁ ϕ₂ ρ :
@eval M ρ (patt_imp ϕ₁ ϕ₂) = ⊤ →
eval ρ ϕ₁ = ⊤ →
eval ρ ϕ₂ = ⊤.
Lemma eval_predicate_impl ϕ₁ ϕ₂ ρ :
M_predicate ϕ₁ →
@eval M ρ (patt_imp ϕ₁ ϕ₂) = ⊤
↔ (eval ρ ϕ₁ = ⊤
→ eval ρ ϕ₂ = ⊤).
(* ϕ is a well-formed body of ex *)
Lemma eval_exists_predicate_full ϕ ρ :
let x := fresh_evar ϕ in
M_predicate (ϕ^{evar: 0 ↦ x}) →
eval ρ (patt_exists ϕ) = ⊤ ↔
∃ (m : Domain M), eval (update_evar_val x m ρ) (ϕ^{evar: 0 ↦ x}) = ⊤.
Lemma eval_exists_empty ϕ ρ :
let x := fresh_evar ϕ in
eval ρ (patt_exists ϕ) = ∅ ↔
∀ (m : Domain M), eval (update_evar_val x m ρ) (ϕ^{evar: 0 ↦ x}) = ∅.
(* Theory,axiom ref. snapshot: Definition 5 *)
End with_explicit_model.
Definition satisfies_model (M : Model) (ϕ : Pattern) : Prop :=
∀ (ρ : Valuation),
eval (M := M) ρ ϕ = ⊤.
Definition satisfies_theory (m : Model) (theory : Theory)
: Prop := ∀ axiom : Pattern, axiom ∈ theory → (satisfies_model m axiom).
(* TODO rename *)
Definition satisfies (theory : Theory) (p: Pattern)
: Prop := ∀ m : Model, (satisfies_theory m theory) → (satisfies_model m p).
Lemma satisfies_theory_iff_satisfies_named_axioms {Σ : Signature} NAs M:
satisfies_theory M (theory_of_NamedAxioms NAs) ↔
∀ (n : NAName NAs), satisfies_model M (NAAxiom _ n).
Lemma satisfies_theory_subseteq M Γ₁ Γ₂:
Γ₁ ⊆ Γ₂ →
satisfies_theory M Γ₂ →
satisfies_theory M Γ₁.
(* theory predicate *)
Definition T_predicate Γ ϕ := ∀ M, satisfies_theory M Γ → M_predicate M ϕ.
Hint Extern 4 (M_predicate _ (evar_open _ _ _)) ⇒ mlSimpl : core.
Hint Extern 4 (T_predicate _ (evar_open _ _ _)) ⇒ mlSimpl : core.
Hint Extern 4 (M_predicate _ (svar_open _ _ _)) ⇒ mlSimpl : core.
Hint Extern 4 (T_predicate _ (svar_open _ _ _)) ⇒ mlSimpl : core.
Lemma T_predicate_impl_M_predicate M Γ ϕ:
satisfies_theory M Γ → T_predicate Γ ϕ → M_predicate M ϕ.
Hint Resolve T_predicate_impl_M_predicate : core.
Lemma T_predicate_impl Γ ϕ₁ ϕ₂ : T_predicate Γ ϕ₁ → T_predicate Γ ϕ₂ → T_predicate Γ (patt_imp ϕ₁ ϕ₂).
Hint Resolve T_predicate_impl : core.
Lemma T_predicate_bot Γ : T_predicate Γ patt_bott.
Hint Resolve T_predicate_bot : core.
(* TODO: top iff exists forall *)
Section with_model.
Context {M : Model}.
(* If phi1 \subseteq phi2, then U_x phi1 \subseteq U_x phi2 *)
Lemma eval_subset_union x ϕ₁ ϕ₂ :
(∀ ρ, (eval ρ ϕ₁) ⊆ (@eval M ρ ϕ₂) )
→ (∀ ρ,
(propset_fa_union (fun e ⇒ eval (update_evar_val x e ρ) ϕ₁))
⊆
(propset_fa_union (fun e ⇒ @eval M (update_evar_val x e ρ) ϕ₂))
).
(* eval unchanged when using fresh element varaiable *)
Lemma eval_free_evar_independent ρ x v ϕ:
evar_is_fresh_in x ϕ →
@eval M (update_evar_val x v ρ) ϕ = eval ρ ϕ.
Lemma eval_free_svar_independent ρ X S ϕ:
svar_is_fresh_in X ϕ →
@eval M (update_svar_val X S ρ) ϕ = eval ρ ϕ.
Lemma Private_eval_fresh_var_open sz ϕ dbi ρ:
pat_size ϕ ≤ sz →
(
∀ X Y S,
svar_is_fresh_in X ϕ →
svar_is_fresh_in Y ϕ →
eval (update_svar_val X S ρ) (ϕ^{svar: dbi ↦ X})
= @eval M (update_svar_val Y S ρ) (ϕ^{svar: dbi ↦ Y})
) ∧
(
∀ x y c,
evar_is_fresh_in x ϕ →
evar_is_fresh_in y ϕ →
@eval M (update_evar_val x c ρ) (ϕ^{evar: dbi ↦ x})
= eval (update_evar_val y c ρ) (ϕ^{evar: dbi ↦ y})
)
.
Lemma eval_fresh_evar_open ϕ x y c dbi ρ:
evar_is_fresh_in x ϕ →
evar_is_fresh_in y ϕ →
@eval M (update_evar_val x c ρ) (ϕ^{evar: dbi ↦ x})
= eval (update_evar_val y c ρ) (ϕ^{evar: dbi ↦ y}).
Lemma eval_fresh_svar_open ϕ X Y S dbi ρ:
svar_is_fresh_in X ϕ →
svar_is_fresh_in Y ϕ →
@eval M (update_svar_val X S ρ) (ϕ^{svar: dbi ↦ X})
= eval (update_svar_val Y S ρ) (ϕ^{svar: dbi ↦ Y}).
(* There are two ways how to plug a pattern phi2 into a pattern phi1:
either substitute it for some variable,
or evaluate phi2 first and then evaluate phi1 with valuation updated to the result of phi2
*)
Lemma Private_plugging_patterns : ∀ (sz : nat) (dbi : db_index) (phi1 phi2 : Pattern),
pat_size phi1 ≤ sz → ∀ (ρ : Valuation) (X : svar),
well_formed_closed phi2 → well_formed_closed_mu_aux phi1 (S dbi) →
¬ elem_of X (free_svars phi1) →
@eval M ρ (phi1^[svar:dbi ↦ phi2])
= eval (update_svar_val X (@eval M ρ phi2) ρ)
(phi1^{svar: dbi ↦ X}).
Lemma set_substitution_lemma : ∀ (dbi : db_index) (phi1 phi2 : Pattern),
∀ (ρ : Valuation) (X : svar),
well_formed_closed phi2 → well_formed_closed_mu_aux phi1 (S dbi) →
¬ elem_of X (free_svars phi1) →
@eval M ρ (phi1^[svar: dbi ↦ phi2])
= eval (update_svar_val X (@eval M ρ phi2) ρ) (phi1^{svar: dbi ↦ X}).
Lemma Private_plugging_patterns_bevar_subst : ∀ (sz : nat) (dbi : db_index)
(phi : Pattern) (y : evar),
pat_size phi ≤ sz → ∀ (ρ : Valuation) (x : evar),
evar_is_fresh_in x phi → well_formed_closed_ex_aux phi (S dbi) →
@eval M ρ (phi^[evar: dbi ↦ patt_free_evar y])
= eval (update_evar_val x (evar_valuation ρ y) ρ) (phi^{evar: dbi ↦ x}).
Lemma element_substitution_lemma
(phi : Pattern) (x y : evar) (ρ : Valuation) (dbi : db_index) :
evar_is_fresh_in x phi → well_formed_closed_ex_aux phi (S dbi) →
eval ρ (phi^[evar: dbi ↦ patt_free_evar y])
= @eval M (update_evar_val x (evar_valuation ρ y) ρ) (phi^{evar: dbi ↦ x}).
(* eval unchanged within subformula over fresh element variable *)
Lemma eval_fresh_evar_subterm ϕ₁ ϕ₂ c dbi ρ :
is_subformula_of_ind ϕ₁ ϕ₂ →
@eval M (update_evar_val (fresh_evar ϕ₂) c ρ) (ϕ₁^{evar: dbi ↦ (fresh_evar ϕ₂)})
= eval (update_evar_val (fresh_evar ϕ₁) c ρ) (ϕ₁^{evar: dbi ↦ (fresh_evar ϕ₁)}).
(* model predicate of evar_open is maintained with change of variables *)
Lemma M_predicate_evar_open_fresh_evar_1 x₁ x₂ ϕ :
evar_is_fresh_in x₁ ϕ →
evar_is_fresh_in x₂ ϕ →
M_predicate M (ϕ^{evar: 0 ↦ x₁}) →
M_predicate M (ϕ^{evar: 0 ↦ x₂}).
Lemma M_predicate_evar_open_fresh_evar_2 x ϕ :
evar_is_fresh_in x ϕ →
M_predicate M (ϕ^{evar: 0 ↦ (fresh_evar ϕ)}) →
M_predicate M (ϕ^{evar: 0 ↦ x}).
(* Similar to plugging_patterns: using free svar substitution instead of
bound svar substitution.
TODO: we may be able to gneeralize this lemma to non-closed psi,
if we deal with nest_mu properly
*)
Lemma Private_free_svar_subst_update_exchange :
∀ sz phi psi X ρ,
le (pat_size phi) sz → well_formed psi → well_formed_closed phi →
eval ρ (phi^[[svar: X ↦ psi]]) =
eval (@update_svar_val M X (eval ρ psi) ρ) phi.
Lemma free_svar_subst_update_exchange: ∀ phi psi X ρ,
well_formed psi → well_formed_closed phi →
eval ρ (phi^[[svar: X ↦ psi]]) =
eval (@update_svar_val M X (eval ρ psi) ρ) phi.
(* rho(psi) = empty then Crho(psi) = empty *)
Lemma propagate_context_empty psi ρ C :
@eval M ρ psi = ∅ →
eval ρ (subst_ctx C psi) = ∅.
(* application to a singleton *)
Definition rel_of ρ ϕ: Domain M → propset (Domain M) :=
λ m₁,
(app_ext (@eval M ρ ϕ) {[ m₁ ]}).
Definition is_total_function f (d c : propset (Domain M)) ρ :=
∀ (m₁ : Domain M),
m₁ ∈ d →
∃ (m₂ : Domain M),
m₂ ∈ c ∧
app_ext (@eval M ρ f) {[ m₁ ]}
= {[ m₂ ]}.
Definition total_function_is_injective f (d : propset (Domain M)) ρ :=
∀ (m₁ : Domain M),
m₁ ∈ d →
∀ (m₂ : Domain M),
m₂ ∈ d →
(rel_of ρ f) m₁ = (rel_of ρ f) m₂ →
m₁ = m₂.
Definition is_functional_pattern ϕ ρ :=
∃ (m : Domain M), @eval M ρ ϕ = {[ m ]}.
Lemma functional_pattern_inj ϕ ρ m₁ m₂ :
is_functional_pattern ϕ ρ →
m₁ ∈ @eval M ρ ϕ →
m₂ ∈ @eval M ρ ϕ →
m₁ = m₂.
End with_model.
End semantics.
Module Notations.
Notation "M ⊨ᴹ phi" := (satisfies_model M phi) (left associativity, at level 50) : ml_scope.
(* FIXME this should not be called `satisfies` *)
Notation "G ⊨ phi" := (satisfies G phi) (left associativity, at level 50) : ml_scope.
Notation "M ⊨ᵀ Gamma" := (satisfies_theory M Gamma)
(left associativity, at level 50) : ml_scope.
End Notations.
(*Module Hints.*)
#[export]
Hint Resolve M_predicate_impl : core.
#[export]
Hint Resolve M_predicate_bott : core.
#[export]
Hint Resolve M_predicate_exists : core.
#[export]
Hint Extern 4 (M_predicate _ (evar_open _ _ _)) ⇒ mlSimpl : core.
#[export]
Hint Extern 4 (T_predicate _ (evar_open _ _ _)) ⇒ mlSimpl : core.
#[export]
Hint Extern 4 (M_predicate _ (svar_open _ _ _)) ⇒ mlSimpl : core.
#[export]
Hint Extern 4 (T_predicate _ (svar_open _ _ _)) ⇒ mlSimpl : core.
#[export]
Hint Resolve T_predicate_impl_M_predicate : core.
#[export]
Hint Resolve T_predicate_impl : core.
#[export]
Hint Resolve T_predicate_bot : core.
(*End Hints.*)
Global Instance app_ext_proper {Σ : Signature} (M : Model)
: Proper ((≡) ==> (≡) ==> (≡)) (@app_ext Σ M).
Context {signature : Signature}.
Open Scope ml_scope.
(* Model of AML ref. snapshot: Definition 2 *)
Section with_model.
Context {M : Model}.
Definition Empty : propset (Domain M) := @empty (propset (Domain M)) _.
Definition Full : propset (Domain M) := @top (propset (Domain M)) _.
(* full set and empty set are distinct *)
Lemma empty_impl_not_full : ∀ (S : propset (Domain M)),
S = Empty → S ≠ Full.
Lemma full_impl_not_empty : ∀ (S : propset (Domain M)),
S = Full → S ≠ Empty.
(* element and set variable valuations *)
Polymorphic Record Valuation : Type := mkValuation
{ evar_valuation : evar → Domain M ;
svar_valuation : svar → propset (Domain M) ;
}.
Definition update_evar_val
(ev : evar) (x : Domain M) (val : Valuation) : Valuation :=
{|
evar_valuation := fun ev' : evar ⇒
if decide (ev = ev') is left _ then x else evar_valuation val ev' ;
svar_valuation := (svar_valuation val)
|}.
Definition update_svar_val
(sv : svar) (X : propset (Domain M)) (val : Valuation) : Valuation :=
{|
evar_valuation := (evar_valuation val);
svar_valuation := fun sv' : svar ⇒
if decide (sv = sv') is left _ then X else svar_valuation val sv' ;
|}.
Lemma update_evar_val_svar_val_comm
(ev : evar) (x : Domain M)
(sv : svar) (X : propset (Domain M))
(ρ : Valuation) :
update_evar_val ev x (update_svar_val sv X ρ)
= update_svar_val sv X (update_evar_val ev x ρ).
Lemma update_svar_val_comm :
∀ (X1 X2 : svar) (S1 S2 : propset (Domain M)) (ρ : Valuation),
X1 ≠ X2 →
update_svar_val X1 S1 (update_svar_val X2 S2 ρ)
= update_svar_val X2 S2 (update_svar_val X1 S1 ρ).
Lemma update_svar_val_shadow : ∀ (X : svar)
(S1 S2 : propset (Domain M))
(ρ : Valuation),
update_svar_val X S1 (update_svar_val X S2 ρ) = update_svar_val X S1 ρ.
Lemma update_svar_val_neq (ρ : Valuation) X1 S X2 :
X1 ≠ X2 → svar_valuation (update_svar_val X1 S ρ) X2 = svar_valuation ρ X2.
Lemma update_evar_val_comm :
∀ (x1 x2 : evar) (m1 m2 : Domain M) (ρ : Valuation),
x1 ≠ x2 →
update_evar_val x1 m1 (update_evar_val x2 m2 ρ)
= update_evar_val x2 m2 (update_evar_val x1 m1 ρ).
Lemma update_evar_val_shadow : ∀ (x : evar)
(m1 m2 : Domain M)
(ρ : Valuation),
update_evar_val x m1 (update_evar_val x m2 ρ) = update_evar_val x m1 ρ.
Lemma update_evar_val_same x m ρ :
evar_valuation (update_evar_val x m ρ) x = m.
Lemma update_evar_val_neq (ρ : Valuation) x1 e x2 :
x1 ≠ x2 → evar_valuation (update_evar_val x1 e ρ) x2 = evar_valuation ρ x2.
Lemma update_evar_val_same_2 x ρ :
update_evar_val x (evar_valuation ρ x) ρ = ρ.
Lemma update_svar_val_same X S ρ :
svar_valuation (update_svar_val X S ρ) X = S.
Lemma update_svar_val_same_2 x ρ :
update_svar_val x (svar_valuation ρ x) ρ = ρ.
(* We use propositional extensionality here. *)
#[export]
Instance propset_leibniz_equiv : LeibnizEquiv (propset (Domain M)).
(* extending pointwise application *)
Lemma app_ext_bot_r :
∀ S : propset (Domain M),
app_ext S ∅ = ∅.
Theorem app_ext_singleton : ∀ (x y : M),
app_ext {[x]} {[y]} = app_interp _ x y.
Lemma app_ext_bot_l :
∀ S : propset (Domain M),
app_ext ∅ S = ∅.
Lemma app_ext_monotonic_l :
∀ (S1 S2 S : propset (Domain M)),
S1 ⊆ S2 → (app_ext S1 S) ⊆ (app_ext S2 S).
Lemma app_ext_monotonic_r :
∀ (S S1 S2 : propset (Domain M)),
S1 ⊆ S2 → (app_ext S S1) ⊆ (app_ext S S2).
(* Semantics of AML ref. snapshot: Definition 3 *)
Let OS := PropsetOrderedSet (Domain M).
Let L := PowersetLattice (Domain M).
Equations? eval (ρ : Valuation) (ϕ : Pattern)
: propset (@Domain M) by wf (pat_size ϕ) :=
eval ρ (patt_free_evar x) := {[ evar_valuation ρ x ]} ;
eval ρ (patt_free_svar X) := svar_valuation ρ X ;
eval ρ (patt_bound_evar n) := ∅ ;
eval ρ (patt_bound_svar n) := ∅ ;
eval ρ (patt_sym s) := @sym_interp M s ;
eval ρ (patt_app ϕ₁ ϕ₂) := app_ext (eval ρ ϕ₁) (eval ρ ϕ₂) ;
eval ρ (patt_bott) := ∅ ;
eval ρ (patt_imp ϕ₁ ϕ₂) := (difference ⊤ (eval ρ ϕ₁)) ∪ (eval ρ ϕ₂) ;
eval ρ (patt_exists ϕ') := let x := fresh_evar ϕ' in
propset_fa_union
(fun e ⇒
let ρ' := (update_evar_val x e ρ) in
eval ρ' (ϕ'^{evar: 0 ↦ x})
) ;
eval ρ (patt_mu ϕ') := let X := fresh_svar ϕ' in
@LeastFixpointOf _ OS L
(fun S ⇒
let ρ' := (update_svar_val X S ρ) in
eval ρ' (ϕ'^{svar: 0 ↦ X})
) .
Definition Fassoc ρ ϕ X :=
λ S, eval (update_svar_val X S ρ) ϕ.
Lemma eval_free_evar_simpl
(ρ : Valuation)
(x : evar) :
eval ρ (patt_free_evar x) = {[ evar_valuation ρ x ]}.
Lemma eval_free_svar_simpl
(ρ : Valuation)
(X : svar) :
eval ρ (patt_free_svar X) = svar_valuation ρ X.
Lemma eval_bound_evar_simpl
(ρ : Valuation)
(x : db_index) :
eval ρ (patt_bound_evar x) = ∅.
Lemma eval_bound_svar_simpl
(ρ : Valuation)
(X : db_index) :
eval ρ (patt_bound_svar X) = ∅.
Lemma eval_sym_simpl
(ρ : Valuation)
(s : symbols) :
eval ρ (patt_sym s) = @sym_interp M s.
Lemma eval_app_simpl
(ρ : Valuation)
(ϕ₁ ϕ₂ : Pattern) :
eval ρ (patt_app ϕ₁ ϕ₂) = app_ext (eval ρ ϕ₁) (eval ρ ϕ₂).
Lemma eval_bott_simpl
(ρ : Valuation) :
eval ρ patt_bott = ∅.
Lemma eval_imp_simpl
(ρ : Valuation)
(ϕ₁ ϕ₂ : Pattern) :
eval ρ (patt_imp ϕ₁ ϕ₂) = (difference ⊤ (eval ρ ϕ₁)) ∪ (eval ρ ϕ₂).
Lemma eval_ex_simpl
(ρ : Valuation)
(ϕ' : Pattern) :
eval ρ (patt_exists ϕ') =
let x := fresh_evar ϕ' in
propset_fa_union
(fun e ⇒
let ρ' := (update_evar_val x e ρ) in
eval ρ' (ϕ'^{evar: 0 ↦ x})
).
Lemma eval_mu_simpl
(ρ : Valuation)
(ϕ' : Pattern) :
eval ρ (patt_mu ϕ') =
let X := fresh_svar ϕ' in
@LeastFixpointOf _ OS L
(fun S ⇒
let ρ' := (update_svar_val X S ρ) in
eval ρ' (ϕ'^{svar: 0 ↦ X})
).
(* TODO extend with derived constructs using typeclasses *)
Definition eval_simpl :=
( eval_free_evar_simpl,
eval_free_svar_simpl,
eval_bound_evar_simpl,
eval_bound_svar_simpl,
eval_sym_simpl,
eval_app_simpl,
eval_bott_simpl,
eval_imp_simpl,
eval_ex_simpl,
eval_mu_simpl
).
End with_model.
Section with_explicit_model.
Context (M : Model).
(* Model predicate. Useful mainly if the pattern is well-formed. *)
Definition M_predicate (ϕ : Pattern) : Prop := ∀ ρ,
@eval M ρ ϕ = ⊤ ∨ eval ρ ϕ = ∅.
Lemma M_predicate_impl ϕ₁ ϕ₂ : M_predicate ϕ₁ → M_predicate ϕ₂ → M_predicate (patt_imp ϕ₁ ϕ₂).
Hint Resolve M_predicate_impl : core.
Lemma M_predicate_bott : M_predicate patt_bott.
Hint Resolve M_predicate_bott : core.
Lemma M_predicate_exists ϕ :
let x := evar_fresh (elements (free_evars ϕ)) in
M_predicate (ϕ^{evar: 0 ↦ x}) → M_predicate (patt_exists ϕ).
Hint Resolve M_predicate_exists : core.
Lemma predicate_not_empty_iff_full ϕ ρ :
M_predicate ϕ →
@eval M ρ ϕ ≠ ∅ ↔
eval ρ ϕ = ⊤.
Lemma predicate_not_full_iff_empty ϕ ρ :
M_predicate ϕ →
@eval M ρ ϕ ≠ ⊤ ↔
eval ρ ϕ = ∅.
Lemma eval_impl_MP ϕ₁ ϕ₂ ρ :
@eval M ρ (patt_imp ϕ₁ ϕ₂) = ⊤ →
eval ρ ϕ₁ = ⊤ →
eval ρ ϕ₂ = ⊤.
Lemma eval_predicate_impl ϕ₁ ϕ₂ ρ :
M_predicate ϕ₁ →
@eval M ρ (patt_imp ϕ₁ ϕ₂) = ⊤
↔ (eval ρ ϕ₁ = ⊤
→ eval ρ ϕ₂ = ⊤).
(* ϕ is a well-formed body of ex *)
Lemma eval_exists_predicate_full ϕ ρ :
let x := fresh_evar ϕ in
M_predicate (ϕ^{evar: 0 ↦ x}) →
eval ρ (patt_exists ϕ) = ⊤ ↔
∃ (m : Domain M), eval (update_evar_val x m ρ) (ϕ^{evar: 0 ↦ x}) = ⊤.
Lemma eval_exists_empty ϕ ρ :
let x := fresh_evar ϕ in
eval ρ (patt_exists ϕ) = ∅ ↔
∀ (m : Domain M), eval (update_evar_val x m ρ) (ϕ^{evar: 0 ↦ x}) = ∅.
(* Theory,axiom ref. snapshot: Definition 5 *)
End with_explicit_model.
Definition satisfies_model (M : Model) (ϕ : Pattern) : Prop :=
∀ (ρ : Valuation),
eval (M := M) ρ ϕ = ⊤.
Definition satisfies_theory (m : Model) (theory : Theory)
: Prop := ∀ axiom : Pattern, axiom ∈ theory → (satisfies_model m axiom).
(* TODO rename *)
Definition satisfies (theory : Theory) (p: Pattern)
: Prop := ∀ m : Model, (satisfies_theory m theory) → (satisfies_model m p).
Lemma satisfies_theory_iff_satisfies_named_axioms {Σ : Signature} NAs M:
satisfies_theory M (theory_of_NamedAxioms NAs) ↔
∀ (n : NAName NAs), satisfies_model M (NAAxiom _ n).
Lemma satisfies_theory_subseteq M Γ₁ Γ₂:
Γ₁ ⊆ Γ₂ →
satisfies_theory M Γ₂ →
satisfies_theory M Γ₁.
(* theory predicate *)
Definition T_predicate Γ ϕ := ∀ M, satisfies_theory M Γ → M_predicate M ϕ.
Hint Extern 4 (M_predicate _ (evar_open _ _ _)) ⇒ mlSimpl : core.
Hint Extern 4 (T_predicate _ (evar_open _ _ _)) ⇒ mlSimpl : core.
Hint Extern 4 (M_predicate _ (svar_open _ _ _)) ⇒ mlSimpl : core.
Hint Extern 4 (T_predicate _ (svar_open _ _ _)) ⇒ mlSimpl : core.
Lemma T_predicate_impl_M_predicate M Γ ϕ:
satisfies_theory M Γ → T_predicate Γ ϕ → M_predicate M ϕ.
Hint Resolve T_predicate_impl_M_predicate : core.
Lemma T_predicate_impl Γ ϕ₁ ϕ₂ : T_predicate Γ ϕ₁ → T_predicate Γ ϕ₂ → T_predicate Γ (patt_imp ϕ₁ ϕ₂).
Hint Resolve T_predicate_impl : core.
Lemma T_predicate_bot Γ : T_predicate Γ patt_bott.
Hint Resolve T_predicate_bot : core.
(* TODO: top iff exists forall *)
Section with_model.
Context {M : Model}.
(* If phi1 \subseteq phi2, then U_x phi1 \subseteq U_x phi2 *)
Lemma eval_subset_union x ϕ₁ ϕ₂ :
(∀ ρ, (eval ρ ϕ₁) ⊆ (@eval M ρ ϕ₂) )
→ (∀ ρ,
(propset_fa_union (fun e ⇒ eval (update_evar_val x e ρ) ϕ₁))
⊆
(propset_fa_union (fun e ⇒ @eval M (update_evar_val x e ρ) ϕ₂))
).
(* eval unchanged when using fresh element varaiable *)
Lemma eval_free_evar_independent ρ x v ϕ:
evar_is_fresh_in x ϕ →
@eval M (update_evar_val x v ρ) ϕ = eval ρ ϕ.
Lemma eval_free_svar_independent ρ X S ϕ:
svar_is_fresh_in X ϕ →
@eval M (update_svar_val X S ρ) ϕ = eval ρ ϕ.
Lemma Private_eval_fresh_var_open sz ϕ dbi ρ:
pat_size ϕ ≤ sz →
(
∀ X Y S,
svar_is_fresh_in X ϕ →
svar_is_fresh_in Y ϕ →
eval (update_svar_val X S ρ) (ϕ^{svar: dbi ↦ X})
= @eval M (update_svar_val Y S ρ) (ϕ^{svar: dbi ↦ Y})
) ∧
(
∀ x y c,
evar_is_fresh_in x ϕ →
evar_is_fresh_in y ϕ →
@eval M (update_evar_val x c ρ) (ϕ^{evar: dbi ↦ x})
= eval (update_evar_val y c ρ) (ϕ^{evar: dbi ↦ y})
)
.
Lemma eval_fresh_evar_open ϕ x y c dbi ρ:
evar_is_fresh_in x ϕ →
evar_is_fresh_in y ϕ →
@eval M (update_evar_val x c ρ) (ϕ^{evar: dbi ↦ x})
= eval (update_evar_val y c ρ) (ϕ^{evar: dbi ↦ y}).
Lemma eval_fresh_svar_open ϕ X Y S dbi ρ:
svar_is_fresh_in X ϕ →
svar_is_fresh_in Y ϕ →
@eval M (update_svar_val X S ρ) (ϕ^{svar: dbi ↦ X})
= eval (update_svar_val Y S ρ) (ϕ^{svar: dbi ↦ Y}).
(* There are two ways how to plug a pattern phi2 into a pattern phi1:
either substitute it for some variable,
or evaluate phi2 first and then evaluate phi1 with valuation updated to the result of phi2
*)
Lemma Private_plugging_patterns : ∀ (sz : nat) (dbi : db_index) (phi1 phi2 : Pattern),
pat_size phi1 ≤ sz → ∀ (ρ : Valuation) (X : svar),
well_formed_closed phi2 → well_formed_closed_mu_aux phi1 (S dbi) →
¬ elem_of X (free_svars phi1) →
@eval M ρ (phi1^[svar:dbi ↦ phi2])
= eval (update_svar_val X (@eval M ρ phi2) ρ)
(phi1^{svar: dbi ↦ X}).
Lemma set_substitution_lemma : ∀ (dbi : db_index) (phi1 phi2 : Pattern),
∀ (ρ : Valuation) (X : svar),
well_formed_closed phi2 → well_formed_closed_mu_aux phi1 (S dbi) →
¬ elem_of X (free_svars phi1) →
@eval M ρ (phi1^[svar: dbi ↦ phi2])
= eval (update_svar_val X (@eval M ρ phi2) ρ) (phi1^{svar: dbi ↦ X}).
Lemma Private_plugging_patterns_bevar_subst : ∀ (sz : nat) (dbi : db_index)
(phi : Pattern) (y : evar),
pat_size phi ≤ sz → ∀ (ρ : Valuation) (x : evar),
evar_is_fresh_in x phi → well_formed_closed_ex_aux phi (S dbi) →
@eval M ρ (phi^[evar: dbi ↦ patt_free_evar y])
= eval (update_evar_val x (evar_valuation ρ y) ρ) (phi^{evar: dbi ↦ x}).
Lemma element_substitution_lemma
(phi : Pattern) (x y : evar) (ρ : Valuation) (dbi : db_index) :
evar_is_fresh_in x phi → well_formed_closed_ex_aux phi (S dbi) →
eval ρ (phi^[evar: dbi ↦ patt_free_evar y])
= @eval M (update_evar_val x (evar_valuation ρ y) ρ) (phi^{evar: dbi ↦ x}).
(* eval unchanged within subformula over fresh element variable *)
Lemma eval_fresh_evar_subterm ϕ₁ ϕ₂ c dbi ρ :
is_subformula_of_ind ϕ₁ ϕ₂ →
@eval M (update_evar_val (fresh_evar ϕ₂) c ρ) (ϕ₁^{evar: dbi ↦ (fresh_evar ϕ₂)})
= eval (update_evar_val (fresh_evar ϕ₁) c ρ) (ϕ₁^{evar: dbi ↦ (fresh_evar ϕ₁)}).
(* model predicate of evar_open is maintained with change of variables *)
Lemma M_predicate_evar_open_fresh_evar_1 x₁ x₂ ϕ :
evar_is_fresh_in x₁ ϕ →
evar_is_fresh_in x₂ ϕ →
M_predicate M (ϕ^{evar: 0 ↦ x₁}) →
M_predicate M (ϕ^{evar: 0 ↦ x₂}).
Lemma M_predicate_evar_open_fresh_evar_2 x ϕ :
evar_is_fresh_in x ϕ →
M_predicate M (ϕ^{evar: 0 ↦ (fresh_evar ϕ)}) →
M_predicate M (ϕ^{evar: 0 ↦ x}).
(* Similar to plugging_patterns: using free svar substitution instead of
bound svar substitution.
TODO: we may be able to gneeralize this lemma to non-closed psi,
if we deal with nest_mu properly
*)
Lemma Private_free_svar_subst_update_exchange :
∀ sz phi psi X ρ,
le (pat_size phi) sz → well_formed psi → well_formed_closed phi →
eval ρ (phi^[[svar: X ↦ psi]]) =
eval (@update_svar_val M X (eval ρ psi) ρ) phi.
Lemma free_svar_subst_update_exchange: ∀ phi psi X ρ,
well_formed psi → well_formed_closed phi →
eval ρ (phi^[[svar: X ↦ psi]]) =
eval (@update_svar_val M X (eval ρ psi) ρ) phi.
(* rho(psi) = empty then Crho(psi) = empty *)
Lemma propagate_context_empty psi ρ C :
@eval M ρ psi = ∅ →
eval ρ (subst_ctx C psi) = ∅.
(* application to a singleton *)
Definition rel_of ρ ϕ: Domain M → propset (Domain M) :=
λ m₁,
(app_ext (@eval M ρ ϕ) {[ m₁ ]}).
Definition is_total_function f (d c : propset (Domain M)) ρ :=
∀ (m₁ : Domain M),
m₁ ∈ d →
∃ (m₂ : Domain M),
m₂ ∈ c ∧
app_ext (@eval M ρ f) {[ m₁ ]}
= {[ m₂ ]}.
Definition total_function_is_injective f (d : propset (Domain M)) ρ :=
∀ (m₁ : Domain M),
m₁ ∈ d →
∀ (m₂ : Domain M),
m₂ ∈ d →
(rel_of ρ f) m₁ = (rel_of ρ f) m₂ →
m₁ = m₂.
Definition is_functional_pattern ϕ ρ :=
∃ (m : Domain M), @eval M ρ ϕ = {[ m ]}.
Lemma functional_pattern_inj ϕ ρ m₁ m₂ :
is_functional_pattern ϕ ρ →
m₁ ∈ @eval M ρ ϕ →
m₂ ∈ @eval M ρ ϕ →
m₁ = m₂.
End with_model.
End semantics.
Module Notations.
Notation "M ⊨ᴹ phi" := (satisfies_model M phi) (left associativity, at level 50) : ml_scope.
(* FIXME this should not be called `satisfies` *)
Notation "G ⊨ phi" := (satisfies G phi) (left associativity, at level 50) : ml_scope.
Notation "M ⊨ᵀ Gamma" := (satisfies_theory M Gamma)
(left associativity, at level 50) : ml_scope.
End Notations.
(*Module Hints.*)
#[export]
Hint Resolve M_predicate_impl : core.
#[export]
Hint Resolve M_predicate_bott : core.
#[export]
Hint Resolve M_predicate_exists : core.
#[export]
Hint Extern 4 (M_predicate _ (evar_open _ _ _)) ⇒ mlSimpl : core.
#[export]
Hint Extern 4 (T_predicate _ (evar_open _ _ _)) ⇒ mlSimpl : core.
#[export]
Hint Extern 4 (M_predicate _ (svar_open _ _ _)) ⇒ mlSimpl : core.
#[export]
Hint Extern 4 (T_predicate _ (svar_open _ _ _)) ⇒ mlSimpl : core.
#[export]
Hint Resolve T_predicate_impl_M_predicate : core.
#[export]
Hint Resolve T_predicate_impl : core.
#[export]
Hint Resolve T_predicate_bot : core.
(*End Hints.*)
Global Instance app_ext_proper {Σ : Signature} (M : Model)
: Proper ((≡) ==> (≡) ==> (≡)) (@app_ext Σ M).
This page has been generated by coqdoc