File Pattern
From Coq Require Import Btauto.
From MatchingLogic Require Export
Signature
extralibrary
stdpp_ext.
(* TODO have different type for element variable and for set variable index *)
Definition db_index := nat.
(* begin snippet Pattern *)
Inductive Pattern {Σ : Signature} : Set :=
| patt_free_evar (x : evar)
| patt_free_svar (x : svar)
| patt_bound_evar (n : db_index)
| patt_bound_svar (n : db_index)
| patt_sym (sigma : symbols) : Pattern
| patt_app (phi1 phi2 : Pattern)
| patt_bott
| patt_imp (phi1 phi2 : Pattern)
| patt_exists (phi : Pattern)
| patt_mu (phi : Pattern)
.
(* end snippet Pattern *)
Global Instance Pattern_countable {Σ : Signature} (sc : Countable symbols) : Countable Pattern.
Fixpoint count_binders
{Σ : Signature}
(ϕ : Pattern)
: nat :=
match ϕ with
| patt_free_evar _ ⇒ 0
| patt_free_svar _ ⇒ 0
| patt_bound_evar _ ⇒ 0
| patt_bound_svar _ ⇒ 0
| patt_sym _ ⇒ 0
| patt_bott ⇒ 0
| patt_imp ϕ₁ ϕ₂ ⇒
count_binders ϕ₁ +
count_binders ϕ₂
| patt_app ϕ₁ ϕ₂ ⇒
count_binders ϕ₁ +
count_binders ϕ₂
| patt_exists ϕ' ⇒
S (count_binders ϕ')
| patt_mu ϕ' ⇒
S (count_binders ϕ')
end
.
Definition Theory {Σ : Signature} := propset Pattern.
Section syntax.
Context {Σ : Signature}.
Fixpoint pat_size (p : Pattern) : nat :=
match p with
| patt_app ls rs ⇒ 1 + (pat_size ls) + (pat_size rs)
| patt_imp ls rs ⇒ 1 + (pat_size ls) + (pat_size rs)
| patt_exists p' ⇒ 1 + pat_size p'
| patt_mu p' ⇒ 1 + pat_size p'
| _ ⇒ 1
end.
(* Global Instance PatternSize : Size Pattern := {
size := pat_size;
}. *)
(* Arguments PatternSize /. *)
From MatchingLogic Require Export
Signature
extralibrary
stdpp_ext.
(* TODO have different type for element variable and for set variable index *)
Definition db_index := nat.
(* begin snippet Pattern *)
Inductive Pattern {Σ : Signature} : Set :=
| patt_free_evar (x : evar)
| patt_free_svar (x : svar)
| patt_bound_evar (n : db_index)
| patt_bound_svar (n : db_index)
| patt_sym (sigma : symbols) : Pattern
| patt_app (phi1 phi2 : Pattern)
| patt_bott
| patt_imp (phi1 phi2 : Pattern)
| patt_exists (phi : Pattern)
| patt_mu (phi : Pattern)
.
(* end snippet Pattern *)
Global Instance Pattern_countable {Σ : Signature} (sc : Countable symbols) : Countable Pattern.
Fixpoint count_binders
{Σ : Signature}
(ϕ : Pattern)
: nat :=
match ϕ with
| patt_free_evar _ ⇒ 0
| patt_free_svar _ ⇒ 0
| patt_bound_evar _ ⇒ 0
| patt_bound_svar _ ⇒ 0
| patt_sym _ ⇒ 0
| patt_bott ⇒ 0
| patt_imp ϕ₁ ϕ₂ ⇒
count_binders ϕ₁ +
count_binders ϕ₂
| patt_app ϕ₁ ϕ₂ ⇒
count_binders ϕ₁ +
count_binders ϕ₂
| patt_exists ϕ' ⇒
S (count_binders ϕ')
| patt_mu ϕ' ⇒
S (count_binders ϕ')
end
.
Definition Theory {Σ : Signature} := propset Pattern.
Section syntax.
Context {Σ : Signature}.
Fixpoint pat_size (p : Pattern) : nat :=
match p with
| patt_app ls rs ⇒ 1 + (pat_size ls) + (pat_size rs)
| patt_imp ls rs ⇒ 1 + (pat_size ls) + (pat_size rs)
| patt_exists p' ⇒ 1 + pat_size p'
| patt_mu p' ⇒ 1 + pat_size p'
| _ ⇒ 1
end.
(* Global Instance PatternSize : Size Pattern := {
size := pat_size;
}. *)
(* Arguments PatternSize /. *)
The free names of a type are defined as follow. Notice the
∃ and mu cases: they do not bind any name.
Definition EVarSet := gset evar.
Definition SVarSet := gset svar.
Fixpoint free_evars (phi : Pattern)
: EVarSet :=
match phi with
| patt_free_evar x ⇒ singleton x
| patt_free_svar X ⇒ empty
| patt_bound_evar x ⇒ empty
| patt_bound_svar X ⇒ empty
| patt_sym sigma ⇒ empty
| patt_app phi1 phi2 ⇒ union (free_evars phi1) (free_evars phi2)
| patt_bott ⇒ empty
| patt_imp phi1 phi2 ⇒ union (free_evars phi1) (free_evars phi2)
| patt_exists phi ⇒ free_evars phi
| patt_mu phi ⇒ free_evars phi
end.
Fixpoint free_svars (phi : Pattern)
: SVarSet :=
match phi with
| patt_free_evar x ⇒ empty
| patt_free_svar X ⇒ singleton X
| patt_bound_evar x ⇒ empty
| patt_bound_svar X ⇒ empty
| patt_sym sigma ⇒ empty
| patt_app phi1 phi2 ⇒ union (free_svars phi1) (free_svars phi2)
| patt_bott ⇒ empty
| patt_imp phi1 phi2 ⇒ union (free_svars phi1) (free_svars phi2)
| patt_exists phi ⇒ free_svars phi
| patt_mu phi ⇒ free_svars phi
end.
Definition free_evars_of_list (l : list Pattern) : EVarSet :=
union_list (map free_evars l).
Lemma free_evars_of_list_foldr :
∀ l g,
free_evars (foldr patt_imp g l) =
free_evars g ∪ free_evars_of_list l.
(* for bound set variables *)
Fixpoint no_negative_occurrence_db_b (dbi : db_index) (ϕ : Pattern) : bool :=
match ϕ with
| patt_free_evar _ | patt_free_svar _ | patt_bound_evar _ | patt_sym _ | patt_bott ⇒ true
| patt_bound_svar n ⇒ true
| patt_app ϕ₁ ϕ₂ ⇒ no_negative_occurrence_db_b dbi ϕ₁ && no_negative_occurrence_db_b dbi ϕ₂
| patt_imp ϕ₁ ϕ₂ ⇒ no_positive_occurrence_db_b dbi ϕ₁ && no_negative_occurrence_db_b dbi ϕ₂
| patt_exists ϕ' ⇒ no_negative_occurrence_db_b dbi ϕ'
| patt_mu ϕ' ⇒ no_negative_occurrence_db_b (S dbi) ϕ'
end
with
no_positive_occurrence_db_b (dbi : db_index) (ϕ : Pattern) : bool :=
match ϕ with
| patt_free_evar _ | patt_free_svar _ | patt_bound_evar _ | patt_sym _ | patt_bott ⇒ true
| patt_bound_svar n ⇒ if decide (n = dbi) is left _ then false else true
| patt_app ϕ₁ ϕ₂ ⇒ no_positive_occurrence_db_b dbi ϕ₁ && no_positive_occurrence_db_b dbi ϕ₂
| patt_imp ϕ₁ ϕ₂ ⇒ no_negative_occurrence_db_b dbi ϕ₁ && no_positive_occurrence_db_b dbi ϕ₂
| patt_exists ϕ' ⇒ no_positive_occurrence_db_b dbi ϕ'
| patt_mu ϕ' ⇒ no_positive_occurrence_db_b (S dbi) ϕ'
end.
(* for free element variables *)
Fixpoint evar_has_positive_occurrence (x : evar) (ϕ : Pattern) : bool :=
match ϕ with
| patt_free_evar x' ⇒ if decide (x = x') is left _ then true else false
| patt_free_svar _ | patt_bound_evar _ | patt_bound_svar _ | patt_sym _ | patt_bott ⇒ false
| patt_app ϕ₁ ϕ₂ ⇒ evar_has_positive_occurrence x ϕ₁ || evar_has_positive_occurrence x ϕ₂
| patt_imp ϕ₁ ϕ₂ ⇒ evar_has_negative_occurrence x ϕ₁ || evar_has_positive_occurrence x ϕ₂
| patt_exists ϕ' ⇒ evar_has_positive_occurrence x ϕ'
| patt_mu ϕ' ⇒ evar_has_positive_occurrence x ϕ'
end
with
evar_has_negative_occurrence (x : evar) (ϕ : Pattern) : bool :=
match ϕ with
| patt_free_evar _ | patt_free_svar _ | patt_bound_evar _ | patt_bound_svar _ | patt_sym _ | patt_bott ⇒ false
| patt_app ϕ₁ ϕ₂ ⇒ evar_has_negative_occurrence x ϕ₁ || evar_has_negative_occurrence x ϕ₂
| patt_imp ϕ₁ ϕ₂ ⇒ evar_has_positive_occurrence x ϕ₁ || evar_has_negative_occurrence x ϕ₂
| patt_exists ϕ' ⇒ evar_has_negative_occurrence x ϕ'
| patt_mu ϕ' ⇒ evar_has_negative_occurrence x ϕ'
end.
(* for free set variables *)
Fixpoint svar_has_positive_occurrence (X : svar) (ϕ : Pattern) : bool :=
match ϕ with
| patt_free_svar X' ⇒ if decide (X = X') is left _ then true else false
| patt_free_evar _ | patt_bound_evar _ | patt_bound_svar _ | patt_sym _ | patt_bott ⇒ false
| patt_app ϕ₁ ϕ₂ ⇒ svar_has_positive_occurrence X ϕ₁ || svar_has_positive_occurrence X ϕ₂
| patt_imp ϕ₁ ϕ₂ ⇒ svar_has_negative_occurrence X ϕ₁ || svar_has_positive_occurrence X ϕ₂
| patt_exists ϕ' ⇒ svar_has_positive_occurrence X ϕ'
| patt_mu ϕ' ⇒ svar_has_positive_occurrence X ϕ'
end
with
svar_has_negative_occurrence (X : svar) (ϕ : Pattern) : bool :=
match ϕ with
| patt_free_evar _ | patt_free_svar _ | patt_bound_evar _ | patt_bound_svar _ | patt_sym _ | patt_bott ⇒ false
| patt_app ϕ₁ ϕ₂ ⇒ svar_has_negative_occurrence X ϕ₁ || svar_has_negative_occurrence X ϕ₂
| patt_imp ϕ₁ ϕ₂ ⇒ svar_has_positive_occurrence X ϕ₁ || svar_has_negative_occurrence X ϕ₂
| patt_exists ϕ' ⇒ svar_has_negative_occurrence X ϕ'
| patt_mu ϕ' ⇒ svar_has_negative_occurrence X ϕ'
end.
Fixpoint well_formed_positive (phi : Pattern) : bool :=
match phi with
| patt_free_evar _ ⇒ true
| patt_free_svar _ ⇒ true
| patt_bound_evar _ ⇒ true
| patt_bound_svar _ ⇒ true
| patt_sym _ ⇒ true
| patt_app psi1 psi2 ⇒ well_formed_positive psi1 && well_formed_positive psi2
| patt_bott ⇒ true
| patt_imp psi1 psi2 ⇒ well_formed_positive psi1 && well_formed_positive psi2
| patt_exists psi ⇒ well_formed_positive psi
| patt_mu psi ⇒ no_negative_occurrence_db_b 0 psi && well_formed_positive psi
end.
Fixpoint well_formed_closed_mu_aux (phi : Pattern) (max_ind_svar : db_index) : bool :=
match phi with
| patt_free_evar _ ⇒ true
| patt_free_svar _ ⇒ true
| patt_bound_evar n ⇒ true
| patt_bound_svar n ⇒ if decide (n < max_ind_svar) is left _ then true else false
| patt_sym _ ⇒ true
| patt_app psi1 psi2 ⇒ well_formed_closed_mu_aux psi1 max_ind_svar &&
well_formed_closed_mu_aux psi2 max_ind_svar
| patt_bott ⇒ true
| patt_imp psi1 psi2 ⇒ well_formed_closed_mu_aux psi1 max_ind_svar &&
well_formed_closed_mu_aux psi2 max_ind_svar
| patt_exists psi ⇒ well_formed_closed_mu_aux psi max_ind_svar
| patt_mu psi ⇒ well_formed_closed_mu_aux psi (S max_ind_svar)
end.
Fixpoint well_formed_closed_ex_aux (phi : Pattern) (max_ind_evar : db_index) : bool :=
match phi with
| patt_free_evar _ ⇒ true
| patt_free_svar _ ⇒ true
| patt_bound_evar n ⇒ if decide (n < max_ind_evar) is left _ then true else false
| patt_bound_svar n ⇒ true
| patt_sym _ ⇒ true
| patt_app psi1 psi2 ⇒ well_formed_closed_ex_aux psi1 max_ind_evar &&
well_formed_closed_ex_aux psi2 max_ind_evar
| patt_bott ⇒ true
| patt_imp psi1 psi2 ⇒ well_formed_closed_ex_aux psi1 max_ind_evar &&
well_formed_closed_ex_aux psi2 max_ind_evar
| patt_exists psi ⇒ well_formed_closed_ex_aux psi (S max_ind_evar)
| patt_mu psi ⇒ well_formed_closed_ex_aux psi max_ind_evar
end.
Definition well_formed_closed (phi : Pattern) : bool
:= well_formed_closed_mu_aux phi 0 && well_formed_closed_ex_aux phi 0.
Lemma well_formed_closed_ex_aux_ind (phi : Pattern) (ind_evar1 ind_evar2 : db_index) :
ind_evar1 ≤ ind_evar2 →
well_formed_closed_ex_aux phi ind_evar1 = true→
well_formed_closed_ex_aux phi ind_evar2 = true.
Lemma well_formed_closed_mu_aux_ind (phi : Pattern) (ind_svar1 ind_svar2 : db_index) :
ind_svar1 ≤ ind_svar2 →
well_formed_closed_mu_aux phi ind_svar1 = true →
well_formed_closed_mu_aux phi ind_svar2 = true.
Definition well_formed (phi : Pattern) := well_formed_positive phi && well_formed_closed phi.
Lemma well_formed_bott:
well_formed patt_bott.
Lemma well_formed_sym s:
well_formed (patt_sym s).
Lemma well_formed_imp ϕ₁ ϕ₂:
well_formed ϕ₁ = true →
well_formed ϕ₂ = true →
well_formed (patt_imp ϕ₁ ϕ₂) = true.
Lemma well_formed_app ϕ₁ ϕ₂:
well_formed ϕ₁ = true →
well_formed ϕ₂ = true →
well_formed (patt_app ϕ₁ ϕ₂) = true.
Lemma well_formed_ex_app ϕ₁ ϕ₂:
well_formed (patt_exists ϕ₁) = true →
well_formed (patt_exists ϕ₂) = true →
well_formed (patt_exists (patt_app ϕ₁ ϕ₂)) = true.
Lemma well_formed_impl_well_formed_ex ϕ:
well_formed ϕ = true →
well_formed (patt_exists ϕ) = true.
(* TODO: why is this Private? It can be useful for not only 0 dbi *)
Lemma Private_wfc_impl_no_neg_pos_occ psi maxsvar dbi:
well_formed_closed_mu_aux psi maxsvar = true →
maxsvar ≤ dbi →
no_negative_occurrence_db_b dbi psi = true
∧ no_positive_occurrence_db_b dbi psi = true.
Corollary wfc_impl_no_neg_occ psi dbi:
well_formed_closed_mu_aux psi 0 = true →
no_negative_occurrence_db_b dbi psi = true.
Corollary wfc_impl_no_pos_occ psi dbi:
well_formed_closed_mu_aux psi 0 = true →
no_positive_occurrence_db_b dbi psi = true.
Lemma well_formed_app_1 : ∀ (phi1 phi2 : Pattern),
well_formed (patt_app phi1 phi2) → well_formed phi1.
Lemma well_formed_app_2 : ∀ (phi1 phi2 : Pattern),
well_formed (patt_app phi1 phi2) → well_formed phi2.
Lemma free_svars_exists : ∀ (ϕ : Pattern),
free_svars (patt_exists ϕ) = free_svars ϕ.
Lemma wfc_impl_no_neg_pos_occ p m:
well_formed_closed_mu_aux p m →
(no_negative_occurrence_db_b m p && no_positive_occurrence_db_b m p) = true.
Fixpoint mu_free (p : Pattern) : bool :=
match p 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 ⇒ mu_free phi1 && mu_free phi2
| patt_bott ⇒ true
| patt_imp phi1 phi2 ⇒ mu_free phi1 && mu_free phi2
| patt_exists phi ⇒ mu_free phi
| patt_mu phi ⇒ false
end.
(* Fragment of matching logic without set variables and mu *)
Fixpoint set_free (p : Pattern) : bool :=
match p with
| patt_free_evar x ⇒ true
| patt_free_svar x ⇒ false
| patt_bound_evar n ⇒ true
| patt_bound_svar n ⇒ false
| patt_sym sigma ⇒ true
| patt_app phi1 phi2 ⇒ set_free phi1 && set_free phi2
| patt_bott ⇒ true
| patt_imp phi1 phi2 ⇒ set_free phi1 && set_free phi2
| patt_exists phi ⇒ set_free phi
| patt_mu phi ⇒ false
end.
Lemma set_free_implies_mu_free p:
set_free p = true → mu_free p = true.
Theorem mu_free_wfp φ :
mu_free φ → well_formed_positive φ.
Lemma wf_imp_wfc ϕ:
well_formed ϕ → well_formed_closed ϕ.
Definition evar_is_fresh_in x ϕ := x ∉ free_evars ϕ.
Definition svar_is_fresh_in x ϕ := x ∉ free_svars ϕ.
This function is used for linear contexts
Fixpoint count_evar_occurrences (x : evar) (p : Pattern) :=
match p with
| patt_free_evar x' ⇒ if decide (x' = x) is left _ then 1 else 0
| patt_free_svar _ ⇒ 0
| patt_bound_evar _ ⇒ 0
| patt_bound_svar _ ⇒ 0
| patt_sym _ ⇒ 0
| patt_app phi1 phi2 ⇒ count_evar_occurrences x phi1 + count_evar_occurrences x phi2
| patt_bott ⇒ 0
| patt_imp phi1 phi2 ⇒ count_evar_occurrences x phi1 + count_evar_occurrences x phi2
| patt_exists phi' ⇒ count_evar_occurrences x phi'
| patt_mu phi' ⇒ count_evar_occurrences x phi'
end.
Lemma count_evar_occurrences_0 (x : evar) (p : Pattern) :
x ∉ free_evars p ↔
count_evar_occurrences x p = 0.
Lemma count_evar_occurrences_not_0 (x : evar) (p : Pattern) :
x ∈ free_evars p ↔
count_evar_occurrences x p > 0.
End syntax.
Lemma well_formed_app_proj1 {Σ : Signature} p q:
well_formed (patt_app p q) →
well_formed p.
Lemma well_formed_app_proj2 {Σ : Signature} p q:
well_formed (patt_app p q) →
well_formed q.
Lemma well_formed_imp_proj1 {Σ : Signature} p q:
well_formed (patt_imp p q) →
well_formed p.
Lemma well_formed_imp_proj2 {Σ : Signature} p q:
well_formed (patt_imp p q) →
well_formed q.
Definition well_formed_xy {Σ : Signature} (x y : nat) (ϕ : Pattern) : bool :=
well_formed_positive ϕ &&
well_formed_closed_ex_aux ϕ x &&
well_formed_closed_mu_aux ϕ y
.
Lemma wfxy00_wf {Σ : Signature} (ϕ : Pattern) :
well_formed_xy 0 0 ϕ = well_formed ϕ.
Lemma wf_wfxy00 {Σ : Signature} (ϕ : Pattern) :
well_formed ϕ = well_formed_xy 0 0 ϕ
.
Lemma wf_wfxy00_compose {Σ : Signature} (ϕ : Pattern) :
well_formed_xy 0 0 ϕ = true →
well_formed ϕ = true
.
Lemma wf_wfxy00_decompose {Σ : Signature} (ϕ : Pattern) :
well_formed ϕ = true →
well_formed_xy 0 0 ϕ = true
.
Definition lwf_xy {Σ : Signature} (x y : nat) (l : list Pattern)
:= fold_right andb true (map (well_formed_xy x y) l).
Definition lwf_positive {Σ : Signature} (l : list Pattern)
:= fold_right andb true (map well_formed_positive l).
Definition lwf_cmu {Σ : Signature} n (l : list Pattern)
:= fold_right andb true (map (fun p ⇒ well_formed_closed_mu_aux p n) l).
Definition lwf_cex {Σ : Signature} n (l : list Pattern)
:= fold_right andb true (map (fun p ⇒ well_formed_closed_ex_aux p n) l).
Definition wf {Σ : Signature} (l : list Pattern) := fold_right andb true (map well_formed l).
Lemma wf_lwf_xy {Σ : Signature} (l : list Pattern) :
wf l = lwf_xy 0 0 l
.
Lemma wf_lwf_xy_compose {Σ : Signature} (l : list Pattern) :
lwf_xy 0 0 l = true →
wf l = true
.
Lemma wf_lwf_xy_decompose {Σ : Signature} (l : list Pattern) :
wf l = true →
lwf_xy 0 0 l = true
.
Lemma wf_corr {Σ : Signature} (l : list Pattern) :
wf l = lwf_positive l && lwf_cmu 0 l && lwf_cex 0 l
.
Lemma lwf_xy_decompose {Σ : Signature} (x y : nat) (l : list Pattern) :
lwf_xy x y l = lwf_positive l && lwf_cmu y l && lwf_cex x l
.
Lemma lwf_xy_cons
{Σ : Signature} (m n : nat) (x : Pattern) (xs : list Pattern)
:
lwf_xy m n (x::xs) = well_formed_xy m n x && lwf_xy m n xs
.
Lemma lwf_xy_cons_compose
{Σ : Signature} (m n : nat) (x : Pattern) (xs : list Pattern)
:
well_formed_xy m n x = true ∧ lwf_xy m n xs = true →
lwf_xy m n (x::xs) = true
.
Lemma lwf_xy_cons_decompose
{Σ : Signature} (m n : nat) (x : Pattern) (xs : list Pattern)
:
lwf_xy m n (x::xs) = true →
well_formed_xy m n x = true ∧ lwf_xy m n xs = true
.
Lemma lwf_positive_cons
{Σ : Signature} (x : Pattern) (xs : list Pattern)
:
lwf_positive (x::xs) = well_formed_positive x && lwf_positive xs
.
Lemma lwf_cmu_cons
{Σ : Signature} (n : nat) (x : Pattern) (xs : list Pattern)
:
lwf_cmu n (x::xs) = well_formed_closed_mu_aux x n && lwf_cmu n xs
.
Lemma lwf_cex_cons
{Σ : Signature} (n : nat) (x : Pattern) (xs : list Pattern)
:
lwf_cex n (x::xs) = well_formed_closed_ex_aux x n && lwf_cex n xs
.
Lemma lwf_xy_app
{Σ : Signature} (m n : nat) (xs ys : list Pattern)
:
lwf_xy m n (xs ++ ys) = lwf_xy m n xs && lwf_xy m n ys
.
Lemma lwf_xy_app_compose
{Σ : Signature} (m n : nat) (xs ys : list Pattern)
:
lwf_xy m n xs = true ∧ lwf_xy m n ys = true →
lwf_xy m n (xs ++ ys) = true
.
Lemma lwf_xy_app_decompose
{Σ : Signature} (m n : nat) (xs ys : list Pattern)
:
lwf_xy m n (xs ++ ys) = true →
lwf_xy m n xs = true ∧ lwf_xy m n ys = true
.
Lemma lwf_positive_app
{Σ : Signature} (xs ys : list Pattern)
:
lwf_positive (xs++ys) = lwf_positive xs && lwf_positive ys
.
Lemma lwf_cmu_app
{Σ : Signature} (n : nat) (xs ys : list Pattern)
:
lwf_cmu n (xs++ys) = lwf_cmu n xs && lwf_cmu n ys
.
Lemma lwf_cex_app
{Σ : Signature} (n : nat) (xs ys : list Pattern)
:
lwf_cex n (xs++ys) = lwf_cex n xs && lwf_cex n ys
.
Lemma well_formed_foldr {Σ : Signature} g xs :
well_formed g = true →
wf xs = true →
well_formed (foldr patt_imp g xs) = true.
Lemma wf_take {Σ : Signature} n xs :
wf xs = true →
wf (take n xs) = true.
Lemma wf_drop {Σ : Signature} n xs:
wf xs = true →
wf (drop n xs) = true.
Lemma wf_insert {Σ : Signature} n p xs:
wf xs = true →
well_formed p = true →
wf (<[n := p]> xs) = true.
Lemma wf_tail' {Σ : Signature} p xs:
wf (p :: xs) = true →
wf xs = true.
Lemma wf_cons {Σ : Signature} x xs:
well_formed x = true →
wf xs = true →
wf (x :: xs) = true.
Lemma wf_app {Σ : Signature} xs ys:
wf xs = true →
wf ys = true →
wf (xs ++ ys) = true.
(* TODO move somewhere else *)
Lemma wfapp_proj_1 {Σ : Signature} l₁ l₂:
wf (l₁ ++ l₂) = true →
wf l₁ = true.
Lemma wfapp_proj_2 {Σ : Signature} l₁ l₂:
wf (l₁ ++ l₂) = true →
wf l₂ = true.
Lemma wfl₁hl₂_proj_l₁ {Σ : Signature} l₁ h l₂:
wf (l₁ ++ h :: l₂) →
wf l₁.
Lemma wfl₁hl₂_proj_h {Σ : Signature} l₁ h l₂:
wf (l₁ ++ h :: l₂) →
well_formed h.
Lemma wfl₁hl₂_proj_l₂ {Σ : Signature} l₁ h l₂:
wf (l₁ ++ h :: l₂) →
wf l₂.
Lemma wfl₁hl₂_proj_l₁l₂ {Σ : Signature} l₁ h l₂:
wf (l₁ ++ h :: l₂) →
wf (l₁ ++ l₂).
Definition wfPattern {Σ : Signature} := {p : Pattern | well_formed p = true}.
Global Instance wfPattern_eqdec {Σ : Signature} : EqDecision wfPattern.
Global Instance wfPattern_countable {Σ : Signature} : Countable wfPattern.
Global Instance Pattern_infinite {Σ : Signature} :
Infinite Pattern.
Global Instance wfPattern_infinite {Σ : Signature} :
Infinite wfPattern.
Lemma map_wf :
∀ {Σ : Signature} (f : Pattern → Pattern) l,
wf l → (∀ p, well_formed p → well_formed (f p)) →
wf (map f l).
(* Allows splitting `wf` without unfolding in-place. *)
Lemma wf_cons_iff {Σ : Signature} x l : wf (x :: l) ↔ well_formed x ∧ wf l.
Section corollaries.
Context {Σ : Signature}.
Lemma Forall_wf_map {A} (t : A → Pattern) l : Forall (well_formed ∘ t) l ↔ wf (map t l).
Corollary wf_fold_left {A : Type} (f : Pattern → A → Pattern) (t : A → Pattern) x xs :
well_formed x →
wf (map t xs) →
(∀ a b, well_formed a → well_formed (t b) → well_formed (f a b)) →
well_formed (fold_left f xs x).
Corollary wf_foldr {A : Type} (f : A → Pattern → Pattern) (t : A → Pattern) x xs :
well_formed x →
wf (map t xs) →
(∀ a b, well_formed a → well_formed (t b) → well_formed (f b a)) →
well_formed (foldr f x xs).
Corollary mf_fold_left {A : Type} (f : Pattern → A → Pattern) (t : A → Pattern) x xs :
mu_free x →
foldr (fun c a ⇒ mu_free c && a) true (map t xs) →
(∀ a b, mu_free a → mu_free (t b) → mu_free (f a b)) →
mu_free (fold_left f xs x).
Corollary mf_foldr {A : Type} (f : A → Pattern → Pattern) (t : A → Pattern) x xs :
mu_free x →
foldr (fun c a ⇒ mu_free c && a) true (map t xs) →
(∀ a b, mu_free a → mu_free (t b) → mu_free (f b a)) →
mu_free (foldr f x xs).
End corollaries.
Ltac size_induction φ :=
match type of φ with
| Pattern ⇒ let sz := fresh "sz" in
let Hsz := fresh "Hsz" in
let H := fresh "H" in
remember (pat_size φ) as sz eqn:H;
assert (pat_size φ ≤ sz) as Hsz by lia;
clear H;
revert φ Hsz;
let sz' := fresh "sz" in
let IHsz := fresh "IHsz" in
induction sz as [|sz' IHsz]; intros φ Hsz; [
destruct φ; simpl pat_size in Hsz; lia
|
destruct φ;
(* unfold PatternSize in Hsz, IHsz; *)
simpl in Hsz
(* replace pat_size with (size : Pattern -> nat) in * by reflexivity *)
]
end.
Local Lemma test_ind :
∀ {Σ : Signature} (φ : Pattern),
size (∅ : EVarSet) = 0 → pat_size φ = pat_size (patt_app φ φ).
Module BoundVarSugar.
(* Element variables - bound *)
Notation b0 := (patt_bound_evar 0).
Notation b1 := (patt_bound_evar 1).
Notation b2 := (patt_bound_evar 2).
Notation b3 := (patt_bound_evar 3).
Notation b4 := (patt_bound_evar 4).
Notation b5 := (patt_bound_evar 5).
Notation b6 := (patt_bound_evar 6).
Notation b7 := (patt_bound_evar 7).
Notation b8 := (patt_bound_evar 8).
Notation b9 := (patt_bound_evar 9).
Notation B0 := (patt_bound_svar 0).
Notation B1 := (patt_bound_svar 1).
Notation B2 := (patt_bound_svar 2).
Notation B3 := (patt_bound_svar 3).
Notation B4 := (patt_bound_svar 4).
Notation B5 := (patt_bound_svar 5).
Notation B6 := (patt_bound_svar 6).
Notation B7 := (patt_bound_svar 7).
Notation B8 := (patt_bound_svar 8).
Notation B9 := (patt_bound_svar 9).
End BoundVarSugar.
Module Notations.
Declare Scope ml_scope.
Delimit Scope ml_scope with ml.
Notation "a ⋅ b" := (patt_app a b) (at level 66, left associativity) : ml_scope.
Notation "⊥" := patt_bott : ml_scope.
Notation "a ---> b" := (patt_imp a b) (at level 75, right associativity) : ml_scope.
Notation "'ex' , phi" := (patt_exists phi) (at level 80) : ml_scope.
Notation "'mu' , phi" := (patt_mu phi) (at level 80) : ml_scope.
(*Notation "AC p " := (subst_ctx AC p) (at level 90) : ml_scope.*)
End Notations.
match p with
| patt_free_evar x' ⇒ if decide (x' = x) is left _ then 1 else 0
| patt_free_svar _ ⇒ 0
| patt_bound_evar _ ⇒ 0
| patt_bound_svar _ ⇒ 0
| patt_sym _ ⇒ 0
| patt_app phi1 phi2 ⇒ count_evar_occurrences x phi1 + count_evar_occurrences x phi2
| patt_bott ⇒ 0
| patt_imp phi1 phi2 ⇒ count_evar_occurrences x phi1 + count_evar_occurrences x phi2
| patt_exists phi' ⇒ count_evar_occurrences x phi'
| patt_mu phi' ⇒ count_evar_occurrences x phi'
end.
Lemma count_evar_occurrences_0 (x : evar) (p : Pattern) :
x ∉ free_evars p ↔
count_evar_occurrences x p = 0.
Lemma count_evar_occurrences_not_0 (x : evar) (p : Pattern) :
x ∈ free_evars p ↔
count_evar_occurrences x p > 0.
End syntax.
Lemma well_formed_app_proj1 {Σ : Signature} p q:
well_formed (patt_app p q) →
well_formed p.
Lemma well_formed_app_proj2 {Σ : Signature} p q:
well_formed (patt_app p q) →
well_formed q.
Lemma well_formed_imp_proj1 {Σ : Signature} p q:
well_formed (patt_imp p q) →
well_formed p.
Lemma well_formed_imp_proj2 {Σ : Signature} p q:
well_formed (patt_imp p q) →
well_formed q.
Definition well_formed_xy {Σ : Signature} (x y : nat) (ϕ : Pattern) : bool :=
well_formed_positive ϕ &&
well_formed_closed_ex_aux ϕ x &&
well_formed_closed_mu_aux ϕ y
.
Lemma wfxy00_wf {Σ : Signature} (ϕ : Pattern) :
well_formed_xy 0 0 ϕ = well_formed ϕ.
Lemma wf_wfxy00 {Σ : Signature} (ϕ : Pattern) :
well_formed ϕ = well_formed_xy 0 0 ϕ
.
Lemma wf_wfxy00_compose {Σ : Signature} (ϕ : Pattern) :
well_formed_xy 0 0 ϕ = true →
well_formed ϕ = true
.
Lemma wf_wfxy00_decompose {Σ : Signature} (ϕ : Pattern) :
well_formed ϕ = true →
well_formed_xy 0 0 ϕ = true
.
Definition lwf_xy {Σ : Signature} (x y : nat) (l : list Pattern)
:= fold_right andb true (map (well_formed_xy x y) l).
Definition lwf_positive {Σ : Signature} (l : list Pattern)
:= fold_right andb true (map well_formed_positive l).
Definition lwf_cmu {Σ : Signature} n (l : list Pattern)
:= fold_right andb true (map (fun p ⇒ well_formed_closed_mu_aux p n) l).
Definition lwf_cex {Σ : Signature} n (l : list Pattern)
:= fold_right andb true (map (fun p ⇒ well_formed_closed_ex_aux p n) l).
Definition wf {Σ : Signature} (l : list Pattern) := fold_right andb true (map well_formed l).
Lemma wf_lwf_xy {Σ : Signature} (l : list Pattern) :
wf l = lwf_xy 0 0 l
.
Lemma wf_lwf_xy_compose {Σ : Signature} (l : list Pattern) :
lwf_xy 0 0 l = true →
wf l = true
.
Lemma wf_lwf_xy_decompose {Σ : Signature} (l : list Pattern) :
wf l = true →
lwf_xy 0 0 l = true
.
Lemma wf_corr {Σ : Signature} (l : list Pattern) :
wf l = lwf_positive l && lwf_cmu 0 l && lwf_cex 0 l
.
Lemma lwf_xy_decompose {Σ : Signature} (x y : nat) (l : list Pattern) :
lwf_xy x y l = lwf_positive l && lwf_cmu y l && lwf_cex x l
.
Lemma lwf_xy_cons
{Σ : Signature} (m n : nat) (x : Pattern) (xs : list Pattern)
:
lwf_xy m n (x::xs) = well_formed_xy m n x && lwf_xy m n xs
.
Lemma lwf_xy_cons_compose
{Σ : Signature} (m n : nat) (x : Pattern) (xs : list Pattern)
:
well_formed_xy m n x = true ∧ lwf_xy m n xs = true →
lwf_xy m n (x::xs) = true
.
Lemma lwf_xy_cons_decompose
{Σ : Signature} (m n : nat) (x : Pattern) (xs : list Pattern)
:
lwf_xy m n (x::xs) = true →
well_formed_xy m n x = true ∧ lwf_xy m n xs = true
.
Lemma lwf_positive_cons
{Σ : Signature} (x : Pattern) (xs : list Pattern)
:
lwf_positive (x::xs) = well_formed_positive x && lwf_positive xs
.
Lemma lwf_cmu_cons
{Σ : Signature} (n : nat) (x : Pattern) (xs : list Pattern)
:
lwf_cmu n (x::xs) = well_formed_closed_mu_aux x n && lwf_cmu n xs
.
Lemma lwf_cex_cons
{Σ : Signature} (n : nat) (x : Pattern) (xs : list Pattern)
:
lwf_cex n (x::xs) = well_formed_closed_ex_aux x n && lwf_cex n xs
.
Lemma lwf_xy_app
{Σ : Signature} (m n : nat) (xs ys : list Pattern)
:
lwf_xy m n (xs ++ ys) = lwf_xy m n xs && lwf_xy m n ys
.
Lemma lwf_xy_app_compose
{Σ : Signature} (m n : nat) (xs ys : list Pattern)
:
lwf_xy m n xs = true ∧ lwf_xy m n ys = true →
lwf_xy m n (xs ++ ys) = true
.
Lemma lwf_xy_app_decompose
{Σ : Signature} (m n : nat) (xs ys : list Pattern)
:
lwf_xy m n (xs ++ ys) = true →
lwf_xy m n xs = true ∧ lwf_xy m n ys = true
.
Lemma lwf_positive_app
{Σ : Signature} (xs ys : list Pattern)
:
lwf_positive (xs++ys) = lwf_positive xs && lwf_positive ys
.
Lemma lwf_cmu_app
{Σ : Signature} (n : nat) (xs ys : list Pattern)
:
lwf_cmu n (xs++ys) = lwf_cmu n xs && lwf_cmu n ys
.
Lemma lwf_cex_app
{Σ : Signature} (n : nat) (xs ys : list Pattern)
:
lwf_cex n (xs++ys) = lwf_cex n xs && lwf_cex n ys
.
Lemma well_formed_foldr {Σ : Signature} g xs :
well_formed g = true →
wf xs = true →
well_formed (foldr patt_imp g xs) = true.
Lemma wf_take {Σ : Signature} n xs :
wf xs = true →
wf (take n xs) = true.
Lemma wf_drop {Σ : Signature} n xs:
wf xs = true →
wf (drop n xs) = true.
Lemma wf_insert {Σ : Signature} n p xs:
wf xs = true →
well_formed p = true →
wf (<[n := p]> xs) = true.
Lemma wf_tail' {Σ : Signature} p xs:
wf (p :: xs) = true →
wf xs = true.
Lemma wf_cons {Σ : Signature} x xs:
well_formed x = true →
wf xs = true →
wf (x :: xs) = true.
Lemma wf_app {Σ : Signature} xs ys:
wf xs = true →
wf ys = true →
wf (xs ++ ys) = true.
(* TODO move somewhere else *)
Lemma wfapp_proj_1 {Σ : Signature} l₁ l₂:
wf (l₁ ++ l₂) = true →
wf l₁ = true.
Lemma wfapp_proj_2 {Σ : Signature} l₁ l₂:
wf (l₁ ++ l₂) = true →
wf l₂ = true.
Lemma wfl₁hl₂_proj_l₁ {Σ : Signature} l₁ h l₂:
wf (l₁ ++ h :: l₂) →
wf l₁.
Lemma wfl₁hl₂_proj_h {Σ : Signature} l₁ h l₂:
wf (l₁ ++ h :: l₂) →
well_formed h.
Lemma wfl₁hl₂_proj_l₂ {Σ : Signature} l₁ h l₂:
wf (l₁ ++ h :: l₂) →
wf l₂.
Lemma wfl₁hl₂_proj_l₁l₂ {Σ : Signature} l₁ h l₂:
wf (l₁ ++ h :: l₂) →
wf (l₁ ++ l₂).
Definition wfPattern {Σ : Signature} := {p : Pattern | well_formed p = true}.
Global Instance wfPattern_eqdec {Σ : Signature} : EqDecision wfPattern.
Global Instance wfPattern_countable {Σ : Signature} : Countable wfPattern.
Global Instance Pattern_infinite {Σ : Signature} :
Infinite Pattern.
Global Instance wfPattern_infinite {Σ : Signature} :
Infinite wfPattern.
Lemma map_wf :
∀ {Σ : Signature} (f : Pattern → Pattern) l,
wf l → (∀ p, well_formed p → well_formed (f p)) →
wf (map f l).
(* Allows splitting `wf` without unfolding in-place. *)
Lemma wf_cons_iff {Σ : Signature} x l : wf (x :: l) ↔ well_formed x ∧ wf l.
Section corollaries.
Context {Σ : Signature}.
Lemma Forall_wf_map {A} (t : A → Pattern) l : Forall (well_formed ∘ t) l ↔ wf (map t l).
Corollary wf_fold_left {A : Type} (f : Pattern → A → Pattern) (t : A → Pattern) x xs :
well_formed x →
wf (map t xs) →
(∀ a b, well_formed a → well_formed (t b) → well_formed (f a b)) →
well_formed (fold_left f xs x).
Corollary wf_foldr {A : Type} (f : A → Pattern → Pattern) (t : A → Pattern) x xs :
well_formed x →
wf (map t xs) →
(∀ a b, well_formed a → well_formed (t b) → well_formed (f b a)) →
well_formed (foldr f x xs).
Corollary mf_fold_left {A : Type} (f : Pattern → A → Pattern) (t : A → Pattern) x xs :
mu_free x →
foldr (fun c a ⇒ mu_free c && a) true (map t xs) →
(∀ a b, mu_free a → mu_free (t b) → mu_free (f a b)) →
mu_free (fold_left f xs x).
Corollary mf_foldr {A : Type} (f : A → Pattern → Pattern) (t : A → Pattern) x xs :
mu_free x →
foldr (fun c a ⇒ mu_free c && a) true (map t xs) →
(∀ a b, mu_free a → mu_free (t b) → mu_free (f b a)) →
mu_free (foldr f x xs).
End corollaries.
Ltac size_induction φ :=
match type of φ with
| Pattern ⇒ let sz := fresh "sz" in
let Hsz := fresh "Hsz" in
let H := fresh "H" in
remember (pat_size φ) as sz eqn:H;
assert (pat_size φ ≤ sz) as Hsz by lia;
clear H;
revert φ Hsz;
let sz' := fresh "sz" in
let IHsz := fresh "IHsz" in
induction sz as [|sz' IHsz]; intros φ Hsz; [
destruct φ; simpl pat_size in Hsz; lia
|
destruct φ;
(* unfold PatternSize in Hsz, IHsz; *)
simpl in Hsz
(* replace pat_size with (size : Pattern -> nat) in * by reflexivity *)
]
end.
Local Lemma test_ind :
∀ {Σ : Signature} (φ : Pattern),
size (∅ : EVarSet) = 0 → pat_size φ = pat_size (patt_app φ φ).
Module BoundVarSugar.
(* Element variables - bound *)
Notation b0 := (patt_bound_evar 0).
Notation b1 := (patt_bound_evar 1).
Notation b2 := (patt_bound_evar 2).
Notation b3 := (patt_bound_evar 3).
Notation b4 := (patt_bound_evar 4).
Notation b5 := (patt_bound_evar 5).
Notation b6 := (patt_bound_evar 6).
Notation b7 := (patt_bound_evar 7).
Notation b8 := (patt_bound_evar 8).
Notation b9 := (patt_bound_evar 9).
Notation B0 := (patt_bound_svar 0).
Notation B1 := (patt_bound_svar 1).
Notation B2 := (patt_bound_svar 2).
Notation B3 := (patt_bound_svar 3).
Notation B4 := (patt_bound_svar 4).
Notation B5 := (patt_bound_svar 5).
Notation B6 := (patt_bound_svar 6).
Notation B7 := (patt_bound_svar 7).
Notation B8 := (patt_bound_svar 8).
Notation B9 := (patt_bound_svar 9).
End BoundVarSugar.
Module Notations.
Declare Scope ml_scope.
Delimit Scope ml_scope with ml.
Notation "a ⋅ b" := (patt_app a b) (at level 66, left associativity) : ml_scope.
Notation "⊥" := patt_bott : ml_scope.
Notation "a ---> b" := (patt_imp a b) (at level 75, right associativity) : ml_scope.
Notation "'ex' , phi" := (patt_exists phi) (at level 80) : ml_scope.
Notation "'mu' , phi" := (patt_mu phi) (at level 80) : ml_scope.
(*Notation "AC p " := (subst_ctx AC p) (at level 90) : ml_scope.*)
End Notations.
This page has been generated by coqdoc