File FreshnessSubstitution
From MatchingLogic Require Export Substitution
Freshness.
Import Substitution.Notations.
Section lemmas.
Context {Σ : Signature}.
Open Scope ml_scope.
Lemma evar_is_fresh_in_free_evar_subst x phi psi:
evar_is_fresh_in x psi →
evar_is_fresh_in x (phi^[[evar: x ↦ psi]]).
Lemma evar_is_fresh_in_evar_quantify x n phi:
evar_is_fresh_in x (phi^{{evar: x ↦ n}}).
Lemma svar_is_fresh_in_free_evar_subst X phi psi:
svar_is_fresh_in X psi →
svar_is_fresh_in X (phi^[[svar: X ↦ psi]]).
Lemma svar_is_fresh_in_svar_quantify X n phi:
svar_is_fresh_in X (phi^{{svar: X ↦ n}}).
(*If phi is a closed body, then (ex, phi) is closed too*)
Corollary wfc_body_to_wfc_ex phi:
wfc_body_ex phi →
well_formed_closed (patt_exists phi) = true.
(* Lemmas about wfc_ex and wfc_mu *)
(* From https://www.chargueraud.org/research/2009/ln/main.pdf in 3.4 (lc_abs_iff_body) *)
(*Conclusion*)
Corollary wfc_body_wfc_ex_iff:
∀ phi,
well_formed_closed (patt_exists phi) = true ↔ wfc_body_ex phi.
(* TODO make a wrapper that does not have the 'sz' variable *)
Lemma bevar_subst_fresh_notin:
∀ phi psi v,
v ∉ (free_evars phi) →
v ∉ (free_evars psi) →
∀ n,
v ∉ (free_evars (phi^[evar: n ↦ psi])).
Lemma bsvar_subst_fresh_notin:
∀ phi psi v,
v ∉ (free_svars phi) →
v ∉ (free_svars psi) →
∀ n,
v ∉ (free_svars (phi^[svar: n ↦ psi])).
Corollary evar_open_fresh_notin:
∀ phi v w,
v ∉ (free_evars phi) →
w ∉ (free_evars phi) →
(v ≠ w) →
∀ n,
v ∉ (free_evars (phi^{evar: n ↦ w})).
Corollary svar_open_fresh_notin:
∀ phi v w,
v ∉ (free_svars phi) →
w ∉ (free_svars phi) →
(v ≠ w) →
∀ n,
v ∉ (free_svars (phi^{svar: n ↦ w})).
Lemma free_evars_svar_open : ∀ (psi : Pattern) (dbi :db_index) (X : svar),
free_evars (psi^{svar: dbi ↦ X}) = free_evars psi.
Lemma fresh_evar_svar_open dbi X phi :
fresh_evar (phi^{svar: dbi ↦ X}) = fresh_evar phi.
Lemma fresh_svar_evar_open dbi x phi :
fresh_svar (phi^{evar: dbi ↦ x}) = fresh_svar phi.
Corollary svar_is_fresh_in_svar_open X Y dbi ϕ:
X ≠ Y →
svar_is_fresh_in X ϕ →
svar_is_fresh_in X (ϕ^{svar: dbi ↦ Y}).
Corollary evar_is_fresh_in_evar_open x y dbi ϕ:
x ≠ y →
evar_is_fresh_in x ϕ →
evar_is_fresh_in x (ϕ^{evar: dbi ↦ y}).
Corollary evar_fresh_svar_open x X dbi ϕ:
evar_is_fresh_in x ϕ →
evar_is_fresh_in x (ϕ^{svar: dbi ↦ X}).
Corollary svar_fresh_evar_open x X dbi ϕ:
svar_is_fresh_in X ϕ →
svar_is_fresh_in X (ϕ^{evar: dbi ↦ x}).
Lemma evar_open_inj : ∀ phi psi x n,
evar_is_fresh_in x phi → evar_is_fresh_in x psi →
phi^{evar: n ↦ x} = psi^{evar: n ↦ x}
→ phi = psi.
Lemma svar_open_inj : ∀ phi psi X n,
svar_is_fresh_in X phi → svar_is_fresh_in X psi →
phi^{svar: n ↦ X} = psi^{svar: n ↦ X}
→ phi = psi.
Lemma evar_open_free_svar_subst_comm: ∀ phi psi fresh n X,
(well_formed_closed_ex_aux psi 0) →
evar_is_fresh_in fresh phi →
evar_is_fresh_in fresh (phi^[[svar: X ↦ psi]])
→
(phi^[[svar: X ↦ psi]])^{evar: n ↦ fresh} = (phi^{evar: n ↦ fresh})^[[svar:X ↦ psi]].
Lemma svar_open_free_svar_subst_comm : ∀ phi psi fresh n X,
(well_formed_closed_mu_aux psi 0) →
svar_is_fresh_in fresh phi → svar_is_fresh_in fresh (phi^[[svar: X ↦ psi]]) → (fresh ≠ X)
→
phi^[[svar: X ↦ psi]]^{svar: n ↦ fresh} = phi^{svar: n ↦ fresh}^[[svar: X ↦ psi]].
Lemma free_evar_subst_preserves_no_negative_occurrence x p q n:
well_formed_closed_mu_aux q 0 = true →
no_negative_occurrence_db_b n p = true →
no_negative_occurrence_db_b n (p^[[evar: x ↦ q]]) = true
with
free_evar_subst_preserves_no_positive_occurrence x p q n:
well_formed_closed_mu_aux q 0 = true →
no_positive_occurrence_db_b n p = true →
no_positive_occurrence_db_b n (p^[[evar: x ↦ q]]) = true
.
Lemma Private_well_formed_free_evar_subst x p q n1 n2:
well_formed q →
well_formed_positive p && well_formed_closed_mu_aux p n2 && well_formed_closed_ex_aux p n1 →
no_negative_occurrence_db_b n2 (p^[[evar: x ↦ q]])
&& no_positive_occurrence_db_b n2 (p^[[evar: x ↦ q]])
&& well_formed_positive (p^[[evar: x ↦ q]])
&& well_formed_closed_mu_aux (p^[[evar: x ↦ q]]) n2
&& well_formed_closed_ex_aux (p^[[evar: x ↦ q]]) n1
= true.
Lemma well_formed_free_evar_subst x p q:
well_formed q = true →
well_formed p = true →
well_formed (p^[[evar: x ↦ q]]) = true.
Lemma well_formed_xy_free_evar_subst x m n p q:
well_formed q = true →
well_formed_xy m n p = true →
well_formed_xy m n (p^[[evar: x ↦ q]]) = true.
Lemma well_formed_free_evar_subst_0 x p q:
well_formed q = true →
well_formed p = true →
well_formed (p^[[evar: x ↦ q]]) = true.
Lemma evar_quantify_fresh x n phi:
evar_is_fresh_in x phi →
phi^{{evar: x ↦ n}} = phi.
Lemma svar_quantify_fresh X n phi:
svar_is_fresh_in X phi →
phi^{{svar: X ↦ n}} = phi.
Lemma svar_hno_bsvar_subst X ϕ ψ dbi:
(svar_has_negative_occurrence X ψ = true → no_positive_occurrence_db_b dbi ϕ = true) →
(svar_has_positive_occurrence X ψ = true → no_negative_occurrence_db_b dbi ϕ = true) →
svar_has_negative_occurrence X ϕ = false →
svar_has_negative_occurrence X (ϕ^[svar: dbi ↦ ψ]) = false
with svar_hpo_bsvar_subst X ϕ ψ dbi:
(svar_has_negative_occurrence X ψ = true → no_negative_occurrence_db_b dbi ϕ = true) →
(svar_has_positive_occurrence X ψ = true → no_positive_occurrence_db_b dbi ϕ = true) →
svar_has_positive_occurrence X ϕ = false →
svar_has_positive_occurrence X (ϕ^[svar: dbi ↦ ψ]) = false.
Lemma svar_hno_false_if_fresh X ϕ:
svar_is_fresh_in X ϕ →
svar_has_negative_occurrence X ϕ = false
with svar_hpo_false_if_fresh X ϕ:
svar_is_fresh_in X ϕ →
svar_has_positive_occurrence X ϕ = false.
(* TODO remove the no-negative-ocurrence assumption from the svar version *)
Lemma wfp_free_evar_subst ϕ ψ x:
well_formed_closed_mu_aux ψ 0 →
well_formed_positive ψ = true →
well_formed_positive ϕ = true →
well_formed_positive (ϕ^[[evar: x ↦ ψ]]) = true
with wfp_neg_free_evar_subst ϕ ψ x:
well_formed_closed_mu_aux ψ 0 →
well_formed_positive ψ = true →
well_formed_positive ϕ = true →
well_formed_positive (ϕ^[[evar: x ↦ ψ]]) = true.
Lemma neg_occurrence_bevar_subst x ϕ y n :
x ≠ y →
evar_has_negative_occurrence x ϕ =
evar_has_negative_occurrence x ϕ^{evar:n↦y}
with
pos_occurrence_bevar_subst x ϕ y n :
x ≠ y →
evar_has_positive_occurrence x ϕ =
evar_has_positive_occurrence x ϕ^{evar:n↦y}.
Lemma neg_occurrence_bsvar_subst x ϕ X n :
evar_has_negative_occurrence x ϕ =
evar_has_negative_occurrence x ϕ^{svar:n↦X}
with
pos_occurrence_bsvar_subst x ϕ X n :
evar_has_positive_occurrence x ϕ =
evar_has_positive_occurrence x ϕ^{svar:n↦X}.
Lemma fresh_svar_no_neg X ϕ :
svar_is_fresh_in X ϕ →
svar_has_negative_occurrence X ϕ = false
with
fresh_svar_no_pos X ϕ :
svar_is_fresh_in X ϕ →
svar_has_positive_occurrence X ϕ = false.
End lemmas.
#[export]
Hint Resolve wfp_free_evar_subst : core.
Freshness.
Import Substitution.Notations.
Section lemmas.
Context {Σ : Signature}.
Open Scope ml_scope.
Lemma evar_is_fresh_in_free_evar_subst x phi psi:
evar_is_fresh_in x psi →
evar_is_fresh_in x (phi^[[evar: x ↦ psi]]).
Lemma evar_is_fresh_in_evar_quantify x n phi:
evar_is_fresh_in x (phi^{{evar: x ↦ n}}).
Lemma svar_is_fresh_in_free_evar_subst X phi psi:
svar_is_fresh_in X psi →
svar_is_fresh_in X (phi^[[svar: X ↦ psi]]).
Lemma svar_is_fresh_in_svar_quantify X n phi:
svar_is_fresh_in X (phi^{{svar: X ↦ n}}).
(*If phi is a closed body, then (ex, phi) is closed too*)
Corollary wfc_body_to_wfc_ex phi:
wfc_body_ex phi →
well_formed_closed (patt_exists phi) = true.
(* Lemmas about wfc_ex and wfc_mu *)
(* From https://www.chargueraud.org/research/2009/ln/main.pdf in 3.4 (lc_abs_iff_body) *)
(*Conclusion*)
Corollary wfc_body_wfc_ex_iff:
∀ phi,
well_formed_closed (patt_exists phi) = true ↔ wfc_body_ex phi.
(* TODO make a wrapper that does not have the 'sz' variable *)
Lemma bevar_subst_fresh_notin:
∀ phi psi v,
v ∉ (free_evars phi) →
v ∉ (free_evars psi) →
∀ n,
v ∉ (free_evars (phi^[evar: n ↦ psi])).
Lemma bsvar_subst_fresh_notin:
∀ phi psi v,
v ∉ (free_svars phi) →
v ∉ (free_svars psi) →
∀ n,
v ∉ (free_svars (phi^[svar: n ↦ psi])).
Corollary evar_open_fresh_notin:
∀ phi v w,
v ∉ (free_evars phi) →
w ∉ (free_evars phi) →
(v ≠ w) →
∀ n,
v ∉ (free_evars (phi^{evar: n ↦ w})).
Corollary svar_open_fresh_notin:
∀ phi v w,
v ∉ (free_svars phi) →
w ∉ (free_svars phi) →
(v ≠ w) →
∀ n,
v ∉ (free_svars (phi^{svar: n ↦ w})).
Lemma free_evars_svar_open : ∀ (psi : Pattern) (dbi :db_index) (X : svar),
free_evars (psi^{svar: dbi ↦ X}) = free_evars psi.
Lemma fresh_evar_svar_open dbi X phi :
fresh_evar (phi^{svar: dbi ↦ X}) = fresh_evar phi.
Lemma fresh_svar_evar_open dbi x phi :
fresh_svar (phi^{evar: dbi ↦ x}) = fresh_svar phi.
Corollary svar_is_fresh_in_svar_open X Y dbi ϕ:
X ≠ Y →
svar_is_fresh_in X ϕ →
svar_is_fresh_in X (ϕ^{svar: dbi ↦ Y}).
Corollary evar_is_fresh_in_evar_open x y dbi ϕ:
x ≠ y →
evar_is_fresh_in x ϕ →
evar_is_fresh_in x (ϕ^{evar: dbi ↦ y}).
Corollary evar_fresh_svar_open x X dbi ϕ:
evar_is_fresh_in x ϕ →
evar_is_fresh_in x (ϕ^{svar: dbi ↦ X}).
Corollary svar_fresh_evar_open x X dbi ϕ:
svar_is_fresh_in X ϕ →
svar_is_fresh_in X (ϕ^{evar: dbi ↦ x}).
Lemma evar_open_inj : ∀ phi psi x n,
evar_is_fresh_in x phi → evar_is_fresh_in x psi →
phi^{evar: n ↦ x} = psi^{evar: n ↦ x}
→ phi = psi.
Lemma svar_open_inj : ∀ phi psi X n,
svar_is_fresh_in X phi → svar_is_fresh_in X psi →
phi^{svar: n ↦ X} = psi^{svar: n ↦ X}
→ phi = psi.
Lemma evar_open_free_svar_subst_comm: ∀ phi psi fresh n X,
(well_formed_closed_ex_aux psi 0) →
evar_is_fresh_in fresh phi →
evar_is_fresh_in fresh (phi^[[svar: X ↦ psi]])
→
(phi^[[svar: X ↦ psi]])^{evar: n ↦ fresh} = (phi^{evar: n ↦ fresh})^[[svar:X ↦ psi]].
Lemma svar_open_free_svar_subst_comm : ∀ phi psi fresh n X,
(well_formed_closed_mu_aux psi 0) →
svar_is_fresh_in fresh phi → svar_is_fresh_in fresh (phi^[[svar: X ↦ psi]]) → (fresh ≠ X)
→
phi^[[svar: X ↦ psi]]^{svar: n ↦ fresh} = phi^{svar: n ↦ fresh}^[[svar: X ↦ psi]].
Lemma free_evar_subst_preserves_no_negative_occurrence x p q n:
well_formed_closed_mu_aux q 0 = true →
no_negative_occurrence_db_b n p = true →
no_negative_occurrence_db_b n (p^[[evar: x ↦ q]]) = true
with
free_evar_subst_preserves_no_positive_occurrence x p q n:
well_formed_closed_mu_aux q 0 = true →
no_positive_occurrence_db_b n p = true →
no_positive_occurrence_db_b n (p^[[evar: x ↦ q]]) = true
.
Lemma Private_well_formed_free_evar_subst x p q n1 n2:
well_formed q →
well_formed_positive p && well_formed_closed_mu_aux p n2 && well_formed_closed_ex_aux p n1 →
no_negative_occurrence_db_b n2 (p^[[evar: x ↦ q]])
&& no_positive_occurrence_db_b n2 (p^[[evar: x ↦ q]])
&& well_formed_positive (p^[[evar: x ↦ q]])
&& well_formed_closed_mu_aux (p^[[evar: x ↦ q]]) n2
&& well_formed_closed_ex_aux (p^[[evar: x ↦ q]]) n1
= true.
Lemma well_formed_free_evar_subst x p q:
well_formed q = true →
well_formed p = true →
well_formed (p^[[evar: x ↦ q]]) = true.
Lemma well_formed_xy_free_evar_subst x m n p q:
well_formed q = true →
well_formed_xy m n p = true →
well_formed_xy m n (p^[[evar: x ↦ q]]) = true.
Lemma well_formed_free_evar_subst_0 x p q:
well_formed q = true →
well_formed p = true →
well_formed (p^[[evar: x ↦ q]]) = true.
Lemma evar_quantify_fresh x n phi:
evar_is_fresh_in x phi →
phi^{{evar: x ↦ n}} = phi.
Lemma svar_quantify_fresh X n phi:
svar_is_fresh_in X phi →
phi^{{svar: X ↦ n}} = phi.
Lemma svar_hno_bsvar_subst X ϕ ψ dbi:
(svar_has_negative_occurrence X ψ = true → no_positive_occurrence_db_b dbi ϕ = true) →
(svar_has_positive_occurrence X ψ = true → no_negative_occurrence_db_b dbi ϕ = true) →
svar_has_negative_occurrence X ϕ = false →
svar_has_negative_occurrence X (ϕ^[svar: dbi ↦ ψ]) = false
with svar_hpo_bsvar_subst X ϕ ψ dbi:
(svar_has_negative_occurrence X ψ = true → no_negative_occurrence_db_b dbi ϕ = true) →
(svar_has_positive_occurrence X ψ = true → no_positive_occurrence_db_b dbi ϕ = true) →
svar_has_positive_occurrence X ϕ = false →
svar_has_positive_occurrence X (ϕ^[svar: dbi ↦ ψ]) = false.
Lemma svar_hno_false_if_fresh X ϕ:
svar_is_fresh_in X ϕ →
svar_has_negative_occurrence X ϕ = false
with svar_hpo_false_if_fresh X ϕ:
svar_is_fresh_in X ϕ →
svar_has_positive_occurrence X ϕ = false.
(* TODO remove the no-negative-ocurrence assumption from the svar version *)
Lemma wfp_free_evar_subst ϕ ψ x:
well_formed_closed_mu_aux ψ 0 →
well_formed_positive ψ = true →
well_formed_positive ϕ = true →
well_formed_positive (ϕ^[[evar: x ↦ ψ]]) = true
with wfp_neg_free_evar_subst ϕ ψ x:
well_formed_closed_mu_aux ψ 0 →
well_formed_positive ψ = true →
well_formed_positive ϕ = true →
well_formed_positive (ϕ^[[evar: x ↦ ψ]]) = true.
Lemma neg_occurrence_bevar_subst x ϕ y n :
x ≠ y →
evar_has_negative_occurrence x ϕ =
evar_has_negative_occurrence x ϕ^{evar:n↦y}
with
pos_occurrence_bevar_subst x ϕ y n :
x ≠ y →
evar_has_positive_occurrence x ϕ =
evar_has_positive_occurrence x ϕ^{evar:n↦y}.
Lemma neg_occurrence_bsvar_subst x ϕ X n :
evar_has_negative_occurrence x ϕ =
evar_has_negative_occurrence x ϕ^{svar:n↦X}
with
pos_occurrence_bsvar_subst x ϕ X n :
evar_has_positive_occurrence x ϕ =
evar_has_positive_occurrence x ϕ^{svar:n↦X}.
Lemma fresh_svar_no_neg X ϕ :
svar_is_fresh_in X ϕ →
svar_has_negative_occurrence X ϕ = false
with
fresh_svar_no_pos X ϕ :
svar_is_fresh_in X ϕ →
svar_has_positive_occurrence X ϕ = false.
End lemmas.
#[export]
Hint Resolve wfp_free_evar_subst : core.
This page has been generated by coqdoc