File Syntax
From Coq Require Import Logic.Classical_Prop.
From MatchingLogic Require Export
SyntaxLemmas.PatternCtxApplicationCtx
SyntaxLemmas.FreshnessApplicationCtx
wftactics
.
Import MatchingLogic.Substitution.Notations.
Close Scope boolean_if_scope.
Section syntax.
Context {Σ : Signature}.
Open Scope ml_scope.
Inductive is_subformula_of_ind : Pattern → Pattern → Prop :=
| sub_eq ϕ₁ ϕ₂ : ϕ₁ = ϕ₂ → is_subformula_of_ind ϕ₁ ϕ₂
| sub_app_l ϕ₁ ϕ₂ ϕ₃ : is_subformula_of_ind ϕ₁ ϕ₂ → is_subformula_of_ind ϕ₁ (patt_app ϕ₂ ϕ₃)
| sub_app_r ϕ₁ ϕ₂ ϕ₃ : is_subformula_of_ind ϕ₁ ϕ₃ → is_subformula_of_ind ϕ₁ (patt_app ϕ₂ ϕ₃)
| sub_imp_l ϕ₁ ϕ₂ ϕ₃ : is_subformula_of_ind ϕ₁ ϕ₂ → is_subformula_of_ind ϕ₁ (patt_imp ϕ₂ ϕ₃)
| sub_imp_r ϕ₁ ϕ₂ ϕ₃ : is_subformula_of_ind ϕ₁ ϕ₃ → is_subformula_of_ind ϕ₁ (patt_imp ϕ₂ ϕ₃)
| sub_exists ϕ₁ ϕ₂ : is_subformula_of_ind ϕ₁ ϕ₂ → is_subformula_of_ind ϕ₁ (patt_exists ϕ₂)
| sub_mu ϕ₁ ϕ₂ : is_subformula_of_ind ϕ₁ ϕ₂ → is_subformula_of_ind ϕ₁ (patt_mu ϕ₂)
.
Fixpoint is_subformula_of ϕ₁ ϕ₂ : bool :=
(decide_rel (=) ϕ₁ ϕ₂)
|| match ϕ₂ with
| patt_app l r | patt_imp l r ⇒ is_subformula_of ϕ₁ l || is_subformula_of ϕ₁ r
| patt_exists phi | patt_mu phi ⇒ is_subformula_of ϕ₁ phi
| _ ⇒ false
end.
Lemma is_subformula_of_P ϕ₁ ϕ₂ : reflect (is_subformula_of_ind ϕ₁ ϕ₂) (is_subformula_of ϕ₁ ϕ₂).
Lemma is_subformula_of_refl ϕ:
is_subformula_of ϕ ϕ = true.
Lemma bsvar_subst_contains_subformula ϕ₁ ϕ₂ dbi :
bsvar_occur ϕ₁ dbi = true →
is_subformula_of_ind ϕ₂ (ϕ₁^[svar: dbi ↦ ϕ₂]).
Lemma bevar_subst_contains_subformula ϕ₁ ϕ₂ dbi :
bevar_occur ϕ₁ dbi = true →
is_subformula_of_ind ϕ₂ (ϕ₁^[evar: dbi ↦ ϕ₂]).
Lemma free_evars_subformula ϕ₁ ϕ₂ :
is_subformula_of_ind ϕ₁ ϕ₂ → free_evars ϕ₁ ⊆ free_evars ϕ₂.
Corollary evar_fresh_in_subformula x ϕ₁ ϕ₂ :
is_subformula_of_ind ϕ₁ ϕ₂ →
evar_is_fresh_in x ϕ₂ →
evar_is_fresh_in x ϕ₁.
Corollary evar_fresh_in_subformula' x ϕ₁ ϕ₂ :
is_subformula_of ϕ₁ ϕ₂ →
evar_is_fresh_in x ϕ₂ →
evar_is_fresh_in x ϕ₁.
Lemma free_svars_subformula ϕ₁ ϕ₂ :
is_subformula_of_ind ϕ₁ ϕ₂ → free_svars ϕ₁ ⊆ free_svars ϕ₂.
Corollary svar_fresh_in_subformula x ϕ₁ ϕ₂ :
is_subformula_of_ind ϕ₁ ϕ₂ →
svar_is_fresh_in x ϕ₂ →
svar_is_fresh_in x ϕ₁.
Lemma free_evars_bsvar_subst ϕ₁ ϕ₂ dbi:
free_evars (ϕ₁^[svar: dbi ↦ ϕ₂]) ⊆ free_evars ϕ₁ ∪ free_evars ϕ₂.
Lemma free_svars_bevar_subst ϕ₁ ϕ₂ dbi:
free_svars (ϕ₁^[evar: dbi ↦ ϕ₂]) ⊆ free_svars ϕ₁ ∪ free_svars ϕ₂.
Lemma free_evars_bsvar_subst_1 ϕ₁ ϕ₂ dbi:
free_evars ϕ₁ ⊆ free_evars (ϕ₁^[svar: dbi ↦ ϕ₂]).
Lemma free_svars_bevar_subst_1 ϕ₁ ϕ₂ dbi:
free_svars ϕ₁ ⊆ free_svars (ϕ₁^[evar: dbi ↦ ϕ₂]).
Corollary free_evars_bsvar_subst_eq ϕ₁ ϕ₂ dbi:
bsvar_occur ϕ₁ dbi →
free_evars (ϕ₁^[svar: dbi ↦ ϕ₂]) = free_evars ϕ₁ ∪ free_evars ϕ₂.
Corollary free_svars_bevar_subst_eq ϕ₁ ϕ₂ dbi:
bevar_occur ϕ₁ dbi →
free_svars (ϕ₁^[evar: dbi ↦ ϕ₂]) = free_svars ϕ₁ ∪ free_svars ϕ₂.
Lemma wfc_mu_aux_implies_not_bsvar_occur phi ns :
well_formed_closed_mu_aux phi ns →
bsvar_occur phi ns = false.
Lemma wfc_ex_aux_implies_not_bevar_occur phi ne :
well_formed_closed_ex_aux phi ne →
bevar_occur phi ne = false.
Corollary wfc_mu_implies_not_bsvar_occur phi n :
well_formed_closed_mu_aux phi 0 →
¬ bsvar_occur phi n.
Lemma wfc_ex_implies_not_bevar_occur phi n :
well_formed_closed_ex_aux phi 0 →
bevar_occur phi n = false.
Lemma not_bsvar_occur_bsvar_subst_2 phi psi n:
well_formed_closed_mu_aux psi 0 → well_formed_closed_mu_aux phi (S n) →
bsvar_occur (phi^[svar: n ↦ psi]) n = false
.
Lemma not_bsvar_occur_bsvar_subst phi psi n:
well_formed_closed_mu_aux psi 0 → well_formed_closed_mu_aux phi n →
¬ bsvar_occur (phi^[svar: n ↦ psi]) n.
Lemma not_bsvar_occur_impl_no_neg_occ_and_no_pos_occ phi n:
¬ bsvar_occur phi n →
no_negative_occurrence_db_b n phi && no_positive_occurrence_db_b n phi.
Corollary not_bsvar_occur_impl_pos_occ_db phi n:
¬ bsvar_occur phi n →
no_positive_occurrence_db_b n phi.
Corollary not_bsvar_occur_impl_neg_occ_db phi n:
¬ bsvar_occur phi n →
no_negative_occurrence_db_b n phi.
End syntax.
Module Notations.
Export MatchingLogic.Pattern.Notations.
Export MatchingLogic.PatternContext.Notations.
End Notations.
#[export]
Hint Resolve
evar_is_fresh_in_richer
set_evar_fresh_is_fresh
set_svar_fresh_is_fresh
x_eq_fresh_impl_x_notin_free_evars
: core.
#[export]
Hint Extern 0 (is_true (@well_formed _ _)) ⇒ unfold is_true : core.
#[export]
Hint Resolve well_formed_bott : core.
#[export]
Hint Resolve well_formed_imp : core.
#[export]
Hint Resolve well_formed_app : core.
#[export]
Hint Resolve wf_sctx : core.
#[export]
Hint Resolve well_formed_ex_app : core.
#[export]
Hint Resolve well_formed_impl_well_formed_ex : core.
#[export]
Hint Resolve well_formed_free_evar_subst : core.
#[export]
Hint Resolve well_formed_free_evar_subst_0 : core.
#[export]
Hint Resolve <- evar_is_fresh_in_exists : core.
#[export]
Hint Resolve evar_is_fresh_in_evar_quantify : core.
(* Tactics for resolving goals involving sets *)
(*
eauto 5 using @sets.elem_of_union_l, @sets.elem_of_union_r with typeclass_instances.
*)
(*
eauto depth using @sets.union_subseteq_l, @sets.union_subseteq_r
with typeclass_instances.
*)
(*
[export] Hint Extern 10 (free_evars _ ⊆ free_evars _) => solve_free_evars_inclusion : core. *)
#[export]
Hint Resolve wf_imp_wfc : core.
#[export]
Hint Resolve wfc_ex_implies_not_bevar_occur : core.
Section with_signature.
Context {Σ : Signature}.
Open Scope ml_scope.
Definition evar_quantify_ctx (x : evar) (n : db_index) (C : PatternCtx) : PatternCtx :=
match decide (x = pcEvar C) with
| left _ ⇒ C
| right pf ⇒ Build_PatternCtx (pcEvar C) ((pcPattern C)^{{evar: x ↦ n}})
end.
Lemma is_linear_context_evar_quantify (x : evar) (n : db_index) (C : PatternCtx) :
is_linear_context C →
is_linear_context (evar_quantify_ctx x n C).
Definition svar_quantify_ctx (X : svar) (n : db_index) (C : PatternCtx) : PatternCtx :=
Build_PatternCtx (pcEvar C) ((pcPattern C)^{{svar: X ↦ n}}).
Lemma is_linear_context_svar_quantify (X : svar) (n : db_index) (C : PatternCtx) :
is_linear_context C →
is_linear_context (svar_quantify_ctx X n C).
Lemma svar_quantify_free_evar_subst ψ ϕ x X n:
ψ^[[evar: x ↦ ϕ]]^{{svar: X ↦ n}} =
ψ^{{svar: X ↦ n}}^[[evar: x ↦ ϕ^{{svar: X ↦ n}}]].
(* OOPS, does not hold. The problem is that free_evar_subst' does not wrap the target
in nest_mu. *)
Lemma svar_quantify_emplace X n C ϕ:
(emplace C ϕ)^{{svar: X ↦ n}} = emplace (svar_quantify_ctx X n C) (ϕ^{{svar: X ↦ n}}).
Lemma evar_quantify_subst_ctx x n AC ϕ:
x ∉ AC_free_evars AC →
(subst_ctx AC ϕ)^{{evar: x ↦ n}} = subst_ctx AC (ϕ^{{evar: x ↦ n}}).
Lemma wfp_free_svar_subst ϕ ψ X:
well_formed_closed_mu_aux ψ 0 →
well_formed_positive ψ = true →
well_formed_positive ϕ = true →
svar_has_negative_occurrence X ϕ = false →
well_formed_positive (ϕ^[[svar: X ↦ ψ]]) = true
with wfp_neg_free_svar_subst ϕ ψ X:
well_formed_closed_mu_aux ψ 0 →
well_formed_positive ψ = true →
well_formed_positive ϕ = true →
svar_has_positive_occurrence X ϕ = false →
well_formed_positive (ϕ^[[svar: X ↦ ψ]]) = true.
Lemma count_evar_occurrences_bevar_subst pcEvar ϕ ψ k:
count_evar_occurrences pcEvar ψ = 0 →
count_evar_occurrences pcEvar (ϕ^[evar: k ↦ ψ]) = count_evar_occurrences pcEvar ϕ.
Lemma count_evar_occurrences_evar_open pcEvar ϕ x:
pcEvar ≠ x →
count_evar_occurrences pcEvar (ϕ^{evar: 0 ↦ x}) = count_evar_occurrences pcEvar ϕ.
Lemma count_evar_occurrences_svar_open x dbi ϕ ψ:
count_evar_occurrences x ψ = 0 →
count_evar_occurrences x (ϕ^[svar: dbi ↦ ψ]) = count_evar_occurrences x ϕ.
Lemma free_evar_subst_bsvar_subst ϕ ψ ξ x dbi:
well_formed_closed_mu_aux ξ 0 →
evar_is_fresh_in x ψ →
(ϕ^[svar: dbi ↦ ψ])^[[evar:x ↦ ξ]]
= (ϕ^[[evar:x ↦ ξ]])^[svar: dbi ↦ ψ].
Lemma wf_svar_open_from_wf_mu X ϕ:
well_formed (patt_mu ϕ) →
well_formed (ϕ^{svar: 0 ↦ X}).
Lemma wfcex_after_subst_impl_wfcex_before ϕ ψ x dbi:
well_formed_closed_ex_aux (ϕ^[[evar:x ↦ ψ]]) dbi = true →
well_formed_closed_ex_aux ϕ dbi = true.
Lemma wfcmu_after_subst_impl_wfcmu_before ϕ ψ x dbi:
well_formed_closed_mu_aux (ϕ^[[evar:x ↦ ψ]]) dbi = true →
well_formed_closed_mu_aux ϕ dbi = true.
Lemma nno_after_subst_impl_nno_before ϕ ψ x dbi:
no_negative_occurrence_db_b dbi (ϕ^[[evar:x ↦ ψ]]) = true →
no_negative_occurrence_db_b dbi ϕ = true
with npo_after_subst_impl_npo_before ϕ ψ x dbi:
no_positive_occurrence_db_b dbi (ϕ^[[evar:x ↦ ψ]]) = true →
no_positive_occurrence_db_b dbi ϕ = true.
Lemma wfp_after_subst_impl_wfp_before ϕ ψ x:
well_formed_positive (ϕ^[[evar:x ↦ ψ]]) = true →
well_formed_positive ϕ = true.
Lemma wf_after_subst_impl_wf_before ϕ ψ x:
well_formed (ϕ^[[evar:x ↦ ψ]]) = true →
well_formed ϕ = true.
Lemma wf_emplaced_impl_wf_context (C : PatternCtx) (ψ : Pattern) :
well_formed (emplace C ψ) = true →
PC_wf C.
Global Instance evar_is_fresh_in_dec (x : evar) (p : Pattern) :
Decision (evar_is_fresh_in x p).
Definition evar_is_fresh_in_list (x : evar) (l : list Pattern) :=
Forall (evar_is_fresh_in x) l.
Global Instance evar_is_fresh_in_list_dec (x : evar) (l : list Pattern) :
Decision (evar_is_fresh_in_list x l).
Lemma evar_fresh_in_foldr x g l:
evar_is_fresh_in x (foldr patt_imp g l) ↔ evar_is_fresh_in x g ∧ evar_is_fresh_in_list x l.
Global Instance svar_is_fresh_in_dec (X : svar) (p : Pattern) :
Decision (svar_is_fresh_in X p).
Definition svar_is_fresh_in_list (X : svar) (l : list Pattern) :=
Forall (svar_is_fresh_in X) l.
Global Instance svar_is_fresh_in_list_dec (X : svar) (l : list Pattern) :
Decision (svar_is_fresh_in_list X l).
Lemma wfc_ex_lower ϕ n:
bevar_occur ϕ n = false →
well_formed_closed_ex_aux ϕ (S n) = true →
well_formed_closed_ex_aux ϕ n = true.
Lemma wfc_mu_lower ϕ n:
bsvar_occur ϕ n = false →
well_formed_closed_mu_aux ϕ (S n) = true →
well_formed_closed_mu_aux ϕ n = true.
Lemma wf_ex_quan_impl_wf (x : evar) (ϕ : Pattern):
bevar_occur ϕ 0 = false →
well_formed (exists_quantify x ϕ) = true →
well_formed ϕ = true.
Lemma bevar_occur_evar_open_2 dbi x ϕ:
well_formed_closed_ex_aux ϕ dbi →
bevar_occur (ϕ^{evar: dbi ↦ x}) dbi = false.
Lemma bsvar_occur_svar_open_2 dbi X ϕ:
well_formed_closed_mu_aux ϕ dbi →
bsvar_occur (ϕ^{svar: dbi ↦ X}) dbi = false.
Lemma svar_has_negative_occurrence_free_evar_subst
(ϕ ψ: Pattern) (x : evar) (X : svar) :
svar_is_fresh_in X ψ →
svar_has_negative_occurrence X ϕ^[[evar:x↦ψ]] = svar_has_negative_occurrence X ϕ
with svar_has_positive_occurrence_free_evar_subst
(ϕ ψ: Pattern) (x : evar) (X : svar) :
svar_is_fresh_in X ψ →
svar_has_positive_occurrence X ϕ^[[evar:x↦ψ]] = svar_has_positive_occurrence X ϕ
.
Fixpoint maximal_mu_depth_to (depth : nat) (E : evar) (ψ : Pattern) : nat :=
match ψ with
| patt_bott ⇒ 0
| patt_sym _ ⇒ 0
| patt_bound_evar _ ⇒ 0
| patt_bound_svar _ ⇒ 0
| patt_free_svar _ ⇒ 0
| patt_free_evar E' ⇒
match (decide (E' = E)) with
| left _ ⇒ depth
| right _ ⇒ 0
end
| patt_imp ψ₁ ψ₂
⇒ Nat.max
(maximal_mu_depth_to depth E ψ₁)
(maximal_mu_depth_to depth E ψ₂)
| patt_app ψ₁ ψ₂
⇒ Nat.max
(maximal_mu_depth_to depth E ψ₁)
(maximal_mu_depth_to depth E ψ₂)
| patt_exists ψ' ⇒
maximal_mu_depth_to depth E ψ'
| patt_mu ψ' ⇒
maximal_mu_depth_to (S depth) E ψ'
end.
Fixpoint maximal_mu_depth_to_sv (depth : nat) (V : svar) (ψ : Pattern) : nat :=
match ψ with
| patt_bott ⇒ 0
| patt_sym _ ⇒ 0
| patt_bound_evar _ ⇒ 0
| patt_bound_svar _ ⇒ 0
| patt_free_evar _ ⇒ 0
| patt_free_svar V' ⇒
match (decide (V' = V)) with
| left _ ⇒ depth
| right _ ⇒ 0
end
| patt_imp ψ₁ ψ₂
⇒ Nat.max
(maximal_mu_depth_to_sv depth V ψ₁)
(maximal_mu_depth_to_sv depth V ψ₂)
| patt_app ψ₁ ψ₂
⇒ Nat.max
(maximal_mu_depth_to_sv depth V ψ₁)
(maximal_mu_depth_to_sv depth V ψ₂)
| patt_exists ψ' ⇒
maximal_mu_depth_to_sv depth V ψ'
| patt_mu ψ' ⇒
maximal_mu_depth_to_sv (S depth) V ψ'
end.
Lemma maximal_mu_depth_to_svar_open depth E n X ψ:
maximal_mu_depth_to depth E (ψ^{svar: n ↦ X})
= maximal_mu_depth_to depth E ψ.
Lemma maximal_mu_depth_to_sv_evar_open depth V n X ψ:
maximal_mu_depth_to_sv depth V (ψ^{evar: n ↦ X})
= maximal_mu_depth_to_sv depth V ψ.
Lemma evar_open_mu_depth depth E n x ψ:
E ≠ x →
maximal_mu_depth_to depth E (ψ^{evar: n ↦ x})
= maximal_mu_depth_to depth E ψ.
Lemma svar_open_mu_depth_sc depth V n x ψ:
V ≠ x →
maximal_mu_depth_to_sv depth V (ψ^{svar: n ↦ x})
= maximal_mu_depth_to_sv depth V ψ.
Lemma svar_open_mu_depth depth E n X ψ:
maximal_mu_depth_to depth E (ψ^{svar: n ↦ X})
= maximal_mu_depth_to depth E ψ.
Lemma maximal_mu_depth_to_0 E ψ depth:
E ∉ free_evars ψ →
maximal_mu_depth_to depth E ψ = 0.
Lemma maximal_mu_depth_to_sv_0 V ψ depth:
V ∉ free_svars ψ →
maximal_mu_depth_to_sv depth V ψ = 0.
Lemma maximal_mu_depth_to_S E ψ depth:
E ∈ free_evars ψ →
maximal_mu_depth_to (S depth) E ψ
= S (maximal_mu_depth_to depth E ψ).
Lemma maximal_mu_depth_to_sv_S V ψ depth:
V ∈ free_svars ψ →
maximal_mu_depth_to_sv (S depth) V ψ
= S (maximal_mu_depth_to_sv depth V ψ).
Definition mu_in_evar_path E ψ sdepth
:= negb (Nat.eqb 0 (maximal_mu_depth_to sdepth E ψ)).
Lemma hbvum_impl_mmdt0 phi dbi x y k:
evar_is_fresh_in x phi →
evar_is_fresh_in y phi →
well_formed_closed_mu_aux phi (S dbi) →
maximal_mu_depth_to k y phi^[svar:dbi↦patt_free_evar y] = 0 →
maximal_mu_depth_to k x phi^[svar:dbi↦patt_free_evar x] = 0
.
Lemma fresh_impl_no_mu_in_evar_path x phi k:
evar_is_fresh_in x phi →
mu_in_evar_path x phi k = false.
(*
Fixpoint bound_svar_depth_is_max
{Σ : Signature}
(ϕ : Pattern)
(dbi : db_index)
(max_depth : nat)
: Prop
:=
match ϕ with
| patt_bound_evar _ => True
| patt_bound_svar idx =>
match (decide (idx = dbi)) with
| left _ => False
| right _ => True
end
| patt_free_evar _ => True
| patt_free_svar _ => True
| patt_bott => True
| patt_sym _ => True
| patt_imp ϕ₁ ϕ₂
=> (bound_svar_depth_is_max ϕ₁ dbi max_depth)
/\ (bound_svar_depth_is_max ϕ₂ dbi max_depth)
| patt_app ϕ₁ ϕ₂
=> (bound_svar_depth_is_max ϕ₁ dbi max_depth)
/\ (bound_svar_depth_is_max ϕ₂ dbi max_depth)
| patt_exists ϕ'
=> bound_svar_depth_is_max ϕ' dbi max_depth
| patt_mu ϕ'
=>
match max_depth with
| 0 => bsvar_occur ϕ' (S dbi) = false
| S (max_depth') => bound_svar_depth_is_max ϕ' (S dbi) max_depth'
end
end.
Fixpoint all_mu_bound_svars_have_max_depth
(ϕ : Pattern)
(max_depth : nat)
: Prop
:=
match ϕ with
| patt_bound_evar _ => True
| patt_bound_svar _ => True
| patt_free_evar _ => True
| patt_free_svar _ => True
| patt_bott => True
| patt_sym _ => True
| patt_imp ϕ₁ ϕ₂
=> (all_mu_bound_svars_have_max_depth ϕ₁ max_depth)
/\ (all_mu_bound_svars_have_max_depth ϕ₂ max_depth)
| patt_app ϕ₁ ϕ₂
=> (all_mu_bound_svars_have_max_depth ϕ₁ max_depth)
/\ (all_mu_bound_svars_have_max_depth ϕ₂ max_depth)
| patt_exists ϕ' =>
all_mu_bound_svars_have_max_depth ϕ' max_depth
| patt_mu ϕ'
=> bound_svar_depth_is_max ϕ' 0 max_depth
/\ all_mu_bound_svars_have_max_depth ϕ' max_depth
end
. *)
Fixpoint bound_svar_is_lt
{Σ : Signature}
(ϕ : Pattern)
(limit : nat)
: Prop
:=
match ϕ with
| patt_bound_evar idx ⇒ True
| patt_bound_svar idx ⇒ idx < limit
| patt_free_evar _ ⇒ True
| patt_free_svar _ ⇒ True
| patt_bott ⇒ True
| patt_sym _ ⇒ True
| patt_imp ϕ₁ ϕ₂
⇒ (bound_svar_is_lt ϕ₁ limit)
∧ (bound_svar_is_lt ϕ₂ limit)
| patt_app ϕ₁ ϕ₂
⇒ (bound_svar_is_lt ϕ₁ limit)
∧ (bound_svar_is_lt ϕ₂ limit)
| patt_exists ϕ' ⇒ bound_svar_is_lt ϕ' limit
| patt_mu ϕ' ⇒ bound_svar_is_lt ϕ' limit
end.
Lemma maximal_mu_depth_to_not_0 ϕ x m:
maximal_mu_depth_to m x ϕ ≠ 0 →
x ∈ free_evars ϕ
.
Lemma bound_svar_is_lt_lt ϕ dbi1 dbi2:
dbi1 < dbi2 →
bound_svar_is_lt ϕ dbi1 →
bound_svar_is_lt ϕ dbi2
.
Lemma bound_svar_is_lt_notfree x ϕ dbi:
well_formed_closed_mu_aux ϕ (S dbi) →
x ∉ free_evars ϕ →
bound_svar_is_lt ϕ dbi →
x ∉ free_evars ϕ^[svar:dbi↦patt_free_evar x]
.
Lemma mu_in_evar_path_svar_subst_evar x ϕ dbi:
well_formed_closed_mu_aux ϕ (S dbi) →
evar_is_fresh_in x ϕ →
bound_svar_is_lt ϕ (S dbi) →
mu_in_evar_path x ϕ^[svar:dbi↦patt_free_evar x] 0 = false
.
Fixpoint mu_depth_to_fev_limited
(E : evar)
(ψ : Pattern)
(limit : nat)
: Prop
:=
match ψ with
| patt_free_evar _ ⇒ True
| patt_free_svar _ ⇒ True
| patt_bound_evar _ ⇒ True
| patt_bound_svar _ ⇒ True
| patt_bott ⇒ True
| patt_sym _ ⇒ True
| patt_imp ϕ₁ ϕ₂
⇒ mu_depth_to_fev_limited E ϕ₁ limit
∧ mu_depth_to_fev_limited E ϕ₂ limit
| patt_app ϕ₁ ϕ₂
⇒ mu_depth_to_fev_limited E ϕ₁ limit
∧ mu_depth_to_fev_limited E ϕ₂ limit
| patt_exists ϕ'
⇒ mu_depth_to_fev_limited E ϕ' limit
| patt_mu ϕ'
⇒ match limit with
| 0 ⇒ evar_is_fresh_in E ϕ'
| S limit' ⇒ mu_depth_to_fev_limited E ϕ' limit'
end
end.
(*
Lemma l x ϕ limit:
evar_is_fresh_in x ϕ ->
mu_depth_to_fev_limited x ϕ limit ->
mu_in_evar_path x ϕ^svar:0↦patt_free_evar x 0 = false
.
*)
Lemma mu_depth_to_fev_limited_evar_open
(E X : evar)
(ϕ : Pattern)
(dbi : db_index)
(mudepth : nat)
:
E ≠ X →
mu_depth_to_fev_limited E ϕ mudepth →
mu_depth_to_fev_limited E ϕ^{evar:dbi↦X} mudepth
.
Fixpoint mu_depth_to_fsv_limited
(X : svar)
(ψ : Pattern)
(limit : nat)
: Prop
:=
match ψ with
| patt_free_evar _ ⇒ True
| patt_free_svar _ ⇒ True
| patt_bound_evar _ ⇒ True
| patt_bound_svar _ ⇒ True
| patt_bott ⇒ True
| patt_sym _ ⇒ True
| patt_imp ϕ₁ ϕ₂
⇒ mu_depth_to_fsv_limited X ϕ₁ limit
∧ mu_depth_to_fsv_limited X ϕ₂ limit
| patt_app ϕ₁ ϕ₂
⇒ mu_depth_to_fsv_limited X ϕ₁ limit
∧ mu_depth_to_fsv_limited X ϕ₂ limit
| patt_exists ϕ'
⇒ mu_depth_to_fsv_limited X ϕ' limit
| patt_mu ϕ'
⇒ match limit with
| 0 ⇒ svar_is_fresh_in X ϕ'
| S limit' ⇒ mu_depth_to_fsv_limited X ϕ' limit'
end
end.
(*
Lemma mu_depth_to_fsv_limited_svar_has_positive_negative_occurrence X ϕ:
mu_depth_to_fsv_limited X ϕ 0 ->
svar_has_positive_occurrence X ϕ = false
/\ svar_has_negative_occurrence X ϕ = false
.
Proof.
induction ϕ; cbn; intros H; split; try reflexivity.
{
destruct (decide (X = x)).
}
Qed.
*)
Lemma mu_depth_to_fsv_limited_svar_open
(E X : svar)
(ϕ : Pattern)
(dbi : db_index)
(mudepth : nat)
:
E ≠ X →
mu_depth_to_fsv_limited E ϕ mudepth →
mu_depth_to_fsv_limited E ϕ^{svar:dbi↦X} mudepth
.
Example ex_not_wfcmu_impl_bound_svar_is_lt:
∃
(ϕ : Pattern)
(mudepth : nat),
well_formed_closed_mu_aux ϕ 0 ∧
¬ bound_svar_is_lt ϕ (S mudepth)
.
Lemma bound_svar_is_lt_free_evar_subst
ϕ iter dbi cvar cpatt:
bound_svar_is_lt ϕ (iter + dbi) →
well_formed_closed_mu_aux cpatt (dbi) →
cvar ∈ free_evars cpatt →
maximal_mu_depth_to 0 cvar cpatt ≤ iter →
bound_svar_is_lt cpatt (iter + dbi) →
bound_svar_is_lt cpatt^[[evar:cvar↦ϕ]] (iter + dbi)
.
Lemma bound_svar_is_lt_bevar_subst cpatt x0 dbi limit:
bound_svar_is_lt cpatt (limit) →
bound_svar_is_lt cpatt^[evar:dbi↦patt_free_evar x0] limit
.
Lemma bound_svar_is_lt_bsvar_subst ϕ dbi limit Z:
bound_svar_is_lt ϕ limit →
bound_svar_is_lt ϕ^[svar:dbi↦patt_free_svar Z] limit
.
Fixpoint bound_svar_is_banned_under_mus
(ϕ : Pattern)
(depth : nat)
(banned : db_index)
: bool
:=
match ϕ with
| patt_bound_evar idx ⇒ true
| patt_bound_svar idx ⇒ true
| patt_free_evar _ ⇒ true
| patt_free_svar _ ⇒ true
| patt_bott ⇒ true
| patt_sym _ ⇒ true
| patt_imp ϕ₁ ϕ₂
⇒ (bound_svar_is_banned_under_mus ϕ₁ depth banned)
&& (bound_svar_is_banned_under_mus ϕ₂ depth banned)
| patt_app ϕ₁ ϕ₂
⇒ (bound_svar_is_banned_under_mus ϕ₁ depth banned)
&& (bound_svar_is_banned_under_mus ϕ₂ depth banned)
| patt_exists ϕ' ⇒ bound_svar_is_banned_under_mus ϕ' depth banned
| patt_mu ϕ' ⇒
match depth with
| 0 ⇒ ~~ (bsvar_occur ϕ' (S banned))
| (S depth') ⇒ bound_svar_is_banned_under_mus ϕ' depth' (S banned)
end
end.
Lemma bsvar_occur_false_impl_banned ϕ banned n:
bsvar_occur ϕ banned = false →
bound_svar_is_banned_under_mus ϕ n banned = true
.
Lemma bound_svar_is_banned_under_mus_lt
(ϕ : Pattern) (depth1 depth2 : nat) (banned : db_index)
:
depth1 ≤ depth2 →
bound_svar_is_banned_under_mus ϕ depth1 banned = true →
bound_svar_is_banned_under_mus ϕ depth2 banned = true
.
Lemma bound_svar_is_banned_notfree x ϕ dbi dbi':
dbi > dbi' →
well_formed_closed_mu_aux ϕ dbi' →
x ∉ free_evars ϕ →
bound_svar_is_banned_under_mus ϕ dbi dbi' = true →
x ∉ free_evars ϕ^[svar:dbi↦patt_free_evar x]
.
Lemma maximal_mu_depth_to_svar_subst_evar_banned x ϕ dbi level d:
well_formed_closed_mu_aux ϕ (S dbi) →
evar_is_fresh_in x ϕ →
bound_svar_is_banned_under_mus ϕ level dbi = true →
maximal_mu_depth_to d x ϕ^[svar:dbi↦patt_free_evar x] ≤ (d + level)
.
Lemma maximal_mu_depth_to_lt a b x ϕ:
a > b →
maximal_mu_depth_to a x ϕ ≤ b →
evar_is_fresh_in x ϕ
.
Lemma maximal_mu_depth_to_svar_subst_evar_banned_back x ϕ dbi level d:
well_formed_closed_mu_aux ϕ (S dbi) →
evar_is_fresh_in x ϕ →
maximal_mu_depth_to d x ϕ^[svar:dbi↦patt_free_evar x] ≤ (d + level) →
bound_svar_is_banned_under_mus ϕ level dbi = true
.
Lemma maximal_mu_depth_to_svar_subst_evar_banned_back_2 x ϕ dbi level d:
well_formed_closed_mu_aux ϕ (S dbi) →
evar_is_fresh_in x ϕ →
maximal_mu_depth_to d x ϕ ≤ (d + level) →
bound_svar_is_banned_under_mus ϕ^[svar:dbi↦patt_free_evar x] level dbi = true
.
Lemma bsvar_occur_bevar_subst ϕ ψ edbi sdbi:
well_formed_closed_mu_aux ψ sdbi →
bsvar_occur ϕ sdbi = false →
bsvar_occur ϕ^[evar:edbi↦ψ] sdbi = false
.
Lemma bound_svar_is_banned_under_mus_bevar_subst ϕ ψ dbi level dbi':
well_formed_closed_mu_aux ψ (S dbi') →
bound_svar_is_banned_under_mus ψ level dbi' = true →
bound_svar_is_banned_under_mus ϕ level dbi' = true →
bound_svar_is_banned_under_mus ϕ^[evar:dbi↦ψ] level dbi' = true
.
Lemma bsvar_occur_free_evar_subst ϕ cvar ψ dbi:
well_formed_closed_mu_aux ψ dbi →
bsvar_occur ϕ dbi = false →
bsvar_occur ϕ^[[evar:cvar↦ψ]] dbi = false
.
(* ϕ ≡ (mu, 0) ---> cvar *)
Lemma bound_svar_is_banned_under_mus_fevar_subst_alternative ϕ ψ cvar level dbi':
well_formed_closed_mu_aux ψ (S dbi') = true →
bound_svar_is_banned_under_mus ψ level dbi' = true →
bound_svar_is_banned_under_mus ϕ level dbi' = true →
bound_svar_is_banned_under_mus ϕ^[[evar:cvar↦ψ]] level dbi' = true
.
(* ϕ ≡ (mu, 0) ---> cvar *)
Lemma bound_svar_is_banned_under_mus_fevar_subst ϕ ψ cvar level dbi':
well_formed_closed_mu_aux ϕ (dbi') = true →
well_formed_closed_mu_aux ψ (S dbi') = true →
bound_svar_is_banned_under_mus ψ level dbi' = true →
bound_svar_is_banned_under_mus ϕ^[[evar:cvar↦ψ]] level dbi' = true
.
Lemma bound_svar_is_banned_under_mus_evar_open x ϕ dbi level dbi':
bound_svar_is_banned_under_mus ϕ level dbi' = true →
bound_svar_is_banned_under_mus ϕ^[evar:dbi↦patt_free_evar x] level dbi' = true
.
Lemma bound_svar_is_lt_implies_bound_svar_is_banned_under_mus ϕ level dbi n:
well_formed_closed_mu_aux ϕ (dbi + n) →
bound_svar_is_lt ϕ (level + n) →
bound_svar_is_banned_under_mus ϕ level (dbi + n) = true
.
Example counterexample_1:
∃ cvar cpatt ϕ dbi iter,
well_formed_closed_mu_aux cpatt (S dbi) ∧
maximal_mu_depth_to 0 cvar cpatt ≤ iter ∧
bound_svar_is_banned_under_mus ϕ iter dbi ∧
bound_svar_is_banned_under_mus cpatt^[[evar:cvar↦ϕ]] iter dbi
.
Fixpoint pattern_kt_well_formed (φ : Pattern) :=
match φ with
| patt_free_evar x ⇒ true
| patt_free_svar x ⇒ true
| patt_bound_evar n ⇒ true
| patt_bound_svar n ⇒ true
| patt_sym sigma ⇒ true
| patt_app phi1 phi2 ⇒ pattern_kt_well_formed phi1 && pattern_kt_well_formed phi2
| patt_bott ⇒ true
| patt_imp phi1 phi2 ⇒ pattern_kt_well_formed phi1 && pattern_kt_well_formed phi2
| patt_exists phi ⇒ pattern_kt_well_formed phi
| patt_mu phi ⇒ bound_svar_is_banned_under_mus phi 0 0 &&
pattern_kt_well_formed phi
end.
Lemma kt_well_formed_evar_open (φ : Pattern) x dbi:
pattern_kt_well_formed φ →
pattern_kt_well_formed φ^{evar:dbi↦x}.
Lemma bsvar_occur_bsvar_subst_wf :
∀ φ ψ dbi x,
well_formed_closed_mu_aux φ (S x) →
~~ bsvar_occur φ dbi →
well_formed_closed_mu_aux ψ 0 →
~~ bsvar_occur (bsvar_subst ψ x φ) dbi.
Lemma bound_svar_is_banned_bsvar_subst :
∀ φ ψ level dbi x,
well_formed_closed_mu_aux ψ 0 →
well_formed_closed_mu_aux φ (S x) →
bound_svar_is_banned_under_mus φ level dbi →
bound_svar_is_banned_under_mus (bsvar_subst ψ x φ) level dbi.
Lemma kt_well_formed_svar_open (φ : Pattern) X dbi:
well_formed_closed_mu_aux φ (S dbi) →
pattern_kt_well_formed φ →
pattern_kt_well_formed φ^{svar:dbi↦X}.
(* Mu-freeness is a stricter property. *)
Lemma mf_imp_ktwf φ : mu_free φ → pattern_kt_well_formed φ.
End with_signature.
(* TODO remove these hints *)
#[export]
Hint Resolve well_formed_positive_svar_quantify : core.
#[export]
Hint Resolve no_positive_occurrence_svar_quantify : core.
#[export]
Hint Resolve no_negative_occurrence_svar_quantify : core.
#[export]
Hint Resolve wfc_impl_no_neg_occ : core.
#[export]
Hint Resolve wfp_free_svar_subst : core.
#[export]
Hint Resolve wfp_neg_free_svar_subst : core.
#[export]
Hint Resolve svar_quantify_closed_ex : core.
#[export]
Hint Resolve svar_quantify_closed_mu : core.
#[export]
Hint Resolve evar_quantify_positive : core.
#[export]
Hint Resolve evar_quantify_closed_mu : core.
#[export]
Hint Resolve evar_quantify_closed_ex : core.
#[export]
Hint Resolve wfp_evar_open : core.
#[export]
Hint Resolve wfc_mu_aux_body_ex_imp1 : core.
#[export]
Hint Resolve wfc_ex_aux_body_ex_imp1 : core.
#[export]
Hint Resolve bevar_subst_positive_2 : core.
#[export]
Hint Resolve wfc_mu_aux_bevar_subst : core.
#[export]
Hint Resolve wfc_ex_aux_bevar_subst : core.
#[export]
Hint Resolve wfp_svar_open : core.
#[export]
Hint Resolve wfc_mu_free_evar_subst : core.
From MatchingLogic Require Export
SyntaxLemmas.PatternCtxApplicationCtx
SyntaxLemmas.FreshnessApplicationCtx
wftactics
.
Import MatchingLogic.Substitution.Notations.
Close Scope boolean_if_scope.
Section syntax.
Context {Σ : Signature}.
Open Scope ml_scope.
Inductive is_subformula_of_ind : Pattern → Pattern → Prop :=
| sub_eq ϕ₁ ϕ₂ : ϕ₁ = ϕ₂ → is_subformula_of_ind ϕ₁ ϕ₂
| sub_app_l ϕ₁ ϕ₂ ϕ₃ : is_subformula_of_ind ϕ₁ ϕ₂ → is_subformula_of_ind ϕ₁ (patt_app ϕ₂ ϕ₃)
| sub_app_r ϕ₁ ϕ₂ ϕ₃ : is_subformula_of_ind ϕ₁ ϕ₃ → is_subformula_of_ind ϕ₁ (patt_app ϕ₂ ϕ₃)
| sub_imp_l ϕ₁ ϕ₂ ϕ₃ : is_subformula_of_ind ϕ₁ ϕ₂ → is_subformula_of_ind ϕ₁ (patt_imp ϕ₂ ϕ₃)
| sub_imp_r ϕ₁ ϕ₂ ϕ₃ : is_subformula_of_ind ϕ₁ ϕ₃ → is_subformula_of_ind ϕ₁ (patt_imp ϕ₂ ϕ₃)
| sub_exists ϕ₁ ϕ₂ : is_subformula_of_ind ϕ₁ ϕ₂ → is_subformula_of_ind ϕ₁ (patt_exists ϕ₂)
| sub_mu ϕ₁ ϕ₂ : is_subformula_of_ind ϕ₁ ϕ₂ → is_subformula_of_ind ϕ₁ (patt_mu ϕ₂)
.
Fixpoint is_subformula_of ϕ₁ ϕ₂ : bool :=
(decide_rel (=) ϕ₁ ϕ₂)
|| match ϕ₂ with
| patt_app l r | patt_imp l r ⇒ is_subformula_of ϕ₁ l || is_subformula_of ϕ₁ r
| patt_exists phi | patt_mu phi ⇒ is_subformula_of ϕ₁ phi
| _ ⇒ false
end.
Lemma is_subformula_of_P ϕ₁ ϕ₂ : reflect (is_subformula_of_ind ϕ₁ ϕ₂) (is_subformula_of ϕ₁ ϕ₂).
Lemma is_subformula_of_refl ϕ:
is_subformula_of ϕ ϕ = true.
Lemma bsvar_subst_contains_subformula ϕ₁ ϕ₂ dbi :
bsvar_occur ϕ₁ dbi = true →
is_subformula_of_ind ϕ₂ (ϕ₁^[svar: dbi ↦ ϕ₂]).
Lemma bevar_subst_contains_subformula ϕ₁ ϕ₂ dbi :
bevar_occur ϕ₁ dbi = true →
is_subformula_of_ind ϕ₂ (ϕ₁^[evar: dbi ↦ ϕ₂]).
Lemma free_evars_subformula ϕ₁ ϕ₂ :
is_subformula_of_ind ϕ₁ ϕ₂ → free_evars ϕ₁ ⊆ free_evars ϕ₂.
Corollary evar_fresh_in_subformula x ϕ₁ ϕ₂ :
is_subformula_of_ind ϕ₁ ϕ₂ →
evar_is_fresh_in x ϕ₂ →
evar_is_fresh_in x ϕ₁.
Corollary evar_fresh_in_subformula' x ϕ₁ ϕ₂ :
is_subformula_of ϕ₁ ϕ₂ →
evar_is_fresh_in x ϕ₂ →
evar_is_fresh_in x ϕ₁.
Lemma free_svars_subformula ϕ₁ ϕ₂ :
is_subformula_of_ind ϕ₁ ϕ₂ → free_svars ϕ₁ ⊆ free_svars ϕ₂.
Corollary svar_fresh_in_subformula x ϕ₁ ϕ₂ :
is_subformula_of_ind ϕ₁ ϕ₂ →
svar_is_fresh_in x ϕ₂ →
svar_is_fresh_in x ϕ₁.
Lemma free_evars_bsvar_subst ϕ₁ ϕ₂ dbi:
free_evars (ϕ₁^[svar: dbi ↦ ϕ₂]) ⊆ free_evars ϕ₁ ∪ free_evars ϕ₂.
Lemma free_svars_bevar_subst ϕ₁ ϕ₂ dbi:
free_svars (ϕ₁^[evar: dbi ↦ ϕ₂]) ⊆ free_svars ϕ₁ ∪ free_svars ϕ₂.
Lemma free_evars_bsvar_subst_1 ϕ₁ ϕ₂ dbi:
free_evars ϕ₁ ⊆ free_evars (ϕ₁^[svar: dbi ↦ ϕ₂]).
Lemma free_svars_bevar_subst_1 ϕ₁ ϕ₂ dbi:
free_svars ϕ₁ ⊆ free_svars (ϕ₁^[evar: dbi ↦ ϕ₂]).
Corollary free_evars_bsvar_subst_eq ϕ₁ ϕ₂ dbi:
bsvar_occur ϕ₁ dbi →
free_evars (ϕ₁^[svar: dbi ↦ ϕ₂]) = free_evars ϕ₁ ∪ free_evars ϕ₂.
Corollary free_svars_bevar_subst_eq ϕ₁ ϕ₂ dbi:
bevar_occur ϕ₁ dbi →
free_svars (ϕ₁^[evar: dbi ↦ ϕ₂]) = free_svars ϕ₁ ∪ free_svars ϕ₂.
Lemma wfc_mu_aux_implies_not_bsvar_occur phi ns :
well_formed_closed_mu_aux phi ns →
bsvar_occur phi ns = false.
Lemma wfc_ex_aux_implies_not_bevar_occur phi ne :
well_formed_closed_ex_aux phi ne →
bevar_occur phi ne = false.
Corollary wfc_mu_implies_not_bsvar_occur phi n :
well_formed_closed_mu_aux phi 0 →
¬ bsvar_occur phi n.
Lemma wfc_ex_implies_not_bevar_occur phi n :
well_formed_closed_ex_aux phi 0 →
bevar_occur phi n = false.
Lemma not_bsvar_occur_bsvar_subst_2 phi psi n:
well_formed_closed_mu_aux psi 0 → well_formed_closed_mu_aux phi (S n) →
bsvar_occur (phi^[svar: n ↦ psi]) n = false
.
Lemma not_bsvar_occur_bsvar_subst phi psi n:
well_formed_closed_mu_aux psi 0 → well_formed_closed_mu_aux phi n →
¬ bsvar_occur (phi^[svar: n ↦ psi]) n.
Lemma not_bsvar_occur_impl_no_neg_occ_and_no_pos_occ phi n:
¬ bsvar_occur phi n →
no_negative_occurrence_db_b n phi && no_positive_occurrence_db_b n phi.
Corollary not_bsvar_occur_impl_pos_occ_db phi n:
¬ bsvar_occur phi n →
no_positive_occurrence_db_b n phi.
Corollary not_bsvar_occur_impl_neg_occ_db phi n:
¬ bsvar_occur phi n →
no_negative_occurrence_db_b n phi.
End syntax.
Module Notations.
Export MatchingLogic.Pattern.Notations.
Export MatchingLogic.PatternContext.Notations.
End Notations.
#[export]
Hint Resolve
evar_is_fresh_in_richer
set_evar_fresh_is_fresh
set_svar_fresh_is_fresh
x_eq_fresh_impl_x_notin_free_evars
: core.
#[export]
Hint Extern 0 (is_true (@well_formed _ _)) ⇒ unfold is_true : core.
#[export]
Hint Resolve well_formed_bott : core.
#[export]
Hint Resolve well_formed_imp : core.
#[export]
Hint Resolve well_formed_app : core.
#[export]
Hint Resolve wf_sctx : core.
#[export]
Hint Resolve well_formed_ex_app : core.
#[export]
Hint Resolve well_formed_impl_well_formed_ex : core.
#[export]
Hint Resolve well_formed_free_evar_subst : core.
#[export]
Hint Resolve well_formed_free_evar_subst_0 : core.
#[export]
Hint Resolve <- evar_is_fresh_in_exists : core.
#[export]
Hint Resolve evar_is_fresh_in_evar_quantify : core.
(* Tactics for resolving goals involving sets *)
(*
eauto 5 using @sets.elem_of_union_l, @sets.elem_of_union_r with typeclass_instances.
*)
(*
eauto depth using @sets.union_subseteq_l, @sets.union_subseteq_r
with typeclass_instances.
*)
(*
[export] Hint Extern 10 (free_evars _ ⊆ free_evars _) => solve_free_evars_inclusion : core. *)
#[export]
Hint Resolve wf_imp_wfc : core.
#[export]
Hint Resolve wfc_ex_implies_not_bevar_occur : core.
Section with_signature.
Context {Σ : Signature}.
Open Scope ml_scope.
Definition evar_quantify_ctx (x : evar) (n : db_index) (C : PatternCtx) : PatternCtx :=
match decide (x = pcEvar C) with
| left _ ⇒ C
| right pf ⇒ Build_PatternCtx (pcEvar C) ((pcPattern C)^{{evar: x ↦ n}})
end.
Lemma is_linear_context_evar_quantify (x : evar) (n : db_index) (C : PatternCtx) :
is_linear_context C →
is_linear_context (evar_quantify_ctx x n C).
Definition svar_quantify_ctx (X : svar) (n : db_index) (C : PatternCtx) : PatternCtx :=
Build_PatternCtx (pcEvar C) ((pcPattern C)^{{svar: X ↦ n}}).
Lemma is_linear_context_svar_quantify (X : svar) (n : db_index) (C : PatternCtx) :
is_linear_context C →
is_linear_context (svar_quantify_ctx X n C).
Lemma svar_quantify_free_evar_subst ψ ϕ x X n:
ψ^[[evar: x ↦ ϕ]]^{{svar: X ↦ n}} =
ψ^{{svar: X ↦ n}}^[[evar: x ↦ ϕ^{{svar: X ↦ n}}]].
(* OOPS, does not hold. The problem is that free_evar_subst' does not wrap the target
in nest_mu. *)
Lemma svar_quantify_emplace X n C ϕ:
(emplace C ϕ)^{{svar: X ↦ n}} = emplace (svar_quantify_ctx X n C) (ϕ^{{svar: X ↦ n}}).
Lemma evar_quantify_subst_ctx x n AC ϕ:
x ∉ AC_free_evars AC →
(subst_ctx AC ϕ)^{{evar: x ↦ n}} = subst_ctx AC (ϕ^{{evar: x ↦ n}}).
Lemma wfp_free_svar_subst ϕ ψ X:
well_formed_closed_mu_aux ψ 0 →
well_formed_positive ψ = true →
well_formed_positive ϕ = true →
svar_has_negative_occurrence X ϕ = false →
well_formed_positive (ϕ^[[svar: X ↦ ψ]]) = true
with wfp_neg_free_svar_subst ϕ ψ X:
well_formed_closed_mu_aux ψ 0 →
well_formed_positive ψ = true →
well_formed_positive ϕ = true →
svar_has_positive_occurrence X ϕ = false →
well_formed_positive (ϕ^[[svar: X ↦ ψ]]) = true.
Lemma count_evar_occurrences_bevar_subst pcEvar ϕ ψ k:
count_evar_occurrences pcEvar ψ = 0 →
count_evar_occurrences pcEvar (ϕ^[evar: k ↦ ψ]) = count_evar_occurrences pcEvar ϕ.
Lemma count_evar_occurrences_evar_open pcEvar ϕ x:
pcEvar ≠ x →
count_evar_occurrences pcEvar (ϕ^{evar: 0 ↦ x}) = count_evar_occurrences pcEvar ϕ.
Lemma count_evar_occurrences_svar_open x dbi ϕ ψ:
count_evar_occurrences x ψ = 0 →
count_evar_occurrences x (ϕ^[svar: dbi ↦ ψ]) = count_evar_occurrences x ϕ.
Lemma free_evar_subst_bsvar_subst ϕ ψ ξ x dbi:
well_formed_closed_mu_aux ξ 0 →
evar_is_fresh_in x ψ →
(ϕ^[svar: dbi ↦ ψ])^[[evar:x ↦ ξ]]
= (ϕ^[[evar:x ↦ ξ]])^[svar: dbi ↦ ψ].
Lemma wf_svar_open_from_wf_mu X ϕ:
well_formed (patt_mu ϕ) →
well_formed (ϕ^{svar: 0 ↦ X}).
Lemma wfcex_after_subst_impl_wfcex_before ϕ ψ x dbi:
well_formed_closed_ex_aux (ϕ^[[evar:x ↦ ψ]]) dbi = true →
well_formed_closed_ex_aux ϕ dbi = true.
Lemma wfcmu_after_subst_impl_wfcmu_before ϕ ψ x dbi:
well_formed_closed_mu_aux (ϕ^[[evar:x ↦ ψ]]) dbi = true →
well_formed_closed_mu_aux ϕ dbi = true.
Lemma nno_after_subst_impl_nno_before ϕ ψ x dbi:
no_negative_occurrence_db_b dbi (ϕ^[[evar:x ↦ ψ]]) = true →
no_negative_occurrence_db_b dbi ϕ = true
with npo_after_subst_impl_npo_before ϕ ψ x dbi:
no_positive_occurrence_db_b dbi (ϕ^[[evar:x ↦ ψ]]) = true →
no_positive_occurrence_db_b dbi ϕ = true.
Lemma wfp_after_subst_impl_wfp_before ϕ ψ x:
well_formed_positive (ϕ^[[evar:x ↦ ψ]]) = true →
well_formed_positive ϕ = true.
Lemma wf_after_subst_impl_wf_before ϕ ψ x:
well_formed (ϕ^[[evar:x ↦ ψ]]) = true →
well_formed ϕ = true.
Lemma wf_emplaced_impl_wf_context (C : PatternCtx) (ψ : Pattern) :
well_formed (emplace C ψ) = true →
PC_wf C.
Global Instance evar_is_fresh_in_dec (x : evar) (p : Pattern) :
Decision (evar_is_fresh_in x p).
Definition evar_is_fresh_in_list (x : evar) (l : list Pattern) :=
Forall (evar_is_fresh_in x) l.
Global Instance evar_is_fresh_in_list_dec (x : evar) (l : list Pattern) :
Decision (evar_is_fresh_in_list x l).
Lemma evar_fresh_in_foldr x g l:
evar_is_fresh_in x (foldr patt_imp g l) ↔ evar_is_fresh_in x g ∧ evar_is_fresh_in_list x l.
Global Instance svar_is_fresh_in_dec (X : svar) (p : Pattern) :
Decision (svar_is_fresh_in X p).
Definition svar_is_fresh_in_list (X : svar) (l : list Pattern) :=
Forall (svar_is_fresh_in X) l.
Global Instance svar_is_fresh_in_list_dec (X : svar) (l : list Pattern) :
Decision (svar_is_fresh_in_list X l).
Lemma wfc_ex_lower ϕ n:
bevar_occur ϕ n = false →
well_formed_closed_ex_aux ϕ (S n) = true →
well_formed_closed_ex_aux ϕ n = true.
Lemma wfc_mu_lower ϕ n:
bsvar_occur ϕ n = false →
well_formed_closed_mu_aux ϕ (S n) = true →
well_formed_closed_mu_aux ϕ n = true.
Lemma wf_ex_quan_impl_wf (x : evar) (ϕ : Pattern):
bevar_occur ϕ 0 = false →
well_formed (exists_quantify x ϕ) = true →
well_formed ϕ = true.
Lemma bevar_occur_evar_open_2 dbi x ϕ:
well_formed_closed_ex_aux ϕ dbi →
bevar_occur (ϕ^{evar: dbi ↦ x}) dbi = false.
Lemma bsvar_occur_svar_open_2 dbi X ϕ:
well_formed_closed_mu_aux ϕ dbi →
bsvar_occur (ϕ^{svar: dbi ↦ X}) dbi = false.
Lemma svar_has_negative_occurrence_free_evar_subst
(ϕ ψ: Pattern) (x : evar) (X : svar) :
svar_is_fresh_in X ψ →
svar_has_negative_occurrence X ϕ^[[evar:x↦ψ]] = svar_has_negative_occurrence X ϕ
with svar_has_positive_occurrence_free_evar_subst
(ϕ ψ: Pattern) (x : evar) (X : svar) :
svar_is_fresh_in X ψ →
svar_has_positive_occurrence X ϕ^[[evar:x↦ψ]] = svar_has_positive_occurrence X ϕ
.
Fixpoint maximal_mu_depth_to (depth : nat) (E : evar) (ψ : Pattern) : nat :=
match ψ with
| patt_bott ⇒ 0
| patt_sym _ ⇒ 0
| patt_bound_evar _ ⇒ 0
| patt_bound_svar _ ⇒ 0
| patt_free_svar _ ⇒ 0
| patt_free_evar E' ⇒
match (decide (E' = E)) with
| left _ ⇒ depth
| right _ ⇒ 0
end
| patt_imp ψ₁ ψ₂
⇒ Nat.max
(maximal_mu_depth_to depth E ψ₁)
(maximal_mu_depth_to depth E ψ₂)
| patt_app ψ₁ ψ₂
⇒ Nat.max
(maximal_mu_depth_to depth E ψ₁)
(maximal_mu_depth_to depth E ψ₂)
| patt_exists ψ' ⇒
maximal_mu_depth_to depth E ψ'
| patt_mu ψ' ⇒
maximal_mu_depth_to (S depth) E ψ'
end.
Fixpoint maximal_mu_depth_to_sv (depth : nat) (V : svar) (ψ : Pattern) : nat :=
match ψ with
| patt_bott ⇒ 0
| patt_sym _ ⇒ 0
| patt_bound_evar _ ⇒ 0
| patt_bound_svar _ ⇒ 0
| patt_free_evar _ ⇒ 0
| patt_free_svar V' ⇒
match (decide (V' = V)) with
| left _ ⇒ depth
| right _ ⇒ 0
end
| patt_imp ψ₁ ψ₂
⇒ Nat.max
(maximal_mu_depth_to_sv depth V ψ₁)
(maximal_mu_depth_to_sv depth V ψ₂)
| patt_app ψ₁ ψ₂
⇒ Nat.max
(maximal_mu_depth_to_sv depth V ψ₁)
(maximal_mu_depth_to_sv depth V ψ₂)
| patt_exists ψ' ⇒
maximal_mu_depth_to_sv depth V ψ'
| patt_mu ψ' ⇒
maximal_mu_depth_to_sv (S depth) V ψ'
end.
Lemma maximal_mu_depth_to_svar_open depth E n X ψ:
maximal_mu_depth_to depth E (ψ^{svar: n ↦ X})
= maximal_mu_depth_to depth E ψ.
Lemma maximal_mu_depth_to_sv_evar_open depth V n X ψ:
maximal_mu_depth_to_sv depth V (ψ^{evar: n ↦ X})
= maximal_mu_depth_to_sv depth V ψ.
Lemma evar_open_mu_depth depth E n x ψ:
E ≠ x →
maximal_mu_depth_to depth E (ψ^{evar: n ↦ x})
= maximal_mu_depth_to depth E ψ.
Lemma svar_open_mu_depth_sc depth V n x ψ:
V ≠ x →
maximal_mu_depth_to_sv depth V (ψ^{svar: n ↦ x})
= maximal_mu_depth_to_sv depth V ψ.
Lemma svar_open_mu_depth depth E n X ψ:
maximal_mu_depth_to depth E (ψ^{svar: n ↦ X})
= maximal_mu_depth_to depth E ψ.
Lemma maximal_mu_depth_to_0 E ψ depth:
E ∉ free_evars ψ →
maximal_mu_depth_to depth E ψ = 0.
Lemma maximal_mu_depth_to_sv_0 V ψ depth:
V ∉ free_svars ψ →
maximal_mu_depth_to_sv depth V ψ = 0.
Lemma maximal_mu_depth_to_S E ψ depth:
E ∈ free_evars ψ →
maximal_mu_depth_to (S depth) E ψ
= S (maximal_mu_depth_to depth E ψ).
Lemma maximal_mu_depth_to_sv_S V ψ depth:
V ∈ free_svars ψ →
maximal_mu_depth_to_sv (S depth) V ψ
= S (maximal_mu_depth_to_sv depth V ψ).
Definition mu_in_evar_path E ψ sdepth
:= negb (Nat.eqb 0 (maximal_mu_depth_to sdepth E ψ)).
Lemma hbvum_impl_mmdt0 phi dbi x y k:
evar_is_fresh_in x phi →
evar_is_fresh_in y phi →
well_formed_closed_mu_aux phi (S dbi) →
maximal_mu_depth_to k y phi^[svar:dbi↦patt_free_evar y] = 0 →
maximal_mu_depth_to k x phi^[svar:dbi↦patt_free_evar x] = 0
.
Lemma fresh_impl_no_mu_in_evar_path x phi k:
evar_is_fresh_in x phi →
mu_in_evar_path x phi k = false.
(*
Fixpoint bound_svar_depth_is_max
{Σ : Signature}
(ϕ : Pattern)
(dbi : db_index)
(max_depth : nat)
: Prop
:=
match ϕ with
| patt_bound_evar _ => True
| patt_bound_svar idx =>
match (decide (idx = dbi)) with
| left _ => False
| right _ => True
end
| patt_free_evar _ => True
| patt_free_svar _ => True
| patt_bott => True
| patt_sym _ => True
| patt_imp ϕ₁ ϕ₂
=> (bound_svar_depth_is_max ϕ₁ dbi max_depth)
/\ (bound_svar_depth_is_max ϕ₂ dbi max_depth)
| patt_app ϕ₁ ϕ₂
=> (bound_svar_depth_is_max ϕ₁ dbi max_depth)
/\ (bound_svar_depth_is_max ϕ₂ dbi max_depth)
| patt_exists ϕ'
=> bound_svar_depth_is_max ϕ' dbi max_depth
| patt_mu ϕ'
=>
match max_depth with
| 0 => bsvar_occur ϕ' (S dbi) = false
| S (max_depth') => bound_svar_depth_is_max ϕ' (S dbi) max_depth'
end
end.
Fixpoint all_mu_bound_svars_have_max_depth
(ϕ : Pattern)
(max_depth : nat)
: Prop
:=
match ϕ with
| patt_bound_evar _ => True
| patt_bound_svar _ => True
| patt_free_evar _ => True
| patt_free_svar _ => True
| patt_bott => True
| patt_sym _ => True
| patt_imp ϕ₁ ϕ₂
=> (all_mu_bound_svars_have_max_depth ϕ₁ max_depth)
/\ (all_mu_bound_svars_have_max_depth ϕ₂ max_depth)
| patt_app ϕ₁ ϕ₂
=> (all_mu_bound_svars_have_max_depth ϕ₁ max_depth)
/\ (all_mu_bound_svars_have_max_depth ϕ₂ max_depth)
| patt_exists ϕ' =>
all_mu_bound_svars_have_max_depth ϕ' max_depth
| patt_mu ϕ'
=> bound_svar_depth_is_max ϕ' 0 max_depth
/\ all_mu_bound_svars_have_max_depth ϕ' max_depth
end
. *)
Fixpoint bound_svar_is_lt
{Σ : Signature}
(ϕ : Pattern)
(limit : nat)
: Prop
:=
match ϕ with
| patt_bound_evar idx ⇒ True
| patt_bound_svar idx ⇒ idx < limit
| patt_free_evar _ ⇒ True
| patt_free_svar _ ⇒ True
| patt_bott ⇒ True
| patt_sym _ ⇒ True
| patt_imp ϕ₁ ϕ₂
⇒ (bound_svar_is_lt ϕ₁ limit)
∧ (bound_svar_is_lt ϕ₂ limit)
| patt_app ϕ₁ ϕ₂
⇒ (bound_svar_is_lt ϕ₁ limit)
∧ (bound_svar_is_lt ϕ₂ limit)
| patt_exists ϕ' ⇒ bound_svar_is_lt ϕ' limit
| patt_mu ϕ' ⇒ bound_svar_is_lt ϕ' limit
end.
Lemma maximal_mu_depth_to_not_0 ϕ x m:
maximal_mu_depth_to m x ϕ ≠ 0 →
x ∈ free_evars ϕ
.
Lemma bound_svar_is_lt_lt ϕ dbi1 dbi2:
dbi1 < dbi2 →
bound_svar_is_lt ϕ dbi1 →
bound_svar_is_lt ϕ dbi2
.
Lemma bound_svar_is_lt_notfree x ϕ dbi:
well_formed_closed_mu_aux ϕ (S dbi) →
x ∉ free_evars ϕ →
bound_svar_is_lt ϕ dbi →
x ∉ free_evars ϕ^[svar:dbi↦patt_free_evar x]
.
Lemma mu_in_evar_path_svar_subst_evar x ϕ dbi:
well_formed_closed_mu_aux ϕ (S dbi) →
evar_is_fresh_in x ϕ →
bound_svar_is_lt ϕ (S dbi) →
mu_in_evar_path x ϕ^[svar:dbi↦patt_free_evar x] 0 = false
.
Fixpoint mu_depth_to_fev_limited
(E : evar)
(ψ : Pattern)
(limit : nat)
: Prop
:=
match ψ with
| patt_free_evar _ ⇒ True
| patt_free_svar _ ⇒ True
| patt_bound_evar _ ⇒ True
| patt_bound_svar _ ⇒ True
| patt_bott ⇒ True
| patt_sym _ ⇒ True
| patt_imp ϕ₁ ϕ₂
⇒ mu_depth_to_fev_limited E ϕ₁ limit
∧ mu_depth_to_fev_limited E ϕ₂ limit
| patt_app ϕ₁ ϕ₂
⇒ mu_depth_to_fev_limited E ϕ₁ limit
∧ mu_depth_to_fev_limited E ϕ₂ limit
| patt_exists ϕ'
⇒ mu_depth_to_fev_limited E ϕ' limit
| patt_mu ϕ'
⇒ match limit with
| 0 ⇒ evar_is_fresh_in E ϕ'
| S limit' ⇒ mu_depth_to_fev_limited E ϕ' limit'
end
end.
(*
Lemma l x ϕ limit:
evar_is_fresh_in x ϕ ->
mu_depth_to_fev_limited x ϕ limit ->
mu_in_evar_path x ϕ^svar:0↦patt_free_evar x 0 = false
.
*)
Lemma mu_depth_to_fev_limited_evar_open
(E X : evar)
(ϕ : Pattern)
(dbi : db_index)
(mudepth : nat)
:
E ≠ X →
mu_depth_to_fev_limited E ϕ mudepth →
mu_depth_to_fev_limited E ϕ^{evar:dbi↦X} mudepth
.
Fixpoint mu_depth_to_fsv_limited
(X : svar)
(ψ : Pattern)
(limit : nat)
: Prop
:=
match ψ with
| patt_free_evar _ ⇒ True
| patt_free_svar _ ⇒ True
| patt_bound_evar _ ⇒ True
| patt_bound_svar _ ⇒ True
| patt_bott ⇒ True
| patt_sym _ ⇒ True
| patt_imp ϕ₁ ϕ₂
⇒ mu_depth_to_fsv_limited X ϕ₁ limit
∧ mu_depth_to_fsv_limited X ϕ₂ limit
| patt_app ϕ₁ ϕ₂
⇒ mu_depth_to_fsv_limited X ϕ₁ limit
∧ mu_depth_to_fsv_limited X ϕ₂ limit
| patt_exists ϕ'
⇒ mu_depth_to_fsv_limited X ϕ' limit
| patt_mu ϕ'
⇒ match limit with
| 0 ⇒ svar_is_fresh_in X ϕ'
| S limit' ⇒ mu_depth_to_fsv_limited X ϕ' limit'
end
end.
(*
Lemma mu_depth_to_fsv_limited_svar_has_positive_negative_occurrence X ϕ:
mu_depth_to_fsv_limited X ϕ 0 ->
svar_has_positive_occurrence X ϕ = false
/\ svar_has_negative_occurrence X ϕ = false
.
Proof.
induction ϕ; cbn; intros H; split; try reflexivity.
{
destruct (decide (X = x)).
}
Qed.
*)
Lemma mu_depth_to_fsv_limited_svar_open
(E X : svar)
(ϕ : Pattern)
(dbi : db_index)
(mudepth : nat)
:
E ≠ X →
mu_depth_to_fsv_limited E ϕ mudepth →
mu_depth_to_fsv_limited E ϕ^{svar:dbi↦X} mudepth
.
Example ex_not_wfcmu_impl_bound_svar_is_lt:
∃
(ϕ : Pattern)
(mudepth : nat),
well_formed_closed_mu_aux ϕ 0 ∧
¬ bound_svar_is_lt ϕ (S mudepth)
.
Lemma bound_svar_is_lt_free_evar_subst
ϕ iter dbi cvar cpatt:
bound_svar_is_lt ϕ (iter + dbi) →
well_formed_closed_mu_aux cpatt (dbi) →
cvar ∈ free_evars cpatt →
maximal_mu_depth_to 0 cvar cpatt ≤ iter →
bound_svar_is_lt cpatt (iter + dbi) →
bound_svar_is_lt cpatt^[[evar:cvar↦ϕ]] (iter + dbi)
.
Lemma bound_svar_is_lt_bevar_subst cpatt x0 dbi limit:
bound_svar_is_lt cpatt (limit) →
bound_svar_is_lt cpatt^[evar:dbi↦patt_free_evar x0] limit
.
Lemma bound_svar_is_lt_bsvar_subst ϕ dbi limit Z:
bound_svar_is_lt ϕ limit →
bound_svar_is_lt ϕ^[svar:dbi↦patt_free_svar Z] limit
.
Fixpoint bound_svar_is_banned_under_mus
(ϕ : Pattern)
(depth : nat)
(banned : db_index)
: bool
:=
match ϕ with
| patt_bound_evar idx ⇒ true
| patt_bound_svar idx ⇒ true
| patt_free_evar _ ⇒ true
| patt_free_svar _ ⇒ true
| patt_bott ⇒ true
| patt_sym _ ⇒ true
| patt_imp ϕ₁ ϕ₂
⇒ (bound_svar_is_banned_under_mus ϕ₁ depth banned)
&& (bound_svar_is_banned_under_mus ϕ₂ depth banned)
| patt_app ϕ₁ ϕ₂
⇒ (bound_svar_is_banned_under_mus ϕ₁ depth banned)
&& (bound_svar_is_banned_under_mus ϕ₂ depth banned)
| patt_exists ϕ' ⇒ bound_svar_is_banned_under_mus ϕ' depth banned
| patt_mu ϕ' ⇒
match depth with
| 0 ⇒ ~~ (bsvar_occur ϕ' (S banned))
| (S depth') ⇒ bound_svar_is_banned_under_mus ϕ' depth' (S banned)
end
end.
Lemma bsvar_occur_false_impl_banned ϕ banned n:
bsvar_occur ϕ banned = false →
bound_svar_is_banned_under_mus ϕ n banned = true
.
Lemma bound_svar_is_banned_under_mus_lt
(ϕ : Pattern) (depth1 depth2 : nat) (banned : db_index)
:
depth1 ≤ depth2 →
bound_svar_is_banned_under_mus ϕ depth1 banned = true →
bound_svar_is_banned_under_mus ϕ depth2 banned = true
.
Lemma bound_svar_is_banned_notfree x ϕ dbi dbi':
dbi > dbi' →
well_formed_closed_mu_aux ϕ dbi' →
x ∉ free_evars ϕ →
bound_svar_is_banned_under_mus ϕ dbi dbi' = true →
x ∉ free_evars ϕ^[svar:dbi↦patt_free_evar x]
.
Lemma maximal_mu_depth_to_svar_subst_evar_banned x ϕ dbi level d:
well_formed_closed_mu_aux ϕ (S dbi) →
evar_is_fresh_in x ϕ →
bound_svar_is_banned_under_mus ϕ level dbi = true →
maximal_mu_depth_to d x ϕ^[svar:dbi↦patt_free_evar x] ≤ (d + level)
.
Lemma maximal_mu_depth_to_lt a b x ϕ:
a > b →
maximal_mu_depth_to a x ϕ ≤ b →
evar_is_fresh_in x ϕ
.
Lemma maximal_mu_depth_to_svar_subst_evar_banned_back x ϕ dbi level d:
well_formed_closed_mu_aux ϕ (S dbi) →
evar_is_fresh_in x ϕ →
maximal_mu_depth_to d x ϕ^[svar:dbi↦patt_free_evar x] ≤ (d + level) →
bound_svar_is_banned_under_mus ϕ level dbi = true
.
Lemma maximal_mu_depth_to_svar_subst_evar_banned_back_2 x ϕ dbi level d:
well_formed_closed_mu_aux ϕ (S dbi) →
evar_is_fresh_in x ϕ →
maximal_mu_depth_to d x ϕ ≤ (d + level) →
bound_svar_is_banned_under_mus ϕ^[svar:dbi↦patt_free_evar x] level dbi = true
.
Lemma bsvar_occur_bevar_subst ϕ ψ edbi sdbi:
well_formed_closed_mu_aux ψ sdbi →
bsvar_occur ϕ sdbi = false →
bsvar_occur ϕ^[evar:edbi↦ψ] sdbi = false
.
Lemma bound_svar_is_banned_under_mus_bevar_subst ϕ ψ dbi level dbi':
well_formed_closed_mu_aux ψ (S dbi') →
bound_svar_is_banned_under_mus ψ level dbi' = true →
bound_svar_is_banned_under_mus ϕ level dbi' = true →
bound_svar_is_banned_under_mus ϕ^[evar:dbi↦ψ] level dbi' = true
.
Lemma bsvar_occur_free_evar_subst ϕ cvar ψ dbi:
well_formed_closed_mu_aux ψ dbi →
bsvar_occur ϕ dbi = false →
bsvar_occur ϕ^[[evar:cvar↦ψ]] dbi = false
.
(* ϕ ≡ (mu, 0) ---> cvar *)
Lemma bound_svar_is_banned_under_mus_fevar_subst_alternative ϕ ψ cvar level dbi':
well_formed_closed_mu_aux ψ (S dbi') = true →
bound_svar_is_banned_under_mus ψ level dbi' = true →
bound_svar_is_banned_under_mus ϕ level dbi' = true →
bound_svar_is_banned_under_mus ϕ^[[evar:cvar↦ψ]] level dbi' = true
.
(* ϕ ≡ (mu, 0) ---> cvar *)
Lemma bound_svar_is_banned_under_mus_fevar_subst ϕ ψ cvar level dbi':
well_formed_closed_mu_aux ϕ (dbi') = true →
well_formed_closed_mu_aux ψ (S dbi') = true →
bound_svar_is_banned_under_mus ψ level dbi' = true →
bound_svar_is_banned_under_mus ϕ^[[evar:cvar↦ψ]] level dbi' = true
.
Lemma bound_svar_is_banned_under_mus_evar_open x ϕ dbi level dbi':
bound_svar_is_banned_under_mus ϕ level dbi' = true →
bound_svar_is_banned_under_mus ϕ^[evar:dbi↦patt_free_evar x] level dbi' = true
.
Lemma bound_svar_is_lt_implies_bound_svar_is_banned_under_mus ϕ level dbi n:
well_formed_closed_mu_aux ϕ (dbi + n) →
bound_svar_is_lt ϕ (level + n) →
bound_svar_is_banned_under_mus ϕ level (dbi + n) = true
.
Example counterexample_1:
∃ cvar cpatt ϕ dbi iter,
well_formed_closed_mu_aux cpatt (S dbi) ∧
maximal_mu_depth_to 0 cvar cpatt ≤ iter ∧
bound_svar_is_banned_under_mus ϕ iter dbi ∧
bound_svar_is_banned_under_mus cpatt^[[evar:cvar↦ϕ]] iter dbi
.
Fixpoint pattern_kt_well_formed (φ : Pattern) :=
match φ with
| patt_free_evar x ⇒ true
| patt_free_svar x ⇒ true
| patt_bound_evar n ⇒ true
| patt_bound_svar n ⇒ true
| patt_sym sigma ⇒ true
| patt_app phi1 phi2 ⇒ pattern_kt_well_formed phi1 && pattern_kt_well_formed phi2
| patt_bott ⇒ true
| patt_imp phi1 phi2 ⇒ pattern_kt_well_formed phi1 && pattern_kt_well_formed phi2
| patt_exists phi ⇒ pattern_kt_well_formed phi
| patt_mu phi ⇒ bound_svar_is_banned_under_mus phi 0 0 &&
pattern_kt_well_formed phi
end.
Lemma kt_well_formed_evar_open (φ : Pattern) x dbi:
pattern_kt_well_formed φ →
pattern_kt_well_formed φ^{evar:dbi↦x}.
Lemma bsvar_occur_bsvar_subst_wf :
∀ φ ψ dbi x,
well_formed_closed_mu_aux φ (S x) →
~~ bsvar_occur φ dbi →
well_formed_closed_mu_aux ψ 0 →
~~ bsvar_occur (bsvar_subst ψ x φ) dbi.
Lemma bound_svar_is_banned_bsvar_subst :
∀ φ ψ level dbi x,
well_formed_closed_mu_aux ψ 0 →
well_formed_closed_mu_aux φ (S x) →
bound_svar_is_banned_under_mus φ level dbi →
bound_svar_is_banned_under_mus (bsvar_subst ψ x φ) level dbi.
Lemma kt_well_formed_svar_open (φ : Pattern) X dbi:
well_formed_closed_mu_aux φ (S dbi) →
pattern_kt_well_formed φ →
pattern_kt_well_formed φ^{svar:dbi↦X}.
(* Mu-freeness is a stricter property. *)
Lemma mf_imp_ktwf φ : mu_free φ → pattern_kt_well_formed φ.
End with_signature.
(* TODO remove these hints *)
#[export]
Hint Resolve well_formed_positive_svar_quantify : core.
#[export]
Hint Resolve no_positive_occurrence_svar_quantify : core.
#[export]
Hint Resolve no_negative_occurrence_svar_quantify : core.
#[export]
Hint Resolve wfc_impl_no_neg_occ : core.
#[export]
Hint Resolve wfp_free_svar_subst : core.
#[export]
Hint Resolve wfp_neg_free_svar_subst : core.
#[export]
Hint Resolve svar_quantify_closed_ex : core.
#[export]
Hint Resolve svar_quantify_closed_mu : core.
#[export]
Hint Resolve evar_quantify_positive : core.
#[export]
Hint Resolve evar_quantify_closed_mu : core.
#[export]
Hint Resolve evar_quantify_closed_ex : core.
#[export]
Hint Resolve wfp_evar_open : core.
#[export]
Hint Resolve wfc_mu_aux_body_ex_imp1 : core.
#[export]
Hint Resolve wfc_ex_aux_body_ex_imp1 : core.
#[export]
Hint Resolve bevar_subst_positive_2 : core.
#[export]
Hint Resolve wfc_mu_aux_bevar_subst : core.
#[export]
Hint Resolve wfc_ex_aux_bevar_subst : core.
#[export]
Hint Resolve wfp_svar_open : core.
#[export]
Hint Resolve wfc_mu_free_evar_subst : core.
This page has been generated by coqdoc