File Substitution
From MatchingLogic Require Export Pattern.
Section subst.
Context {Σ : Signature}.
(* There are two substitution operations over patterns, bevar_subst and bsvar_subst. *)
(* substitute bound variable x for psi in phi *)
Fixpoint bevar_subst (psi : Pattern) (x : db_index) (phi : Pattern) :=
match phi with
| patt_free_evar x' ⇒ patt_free_evar x'
| patt_free_svar x' ⇒ patt_free_svar x'
| patt_bound_evar n ⇒ match compare_nat n x with
| Nat_less _ _ _ ⇒ patt_bound_evar n
| Nat_equal _ _ _ ⇒ psi
| Nat_greater _ _ _ ⇒ patt_bound_evar (Nat.pred n)
end
| patt_bound_svar n ⇒ patt_bound_svar n
| patt_sym sigma ⇒ patt_sym sigma
| patt_app phi1 phi2 ⇒ patt_app (bevar_subst psi x phi1)
(bevar_subst psi x phi2)
| patt_bott ⇒ patt_bott
| patt_imp phi1 phi2 ⇒ patt_imp (bevar_subst psi x phi1) (bevar_subst psi x phi2)
| patt_exists phi' ⇒ patt_exists (bevar_subst psi (S x) phi')
| patt_mu phi' ⇒ patt_mu (bevar_subst psi x phi')
end.
Fixpoint bsvar_subst (psi : Pattern) (x : db_index) (phi : Pattern) :=
match phi with
| patt_free_evar x' ⇒ patt_free_evar x'
| patt_free_svar x' ⇒ patt_free_svar x'
| patt_bound_evar n ⇒ patt_bound_evar n
| patt_bound_svar n ⇒ match compare_nat n x with
| Nat_less _ _ _ ⇒ patt_bound_svar n
| Nat_equal _ _ _ ⇒ psi
| Nat_greater _ _ _ ⇒ patt_bound_svar (Nat.pred n)
end
| patt_sym sigma ⇒ patt_sym sigma
| patt_app phi1 phi2 ⇒ patt_app (bsvar_subst psi x phi1)
(bsvar_subst psi x phi2)
| patt_bott ⇒ patt_bott
| patt_imp phi1 phi2 ⇒ patt_imp (bsvar_subst psi x phi1) (bsvar_subst psi x phi2)
| patt_exists phi' ⇒ patt_exists (bsvar_subst psi x phi')
| patt_mu phi' ⇒ patt_mu (bsvar_subst psi(S x) phi')
end.
Fixpoint bevar_occur (phi : Pattern) (x : db_index) : bool :=
match phi with
| patt_free_evar x' ⇒ false
| patt_free_svar x' ⇒ false
| patt_bound_evar n ⇒ if decide (n = x) is left _ then true else false
| patt_bound_svar n ⇒ false
| patt_sym sigma ⇒ false
| patt_app phi1 phi2 ⇒ orb (bevar_occur phi1 x)
(bevar_occur phi2 x)
| patt_bott ⇒ false
| patt_imp phi1 phi2 ⇒ orb (bevar_occur phi1 x) (bevar_occur phi2 x)
| patt_exists phi' ⇒ bevar_occur phi' (S x)
| patt_mu phi' ⇒ bevar_occur phi' x
end.
Fixpoint bsvar_occur (phi : Pattern) (x : db_index) : bool :=
match phi with
| patt_free_evar x' ⇒ false
| patt_free_svar x' ⇒ false
| patt_bound_evar n ⇒ false
| patt_bound_svar n ⇒ if (decide (n = x)) is left _ then true else false
| patt_sym sigma ⇒ false
| patt_app phi1 phi2 ⇒ orb (bsvar_occur phi1 x)
(bsvar_occur phi2 x)
| patt_bott ⇒ false
| patt_imp phi1 phi2 ⇒ orb (bsvar_occur phi1 x) (bsvar_occur phi2 x)
| patt_exists phi' ⇒ bsvar_occur phi' x
| patt_mu phi' ⇒ bsvar_occur phi' (S x)
end.
(* substitute free element variable x for psi in phi *)
Fixpoint free_evar_subst (psi : Pattern) (x : evar) (phi : Pattern) :=
match phi with
| patt_free_evar x' ⇒ if decide (x = x') is left _ then psi else patt_free_evar x'
| patt_free_svar X ⇒ patt_free_svar X
| patt_bound_evar x' ⇒ patt_bound_evar x'
| patt_bound_svar X ⇒ patt_bound_svar X
| patt_sym sigma ⇒ patt_sym sigma
| patt_app phi1 phi2 ⇒ patt_app (free_evar_subst psi x phi1)
(free_evar_subst psi x phi2)
| patt_bott ⇒ patt_bott
| patt_imp phi1 phi2 ⇒ patt_imp (free_evar_subst psi x phi1) (free_evar_subst psi x phi2)
| patt_exists phi' ⇒ patt_exists (free_evar_subst psi x phi')
| patt_mu phi' ⇒ patt_mu (free_evar_subst psi x phi')
end.
(* substitute free set variable X for psi in phi *)
Fixpoint free_svar_subst (psi : Pattern) (X : svar) (phi : Pattern) : Pattern :=
match phi with
| patt_free_evar x ⇒ patt_free_evar x
| patt_free_svar X' ⇒ if decide (X = X') is left _ then psi else patt_free_svar X'
| patt_bound_evar x ⇒ patt_bound_evar x
| patt_bound_svar X' ⇒ patt_bound_svar X'
| patt_sym sigma ⇒ patt_sym sigma
| patt_app phi1 phi2 ⇒ patt_app (free_svar_subst psi X phi1)
(free_svar_subst psi X phi2)
| patt_bott ⇒ patt_bott
| patt_imp phi1 phi2 ⇒ patt_imp (free_svar_subst psi X phi1) (free_svar_subst psi X phi2)
| patt_exists phi' ⇒ patt_exists (free_svar_subst psi X phi')
| patt_mu phi' ⇒ patt_mu (free_svar_subst psi X phi')
end.
(* instantiate exists x. p or mu x. p with psi for p *)
Definition instantiate (phi psi : Pattern) :=
match phi with
| patt_exists phi' ⇒ bevar_subst psi 0 phi'
| patt_mu phi' ⇒ bsvar_subst psi 0 phi'
| _ ⇒ phi
end.
(* replace element variable x with de Bruijn index level *)
Fixpoint evar_quantify (x : evar) (level : db_index)
(p : Pattern) : Pattern :=
match p with
| patt_free_evar x' ⇒ if decide (x = x') is left _ then patt_bound_evar level else patt_free_evar x'
| patt_free_svar x' ⇒ patt_free_svar x'
| patt_bound_evar x' ⇒ patt_bound_evar x'
| patt_bound_svar X ⇒ patt_bound_svar X
| patt_sym s ⇒ patt_sym s
| patt_app ls rs ⇒ patt_app (evar_quantify x level ls) (evar_quantify x level rs)
| patt_bott ⇒ patt_bott
| patt_imp ls rs ⇒ patt_imp (evar_quantify x level ls) (evar_quantify x level rs)
| patt_exists p' ⇒ patt_exists (evar_quantify x (S level) p')
| patt_mu p' ⇒ patt_mu (evar_quantify x level p')
end.
(* replace set variable X with de Bruijn index level *)
Fixpoint svar_quantify (X : svar) (level : db_index)
(p : Pattern) : Pattern :=
match p with
| patt_free_evar x' ⇒ patt_free_evar x'
| patt_free_svar X' ⇒ if decide (X = X') is left _ then patt_bound_svar level else patt_free_svar X'
| patt_bound_evar x' ⇒ patt_bound_evar x'
| patt_bound_svar X ⇒ patt_bound_svar X
| patt_sym s ⇒ patt_sym s
| patt_app ls rs ⇒ patt_app (svar_quantify X level ls) (svar_quantify X level rs)
| patt_bott ⇒ patt_bott
| patt_imp ls rs ⇒ patt_imp (svar_quantify X level ls) (svar_quantify X level rs)
| patt_exists p' ⇒ patt_exists (svar_quantify X level p')
| patt_mu p' ⇒ patt_mu (svar_quantify X (S level) p')
end.
(* replace de Bruijn index k with element variable n *)
Definition evar_open (x : evar) (k : db_index) (p : Pattern) : Pattern :=
bevar_subst (patt_free_evar x) k p.
(* replace de Bruijn index k with set variable n *)
Definition svar_open (X : svar) (k : db_index) (p : Pattern) : Pattern :=
bsvar_subst (patt_free_svar X) k p.
End subst.
Module Notations.
Notation "e ^[ 'evar:' dbi ↦ e' ]" := (bevar_subst e' dbi e) (at level 2, e' at level 200, left associativity,
format "e ^[ 'evar:' dbi ↦ e' ]" ) : ml_scope.
Notation "e ^[ 'svar:' dbi ↦ e' ]" := (bsvar_subst e' dbi e) (at level 2, e' at level 200, left associativity,
format "e ^[ 'svar:' dbi ↦ e' ]" ) : ml_scope.
Notation "e ^[[ 'evar:' x ↦ e' ]]" := (free_evar_subst e' x e) (at level 2, e' at level 200, left associativity,
format "e ^[[ 'evar:' x ↦ e' ]]" ) : ml_scope.
Notation "e ^[[ 'svar:' X ↦ e' ]]" := (free_svar_subst e' X e) (at level 2, e' at level 200, left associativity,
format "e ^[[ 'svar:' X ↦ e' ]]" ) : ml_scope.
Notation "e ^{ 'evar:' db ↦ x }" := (evar_open x db e) (at level 2, x at level 200, left associativity,
format "e ^{ 'evar:' db ↦ x }" ) : ml_scope.
Notation "e ^{ 'svar:' db ↦ x }" := (svar_open x db e) (at level 2, x at level 200, left associativity,
format "e ^{ 'svar:' db ↦ x }" ) : ml_scope.
Notation "e ^{{ 'evar:' x ↦ db }}" := (evar_quantify x db e) (at level 2, x at level 200, left associativity,
format "e ^{{ 'evar:' x ↦ db }}" ) : ml_scope.
Notation "e ^{{ 'svar:' x ↦ db }}" := (svar_quantify x db e) (at level 2, x at level 200, left associativity,
format "e ^{{ 'svar:' x ↦ db }}" ) : ml_scope.
Notation "e ^[ e' ]" := (instantiate e e') (at level 2, e' at level 200, left associativity, format "e ^[ e' ]") : ml_scope.
End Notations.
Section subst.
Import Notations.
Open Scope ml_scope.
Context {Σ : Signature}.
Definition exists_quantify (x : evar)
(p : Pattern) : Pattern :=
patt_exists (p^{{evar: x ↦ 0}}).
Definition mu_quantify (X : svar)
(p : Pattern) : Pattern :=
patt_mu (p^{{svar: X ↦ 0}}).
Lemma evar_open_size :
∀ (k : db_index) (n : evar) (p : Pattern),
pat_size p = pat_size (p^{evar: k ↦ n}).
Lemma svar_open_size :
∀ (k : db_index) (n : svar) (p : Pattern),
pat_size p = pat_size (p^{svar: k ↦ n}).
(* From https://www.chargueraud.org/research/2009/ln/main.pdf in 3.3 (body def.) *)
Definition wfc_body_ex phi := ∀ x,
¬ elem_of x (free_evars phi) → well_formed_closed (phi^{evar: 0 ↦ x}) = true.
Lemma positive_negative_occurrence_evar_open_and : ∀ (phi : Pattern) (db1 db2 : db_index) (x : evar),
(*le db1 db2 ->*)
(no_positive_occurrence_db_b db1 phi → no_positive_occurrence_db_b db1 (phi^{evar: db2 ↦ x}))
∧ (no_negative_occurrence_db_b db1 phi → no_negative_occurrence_db_b db1 (phi^{evar: db2 ↦ x})).
Lemma no_negative_occurrence_evar_open phi db1 db2 x:
no_negative_occurrence_db_b db1 phi = true →
no_negative_occurrence_db_b db1 (phi^{evar: db2 ↦ x}) = true.
Lemma no_positive_occurrence_evar_open phi db1 db2 x:
no_positive_occurrence_db_b db1 phi = true →
no_positive_occurrence_db_b db1 (phi^{evar: db2 ↦ x}) = true.
(*Helper lemma for wf_body_to_wf_ex*)
Lemma wfc_ex_aux_body_ex_imp2:
∀ phi n x,
well_formed_closed_ex_aux (phi^{evar: n ↦ x}) n = true
→
well_formed_closed_ex_aux phi (S n) = true.
(*Helper lemma for wf_body_to_wf_ex*)
Lemma wfc_mu_aux_body_ex_imp2:
∀ phi n n' x,
well_formed_closed_mu_aux (phi^{evar: n ↦ x}) n' = true
→
well_formed_closed_mu_aux phi n' = true.
Lemma wfc_ex_aux_body_mu_imp2:
∀ phi n n' X,
well_formed_closed_ex_aux (phi^{svar: n ↦ X}) n' = true
→
well_formed_closed_ex_aux phi n' = true.
Lemma wfc_mu_aux_body_mu_imp2:
∀ phi n X,
well_formed_closed_mu_aux (phi^{svar: n ↦ X}) n = true
→
well_formed_closed_mu_aux phi (S n) = true.
Lemma wfc_ex_aux_bevar_subst :
∀ phi psi n,
well_formed_closed_ex_aux phi (S n) = true
→ well_formed_closed_ex_aux psi n = true
→ well_formed_closed_ex_aux (phi^[evar: n ↦ psi]) n = true.
Lemma wfc_mu_aux_bevar_subst :
∀ phi psi n n',
well_formed_closed_mu_aux phi n' = true
→ well_formed_closed_mu_aux psi n' = true
→ well_formed_closed_mu_aux (phi^[evar: n ↦ psi]) n' = true.
Lemma wfc_ex_aux_bsvar_subst :
∀ phi psi n n',
well_formed_closed_ex_aux phi n = true
→ well_formed_closed_ex_aux psi n = true
→ well_formed_closed_ex_aux (phi^[svar: n' ↦ psi]) n = true.
Lemma wfc_mu_aux_bsvar_subst :
∀ phi psi n',
well_formed_closed_mu_aux phi (S n') = true
→ well_formed_closed_mu_aux psi n' = true
→ well_formed_closed_mu_aux (phi^[svar: n' ↦ psi]) n' = true.
(*Helper lemma for wf_ex_to_wf_body *)
Corollary wfc_ex_aux_body_ex_imp1:
∀ phi n x,
well_formed_closed_ex_aux phi (S n) = true
→
well_formed_closed_ex_aux (phi^{evar: n ↦ x}) n = true.
Corollary wfc_mu_aux_body_ex_imp1:
∀ phi n n' x,
well_formed_closed_mu_aux phi n' = true
→
well_formed_closed_mu_aux (phi^{evar: n ↦ x}) n' = true.
Corollary wfc_ex_aux_body_mu_imp1:
∀ phi n n' X,
well_formed_closed_ex_aux phi n' = true
→
well_formed_closed_ex_aux (phi^{svar: n ↦ X}) n' = true.
Corollary wfc_mu_aux_body_mu_imp1:
∀ phi n X,
well_formed_closed_mu_aux phi (S n) = true
→
well_formed_closed_mu_aux (phi^{svar: n ↦ X}) n = true.
Lemma wfc_mu_aux_bsvar_subst_le :
∀ phi psi n n', n' ≤ n →
well_formed_closed_mu_aux phi (S n) = true →
well_formed_closed_mu_aux psi n
→
well_formed_closed_mu_aux (phi^[svar:n' ↦ psi]) n = true.
Lemma wfc_ex_aux_bsvar_subst_le:
∀ phi psi n n', n' ≤ n →
well_formed_closed_ex_aux phi (S n) = true →
well_formed_closed_ex_aux psi n = true
→
well_formed_closed_ex_aux (phi^[evar:n'↦psi]) n = true.
Corollary wfc_mu_aux_body_mu_imp3:
∀ phi n n' X, n' ≤ n →
well_formed_closed_mu_aux phi (S n) = true
→
well_formed_closed_mu_aux (phi^{svar: n' ↦ X}) n = true.
Corollary wfc_mu_aux_body_ex_imp3:
∀ phi n n' X, n' ≤ n →
well_formed_closed_ex_aux phi (S n) = true
→
well_formed_closed_ex_aux (phi^{evar: n' ↦ X}) n = true.
Corollary wfc_ex_aux_body_iff:
∀ phi n x,
well_formed_closed_ex_aux phi (S n) = true
↔
well_formed_closed_ex_aux (phi^{evar: n ↦ x}) n = true.
Corollary wfc_mu_aux_body_iff:
∀ phi n X,
well_formed_closed_mu_aux phi (S n) = true
↔
well_formed_closed_mu_aux (phi^{svar: n ↦ X}) n = true.
(*If (ex, phi) is closed, then its body is closed too*)
Corollary wfc_ex_to_wfc_body:
∀ phi, well_formed_closed (patt_exists phi) = true → wfc_body_ex phi.
Lemma no_neg_occ_db_bevar_subst phi psi dbi1 dbi2:
well_formed_closed_mu_aux psi 0 = true →
no_negative_occurrence_db_b dbi1 phi = true →
no_negative_occurrence_db_b dbi1 (phi^[evar: dbi2 ↦ psi]) = true
with no_pos_occ_db_bevar_subst phi psi dbi1 dbi2:
well_formed_closed_mu_aux psi 0 = true →
no_positive_occurrence_db_b dbi1 phi = true →
no_positive_occurrence_db_b dbi1 (phi^[evar: dbi2 ↦ psi]) = true.
Lemma bevar_subst_positive_2 :
∀ φ ψ n,
well_formed_closed_mu_aux ψ 0 = true →
well_formed_positive φ = true →
well_formed_positive ψ = true →
well_formed_positive (φ^[evar: n ↦ ψ]) = true.
Corollary wfp_evar_open : ∀ phi x n,
well_formed_positive phi = true →
well_formed_positive (phi^{evar: n ↦ x}) = true.
(* Additional lemmas: evar_open, svar_open, freshness, well_formedness, etc. *)
(* evar_open and evar_quantify are inverses *)
Lemma evar_open_evar_quantify x n phi:
well_formed_closed_ex_aux phi n →
((phi^{{evar: x ↦ n}})^{evar: n ↦ x}) = phi.
Lemma svar_open_svar_quantify X n phi:
well_formed_closed_mu_aux phi n →
((phi^{{svar: X ↦ n}})^{svar: n ↦ X}) = phi.
Lemma evar_quantify_evar_open x n phi:
x ∉ free_evars phi → well_formed_closed_ex_aux phi (S n) →
((phi^{evar: n ↦ x})^{{evar: x ↦ n}}) = phi.
Lemma svar_quantify_svar_open X n phi:
X ∉ free_svars phi → well_formed_closed_mu_aux phi (S n) →
((phi^{svar: n ↦ X})^{{svar: X ↦ n}}) = phi.
Lemma double_evar_quantify φ : ∀ x n,
φ^{{evar: x ↦ n}}^{{evar: x ↦ n}} = φ^{{evar: x ↦ n}}.
Lemma double_svar_quantify φ : ∀ X n,
φ^{{svar: X ↦ n}}^{{svar: X ↦ n}} = φ^{{svar: X ↦ n}}.
Lemma well_formed_bevar_subst φ : ∀ ψ n m,
m ≥ n → well_formed_closed_ex_aux φ n →
(φ^[evar: m ↦ ψ]) = φ.
Lemma well_formed_bsvar_subst φ : ∀ ψ k m,
m ≥ k → well_formed_closed_mu_aux φ k →
(φ^[svar: m ↦ ψ]) = φ.
(* bevar_subst is identity if n does not occur in phi *)
Corollary bevar_subst_not_occur n ψ ϕ :
well_formed_closed_ex_aux ϕ n →
(ϕ^[evar: n ↦ ψ]) = ϕ.
(* evar_open is identity if n does not occur in phi *)
Corollary evar_open_not_occur n x ϕ :
well_formed_closed_ex_aux ϕ n →
ϕ^{evar: n ↦ x} = ϕ.
(* bsvar_subst is identity if n does not occur in phi *)
Corollary bsvar_subst_not_occur n ψ ϕ :
well_formed_closed_mu_aux ϕ n →
(ϕ^[svar: n ↦ ψ]) = ϕ.
(* evar_open is identity if n does not occur in phi *)
Corollary svar_open_not_occur n x ϕ :
well_formed_closed_mu_aux ϕ n →
ϕ^{svar: n ↦ x} = ϕ.
(* opening on closed patterns is identity *)
Lemma evar_open_closed :
∀ phi,
well_formed_closed_ex_aux phi 0 →
∀ n v,
phi^{evar: n ↦ v} = phi.
Lemma svar_open_closed :
∀ phi,
well_formed_closed_mu_aux phi 0 →
∀ n v,
phi^{svar: n ↦ v} = phi.
Lemma bevar_subst_comm_higher :
∀ phi psi1 psi2 n m,
n > m → well_formed_closed_ex_aux psi1 0 → well_formed_closed_ex_aux psi2 0 →
(phi^[evar: n ↦ psi1])^[evar: m ↦ psi2] =
(phi^[evar: m ↦ psi2])^[evar: pred n ↦ psi1].
Lemma bevar_subst_comm_lower :
∀ phi psi1 psi2 n m,
n < m → well_formed_closed_ex_aux psi1 0 → well_formed_closed_ex_aux psi2 0 →
(phi^[evar: n ↦ psi1])^[evar: m ↦ psi2] =
(phi^[evar: S m ↦ psi2])^[evar: n ↦ psi1].
Lemma bsvar_subst_comm_higher :
∀ phi psi1 psi2 n m,
n > m → well_formed_closed_mu_aux psi1 0 → well_formed_closed_mu_aux psi2 0 →
(phi^[svar: n ↦ psi1])^[svar: m ↦ psi2] =
(phi^[svar: m ↦ psi2])^[svar: pred n ↦ psi1].
Lemma bsvar_subst_comm_lower :
∀ phi psi1 psi2 n m,
n < m → well_formed_closed_mu_aux psi1 0 → well_formed_closed_mu_aux psi2 0 →
(phi^[svar: n ↦ psi1])^[svar: m ↦ psi2] =
(phi^[svar: S m ↦ psi2])^[svar: n ↦ psi1].
Corollary evar_open_comm_higher:
∀ n m,
n < m
→
∀ x y phi,
phi^{evar: m ↦ y}^{evar: n ↦ x} = phi^{evar: n ↦ x}^{evar: pred m ↦ y}.
Corollary evar_open_comm_lower:
∀ n m,
n > m
→
∀ x y phi,
phi^{evar: m ↦ y}^{evar: n ↦ x} = phi^{evar: S n ↦ x}^{evar: m ↦ y}.
Corollary svar_open_comm_higher:
∀ n m,
n < m
→
∀ X Y phi,
phi^{svar: m ↦ Y}^{svar: n ↦ X} = phi^{svar: n ↦ X}^{svar: pred m ↦ Y} .
Corollary svar_open_comm_lower:
∀ n m,
n > m
→
∀ X Y phi,
phi^{svar: m ↦ Y} ^{svar: n ↦ X} = phi^{svar: S n ↦ X} ^{svar: m ↦ Y}.
Lemma bevar_subst_bsvar_subst phi psi1 psi2 dbi1 dbi2
: well_formed_closed psi1 → well_formed_closed psi2 →
(phi^[svar: dbi1 ↦ psi1])^[evar: dbi2 ↦ psi2] =
(phi^[evar: dbi2 ↦ psi2])^[svar: dbi1 ↦ psi1].
Corollary svar_open_evar_open_comm
: ∀ (phi : Pattern) (dbi1 : db_index)(x : evar)(dbi2 : db_index)(X : svar),
phi^{svar: dbi2 ↦ X}^{evar: dbi1 ↦ x} = phi^{evar: dbi1 ↦ x}^{svar: dbi2 ↦ X} .
Lemma free_svars_evar_open : ∀ (ϕ : Pattern) (dbi :db_index) (x : evar),
free_svars ϕ^{evar: dbi ↦ x} = free_svars ϕ.
Lemma positive_negative_occurrence_db_named :
∀ (phi : Pattern) (dbi : db_index) (X : svar),
(no_positive_occurrence_db_b dbi phi →
svar_has_positive_occurrence X phi = false →
svar_has_positive_occurrence X (phi^{svar: dbi ↦ X}) = false)
∧ (no_negative_occurrence_db_b dbi phi →
svar_has_negative_occurrence X phi = false →
svar_has_negative_occurrence X (phi^{svar: dbi ↦ X}) = false).
Lemma positive_negative_occurrence_evar_open : ∀ (ϕ : Pattern) (X : svar) (dbi : db_index) (x : evar),
(svar_has_positive_occurrence X (ϕ^{evar: dbi ↦ x}) = false ↔ svar_has_positive_occurrence X ϕ = false)
∧ (svar_has_negative_occurrence X (ϕ^{evar: dbi ↦ x}) = false ↔ svar_has_negative_occurrence X ϕ = false).
Corollary positive_occurrence_evar_open : ∀ (ϕ : Pattern) (X : svar) (dbi : db_index) (x : evar),
svar_has_positive_occurrence X (ϕ^{evar: dbi ↦ x}) = false ↔ svar_has_positive_occurrence X ϕ = false.
Corollary negative_occurrence_evar_open : ∀ (ϕ : Pattern) (X : svar) (dbi : db_index) (x : evar),
svar_has_negative_occurrence X (ϕ^{evar: dbi ↦ x}) = false ↔ svar_has_negative_occurrence X ϕ = false.
Lemma positive_negative_occurrence_db_svar_open_le : ∀ (phi : Pattern) (dbi1 dbi2 : db_index) (X : svar),
dbi1 < dbi2 →
(
no_positive_occurrence_db_b dbi1 phi →
no_positive_occurrence_db_b dbi1 (phi^{svar: dbi2 ↦ X})
)
∧ (no_negative_occurrence_db_b dbi1 phi → no_negative_occurrence_db_b dbi1 (phi^{svar: dbi2 ↦ X})).
Lemma wfp_svar_open : ∀ (phi : Pattern) (dbi : db_index) (X : svar),
well_formed_positive phi = true →
well_formed_positive (phi^{svar: dbi ↦ X}) = true.
Lemma positive_negative_occurrence_named_svar_open :
∀ (phi : Pattern) (X Y : svar) (dbi : db_index),
X ≠ Y →
(
svar_has_negative_occurrence X phi = false →
svar_has_negative_occurrence X (phi^{svar: dbi ↦ Y}) = false
) ∧ (
svar_has_positive_occurrence X phi = false →
svar_has_positive_occurrence X (phi^{svar: dbi ↦ Y}) = false
).
Corollary evar_open_wfc_aux db1 db2 X phi :
db1 ≤ db2 →
well_formed_closed_ex_aux phi db1 →
phi^{evar: db2 ↦ X} = phi.
Corollary evar_open_wfc m X phi : well_formed_closed_ex_aux phi 0 → phi^{evar: m ↦ X} = phi.
Corollary svar_open_wfc_aux db1 db2 X phi :
db1 ≤ db2 →
well_formed_closed_mu_aux phi db1 →
phi^{svar: db2 ↦ X} = phi.
Corollary svar_open_wfc m X phi : well_formed_closed_mu_aux phi 0 → phi^{svar: m ↦ X} = phi.
Corollary evar_open_bsvar_subst m phi1 phi2 dbi X
: well_formed_closed phi2 →
phi1^[svar: dbi ↦ phi2]^{evar: m ↦ X}
= phi1^{evar: m ↦ X}^[svar: dbi ↦ phi2].
Corollary svar_open_bevar_subst m phi1 phi2 dbi X
: well_formed_closed phi2 →
phi1^[evar: dbi ↦ phi2]^{svar: m ↦ X}
= phi1^{svar: m ↦ X}^[evar: dbi ↦ phi2].
Corollary svar_open_bsvar_subst_higher m phi1 phi2 dbi X
: well_formed_closed phi2 →
m < dbi →
phi1^[svar: dbi ↦ phi2]^{svar: m ↦ X}
= phi1^{svar: m ↦ X}^[svar: pred dbi ↦ phi2].
Corollary svar_open_bsvar_subst_lower m phi1 phi2 dbi X
: well_formed_closed phi2 →
m > dbi →
phi1^[svar: dbi ↦ phi2]^{svar: m ↦ X}
= phi1^{svar: S m ↦ X}^[svar: dbi ↦ phi2].
Corollary evar_open_bevar_subst_higher m phi1 phi2 dbi X
: well_formed_closed_ex_aux phi2 0 →
m < dbi →
phi1^[evar: dbi ↦ phi2]^{evar: m ↦ X}
= phi1^{evar: m ↦ X}^[evar: pred dbi ↦ phi2].
Corollary evar_open_bevar_subst_lower m phi1 phi2 dbi X
: well_formed_closed phi2 →
m > dbi →
phi1^[evar: dbi ↦ phi2]^{evar: m ↦ X}
= phi1^{evar: S m ↦ X}^[evar: dbi ↦ phi2].
Lemma free_svars_bsvar_subst' :
∀ φ ψ dbi X,
(X ∈ free_svars (φ^[svar: dbi ↦ ψ])) ↔
((X ∈ (free_svars ψ) ∧ bsvar_occur φ dbi) ∨ (X ∈ (free_svars φ))).
Lemma free_evars_bsvar_subst' :
∀ φ ψ dbi x,
(x ∈ free_evars (φ^[svar: dbi ↦ ψ])) ↔
((x ∈ (free_evars ψ) ∧ bsvar_occur φ dbi) ∨ (x ∈ (free_evars φ))).
Lemma free_evars_bevar_subst' :
∀ φ ψ dbi X,
(X ∈ free_evars (φ^[evar: dbi ↦ ψ])) ↔
((X ∈ (free_evars ψ) ∧ bevar_occur φ dbi) ∨ (X ∈ (free_evars φ))).
Lemma free_svars_bsvar_subst :
∀ φ ψ dbi,
free_svars (φ^[svar: dbi ↦ ψ]) ⊆ union (free_svars ψ) (free_svars φ).
Lemma free_evars_bevar_subst :
∀ φ ψ dbi,
free_evars (φ^[evar: dbi ↦ ψ]) ⊆ union (free_evars ψ) (free_evars φ).
Lemma free_svars_svar_open'' :
∀ φ dbi X Y,
(X ∈ free_svars (φ^{svar: dbi ↦ Y})) ↔
(((X = Y) ∧ (bsvar_occur φ dbi)) ∨ (X ∈ (free_svars φ))).
Corollary free_svars_svar_open ϕ X dbi :
free_svars (ϕ^{svar: dbi ↦ X}) ⊆ union (singleton X) (free_svars ϕ).
Lemma free_evars_evar_open'' :
∀ φ dbi x y,
(x ∈ free_evars (φ^{evar: dbi ↦ y})) ↔
((x = y ∧ bevar_occur φ dbi) ∨ (x ∈ (free_evars φ))).
Corollary free_evars_evar_open ϕ x dbi :
free_evars (ϕ^{evar: dbi ↦ x}) ⊆ union (singleton x) (free_evars ϕ).
Lemma free_evars_evar_open' ϕ x dbi:
free_evars ϕ ⊆ free_evars (ϕ^{evar: dbi ↦ x}).
Lemma free_evar_subst_no_occurrence x p q:
x ∉ free_evars p →
p^[[evar:x ↦ q]] = p.
(*
Lemma Private_bsvar_occur_evar_open sz dbi1 dbi2 X phi:
size phi <= sz ->
bsvar_occur phi dbi1 = false ->
bsvar_occur (phi^{evar: dbi2 ↦ X}) dbi1 = false.
Proof.
move: phi dbi1 dbi2.
induction sz; move=> phi; destruct phi; simpl; move=> dbi1 dbi2 Hsz H; try rewrite !IHsz; auto; try lia; try apply orb_false_elim in H; firstorder.
2: { simpl. lia. }
cbn. case_match; reflexivity.
Qed. *)
Corollary bsvar_occur_evar_open dbi1 dbi2 X phi:
bsvar_occur phi dbi1 = false →
bsvar_occur (phi^{evar: dbi2 ↦ X}) dbi1 = false.
(* Lemma Private_bevar_occur_svar_open sz dbi1 dbi2 X phi:
size phi <= sz ->
bevar_occur phi dbi1 = false ->
bevar_occur (phi^{svar: dbi2 ↦ X}) dbi1 = false.
Proof.
move: phi dbi1 dbi2.
induction sz; move=> phi; destruct phi; simpl; move=> dbi1 dbi2 Hsz H; try rewrite !IHsz; auto; try lia; try apply orb_false_elim in H; firstorder.
{ cbn. case_match; reflexivity. }
simpl. lia.
Qed. *)
Corollary bevar_occur_svar_open dbi1 dbi2 X phi:
bevar_occur phi dbi1 = false →
bevar_occur (phi^{svar: dbi2 ↦ X}) dbi1 = false.
(* Lemma Private_bevar_occur_evar_open sz dbi1 dbi2 X phi:
size phi <= sz -> dbi1 < dbi2 ->
bevar_occur phi dbi1 = false ->
bevar_occur (phi^{evar: dbi2 ↦ X}) dbi1 = false.
Proof.
move: phi dbi1 dbi2.
induction sz; move=> phi; destruct phi; simpl; move=> dbi1 dbi2 Hsz H H1; try rewrite !IHsz; auto; try lia; try apply orb_false_elim in H1; firstorder.
{ cbn. repeat case_match; simpl; auto; try lia.
{ rewrite H0. reflexivity. }
{ case_match; try lia. }
}
simpl. lia.
Qed. *)
Corollary bevar_occur_evar_open dbi1 dbi2 X phi:
bevar_occur phi dbi1 = false → dbi1 < dbi2 →
bevar_occur (phi^{evar: dbi2 ↦ X}) dbi1 = false.
Lemma well_formed_positive_bevar_subst φ : ∀ n ψ,
mu_free φ →
well_formed_positive φ = true → well_formed_positive ψ = true
→
well_formed_positive (φ^[evar: n ↦ ψ]) = true.
Lemma mu_free_bevar_subst :
∀ φ ψ, mu_free φ → mu_free ψ → ∀ n, mu_free (φ^[evar: n ↦ ψ]).
Corollary mu_free_evar_open :
∀ φ, mu_free φ → ∀ x n, mu_free (φ^{evar: n ↦ x}).
Theorem evar_open_free_evar_subst_swap :
∀ φ x n ψ y, x ≠ y → well_formed ψ →
φ^[[evar: y ↦ ψ]]^{evar: n ↦ x} = φ^{evar: n ↦ x}^[[evar: y ↦ ψ]].
Lemma free_evars_free_evar_subst : ∀ φ ψ x,
free_evars (φ^[[evar: x ↦ ψ]]) ⊆ free_evars φ ∪ free_evars ψ.
Lemma bound_to_free_variable_subst :
∀ φ x m n ψ,
m > n →
well_formed_closed_ex_aux ψ 0 →
well_formed_closed_ex_aux φ m → x ∉ free_evars φ →
φ^[evar: n ↦ ψ] = φ^{evar: n ↦ x}^[[evar: x ↦ ψ]].
Lemma bound_to_free_set_variable_subst :
∀ φ X m n ψ,
m > n →
well_formed_closed_mu_aux ψ 0 →
well_formed_closed_mu_aux φ m → X ∉ free_svars φ →
φ^[svar: n ↦ ψ] = φ^{svar: n ↦ X}^[[svar: X ↦ ψ]].
Lemma evar_open_no_negative_occurrence :
∀ φ db1 db2 x,
(no_negative_occurrence_db_b db1 (φ^{evar: db2 ↦ x}) →
no_negative_occurrence_db_b db1 φ) ∧
(no_positive_occurrence_db_b db1 (φ^{evar: db2 ↦ x}) →
no_positive_occurrence_db_b db1 φ).
Lemma evar_open_positive : ∀ φ n x,
well_formed_positive (φ^{evar: n ↦ x}) = true →
well_formed_positive φ = true.
Lemma bevar_subst_closed_mu :
∀ φ ψ n m,
well_formed_closed_mu_aux φ m = true →
well_formed_closed_mu_aux ψ m = true
→
well_formed_closed_mu_aux (φ^[evar: n ↦ ψ]) m = true.
Lemma bevar_subst_closed_ex :
∀ φ ψ n,
well_formed_closed_ex_aux φ (S n) = true →
well_formed_closed_ex_aux ψ n = true
→
well_formed_closed_ex_aux (φ^[evar: n ↦ ψ]) n = true.
Lemma bevar_subst_positive :
∀ φ ψ n, mu_free φ →
well_formed_positive φ = true → well_formed_positive ψ = true
→
well_formed_positive (φ^[evar: n ↦ ψ]) = true.
Theorem evar_quantify_closed_ex :
∀ φ x n, well_formed_closed_ex_aux φ n →
well_formed_closed_ex_aux (φ^{{evar: x ↦ n}}) (S n) = true.
Theorem svar_quantify_closed_mu :
∀ φ X n, well_formed_closed_mu_aux φ n →
well_formed_closed_mu_aux (φ^{{svar: X ↦ n}}) (S n) = true.
Theorem evar_quantify_closed_mu :
∀ φ x n m, well_formed_closed_mu_aux φ m →
well_formed_closed_mu_aux (φ^{{evar: x ↦ n}}) m = true.
Theorem svar_quantify_closed_ex :
∀ φ X n m, well_formed_closed_ex_aux φ m →
well_formed_closed_ex_aux (φ^{{svar: X ↦ n}}) m = true.
Theorem no_occ_quantify :
∀ (φ : Pattern) (db1 db2 : db_index) (x : evar),
(no_negative_occurrence_db_b db1 φ
→ no_negative_occurrence_db_b db1 (φ^{{evar: x ↦ db2}}))
∧ (no_positive_occurrence_db_b db1 φ
→ no_positive_occurrence_db_b db1 (φ^{{evar: x ↦ db2}})).
Theorem evar_quantify_positive :
∀ φ x n, well_formed_positive φ →
well_formed_positive (φ^{{evar: x ↦ n}}) = true.
Corollary evar_quantify_well_formed :
∀ φ x, well_formed φ →
well_formed (patt_exists (φ^{{evar: x ↦ 0}})) = true.
Theorem evar_quantify_no_occurrence :
∀ φ x n, x ∉ (free_evars (φ^{{evar: x ↦ n}})).
Theorem svar_quantify_not_free :
∀ φ X n, X ∉ (free_svars (φ^{{svar: X ↦ n}})).
Lemma evar_quantify_not_free_evars :
∀ φ x n,
x ∉ free_evars φ →
φ^{{evar: x ↦ n}} = φ.
Lemma wf_ex_evar_quantify x p:
well_formed p = true →
well_formed (patt_exists (p^{{evar: x ↦ 0}})) = true.
Lemma free_evars_evar_quantify x n p:
free_evars (p^{{evar: x ↦ n}}) = free_evars p ∖ {[x]}.
Lemma free_svars_svar_quantify X n p:
free_svars (p^{{svar: X ↦ n}}) = free_svars p ∖ {[X]}.
Lemma no_neg_occ_db_bsvar_subst phi psi dbi1 dbi2:
well_formed_closed_mu_aux psi 0 = true → dbi1 < dbi2 →
(no_negative_occurrence_db_b dbi1 phi = true →
no_negative_occurrence_db_b dbi1 (phi^[svar: dbi2 ↦ psi]) = true)
∧ (no_positive_occurrence_db_b dbi1 phi = true →
no_positive_occurrence_db_b dbi1 (phi^[svar: dbi2 ↦ psi]) = true).
Lemma Private_wfp_bsvar_subst (phi psi : Pattern) (n : nat) :
well_formed_positive psi →
well_formed_closed_mu_aux psi 0 →
well_formed_positive phi →
(
no_negative_occurrence_db_b n phi →
well_formed_positive (phi^[svar: n ↦ psi]) )
∧ (no_positive_occurrence_db_b n phi →
∀ phi',
well_formed_positive phi' →
well_formed_positive (patt_imp (phi^[svar: n ↦ psi]) phi')
)
.
Corollary wfp_bsvar_subst (phi psi : Pattern) :
well_formed_positive (patt_mu phi) →
well_formed_positive psi →
well_formed_closed_mu_aux psi 0 →
well_formed_positive (phi^[svar: 0 ↦ psi]).
Lemma bevar_subst_evar_quantify_free_evar x dbi ϕ:
well_formed_closed_ex_aux ϕ dbi →
(ϕ^{{evar: x ↦ dbi}})^[evar: dbi ↦ patt_free_evar x] = ϕ.
Lemma bsvar_subst_svar_quantify_free_svar X dbi ϕ:
well_formed_closed_mu_aux ϕ dbi →
(ϕ^{{svar: X ↦ dbi}})^[svar: dbi ↦ (patt_free_svar X)] = ϕ.
Lemma free_svar_subst_fresh phi psi X:
svar_is_fresh_in X phi →
phi^[[svar: X ↦ psi]] = phi.
Lemma wfc_mu_free_svar_subst level ϕ ψ X:
well_formed_closed_mu_aux ϕ level →
well_formed_closed_mu_aux ψ level →
well_formed_closed_mu_aux (ϕ^[[svar: X ↦ ψ]]) level = true.
Lemma wfc_ex_free_svar_subst level ϕ ψ X:
well_formed_closed_ex_aux ϕ level →
well_formed_closed_ex_aux ψ level →
well_formed_closed_ex_aux (ϕ^[[svar: X ↦ ψ]]) level = true.
Lemma wfc_ex_free_evar_subst_2 level ϕ ψ x:
well_formed_closed_ex_aux ϕ level →
well_formed_closed_ex_aux ψ level →
well_formed_closed_ex_aux (ϕ^[[evar: x ↦ ψ]]) level = true.
Lemma wfc_mu_free_evar_subst level ϕ ψ x:
well_formed_closed_mu_aux ϕ level →
well_formed_closed_mu_aux ψ level →
well_formed_closed_mu_aux (ϕ^[[evar: x ↦ ψ]]) level = true.
Lemma wf_evar_open_from_wf_ex x ϕ:
well_formed (patt_exists ϕ) →
well_formed (ϕ^{evar: 0 ↦ x}).
Definition bcmcloseex
(l : list (prod db_index evar))
(ϕ : Pattern) : Pattern
:= fold_left (λ ϕ' p, ϕ'^{evar: p.1 ↦ p.2}) l ϕ.
Lemma bcmcloseex_append (l₁ l₂ : list (prod db_index evar)) (ϕ : Pattern) :
bcmcloseex (l₁ ++ l₂) ϕ = bcmcloseex l₂ (bcmcloseex l₁ ϕ).
(*
Lemma bmcloseex_wfcex
{Σ : Signature}
(l : list (prod db_index evar))
(ϕ : Pattern)
: well_formed_closed_ex_aux ϕ from ->
(bcmcloseex from l ϕ) = ϕ.
Proof.
intros H.
induction l.
{ reflexivity. }
{ simpl. rewrite IHl. by rewrite evar_open_not_occur. }
Qed.
*)
Lemma bcmcloseex_bott
(l : list (prod db_index evar))
: bcmcloseex l patt_bott = patt_bott.
Lemma bcmcloseex_sym
(l : list (prod db_index evar))
(s : symbols)
: bcmcloseex l (patt_sym s) = (patt_sym s).
Lemma bcmcloseex_imp
(l : list (prod db_index evar))
(p q : Pattern)
: bcmcloseex l (patt_imp p q) = patt_imp (bcmcloseex l p) (bcmcloseex l q).
Lemma bcmcloseex_app
(l : list (prod db_index evar))
(p q : Pattern)
: bcmcloseex l (patt_app p q) = patt_app (bcmcloseex l p) (bcmcloseex l q).
Lemma bcmcloseex_ex
(l : list (prod db_index evar))
(q : Pattern)
: bcmcloseex l (patt_exists q) = patt_exists (bcmcloseex (map (λ p, (S p.1,p.2)) l) q).
Lemma bcmcloseex_mu
(l : list (prod db_index evar))
(q : Pattern)
: bcmcloseex l (patt_mu q) = patt_mu (bcmcloseex l q).
Lemma wfc_ex_aux_S_bevar_subst_fe k ϕ x:
well_formed_closed_ex_aux ϕ^[evar:k↦patt_free_evar x] k = true →
well_formed_closed_ex_aux ϕ (S k) = true.
Lemma wfc_ex_aux_evar_open_gt dbi x k ϕ:
k > dbi →
well_formed_closed_ex_aux (ϕ^{evar: dbi ↦ x}) k →
well_formed_closed_ex_aux ϕ (S k).
Lemma wfc_ex_aux_evar_open_lt dbi x k ϕ:
k < dbi →
well_formed_closed_ex_aux (ϕ^{evar: dbi ↦ x}) k = true →
well_formed_closed_ex_aux ϕ (S dbi) = true.
Lemma evar_open_twice_not_occur n x y ϕ:
bevar_occur ϕ n = false →
ϕ^{evar: n ↦ x}^{evar: n ↦ y} = ϕ^{evar: S n ↦ y}^{evar: n ↦ x}.
Lemma wfc_ex_aux_bcmcloseex l k ϕ:
Forall (λ p : nat × evar, p.1 ≤ k) l →
well_formed_closed_ex_aux (bcmcloseex l (patt_exists ϕ)) k = true →
well_formed_closed_ex_aux (bcmcloseex (map (λ p : nat × evar, (S p.1, p.2)) l) ϕ) (S k) = true.
Lemma free_svars_free_evar_subst ϕ x ψ:
free_svars (ϕ^[[evar: x ↦ ψ]]) ⊆ free_svars ϕ ∪ free_svars ψ.
Lemma no_neg_occ_quan_impl_no_neg_occ x n1 n2 ϕ:
no_negative_occurrence_db_b n1 (ϕ^{{evar: x ↦ n2}}) = true →
no_negative_occurrence_db_b n1 ϕ = true
with no_pos_occ_quan_impl_no_pos_occ x n1 n2 ϕ:
no_positive_occurrence_db_b n1 (ϕ^{{evar: x ↦ n2}}) = true →
no_positive_occurrence_db_b n1 ϕ = true.
Lemma wfp_evar_quan_impl_wfp x n ϕ:
well_formed_positive (ϕ^{{evar: x ↦ n}}) = true →
well_formed_positive ϕ.
Lemma wfp_evar_quan x n ϕ:
well_formed_positive (ϕ^{{evar: x ↦ n}}) = well_formed_positive ϕ.
Lemma wfcmu_evar_quan_impl_wfcmu x n dbi ϕ:
well_formed_closed_mu_aux (ϕ^{{evar: x ↦ n}}) dbi = true →
well_formed_closed_mu_aux ϕ dbi.
Lemma wfcmu_evar_quan x n dbi ϕ:
well_formed_closed_mu_aux (ϕ^{{evar: x ↦ n}}) dbi
= well_formed_closed_mu_aux ϕ dbi.
Lemma wfcex_evar_quan_impl_wfcex x n dbi ϕ:
well_formed_closed_ex_aux (ϕ^{{evar: x ↦ n}}) dbi = true →
well_formed_closed_ex_aux ϕ dbi.
Lemma nno_free_svar_subst dbi ϕ ψ X:
well_formed_closed_mu_aux ψ dbi →
no_negative_occurrence_db_b dbi (ϕ^[[svar: X ↦ ψ]])
= no_negative_occurrence_db_b dbi ϕ
with npo_free_svar_subst dbi ϕ ψ X:
well_formed_closed_mu_aux ψ dbi →
no_positive_occurrence_db_b dbi (ϕ^[[svar: X ↦ ψ]])
= no_positive_occurrence_db_b dbi ϕ.
Lemma wfp_free_svar_subst_1 ϕ ψ X:
well_formed_closed ψ = true →
well_formed_positive ψ = true →
well_formed_positive ϕ = true →
well_formed_positive (ϕ^[[svar: X ↦ ψ]]) = true.
Lemma Private_no_negative_occurrence_svar_quantify ϕ level X:
(
no_negative_occurrence_db_b level ϕ = true →
svar_has_negative_occurrence X ϕ = false →
no_negative_occurrence_db_b level (ϕ^{{svar: X ↦ level}}) = true
)
∧
(
no_positive_occurrence_db_b level ϕ = true →
svar_has_positive_occurrence X ϕ = false →
no_positive_occurrence_db_b level (ϕ^{{svar: X ↦ level}}) = true
).
Lemma no_negative_occurrence_svar_quantify ϕ level X:
no_negative_occurrence_db_b level ϕ = true →
svar_has_negative_occurrence X ϕ = false →
no_negative_occurrence_db_b level (ϕ^{{svar: X ↦ level}}) = true.
Lemma no_positive_occurrence_svar_quantify ϕ level X:
no_positive_occurrence_db_b level ϕ = true →
svar_has_positive_occurrence X ϕ = false →
no_positive_occurrence_db_b level (ϕ^{{svar: X ↦ level}}) = true.
Lemma no_negative_occurrence_svar_quantify_2 X dbi1 dbi2 ϕ:
dbi1 ≠ dbi2 →
no_negative_occurrence_db_b dbi1 (ϕ^{{svar: X ↦ dbi2}}) = no_negative_occurrence_db_b dbi1 ϕ
with no_positive_occurrence_svar_quantify_2 X dbi1 dbi2 ϕ:
dbi1 ≠ dbi2 →
no_positive_occurrence_db_b dbi1 (ϕ^{{svar: X ↦ dbi2}}) = no_positive_occurrence_db_b dbi1 ϕ.
Lemma well_formed_positive_svar_quantify X dbi ϕ:
well_formed_positive ϕ →
well_formed_positive (ϕ^{{svar: X ↦ dbi}}) = true.
Lemma free_evar_subst_bevar_subst φ ψ η x n :
well_formed_closed_ex_aux ψ n →
φ^[[evar:x ↦ ψ]]^[evar:n ↦ η^[[evar:x ↦ ψ]]] =
φ^[evar:n ↦ η]^[[evar:x ↦ ψ]].
Corollary free_evar_subst_bevar_subst_fresh φ ψ η x n :
well_formed_closed_ex_aux ψ n →
x ∉ free_evars η →
φ^[[evar:x ↦ ψ]]^[evar:n ↦ η] =
φ^[evar:n ↦ η]^[[evar:x ↦ ψ]].
Lemma free_svar_subst_bsvar_subst φ ψ η X n :
well_formed_closed_mu_aux ψ n →
φ^[[svar:X ↦ ψ]]^[svar:n ↦ η^[[svar:X ↦ ψ]]] =
φ^[svar:n ↦ η]^[[svar:X ↦ ψ]].
Corollary free_evar_subst_bsvar_subst_fresh φ ψ η X n :
well_formed_closed_mu_aux ψ n →
X ∉ free_svars η →
φ^[[svar:X ↦ ψ]]^[svar:n ↦ η] =
φ^[svar:n ↦ η]^[[svar:X ↦ ψ]].
Lemma subst_svar_evar_svar ϕ x ψ n :
x ∉ free_evars ϕ →
ϕ^[svar:n↦patt_free_evar x]^[[evar:x↦ψ]] = ϕ^[svar:n↦ψ].
Lemma no_neg_svar_subst ϕ x n :
x ∉ free_evars ϕ →
no_negative_occurrence_db_b n ϕ = true →
~~evar_has_negative_occurrence x ϕ^[svar:n↦patt_free_evar x]
with
no_pos_svar_subst ϕ x n :
x ∉ free_evars ϕ →
no_positive_occurrence_db_b n ϕ = true →
~~evar_has_positive_occurrence x ϕ^[svar:n↦patt_free_evar x].
Theorem mu_free_evar_quantify:
∀ {Σ : Signature} (p : Pattern) (x : evar) (n : db_index),
mu_free p = mu_free (p^{{evar:x↦n}}).
Lemma free_evar_subst_id :
∀ φ x, φ^[[evar: x ↦ patt_free_evar x]] = φ.
Lemma free_evar_subst_chain :
∀ φ x y ψ,
y ∉ free_evars φ →
φ^[[evar: x ↦ patt_free_evar y]]^[[evar:y ↦ ψ]] =
φ^[[evar: x ↦ ψ]].
Lemma patt_free_evar_subst : ∀ x φ, (patt_free_evar x)^[[evar: x ↦ φ]] = φ.
Lemma mu_free_free_evar_subst :
∀ φ ψ x,
mu_free φ → mu_free ψ →
mu_free (free_evar_subst ψ x φ).
(* Same proof as `bevar_subst_evar_quantify_free_evar`, *)
(* but more general statement. *)
Lemma bevar_subst_evar_quantify x p dbi ϕ:
well_formed_closed_ex_aux ϕ dbi →
(ϕ^{{evar: x ↦ dbi}})^[evar: dbi ↦ p] = ϕ^[[evar: x ↦ p]].
End subst.
(*
[export] Hint Resolve wfc_mu_free_svar_subst : core. export
Hint Resolve wfc_mu_free_svar_subst : core.
[export] Hint Resolve wfc_ex_free_evar_subst_2 : core. *)
Section subst.
Context {Σ : Signature}.
(* There are two substitution operations over patterns, bevar_subst and bsvar_subst. *)
(* substitute bound variable x for psi in phi *)
Fixpoint bevar_subst (psi : Pattern) (x : db_index) (phi : Pattern) :=
match phi with
| patt_free_evar x' ⇒ patt_free_evar x'
| patt_free_svar x' ⇒ patt_free_svar x'
| patt_bound_evar n ⇒ match compare_nat n x with
| Nat_less _ _ _ ⇒ patt_bound_evar n
| Nat_equal _ _ _ ⇒ psi
| Nat_greater _ _ _ ⇒ patt_bound_evar (Nat.pred n)
end
| patt_bound_svar n ⇒ patt_bound_svar n
| patt_sym sigma ⇒ patt_sym sigma
| patt_app phi1 phi2 ⇒ patt_app (bevar_subst psi x phi1)
(bevar_subst psi x phi2)
| patt_bott ⇒ patt_bott
| patt_imp phi1 phi2 ⇒ patt_imp (bevar_subst psi x phi1) (bevar_subst psi x phi2)
| patt_exists phi' ⇒ patt_exists (bevar_subst psi (S x) phi')
| patt_mu phi' ⇒ patt_mu (bevar_subst psi x phi')
end.
Fixpoint bsvar_subst (psi : Pattern) (x : db_index) (phi : Pattern) :=
match phi with
| patt_free_evar x' ⇒ patt_free_evar x'
| patt_free_svar x' ⇒ patt_free_svar x'
| patt_bound_evar n ⇒ patt_bound_evar n
| patt_bound_svar n ⇒ match compare_nat n x with
| Nat_less _ _ _ ⇒ patt_bound_svar n
| Nat_equal _ _ _ ⇒ psi
| Nat_greater _ _ _ ⇒ patt_bound_svar (Nat.pred n)
end
| patt_sym sigma ⇒ patt_sym sigma
| patt_app phi1 phi2 ⇒ patt_app (bsvar_subst psi x phi1)
(bsvar_subst psi x phi2)
| patt_bott ⇒ patt_bott
| patt_imp phi1 phi2 ⇒ patt_imp (bsvar_subst psi x phi1) (bsvar_subst psi x phi2)
| patt_exists phi' ⇒ patt_exists (bsvar_subst psi x phi')
| patt_mu phi' ⇒ patt_mu (bsvar_subst psi(S x) phi')
end.
Fixpoint bevar_occur (phi : Pattern) (x : db_index) : bool :=
match phi with
| patt_free_evar x' ⇒ false
| patt_free_svar x' ⇒ false
| patt_bound_evar n ⇒ if decide (n = x) is left _ then true else false
| patt_bound_svar n ⇒ false
| patt_sym sigma ⇒ false
| patt_app phi1 phi2 ⇒ orb (bevar_occur phi1 x)
(bevar_occur phi2 x)
| patt_bott ⇒ false
| patt_imp phi1 phi2 ⇒ orb (bevar_occur phi1 x) (bevar_occur phi2 x)
| patt_exists phi' ⇒ bevar_occur phi' (S x)
| patt_mu phi' ⇒ bevar_occur phi' x
end.
Fixpoint bsvar_occur (phi : Pattern) (x : db_index) : bool :=
match phi with
| patt_free_evar x' ⇒ false
| patt_free_svar x' ⇒ false
| patt_bound_evar n ⇒ false
| patt_bound_svar n ⇒ if (decide (n = x)) is left _ then true else false
| patt_sym sigma ⇒ false
| patt_app phi1 phi2 ⇒ orb (bsvar_occur phi1 x)
(bsvar_occur phi2 x)
| patt_bott ⇒ false
| patt_imp phi1 phi2 ⇒ orb (bsvar_occur phi1 x) (bsvar_occur phi2 x)
| patt_exists phi' ⇒ bsvar_occur phi' x
| patt_mu phi' ⇒ bsvar_occur phi' (S x)
end.
(* substitute free element variable x for psi in phi *)
Fixpoint free_evar_subst (psi : Pattern) (x : evar) (phi : Pattern) :=
match phi with
| patt_free_evar x' ⇒ if decide (x = x') is left _ then psi else patt_free_evar x'
| patt_free_svar X ⇒ patt_free_svar X
| patt_bound_evar x' ⇒ patt_bound_evar x'
| patt_bound_svar X ⇒ patt_bound_svar X
| patt_sym sigma ⇒ patt_sym sigma
| patt_app phi1 phi2 ⇒ patt_app (free_evar_subst psi x phi1)
(free_evar_subst psi x phi2)
| patt_bott ⇒ patt_bott
| patt_imp phi1 phi2 ⇒ patt_imp (free_evar_subst psi x phi1) (free_evar_subst psi x phi2)
| patt_exists phi' ⇒ patt_exists (free_evar_subst psi x phi')
| patt_mu phi' ⇒ patt_mu (free_evar_subst psi x phi')
end.
(* substitute free set variable X for psi in phi *)
Fixpoint free_svar_subst (psi : Pattern) (X : svar) (phi : Pattern) : Pattern :=
match phi with
| patt_free_evar x ⇒ patt_free_evar x
| patt_free_svar X' ⇒ if decide (X = X') is left _ then psi else patt_free_svar X'
| patt_bound_evar x ⇒ patt_bound_evar x
| patt_bound_svar X' ⇒ patt_bound_svar X'
| patt_sym sigma ⇒ patt_sym sigma
| patt_app phi1 phi2 ⇒ patt_app (free_svar_subst psi X phi1)
(free_svar_subst psi X phi2)
| patt_bott ⇒ patt_bott
| patt_imp phi1 phi2 ⇒ patt_imp (free_svar_subst psi X phi1) (free_svar_subst psi X phi2)
| patt_exists phi' ⇒ patt_exists (free_svar_subst psi X phi')
| patt_mu phi' ⇒ patt_mu (free_svar_subst psi X phi')
end.
(* instantiate exists x. p or mu x. p with psi for p *)
Definition instantiate (phi psi : Pattern) :=
match phi with
| patt_exists phi' ⇒ bevar_subst psi 0 phi'
| patt_mu phi' ⇒ bsvar_subst psi 0 phi'
| _ ⇒ phi
end.
(* replace element variable x with de Bruijn index level *)
Fixpoint evar_quantify (x : evar) (level : db_index)
(p : Pattern) : Pattern :=
match p with
| patt_free_evar x' ⇒ if decide (x = x') is left _ then patt_bound_evar level else patt_free_evar x'
| patt_free_svar x' ⇒ patt_free_svar x'
| patt_bound_evar x' ⇒ patt_bound_evar x'
| patt_bound_svar X ⇒ patt_bound_svar X
| patt_sym s ⇒ patt_sym s
| patt_app ls rs ⇒ patt_app (evar_quantify x level ls) (evar_quantify x level rs)
| patt_bott ⇒ patt_bott
| patt_imp ls rs ⇒ patt_imp (evar_quantify x level ls) (evar_quantify x level rs)
| patt_exists p' ⇒ patt_exists (evar_quantify x (S level) p')
| patt_mu p' ⇒ patt_mu (evar_quantify x level p')
end.
(* replace set variable X with de Bruijn index level *)
Fixpoint svar_quantify (X : svar) (level : db_index)
(p : Pattern) : Pattern :=
match p with
| patt_free_evar x' ⇒ patt_free_evar x'
| patt_free_svar X' ⇒ if decide (X = X') is left _ then patt_bound_svar level else patt_free_svar X'
| patt_bound_evar x' ⇒ patt_bound_evar x'
| patt_bound_svar X ⇒ patt_bound_svar X
| patt_sym s ⇒ patt_sym s
| patt_app ls rs ⇒ patt_app (svar_quantify X level ls) (svar_quantify X level rs)
| patt_bott ⇒ patt_bott
| patt_imp ls rs ⇒ patt_imp (svar_quantify X level ls) (svar_quantify X level rs)
| patt_exists p' ⇒ patt_exists (svar_quantify X level p')
| patt_mu p' ⇒ patt_mu (svar_quantify X (S level) p')
end.
(* replace de Bruijn index k with element variable n *)
Definition evar_open (x : evar) (k : db_index) (p : Pattern) : Pattern :=
bevar_subst (patt_free_evar x) k p.
(* replace de Bruijn index k with set variable n *)
Definition svar_open (X : svar) (k : db_index) (p : Pattern) : Pattern :=
bsvar_subst (patt_free_svar X) k p.
End subst.
Module Notations.
Notation "e ^[ 'evar:' dbi ↦ e' ]" := (bevar_subst e' dbi e) (at level 2, e' at level 200, left associativity,
format "e ^[ 'evar:' dbi ↦ e' ]" ) : ml_scope.
Notation "e ^[ 'svar:' dbi ↦ e' ]" := (bsvar_subst e' dbi e) (at level 2, e' at level 200, left associativity,
format "e ^[ 'svar:' dbi ↦ e' ]" ) : ml_scope.
Notation "e ^[[ 'evar:' x ↦ e' ]]" := (free_evar_subst e' x e) (at level 2, e' at level 200, left associativity,
format "e ^[[ 'evar:' x ↦ e' ]]" ) : ml_scope.
Notation "e ^[[ 'svar:' X ↦ e' ]]" := (free_svar_subst e' X e) (at level 2, e' at level 200, left associativity,
format "e ^[[ 'svar:' X ↦ e' ]]" ) : ml_scope.
Notation "e ^{ 'evar:' db ↦ x }" := (evar_open x db e) (at level 2, x at level 200, left associativity,
format "e ^{ 'evar:' db ↦ x }" ) : ml_scope.
Notation "e ^{ 'svar:' db ↦ x }" := (svar_open x db e) (at level 2, x at level 200, left associativity,
format "e ^{ 'svar:' db ↦ x }" ) : ml_scope.
Notation "e ^{{ 'evar:' x ↦ db }}" := (evar_quantify x db e) (at level 2, x at level 200, left associativity,
format "e ^{{ 'evar:' x ↦ db }}" ) : ml_scope.
Notation "e ^{{ 'svar:' x ↦ db }}" := (svar_quantify x db e) (at level 2, x at level 200, left associativity,
format "e ^{{ 'svar:' x ↦ db }}" ) : ml_scope.
Notation "e ^[ e' ]" := (instantiate e e') (at level 2, e' at level 200, left associativity, format "e ^[ e' ]") : ml_scope.
End Notations.
Section subst.
Import Notations.
Open Scope ml_scope.
Context {Σ : Signature}.
Definition exists_quantify (x : evar)
(p : Pattern) : Pattern :=
patt_exists (p^{{evar: x ↦ 0}}).
Definition mu_quantify (X : svar)
(p : Pattern) : Pattern :=
patt_mu (p^{{svar: X ↦ 0}}).
Lemma evar_open_size :
∀ (k : db_index) (n : evar) (p : Pattern),
pat_size p = pat_size (p^{evar: k ↦ n}).
Lemma svar_open_size :
∀ (k : db_index) (n : svar) (p : Pattern),
pat_size p = pat_size (p^{svar: k ↦ n}).
(* From https://www.chargueraud.org/research/2009/ln/main.pdf in 3.3 (body def.) *)
Definition wfc_body_ex phi := ∀ x,
¬ elem_of x (free_evars phi) → well_formed_closed (phi^{evar: 0 ↦ x}) = true.
Lemma positive_negative_occurrence_evar_open_and : ∀ (phi : Pattern) (db1 db2 : db_index) (x : evar),
(*le db1 db2 ->*)
(no_positive_occurrence_db_b db1 phi → no_positive_occurrence_db_b db1 (phi^{evar: db2 ↦ x}))
∧ (no_negative_occurrence_db_b db1 phi → no_negative_occurrence_db_b db1 (phi^{evar: db2 ↦ x})).
Lemma no_negative_occurrence_evar_open phi db1 db2 x:
no_negative_occurrence_db_b db1 phi = true →
no_negative_occurrence_db_b db1 (phi^{evar: db2 ↦ x}) = true.
Lemma no_positive_occurrence_evar_open phi db1 db2 x:
no_positive_occurrence_db_b db1 phi = true →
no_positive_occurrence_db_b db1 (phi^{evar: db2 ↦ x}) = true.
(*Helper lemma for wf_body_to_wf_ex*)
Lemma wfc_ex_aux_body_ex_imp2:
∀ phi n x,
well_formed_closed_ex_aux (phi^{evar: n ↦ x}) n = true
→
well_formed_closed_ex_aux phi (S n) = true.
(*Helper lemma for wf_body_to_wf_ex*)
Lemma wfc_mu_aux_body_ex_imp2:
∀ phi n n' x,
well_formed_closed_mu_aux (phi^{evar: n ↦ x}) n' = true
→
well_formed_closed_mu_aux phi n' = true.
Lemma wfc_ex_aux_body_mu_imp2:
∀ phi n n' X,
well_formed_closed_ex_aux (phi^{svar: n ↦ X}) n' = true
→
well_formed_closed_ex_aux phi n' = true.
Lemma wfc_mu_aux_body_mu_imp2:
∀ phi n X,
well_formed_closed_mu_aux (phi^{svar: n ↦ X}) n = true
→
well_formed_closed_mu_aux phi (S n) = true.
Lemma wfc_ex_aux_bevar_subst :
∀ phi psi n,
well_formed_closed_ex_aux phi (S n) = true
→ well_formed_closed_ex_aux psi n = true
→ well_formed_closed_ex_aux (phi^[evar: n ↦ psi]) n = true.
Lemma wfc_mu_aux_bevar_subst :
∀ phi psi n n',
well_formed_closed_mu_aux phi n' = true
→ well_formed_closed_mu_aux psi n' = true
→ well_formed_closed_mu_aux (phi^[evar: n ↦ psi]) n' = true.
Lemma wfc_ex_aux_bsvar_subst :
∀ phi psi n n',
well_formed_closed_ex_aux phi n = true
→ well_formed_closed_ex_aux psi n = true
→ well_formed_closed_ex_aux (phi^[svar: n' ↦ psi]) n = true.
Lemma wfc_mu_aux_bsvar_subst :
∀ phi psi n',
well_formed_closed_mu_aux phi (S n') = true
→ well_formed_closed_mu_aux psi n' = true
→ well_formed_closed_mu_aux (phi^[svar: n' ↦ psi]) n' = true.
(*Helper lemma for wf_ex_to_wf_body *)
Corollary wfc_ex_aux_body_ex_imp1:
∀ phi n x,
well_formed_closed_ex_aux phi (S n) = true
→
well_formed_closed_ex_aux (phi^{evar: n ↦ x}) n = true.
Corollary wfc_mu_aux_body_ex_imp1:
∀ phi n n' x,
well_formed_closed_mu_aux phi n' = true
→
well_formed_closed_mu_aux (phi^{evar: n ↦ x}) n' = true.
Corollary wfc_ex_aux_body_mu_imp1:
∀ phi n n' X,
well_formed_closed_ex_aux phi n' = true
→
well_formed_closed_ex_aux (phi^{svar: n ↦ X}) n' = true.
Corollary wfc_mu_aux_body_mu_imp1:
∀ phi n X,
well_formed_closed_mu_aux phi (S n) = true
→
well_formed_closed_mu_aux (phi^{svar: n ↦ X}) n = true.
Lemma wfc_mu_aux_bsvar_subst_le :
∀ phi psi n n', n' ≤ n →
well_formed_closed_mu_aux phi (S n) = true →
well_formed_closed_mu_aux psi n
→
well_formed_closed_mu_aux (phi^[svar:n' ↦ psi]) n = true.
Lemma wfc_ex_aux_bsvar_subst_le:
∀ phi psi n n', n' ≤ n →
well_formed_closed_ex_aux phi (S n) = true →
well_formed_closed_ex_aux psi n = true
→
well_formed_closed_ex_aux (phi^[evar:n'↦psi]) n = true.
Corollary wfc_mu_aux_body_mu_imp3:
∀ phi n n' X, n' ≤ n →
well_formed_closed_mu_aux phi (S n) = true
→
well_formed_closed_mu_aux (phi^{svar: n' ↦ X}) n = true.
Corollary wfc_mu_aux_body_ex_imp3:
∀ phi n n' X, n' ≤ n →
well_formed_closed_ex_aux phi (S n) = true
→
well_formed_closed_ex_aux (phi^{evar: n' ↦ X}) n = true.
Corollary wfc_ex_aux_body_iff:
∀ phi n x,
well_formed_closed_ex_aux phi (S n) = true
↔
well_formed_closed_ex_aux (phi^{evar: n ↦ x}) n = true.
Corollary wfc_mu_aux_body_iff:
∀ phi n X,
well_formed_closed_mu_aux phi (S n) = true
↔
well_formed_closed_mu_aux (phi^{svar: n ↦ X}) n = true.
(*If (ex, phi) is closed, then its body is closed too*)
Corollary wfc_ex_to_wfc_body:
∀ phi, well_formed_closed (patt_exists phi) = true → wfc_body_ex phi.
Lemma no_neg_occ_db_bevar_subst phi psi dbi1 dbi2:
well_formed_closed_mu_aux psi 0 = true →
no_negative_occurrence_db_b dbi1 phi = true →
no_negative_occurrence_db_b dbi1 (phi^[evar: dbi2 ↦ psi]) = true
with no_pos_occ_db_bevar_subst phi psi dbi1 dbi2:
well_formed_closed_mu_aux psi 0 = true →
no_positive_occurrence_db_b dbi1 phi = true →
no_positive_occurrence_db_b dbi1 (phi^[evar: dbi2 ↦ psi]) = true.
Lemma bevar_subst_positive_2 :
∀ φ ψ n,
well_formed_closed_mu_aux ψ 0 = true →
well_formed_positive φ = true →
well_formed_positive ψ = true →
well_formed_positive (φ^[evar: n ↦ ψ]) = true.
Corollary wfp_evar_open : ∀ phi x n,
well_formed_positive phi = true →
well_formed_positive (phi^{evar: n ↦ x}) = true.
(* Additional lemmas: evar_open, svar_open, freshness, well_formedness, etc. *)
(* evar_open and evar_quantify are inverses *)
Lemma evar_open_evar_quantify x n phi:
well_formed_closed_ex_aux phi n →
((phi^{{evar: x ↦ n}})^{evar: n ↦ x}) = phi.
Lemma svar_open_svar_quantify X n phi:
well_formed_closed_mu_aux phi n →
((phi^{{svar: X ↦ n}})^{svar: n ↦ X}) = phi.
Lemma evar_quantify_evar_open x n phi:
x ∉ free_evars phi → well_formed_closed_ex_aux phi (S n) →
((phi^{evar: n ↦ x})^{{evar: x ↦ n}}) = phi.
Lemma svar_quantify_svar_open X n phi:
X ∉ free_svars phi → well_formed_closed_mu_aux phi (S n) →
((phi^{svar: n ↦ X})^{{svar: X ↦ n}}) = phi.
Lemma double_evar_quantify φ : ∀ x n,
φ^{{evar: x ↦ n}}^{{evar: x ↦ n}} = φ^{{evar: x ↦ n}}.
Lemma double_svar_quantify φ : ∀ X n,
φ^{{svar: X ↦ n}}^{{svar: X ↦ n}} = φ^{{svar: X ↦ n}}.
Lemma well_formed_bevar_subst φ : ∀ ψ n m,
m ≥ n → well_formed_closed_ex_aux φ n →
(φ^[evar: m ↦ ψ]) = φ.
Lemma well_formed_bsvar_subst φ : ∀ ψ k m,
m ≥ k → well_formed_closed_mu_aux φ k →
(φ^[svar: m ↦ ψ]) = φ.
(* bevar_subst is identity if n does not occur in phi *)
Corollary bevar_subst_not_occur n ψ ϕ :
well_formed_closed_ex_aux ϕ n →
(ϕ^[evar: n ↦ ψ]) = ϕ.
(* evar_open is identity if n does not occur in phi *)
Corollary evar_open_not_occur n x ϕ :
well_formed_closed_ex_aux ϕ n →
ϕ^{evar: n ↦ x} = ϕ.
(* bsvar_subst is identity if n does not occur in phi *)
Corollary bsvar_subst_not_occur n ψ ϕ :
well_formed_closed_mu_aux ϕ n →
(ϕ^[svar: n ↦ ψ]) = ϕ.
(* evar_open is identity if n does not occur in phi *)
Corollary svar_open_not_occur n x ϕ :
well_formed_closed_mu_aux ϕ n →
ϕ^{svar: n ↦ x} = ϕ.
(* opening on closed patterns is identity *)
Lemma evar_open_closed :
∀ phi,
well_formed_closed_ex_aux phi 0 →
∀ n v,
phi^{evar: n ↦ v} = phi.
Lemma svar_open_closed :
∀ phi,
well_formed_closed_mu_aux phi 0 →
∀ n v,
phi^{svar: n ↦ v} = phi.
Lemma bevar_subst_comm_higher :
∀ phi psi1 psi2 n m,
n > m → well_formed_closed_ex_aux psi1 0 → well_formed_closed_ex_aux psi2 0 →
(phi^[evar: n ↦ psi1])^[evar: m ↦ psi2] =
(phi^[evar: m ↦ psi2])^[evar: pred n ↦ psi1].
Lemma bevar_subst_comm_lower :
∀ phi psi1 psi2 n m,
n < m → well_formed_closed_ex_aux psi1 0 → well_formed_closed_ex_aux psi2 0 →
(phi^[evar: n ↦ psi1])^[evar: m ↦ psi2] =
(phi^[evar: S m ↦ psi2])^[evar: n ↦ psi1].
Lemma bsvar_subst_comm_higher :
∀ phi psi1 psi2 n m,
n > m → well_formed_closed_mu_aux psi1 0 → well_formed_closed_mu_aux psi2 0 →
(phi^[svar: n ↦ psi1])^[svar: m ↦ psi2] =
(phi^[svar: m ↦ psi2])^[svar: pred n ↦ psi1].
Lemma bsvar_subst_comm_lower :
∀ phi psi1 psi2 n m,
n < m → well_formed_closed_mu_aux psi1 0 → well_formed_closed_mu_aux psi2 0 →
(phi^[svar: n ↦ psi1])^[svar: m ↦ psi2] =
(phi^[svar: S m ↦ psi2])^[svar: n ↦ psi1].
Corollary evar_open_comm_higher:
∀ n m,
n < m
→
∀ x y phi,
phi^{evar: m ↦ y}^{evar: n ↦ x} = phi^{evar: n ↦ x}^{evar: pred m ↦ y}.
Corollary evar_open_comm_lower:
∀ n m,
n > m
→
∀ x y phi,
phi^{evar: m ↦ y}^{evar: n ↦ x} = phi^{evar: S n ↦ x}^{evar: m ↦ y}.
Corollary svar_open_comm_higher:
∀ n m,
n < m
→
∀ X Y phi,
phi^{svar: m ↦ Y}^{svar: n ↦ X} = phi^{svar: n ↦ X}^{svar: pred m ↦ Y} .
Corollary svar_open_comm_lower:
∀ n m,
n > m
→
∀ X Y phi,
phi^{svar: m ↦ Y} ^{svar: n ↦ X} = phi^{svar: S n ↦ X} ^{svar: m ↦ Y}.
Lemma bevar_subst_bsvar_subst phi psi1 psi2 dbi1 dbi2
: well_formed_closed psi1 → well_formed_closed psi2 →
(phi^[svar: dbi1 ↦ psi1])^[evar: dbi2 ↦ psi2] =
(phi^[evar: dbi2 ↦ psi2])^[svar: dbi1 ↦ psi1].
Corollary svar_open_evar_open_comm
: ∀ (phi : Pattern) (dbi1 : db_index)(x : evar)(dbi2 : db_index)(X : svar),
phi^{svar: dbi2 ↦ X}^{evar: dbi1 ↦ x} = phi^{evar: dbi1 ↦ x}^{svar: dbi2 ↦ X} .
Lemma free_svars_evar_open : ∀ (ϕ : Pattern) (dbi :db_index) (x : evar),
free_svars ϕ^{evar: dbi ↦ x} = free_svars ϕ.
Lemma positive_negative_occurrence_db_named :
∀ (phi : Pattern) (dbi : db_index) (X : svar),
(no_positive_occurrence_db_b dbi phi →
svar_has_positive_occurrence X phi = false →
svar_has_positive_occurrence X (phi^{svar: dbi ↦ X}) = false)
∧ (no_negative_occurrence_db_b dbi phi →
svar_has_negative_occurrence X phi = false →
svar_has_negative_occurrence X (phi^{svar: dbi ↦ X}) = false).
Lemma positive_negative_occurrence_evar_open : ∀ (ϕ : Pattern) (X : svar) (dbi : db_index) (x : evar),
(svar_has_positive_occurrence X (ϕ^{evar: dbi ↦ x}) = false ↔ svar_has_positive_occurrence X ϕ = false)
∧ (svar_has_negative_occurrence X (ϕ^{evar: dbi ↦ x}) = false ↔ svar_has_negative_occurrence X ϕ = false).
Corollary positive_occurrence_evar_open : ∀ (ϕ : Pattern) (X : svar) (dbi : db_index) (x : evar),
svar_has_positive_occurrence X (ϕ^{evar: dbi ↦ x}) = false ↔ svar_has_positive_occurrence X ϕ = false.
Corollary negative_occurrence_evar_open : ∀ (ϕ : Pattern) (X : svar) (dbi : db_index) (x : evar),
svar_has_negative_occurrence X (ϕ^{evar: dbi ↦ x}) = false ↔ svar_has_negative_occurrence X ϕ = false.
Lemma positive_negative_occurrence_db_svar_open_le : ∀ (phi : Pattern) (dbi1 dbi2 : db_index) (X : svar),
dbi1 < dbi2 →
(
no_positive_occurrence_db_b dbi1 phi →
no_positive_occurrence_db_b dbi1 (phi^{svar: dbi2 ↦ X})
)
∧ (no_negative_occurrence_db_b dbi1 phi → no_negative_occurrence_db_b dbi1 (phi^{svar: dbi2 ↦ X})).
Lemma wfp_svar_open : ∀ (phi : Pattern) (dbi : db_index) (X : svar),
well_formed_positive phi = true →
well_formed_positive (phi^{svar: dbi ↦ X}) = true.
Lemma positive_negative_occurrence_named_svar_open :
∀ (phi : Pattern) (X Y : svar) (dbi : db_index),
X ≠ Y →
(
svar_has_negative_occurrence X phi = false →
svar_has_negative_occurrence X (phi^{svar: dbi ↦ Y}) = false
) ∧ (
svar_has_positive_occurrence X phi = false →
svar_has_positive_occurrence X (phi^{svar: dbi ↦ Y}) = false
).
Corollary evar_open_wfc_aux db1 db2 X phi :
db1 ≤ db2 →
well_formed_closed_ex_aux phi db1 →
phi^{evar: db2 ↦ X} = phi.
Corollary evar_open_wfc m X phi : well_formed_closed_ex_aux phi 0 → phi^{evar: m ↦ X} = phi.
Corollary svar_open_wfc_aux db1 db2 X phi :
db1 ≤ db2 →
well_formed_closed_mu_aux phi db1 →
phi^{svar: db2 ↦ X} = phi.
Corollary svar_open_wfc m X phi : well_formed_closed_mu_aux phi 0 → phi^{svar: m ↦ X} = phi.
Corollary evar_open_bsvar_subst m phi1 phi2 dbi X
: well_formed_closed phi2 →
phi1^[svar: dbi ↦ phi2]^{evar: m ↦ X}
= phi1^{evar: m ↦ X}^[svar: dbi ↦ phi2].
Corollary svar_open_bevar_subst m phi1 phi2 dbi X
: well_formed_closed phi2 →
phi1^[evar: dbi ↦ phi2]^{svar: m ↦ X}
= phi1^{svar: m ↦ X}^[evar: dbi ↦ phi2].
Corollary svar_open_bsvar_subst_higher m phi1 phi2 dbi X
: well_formed_closed phi2 →
m < dbi →
phi1^[svar: dbi ↦ phi2]^{svar: m ↦ X}
= phi1^{svar: m ↦ X}^[svar: pred dbi ↦ phi2].
Corollary svar_open_bsvar_subst_lower m phi1 phi2 dbi X
: well_formed_closed phi2 →
m > dbi →
phi1^[svar: dbi ↦ phi2]^{svar: m ↦ X}
= phi1^{svar: S m ↦ X}^[svar: dbi ↦ phi2].
Corollary evar_open_bevar_subst_higher m phi1 phi2 dbi X
: well_formed_closed_ex_aux phi2 0 →
m < dbi →
phi1^[evar: dbi ↦ phi2]^{evar: m ↦ X}
= phi1^{evar: m ↦ X}^[evar: pred dbi ↦ phi2].
Corollary evar_open_bevar_subst_lower m phi1 phi2 dbi X
: well_formed_closed phi2 →
m > dbi →
phi1^[evar: dbi ↦ phi2]^{evar: m ↦ X}
= phi1^{evar: S m ↦ X}^[evar: dbi ↦ phi2].
Lemma free_svars_bsvar_subst' :
∀ φ ψ dbi X,
(X ∈ free_svars (φ^[svar: dbi ↦ ψ])) ↔
((X ∈ (free_svars ψ) ∧ bsvar_occur φ dbi) ∨ (X ∈ (free_svars φ))).
Lemma free_evars_bsvar_subst' :
∀ φ ψ dbi x,
(x ∈ free_evars (φ^[svar: dbi ↦ ψ])) ↔
((x ∈ (free_evars ψ) ∧ bsvar_occur φ dbi) ∨ (x ∈ (free_evars φ))).
Lemma free_evars_bevar_subst' :
∀ φ ψ dbi X,
(X ∈ free_evars (φ^[evar: dbi ↦ ψ])) ↔
((X ∈ (free_evars ψ) ∧ bevar_occur φ dbi) ∨ (X ∈ (free_evars φ))).
Lemma free_svars_bsvar_subst :
∀ φ ψ dbi,
free_svars (φ^[svar: dbi ↦ ψ]) ⊆ union (free_svars ψ) (free_svars φ).
Lemma free_evars_bevar_subst :
∀ φ ψ dbi,
free_evars (φ^[evar: dbi ↦ ψ]) ⊆ union (free_evars ψ) (free_evars φ).
Lemma free_svars_svar_open'' :
∀ φ dbi X Y,
(X ∈ free_svars (φ^{svar: dbi ↦ Y})) ↔
(((X = Y) ∧ (bsvar_occur φ dbi)) ∨ (X ∈ (free_svars φ))).
Corollary free_svars_svar_open ϕ X dbi :
free_svars (ϕ^{svar: dbi ↦ X}) ⊆ union (singleton X) (free_svars ϕ).
Lemma free_evars_evar_open'' :
∀ φ dbi x y,
(x ∈ free_evars (φ^{evar: dbi ↦ y})) ↔
((x = y ∧ bevar_occur φ dbi) ∨ (x ∈ (free_evars φ))).
Corollary free_evars_evar_open ϕ x dbi :
free_evars (ϕ^{evar: dbi ↦ x}) ⊆ union (singleton x) (free_evars ϕ).
Lemma free_evars_evar_open' ϕ x dbi:
free_evars ϕ ⊆ free_evars (ϕ^{evar: dbi ↦ x}).
Lemma free_evar_subst_no_occurrence x p q:
x ∉ free_evars p →
p^[[evar:x ↦ q]] = p.
(*
Lemma Private_bsvar_occur_evar_open sz dbi1 dbi2 X phi:
size phi <= sz ->
bsvar_occur phi dbi1 = false ->
bsvar_occur (phi^{evar: dbi2 ↦ X}) dbi1 = false.
Proof.
move: phi dbi1 dbi2.
induction sz; move=> phi; destruct phi; simpl; move=> dbi1 dbi2 Hsz H; try rewrite !IHsz; auto; try lia; try apply orb_false_elim in H; firstorder.
2: { simpl. lia. }
cbn. case_match; reflexivity.
Qed. *)
Corollary bsvar_occur_evar_open dbi1 dbi2 X phi:
bsvar_occur phi dbi1 = false →
bsvar_occur (phi^{evar: dbi2 ↦ X}) dbi1 = false.
(* Lemma Private_bevar_occur_svar_open sz dbi1 dbi2 X phi:
size phi <= sz ->
bevar_occur phi dbi1 = false ->
bevar_occur (phi^{svar: dbi2 ↦ X}) dbi1 = false.
Proof.
move: phi dbi1 dbi2.
induction sz; move=> phi; destruct phi; simpl; move=> dbi1 dbi2 Hsz H; try rewrite !IHsz; auto; try lia; try apply orb_false_elim in H; firstorder.
{ cbn. case_match; reflexivity. }
simpl. lia.
Qed. *)
Corollary bevar_occur_svar_open dbi1 dbi2 X phi:
bevar_occur phi dbi1 = false →
bevar_occur (phi^{svar: dbi2 ↦ X}) dbi1 = false.
(* Lemma Private_bevar_occur_evar_open sz dbi1 dbi2 X phi:
size phi <= sz -> dbi1 < dbi2 ->
bevar_occur phi dbi1 = false ->
bevar_occur (phi^{evar: dbi2 ↦ X}) dbi1 = false.
Proof.
move: phi dbi1 dbi2.
induction sz; move=> phi; destruct phi; simpl; move=> dbi1 dbi2 Hsz H H1; try rewrite !IHsz; auto; try lia; try apply orb_false_elim in H1; firstorder.
{ cbn. repeat case_match; simpl; auto; try lia.
{ rewrite H0. reflexivity. }
{ case_match; try lia. }
}
simpl. lia.
Qed. *)
Corollary bevar_occur_evar_open dbi1 dbi2 X phi:
bevar_occur phi dbi1 = false → dbi1 < dbi2 →
bevar_occur (phi^{evar: dbi2 ↦ X}) dbi1 = false.
Lemma well_formed_positive_bevar_subst φ : ∀ n ψ,
mu_free φ →
well_formed_positive φ = true → well_formed_positive ψ = true
→
well_formed_positive (φ^[evar: n ↦ ψ]) = true.
Lemma mu_free_bevar_subst :
∀ φ ψ, mu_free φ → mu_free ψ → ∀ n, mu_free (φ^[evar: n ↦ ψ]).
Corollary mu_free_evar_open :
∀ φ, mu_free φ → ∀ x n, mu_free (φ^{evar: n ↦ x}).
Theorem evar_open_free_evar_subst_swap :
∀ φ x n ψ y, x ≠ y → well_formed ψ →
φ^[[evar: y ↦ ψ]]^{evar: n ↦ x} = φ^{evar: n ↦ x}^[[evar: y ↦ ψ]].
Lemma free_evars_free_evar_subst : ∀ φ ψ x,
free_evars (φ^[[evar: x ↦ ψ]]) ⊆ free_evars φ ∪ free_evars ψ.
Lemma bound_to_free_variable_subst :
∀ φ x m n ψ,
m > n →
well_formed_closed_ex_aux ψ 0 →
well_formed_closed_ex_aux φ m → x ∉ free_evars φ →
φ^[evar: n ↦ ψ] = φ^{evar: n ↦ x}^[[evar: x ↦ ψ]].
Lemma bound_to_free_set_variable_subst :
∀ φ X m n ψ,
m > n →
well_formed_closed_mu_aux ψ 0 →
well_formed_closed_mu_aux φ m → X ∉ free_svars φ →
φ^[svar: n ↦ ψ] = φ^{svar: n ↦ X}^[[svar: X ↦ ψ]].
Lemma evar_open_no_negative_occurrence :
∀ φ db1 db2 x,
(no_negative_occurrence_db_b db1 (φ^{evar: db2 ↦ x}) →
no_negative_occurrence_db_b db1 φ) ∧
(no_positive_occurrence_db_b db1 (φ^{evar: db2 ↦ x}) →
no_positive_occurrence_db_b db1 φ).
Lemma evar_open_positive : ∀ φ n x,
well_formed_positive (φ^{evar: n ↦ x}) = true →
well_formed_positive φ = true.
Lemma bevar_subst_closed_mu :
∀ φ ψ n m,
well_formed_closed_mu_aux φ m = true →
well_formed_closed_mu_aux ψ m = true
→
well_formed_closed_mu_aux (φ^[evar: n ↦ ψ]) m = true.
Lemma bevar_subst_closed_ex :
∀ φ ψ n,
well_formed_closed_ex_aux φ (S n) = true →
well_formed_closed_ex_aux ψ n = true
→
well_formed_closed_ex_aux (φ^[evar: n ↦ ψ]) n = true.
Lemma bevar_subst_positive :
∀ φ ψ n, mu_free φ →
well_formed_positive φ = true → well_formed_positive ψ = true
→
well_formed_positive (φ^[evar: n ↦ ψ]) = true.
Theorem evar_quantify_closed_ex :
∀ φ x n, well_formed_closed_ex_aux φ n →
well_formed_closed_ex_aux (φ^{{evar: x ↦ n}}) (S n) = true.
Theorem svar_quantify_closed_mu :
∀ φ X n, well_formed_closed_mu_aux φ n →
well_formed_closed_mu_aux (φ^{{svar: X ↦ n}}) (S n) = true.
Theorem evar_quantify_closed_mu :
∀ φ x n m, well_formed_closed_mu_aux φ m →
well_formed_closed_mu_aux (φ^{{evar: x ↦ n}}) m = true.
Theorem svar_quantify_closed_ex :
∀ φ X n m, well_formed_closed_ex_aux φ m →
well_formed_closed_ex_aux (φ^{{svar: X ↦ n}}) m = true.
Theorem no_occ_quantify :
∀ (φ : Pattern) (db1 db2 : db_index) (x : evar),
(no_negative_occurrence_db_b db1 φ
→ no_negative_occurrence_db_b db1 (φ^{{evar: x ↦ db2}}))
∧ (no_positive_occurrence_db_b db1 φ
→ no_positive_occurrence_db_b db1 (φ^{{evar: x ↦ db2}})).
Theorem evar_quantify_positive :
∀ φ x n, well_formed_positive φ →
well_formed_positive (φ^{{evar: x ↦ n}}) = true.
Corollary evar_quantify_well_formed :
∀ φ x, well_formed φ →
well_formed (patt_exists (φ^{{evar: x ↦ 0}})) = true.
Theorem evar_quantify_no_occurrence :
∀ φ x n, x ∉ (free_evars (φ^{{evar: x ↦ n}})).
Theorem svar_quantify_not_free :
∀ φ X n, X ∉ (free_svars (φ^{{svar: X ↦ n}})).
Lemma evar_quantify_not_free_evars :
∀ φ x n,
x ∉ free_evars φ →
φ^{{evar: x ↦ n}} = φ.
Lemma wf_ex_evar_quantify x p:
well_formed p = true →
well_formed (patt_exists (p^{{evar: x ↦ 0}})) = true.
Lemma free_evars_evar_quantify x n p:
free_evars (p^{{evar: x ↦ n}}) = free_evars p ∖ {[x]}.
Lemma free_svars_svar_quantify X n p:
free_svars (p^{{svar: X ↦ n}}) = free_svars p ∖ {[X]}.
Lemma no_neg_occ_db_bsvar_subst phi psi dbi1 dbi2:
well_formed_closed_mu_aux psi 0 = true → dbi1 < dbi2 →
(no_negative_occurrence_db_b dbi1 phi = true →
no_negative_occurrence_db_b dbi1 (phi^[svar: dbi2 ↦ psi]) = true)
∧ (no_positive_occurrence_db_b dbi1 phi = true →
no_positive_occurrence_db_b dbi1 (phi^[svar: dbi2 ↦ psi]) = true).
Lemma Private_wfp_bsvar_subst (phi psi : Pattern) (n : nat) :
well_formed_positive psi →
well_formed_closed_mu_aux psi 0 →
well_formed_positive phi →
(
no_negative_occurrence_db_b n phi →
well_formed_positive (phi^[svar: n ↦ psi]) )
∧ (no_positive_occurrence_db_b n phi →
∀ phi',
well_formed_positive phi' →
well_formed_positive (patt_imp (phi^[svar: n ↦ psi]) phi')
)
.
Corollary wfp_bsvar_subst (phi psi : Pattern) :
well_formed_positive (patt_mu phi) →
well_formed_positive psi →
well_formed_closed_mu_aux psi 0 →
well_formed_positive (phi^[svar: 0 ↦ psi]).
Lemma bevar_subst_evar_quantify_free_evar x dbi ϕ:
well_formed_closed_ex_aux ϕ dbi →
(ϕ^{{evar: x ↦ dbi}})^[evar: dbi ↦ patt_free_evar x] = ϕ.
Lemma bsvar_subst_svar_quantify_free_svar X dbi ϕ:
well_formed_closed_mu_aux ϕ dbi →
(ϕ^{{svar: X ↦ dbi}})^[svar: dbi ↦ (patt_free_svar X)] = ϕ.
Lemma free_svar_subst_fresh phi psi X:
svar_is_fresh_in X phi →
phi^[[svar: X ↦ psi]] = phi.
Lemma wfc_mu_free_svar_subst level ϕ ψ X:
well_formed_closed_mu_aux ϕ level →
well_formed_closed_mu_aux ψ level →
well_formed_closed_mu_aux (ϕ^[[svar: X ↦ ψ]]) level = true.
Lemma wfc_ex_free_svar_subst level ϕ ψ X:
well_formed_closed_ex_aux ϕ level →
well_formed_closed_ex_aux ψ level →
well_formed_closed_ex_aux (ϕ^[[svar: X ↦ ψ]]) level = true.
Lemma wfc_ex_free_evar_subst_2 level ϕ ψ x:
well_formed_closed_ex_aux ϕ level →
well_formed_closed_ex_aux ψ level →
well_formed_closed_ex_aux (ϕ^[[evar: x ↦ ψ]]) level = true.
Lemma wfc_mu_free_evar_subst level ϕ ψ x:
well_formed_closed_mu_aux ϕ level →
well_formed_closed_mu_aux ψ level →
well_formed_closed_mu_aux (ϕ^[[evar: x ↦ ψ]]) level = true.
Lemma wf_evar_open_from_wf_ex x ϕ:
well_formed (patt_exists ϕ) →
well_formed (ϕ^{evar: 0 ↦ x}).
Definition bcmcloseex
(l : list (prod db_index evar))
(ϕ : Pattern) : Pattern
:= fold_left (λ ϕ' p, ϕ'^{evar: p.1 ↦ p.2}) l ϕ.
Lemma bcmcloseex_append (l₁ l₂ : list (prod db_index evar)) (ϕ : Pattern) :
bcmcloseex (l₁ ++ l₂) ϕ = bcmcloseex l₂ (bcmcloseex l₁ ϕ).
(*
Lemma bmcloseex_wfcex
{Σ : Signature}
(l : list (prod db_index evar))
(ϕ : Pattern)
: well_formed_closed_ex_aux ϕ from ->
(bcmcloseex from l ϕ) = ϕ.
Proof.
intros H.
induction l.
{ reflexivity. }
{ simpl. rewrite IHl. by rewrite evar_open_not_occur. }
Qed.
*)
Lemma bcmcloseex_bott
(l : list (prod db_index evar))
: bcmcloseex l patt_bott = patt_bott.
Lemma bcmcloseex_sym
(l : list (prod db_index evar))
(s : symbols)
: bcmcloseex l (patt_sym s) = (patt_sym s).
Lemma bcmcloseex_imp
(l : list (prod db_index evar))
(p q : Pattern)
: bcmcloseex l (patt_imp p q) = patt_imp (bcmcloseex l p) (bcmcloseex l q).
Lemma bcmcloseex_app
(l : list (prod db_index evar))
(p q : Pattern)
: bcmcloseex l (patt_app p q) = patt_app (bcmcloseex l p) (bcmcloseex l q).
Lemma bcmcloseex_ex
(l : list (prod db_index evar))
(q : Pattern)
: bcmcloseex l (patt_exists q) = patt_exists (bcmcloseex (map (λ p, (S p.1,p.2)) l) q).
Lemma bcmcloseex_mu
(l : list (prod db_index evar))
(q : Pattern)
: bcmcloseex l (patt_mu q) = patt_mu (bcmcloseex l q).
Lemma wfc_ex_aux_S_bevar_subst_fe k ϕ x:
well_formed_closed_ex_aux ϕ^[evar:k↦patt_free_evar x] k = true →
well_formed_closed_ex_aux ϕ (S k) = true.
Lemma wfc_ex_aux_evar_open_gt dbi x k ϕ:
k > dbi →
well_formed_closed_ex_aux (ϕ^{evar: dbi ↦ x}) k →
well_formed_closed_ex_aux ϕ (S k).
Lemma wfc_ex_aux_evar_open_lt dbi x k ϕ:
k < dbi →
well_formed_closed_ex_aux (ϕ^{evar: dbi ↦ x}) k = true →
well_formed_closed_ex_aux ϕ (S dbi) = true.
Lemma evar_open_twice_not_occur n x y ϕ:
bevar_occur ϕ n = false →
ϕ^{evar: n ↦ x}^{evar: n ↦ y} = ϕ^{evar: S n ↦ y}^{evar: n ↦ x}.
Lemma wfc_ex_aux_bcmcloseex l k ϕ:
Forall (λ p : nat × evar, p.1 ≤ k) l →
well_formed_closed_ex_aux (bcmcloseex l (patt_exists ϕ)) k = true →
well_formed_closed_ex_aux (bcmcloseex (map (λ p : nat × evar, (S p.1, p.2)) l) ϕ) (S k) = true.
Lemma free_svars_free_evar_subst ϕ x ψ:
free_svars (ϕ^[[evar: x ↦ ψ]]) ⊆ free_svars ϕ ∪ free_svars ψ.
Lemma no_neg_occ_quan_impl_no_neg_occ x n1 n2 ϕ:
no_negative_occurrence_db_b n1 (ϕ^{{evar: x ↦ n2}}) = true →
no_negative_occurrence_db_b n1 ϕ = true
with no_pos_occ_quan_impl_no_pos_occ x n1 n2 ϕ:
no_positive_occurrence_db_b n1 (ϕ^{{evar: x ↦ n2}}) = true →
no_positive_occurrence_db_b n1 ϕ = true.
Lemma wfp_evar_quan_impl_wfp x n ϕ:
well_formed_positive (ϕ^{{evar: x ↦ n}}) = true →
well_formed_positive ϕ.
Lemma wfp_evar_quan x n ϕ:
well_formed_positive (ϕ^{{evar: x ↦ n}}) = well_formed_positive ϕ.
Lemma wfcmu_evar_quan_impl_wfcmu x n dbi ϕ:
well_formed_closed_mu_aux (ϕ^{{evar: x ↦ n}}) dbi = true →
well_formed_closed_mu_aux ϕ dbi.
Lemma wfcmu_evar_quan x n dbi ϕ:
well_formed_closed_mu_aux (ϕ^{{evar: x ↦ n}}) dbi
= well_formed_closed_mu_aux ϕ dbi.
Lemma wfcex_evar_quan_impl_wfcex x n dbi ϕ:
well_formed_closed_ex_aux (ϕ^{{evar: x ↦ n}}) dbi = true →
well_formed_closed_ex_aux ϕ dbi.
Lemma nno_free_svar_subst dbi ϕ ψ X:
well_formed_closed_mu_aux ψ dbi →
no_negative_occurrence_db_b dbi (ϕ^[[svar: X ↦ ψ]])
= no_negative_occurrence_db_b dbi ϕ
with npo_free_svar_subst dbi ϕ ψ X:
well_formed_closed_mu_aux ψ dbi →
no_positive_occurrence_db_b dbi (ϕ^[[svar: X ↦ ψ]])
= no_positive_occurrence_db_b dbi ϕ.
Lemma wfp_free_svar_subst_1 ϕ ψ X:
well_formed_closed ψ = true →
well_formed_positive ψ = true →
well_formed_positive ϕ = true →
well_formed_positive (ϕ^[[svar: X ↦ ψ]]) = true.
Lemma Private_no_negative_occurrence_svar_quantify ϕ level X:
(
no_negative_occurrence_db_b level ϕ = true →
svar_has_negative_occurrence X ϕ = false →
no_negative_occurrence_db_b level (ϕ^{{svar: X ↦ level}}) = true
)
∧
(
no_positive_occurrence_db_b level ϕ = true →
svar_has_positive_occurrence X ϕ = false →
no_positive_occurrence_db_b level (ϕ^{{svar: X ↦ level}}) = true
).
Lemma no_negative_occurrence_svar_quantify ϕ level X:
no_negative_occurrence_db_b level ϕ = true →
svar_has_negative_occurrence X ϕ = false →
no_negative_occurrence_db_b level (ϕ^{{svar: X ↦ level}}) = true.
Lemma no_positive_occurrence_svar_quantify ϕ level X:
no_positive_occurrence_db_b level ϕ = true →
svar_has_positive_occurrence X ϕ = false →
no_positive_occurrence_db_b level (ϕ^{{svar: X ↦ level}}) = true.
Lemma no_negative_occurrence_svar_quantify_2 X dbi1 dbi2 ϕ:
dbi1 ≠ dbi2 →
no_negative_occurrence_db_b dbi1 (ϕ^{{svar: X ↦ dbi2}}) = no_negative_occurrence_db_b dbi1 ϕ
with no_positive_occurrence_svar_quantify_2 X dbi1 dbi2 ϕ:
dbi1 ≠ dbi2 →
no_positive_occurrence_db_b dbi1 (ϕ^{{svar: X ↦ dbi2}}) = no_positive_occurrence_db_b dbi1 ϕ.
Lemma well_formed_positive_svar_quantify X dbi ϕ:
well_formed_positive ϕ →
well_formed_positive (ϕ^{{svar: X ↦ dbi}}) = true.
Lemma free_evar_subst_bevar_subst φ ψ η x n :
well_formed_closed_ex_aux ψ n →
φ^[[evar:x ↦ ψ]]^[evar:n ↦ η^[[evar:x ↦ ψ]]] =
φ^[evar:n ↦ η]^[[evar:x ↦ ψ]].
Corollary free_evar_subst_bevar_subst_fresh φ ψ η x n :
well_formed_closed_ex_aux ψ n →
x ∉ free_evars η →
φ^[[evar:x ↦ ψ]]^[evar:n ↦ η] =
φ^[evar:n ↦ η]^[[evar:x ↦ ψ]].
Lemma free_svar_subst_bsvar_subst φ ψ η X n :
well_formed_closed_mu_aux ψ n →
φ^[[svar:X ↦ ψ]]^[svar:n ↦ η^[[svar:X ↦ ψ]]] =
φ^[svar:n ↦ η]^[[svar:X ↦ ψ]].
Corollary free_evar_subst_bsvar_subst_fresh φ ψ η X n :
well_formed_closed_mu_aux ψ n →
X ∉ free_svars η →
φ^[[svar:X ↦ ψ]]^[svar:n ↦ η] =
φ^[svar:n ↦ η]^[[svar:X ↦ ψ]].
Lemma subst_svar_evar_svar ϕ x ψ n :
x ∉ free_evars ϕ →
ϕ^[svar:n↦patt_free_evar x]^[[evar:x↦ψ]] = ϕ^[svar:n↦ψ].
Lemma no_neg_svar_subst ϕ x n :
x ∉ free_evars ϕ →
no_negative_occurrence_db_b n ϕ = true →
~~evar_has_negative_occurrence x ϕ^[svar:n↦patt_free_evar x]
with
no_pos_svar_subst ϕ x n :
x ∉ free_evars ϕ →
no_positive_occurrence_db_b n ϕ = true →
~~evar_has_positive_occurrence x ϕ^[svar:n↦patt_free_evar x].
Theorem mu_free_evar_quantify:
∀ {Σ : Signature} (p : Pattern) (x : evar) (n : db_index),
mu_free p = mu_free (p^{{evar:x↦n}}).
Lemma free_evar_subst_id :
∀ φ x, φ^[[evar: x ↦ patt_free_evar x]] = φ.
Lemma free_evar_subst_chain :
∀ φ x y ψ,
y ∉ free_evars φ →
φ^[[evar: x ↦ patt_free_evar y]]^[[evar:y ↦ ψ]] =
φ^[[evar: x ↦ ψ]].
Lemma patt_free_evar_subst : ∀ x φ, (patt_free_evar x)^[[evar: x ↦ φ]] = φ.
Lemma mu_free_free_evar_subst :
∀ φ ψ x,
mu_free φ → mu_free ψ →
mu_free (free_evar_subst ψ x φ).
(* Same proof as `bevar_subst_evar_quantify_free_evar`, *)
(* but more general statement. *)
Lemma bevar_subst_evar_quantify x p dbi ϕ:
well_formed_closed_ex_aux ϕ dbi →
(ϕ^{{evar: x ↦ dbi}})^[evar: dbi ↦ p] = ϕ^[[evar: x ↦ p]].
End subst.
(*
[export] Hint Resolve wfc_mu_free_svar_subst : core. export
Hint Resolve wfc_mu_free_svar_subst : core.
[export] Hint Resolve wfc_ex_free_evar_subst_2 : core. *)
This page has been generated by coqdoc