File Freshness
From MatchingLogic Require Export Pattern.
Section freshness.
Context {Σ : Signature}.
(* fresh variables *)
Definition evar_fresh (l : list evar) : evar := fresh l.
Definition svar_fresh (l : list svar) : svar := fresh l.
Definition evar_fresh_s (s : EVarSet) : evar := evar_fresh (elements s).
Definition svar_fresh_s (s : SVarSet) : svar := svar_fresh (elements s).
Definition fresh_evar ϕ := evar_fresh_s (free_evars ϕ).
Definition fresh_svar ϕ := svar_fresh_s (free_svars ϕ).
(* Lemmas about fresh variables *)
Lemma set_evar_fresh_is_fresh'' (S : list evar) : (evar_fresh S) ∉ S.
Lemma set_evar_fresh_is_fresh' (S : EVarSet) : evar_fresh (elements S) ∉ S.
Lemma set_evar_fresh_is_fresh ϕ : evar_is_fresh_in (fresh_evar ϕ) ϕ.
Hint Resolve set_evar_fresh_is_fresh : core.
Lemma set_svar_fresh_is_fresh'' (S : list svar) : (svar_fresh S) ∉ S.
Lemma set_svar_fresh_is_fresh' (S : SVarSet) : svar_fresh (elements S) ∉ S.
Lemma set_svar_fresh_is_fresh ϕ : svar_is_fresh_in (fresh_svar ϕ) ϕ.
Hint Resolve set_svar_fresh_is_fresh : core.
Lemma evar_is_fresh_in_richer' x ϕ B:
free_evars ϕ ⊆ B →
x ∉ B →
evar_is_fresh_in x ϕ.
Lemma evar_is_fresh_in_richer x ϕ₁ ϕ₂:
free_evars ϕ₁ ⊆ free_evars ϕ₂ →
evar_is_fresh_in x ϕ₂ →
evar_is_fresh_in x ϕ₁.
Lemma svar_is_fresh_in_richer' X ϕ B:
free_svars ϕ ⊆ B →
X ∉ B →
svar_is_fresh_in X ϕ.
Lemma svar_is_fresh_in_richer X ϕ₁ ϕ₂:
free_svars ϕ₁ ⊆ free_svars ϕ₂ →
svar_is_fresh_in X ϕ₂ →
svar_is_fresh_in X ϕ₁.
(*
Lemma fresh_neq_fresh_l ϕ₁ ϕ₂ :
(*~ evar_is_fresh_in (fresh_evar ϕ₁) ϕ₂ ->*)
free_evars ϕ₁ ⊈
fresh_evar ϕ₁ ≠ fresh_evar ϕ₂.
Proof.
intros H.
unfold fresh_evar at 2.
*)
Hint Resolve evar_is_fresh_in_richer : core.
Lemma not_free_implies_positive_negative_occurrence :
∀ (phi : Pattern) (X : svar),
X ∉ (free_svars phi) →
svar_has_positive_occurrence X phi = false ∧ svar_has_negative_occurrence X phi = false.
Corollary evar_is_fresh_in_app_l x ϕ₁ ϕ₂ :
evar_is_fresh_in x (patt_app ϕ₁ ϕ₂) → evar_is_fresh_in x ϕ₁.
Corollary svar_is_fresh_in_app_l X ϕ₁ ϕ₂ :
svar_is_fresh_in X (patt_app ϕ₁ ϕ₂) → svar_is_fresh_in X ϕ₁.
(*Hint Resolve evar_is_fresh_in_app_l : core.*)
Corollary evar_is_fresh_in_app_r x ϕ₁ ϕ₂ :
evar_is_fresh_in x (patt_app ϕ₁ ϕ₂) → evar_is_fresh_in x ϕ₂.
Corollary svar_is_fresh_in_app_r X ϕ₁ ϕ₂ :
svar_is_fresh_in X (patt_app ϕ₁ ϕ₂) → svar_is_fresh_in X ϕ₂.
Lemma evar_is_fresh_in_app x ϕ₁ ϕ₂ :
evar_is_fresh_in x (patt_app ϕ₁ ϕ₂)
↔ (evar_is_fresh_in x ϕ₁ ∧ evar_is_fresh_in x ϕ₂).
Lemma svar_is_fresh_in_app X ϕ₁ ϕ₂ :
svar_is_fresh_in X (patt_app ϕ₁ ϕ₂)
↔ (svar_is_fresh_in X ϕ₁ ∧ svar_is_fresh_in X ϕ₂).
(*Hint Resolve evar_is_fresh_in_app_r : core.*)
Corollary evar_is_fresh_in_imp_l x ϕ₁ ϕ₂ :
evar_is_fresh_in x (patt_imp ϕ₁ ϕ₂) → evar_is_fresh_in x ϕ₁.
Corollary svar_is_fresh_in_imp_l X ϕ₁ ϕ₂ :
svar_is_fresh_in X (patt_imp ϕ₁ ϕ₂) → svar_is_fresh_in X ϕ₁.
(*Hint Resolve evar_is_fresh_in_imp_l : core.*)
Corollary evar_is_fresh_in_imp_r x ϕ₁ ϕ₂ :
evar_is_fresh_in x (patt_imp ϕ₁ ϕ₂) → evar_is_fresh_in x ϕ₂.
Corollary svar_is_fresh_in_imp_r X ϕ₁ ϕ₂ :
svar_is_fresh_in X (patt_imp ϕ₁ ϕ₂) → svar_is_fresh_in X ϕ₂.
Lemma evar_is_fresh_in_imp x ϕ₁ ϕ₂ :
evar_is_fresh_in x (patt_imp ϕ₁ ϕ₂)
↔ (evar_is_fresh_in x ϕ₁ ∧ evar_is_fresh_in x ϕ₂).
Lemma svar_is_fresh_in_imp X ϕ₁ ϕ₂ :
svar_is_fresh_in X (patt_imp ϕ₁ ϕ₂)
↔ (svar_is_fresh_in X ϕ₁ ∧ svar_is_fresh_in X ϕ₂).
(*Hint Resolve evar_is_fresh_in_imp_r : core.*)
Corollary evar_is_fresh_in_exists x ϕ :
evar_is_fresh_in x (patt_exists ϕ) ↔ evar_is_fresh_in x ϕ.
(*Hint Resolve evar_is_fresh_in_exists : core.*)
Corollary evar_is_fresh_in_mu x ϕ :
evar_is_fresh_in x (patt_mu ϕ) ↔ evar_is_fresh_in x ϕ.
(*Hint Resolve evar_is_fresh_in_mu : core.*)
Corollary svar_is_fresh_in_exists x ϕ :
svar_is_fresh_in x (patt_exists ϕ) ↔ svar_is_fresh_in x ϕ.
Corollary svar_is_fresh_in_mu x ϕ :
svar_is_fresh_in x (patt_mu ϕ) ↔ svar_is_fresh_in x ϕ.
Lemma X_eq_fresh_impl_X_notin_free_svars X ϕ:
X = fresh_svar ϕ →
X ∉ free_svars ϕ.
Lemma X_eq_evar_fresh_impl_X_notin_S X (S:EVarSet):
X = evar_fresh (elements S) →
X ∉ S.
Lemma X_eq_svar_fresh_impl_X_notin_S X (S:SVarSet):
X = svar_fresh (elements S) →
X ∉ S.
Hint Resolve X_eq_fresh_impl_X_notin_free_svars : core.
Definition simpl_free_evars :=
(
(@left_id_L EVarSet ∅ (@union _ _)),
(@right_id_L EVarSet ∅ (@union _ _))
).
Definition simpl_free_svars :=
(
(@left_id_L SVarSet ∅ (@union _ _)),
(@right_id_L SVarSet ∅ (@union _ _))
).
Lemma x_eq_fresh_impl_x_notin_free_evars x ϕ:
x = fresh_evar ϕ →
x ∉ free_evars ϕ.
Hint Resolve x_eq_fresh_impl_x_notin_free_evars : core.
End freshness.
Ltac remember_fresh_svars :=
unfold fresh_svar,svar_fresh_s in *;
repeat(
match goal with
| |- context G [svar_fresh ?Y] ⇒
match goal with
| H: ?X = svar_fresh Y |- _ ⇒ fail 2
| _ ⇒ remember (svar_fresh Y)
end
| H1: context G [svar_fresh ?Y] |- _ ⇒
match goal with
| H2: ?X = svar_fresh Y |- _ ⇒ fail 2
| _ ⇒ remember (svar_fresh Y)
end
end
).
Ltac remember_fresh_evars :=
unfold fresh_evar,evar_fresh_s in *;
repeat(
match goal with
| |- context G [evar_fresh ?Y] ⇒
match goal with
| H: ?X = evar_fresh Y |- _ ⇒ fail 2
| _ ⇒ remember (evar_fresh Y)
end
| H1: context G [evar_fresh ?Y] |- _ ⇒
match goal with
| H2: ?X = evar_fresh Y |- _ ⇒ fail 2
| _ ⇒ remember (evar_fresh Y)
end
end
).
(* assumes a goal `x₁ ≠ x₂` and a hypothesis of the shape `x₁ = fresh_evar ...`
or `x₂ = fresh_evar ...`
*)
Ltac solve_fresh_neq' :=
repeat (
match goal with
| Heq: (eq ?x ?t) |- not (eq ?x ?y) ⇒
pose proof (X_eq_evar_fresh_impl_X_notin_S _ _ Heq); clear dependent Heq
| Heq: (eq ?x ?t) |- not (eq ?y ?x) ⇒
pose proof (X_eq_evar_fresh_impl_X_notin_S _ _ Heq); clear dependent Heq
end
);
(idtac + apply nesym);
match goal with
| H: not (elem_of ?x ?S) |- not (eq ?x ?y) ⇒
simpl in H;
(do ? rewrite simpl_free_evars/= in H);
auto;
rewrite -?union_assoc_L in H;
repeat (
match goal with
| H: (not (elem_of ?x (singleton ?y))) |- _ ⇒
apply not_elem_of_singleton_1 in H;
first [ exact H | clear dependent H]
| H: (not (elem_of ?x (union ?l ?r))) |- _ ⇒ (apply not_elem_of_union in H; destruct H)
end
);
fail
end.
Ltac solve_fresh_neq := subst; remember_fresh_evars; solve_fresh_neq'.
Ltac solve_fresh_svar_neq :=
subst; remember_fresh_svars;
repeat (
match goal with
| Heq: (eq ?x ?t) |- not (eq ?x ?y) ⇒
pose proof (X_eq_svar_fresh_impl_X_notin_S _ _ Heq); clear dependent Heq
| Heq: (eq ?x ?t) |- not (eq ?y ?x) ⇒
pose proof (X_eq_svar_fresh_impl_X_notin_S _ _ Heq); clear dependent Heq
end
);
(idtac + apply nesym);
match goal with
| H: not (elem_of ?x ?S) |- not (eq ?x ?y) ⇒
simpl in H;
(do ? rewrite simpl_free_svars/= in H);
auto;
rewrite -?union_assoc_L in H;
repeat (
match goal with
| H: (not (elem_of ?x (singleton ?y))) |- _ ⇒
apply not_elem_of_singleton_1 in H;
first [ exact H | clear dependent H]
| H: (not (elem_of ?x (union ?l ?r))) |- _ ⇒ (apply not_elem_of_union in H; destruct H)
end
);
fail
end.
Definition evar_fresh_dep {Σ : Signature} (S : EVarSet) : {x : evar & x ∉ S} :=
@existT evar (fun x ⇒ x ∉ S) (evar_fresh_s S) (set_evar_fresh_is_fresh' S).
Definition svar_fresh_dep {Σ : Signature} (S : SVarSet) : {X : svar & X ∉ S} :=
@existT svar (fun x ⇒ x ∉ S) (svar_fresh_s S) (set_svar_fresh_is_fresh' S).
Fixpoint evar_fresh_seq {Σ : Signature} (avoid : EVarSet) (n : nat) : list evar :=
match n with
| 0 ⇒ []
| S n' ⇒
let x := (evar_fresh_s avoid) in
x :: evar_fresh_seq ({[x]} ∪ avoid) (n')
end.
Fixpoint svar_fresh_seq {Σ : Signature} (avoid : SVarSet) (n : nat) : list svar :=
match n with
| 0 ⇒ []
| S n' ⇒
let X := (svar_fresh_s avoid) in
X :: svar_fresh_seq ({[X]} ∪ avoid) (n')
end.
Lemma evar_fresh_seq_disj {Σ : Signature} S n:
list_to_set (evar_fresh_seq S n) ## S.
Lemma svar_fresh_seq_disj {Σ : Signature} S n:
list_to_set (svar_fresh_seq S n) ## S.
Section freshness.
Context {Σ : Signature}.
(* fresh variables *)
Definition evar_fresh (l : list evar) : evar := fresh l.
Definition svar_fresh (l : list svar) : svar := fresh l.
Definition evar_fresh_s (s : EVarSet) : evar := evar_fresh (elements s).
Definition svar_fresh_s (s : SVarSet) : svar := svar_fresh (elements s).
Definition fresh_evar ϕ := evar_fresh_s (free_evars ϕ).
Definition fresh_svar ϕ := svar_fresh_s (free_svars ϕ).
(* Lemmas about fresh variables *)
Lemma set_evar_fresh_is_fresh'' (S : list evar) : (evar_fresh S) ∉ S.
Lemma set_evar_fresh_is_fresh' (S : EVarSet) : evar_fresh (elements S) ∉ S.
Lemma set_evar_fresh_is_fresh ϕ : evar_is_fresh_in (fresh_evar ϕ) ϕ.
Hint Resolve set_evar_fresh_is_fresh : core.
Lemma set_svar_fresh_is_fresh'' (S : list svar) : (svar_fresh S) ∉ S.
Lemma set_svar_fresh_is_fresh' (S : SVarSet) : svar_fresh (elements S) ∉ S.
Lemma set_svar_fresh_is_fresh ϕ : svar_is_fresh_in (fresh_svar ϕ) ϕ.
Hint Resolve set_svar_fresh_is_fresh : core.
Lemma evar_is_fresh_in_richer' x ϕ B:
free_evars ϕ ⊆ B →
x ∉ B →
evar_is_fresh_in x ϕ.
Lemma evar_is_fresh_in_richer x ϕ₁ ϕ₂:
free_evars ϕ₁ ⊆ free_evars ϕ₂ →
evar_is_fresh_in x ϕ₂ →
evar_is_fresh_in x ϕ₁.
Lemma svar_is_fresh_in_richer' X ϕ B:
free_svars ϕ ⊆ B →
X ∉ B →
svar_is_fresh_in X ϕ.
Lemma svar_is_fresh_in_richer X ϕ₁ ϕ₂:
free_svars ϕ₁ ⊆ free_svars ϕ₂ →
svar_is_fresh_in X ϕ₂ →
svar_is_fresh_in X ϕ₁.
(*
Lemma fresh_neq_fresh_l ϕ₁ ϕ₂ :
(*~ evar_is_fresh_in (fresh_evar ϕ₁) ϕ₂ ->*)
free_evars ϕ₁ ⊈
fresh_evar ϕ₁ ≠ fresh_evar ϕ₂.
Proof.
intros H.
unfold fresh_evar at 2.
*)
Hint Resolve evar_is_fresh_in_richer : core.
Lemma not_free_implies_positive_negative_occurrence :
∀ (phi : Pattern) (X : svar),
X ∉ (free_svars phi) →
svar_has_positive_occurrence X phi = false ∧ svar_has_negative_occurrence X phi = false.
Corollary evar_is_fresh_in_app_l x ϕ₁ ϕ₂ :
evar_is_fresh_in x (patt_app ϕ₁ ϕ₂) → evar_is_fresh_in x ϕ₁.
Corollary svar_is_fresh_in_app_l X ϕ₁ ϕ₂ :
svar_is_fresh_in X (patt_app ϕ₁ ϕ₂) → svar_is_fresh_in X ϕ₁.
(*Hint Resolve evar_is_fresh_in_app_l : core.*)
Corollary evar_is_fresh_in_app_r x ϕ₁ ϕ₂ :
evar_is_fresh_in x (patt_app ϕ₁ ϕ₂) → evar_is_fresh_in x ϕ₂.
Corollary svar_is_fresh_in_app_r X ϕ₁ ϕ₂ :
svar_is_fresh_in X (patt_app ϕ₁ ϕ₂) → svar_is_fresh_in X ϕ₂.
Lemma evar_is_fresh_in_app x ϕ₁ ϕ₂ :
evar_is_fresh_in x (patt_app ϕ₁ ϕ₂)
↔ (evar_is_fresh_in x ϕ₁ ∧ evar_is_fresh_in x ϕ₂).
Lemma svar_is_fresh_in_app X ϕ₁ ϕ₂ :
svar_is_fresh_in X (patt_app ϕ₁ ϕ₂)
↔ (svar_is_fresh_in X ϕ₁ ∧ svar_is_fresh_in X ϕ₂).
(*Hint Resolve evar_is_fresh_in_app_r : core.*)
Corollary evar_is_fresh_in_imp_l x ϕ₁ ϕ₂ :
evar_is_fresh_in x (patt_imp ϕ₁ ϕ₂) → evar_is_fresh_in x ϕ₁.
Corollary svar_is_fresh_in_imp_l X ϕ₁ ϕ₂ :
svar_is_fresh_in X (patt_imp ϕ₁ ϕ₂) → svar_is_fresh_in X ϕ₁.
(*Hint Resolve evar_is_fresh_in_imp_l : core.*)
Corollary evar_is_fresh_in_imp_r x ϕ₁ ϕ₂ :
evar_is_fresh_in x (patt_imp ϕ₁ ϕ₂) → evar_is_fresh_in x ϕ₂.
Corollary svar_is_fresh_in_imp_r X ϕ₁ ϕ₂ :
svar_is_fresh_in X (patt_imp ϕ₁ ϕ₂) → svar_is_fresh_in X ϕ₂.
Lemma evar_is_fresh_in_imp x ϕ₁ ϕ₂ :
evar_is_fresh_in x (patt_imp ϕ₁ ϕ₂)
↔ (evar_is_fresh_in x ϕ₁ ∧ evar_is_fresh_in x ϕ₂).
Lemma svar_is_fresh_in_imp X ϕ₁ ϕ₂ :
svar_is_fresh_in X (patt_imp ϕ₁ ϕ₂)
↔ (svar_is_fresh_in X ϕ₁ ∧ svar_is_fresh_in X ϕ₂).
(*Hint Resolve evar_is_fresh_in_imp_r : core.*)
Corollary evar_is_fresh_in_exists x ϕ :
evar_is_fresh_in x (patt_exists ϕ) ↔ evar_is_fresh_in x ϕ.
(*Hint Resolve evar_is_fresh_in_exists : core.*)
Corollary evar_is_fresh_in_mu x ϕ :
evar_is_fresh_in x (patt_mu ϕ) ↔ evar_is_fresh_in x ϕ.
(*Hint Resolve evar_is_fresh_in_mu : core.*)
Corollary svar_is_fresh_in_exists x ϕ :
svar_is_fresh_in x (patt_exists ϕ) ↔ svar_is_fresh_in x ϕ.
Corollary svar_is_fresh_in_mu x ϕ :
svar_is_fresh_in x (patt_mu ϕ) ↔ svar_is_fresh_in x ϕ.
Lemma X_eq_fresh_impl_X_notin_free_svars X ϕ:
X = fresh_svar ϕ →
X ∉ free_svars ϕ.
Lemma X_eq_evar_fresh_impl_X_notin_S X (S:EVarSet):
X = evar_fresh (elements S) →
X ∉ S.
Lemma X_eq_svar_fresh_impl_X_notin_S X (S:SVarSet):
X = svar_fresh (elements S) →
X ∉ S.
Hint Resolve X_eq_fresh_impl_X_notin_free_svars : core.
Definition simpl_free_evars :=
(
(@left_id_L EVarSet ∅ (@union _ _)),
(@right_id_L EVarSet ∅ (@union _ _))
).
Definition simpl_free_svars :=
(
(@left_id_L SVarSet ∅ (@union _ _)),
(@right_id_L SVarSet ∅ (@union _ _))
).
Lemma x_eq_fresh_impl_x_notin_free_evars x ϕ:
x = fresh_evar ϕ →
x ∉ free_evars ϕ.
Hint Resolve x_eq_fresh_impl_x_notin_free_evars : core.
End freshness.
Ltac remember_fresh_svars :=
unfold fresh_svar,svar_fresh_s in *;
repeat(
match goal with
| |- context G [svar_fresh ?Y] ⇒
match goal with
| H: ?X = svar_fresh Y |- _ ⇒ fail 2
| _ ⇒ remember (svar_fresh Y)
end
| H1: context G [svar_fresh ?Y] |- _ ⇒
match goal with
| H2: ?X = svar_fresh Y |- _ ⇒ fail 2
| _ ⇒ remember (svar_fresh Y)
end
end
).
Ltac remember_fresh_evars :=
unfold fresh_evar,evar_fresh_s in *;
repeat(
match goal with
| |- context G [evar_fresh ?Y] ⇒
match goal with
| H: ?X = evar_fresh Y |- _ ⇒ fail 2
| _ ⇒ remember (evar_fresh Y)
end
| H1: context G [evar_fresh ?Y] |- _ ⇒
match goal with
| H2: ?X = evar_fresh Y |- _ ⇒ fail 2
| _ ⇒ remember (evar_fresh Y)
end
end
).
(* assumes a goal `x₁ ≠ x₂` and a hypothesis of the shape `x₁ = fresh_evar ...`
or `x₂ = fresh_evar ...`
*)
Ltac solve_fresh_neq' :=
repeat (
match goal with
| Heq: (eq ?x ?t) |- not (eq ?x ?y) ⇒
pose proof (X_eq_evar_fresh_impl_X_notin_S _ _ Heq); clear dependent Heq
| Heq: (eq ?x ?t) |- not (eq ?y ?x) ⇒
pose proof (X_eq_evar_fresh_impl_X_notin_S _ _ Heq); clear dependent Heq
end
);
(idtac + apply nesym);
match goal with
| H: not (elem_of ?x ?S) |- not (eq ?x ?y) ⇒
simpl in H;
(do ? rewrite simpl_free_evars/= in H);
auto;
rewrite -?union_assoc_L in H;
repeat (
match goal with
| H: (not (elem_of ?x (singleton ?y))) |- _ ⇒
apply not_elem_of_singleton_1 in H;
first [ exact H | clear dependent H]
| H: (not (elem_of ?x (union ?l ?r))) |- _ ⇒ (apply not_elem_of_union in H; destruct H)
end
);
fail
end.
Ltac solve_fresh_neq := subst; remember_fresh_evars; solve_fresh_neq'.
Ltac solve_fresh_svar_neq :=
subst; remember_fresh_svars;
repeat (
match goal with
| Heq: (eq ?x ?t) |- not (eq ?x ?y) ⇒
pose proof (X_eq_svar_fresh_impl_X_notin_S _ _ Heq); clear dependent Heq
| Heq: (eq ?x ?t) |- not (eq ?y ?x) ⇒
pose proof (X_eq_svar_fresh_impl_X_notin_S _ _ Heq); clear dependent Heq
end
);
(idtac + apply nesym);
match goal with
| H: not (elem_of ?x ?S) |- not (eq ?x ?y) ⇒
simpl in H;
(do ? rewrite simpl_free_svars/= in H);
auto;
rewrite -?union_assoc_L in H;
repeat (
match goal with
| H: (not (elem_of ?x (singleton ?y))) |- _ ⇒
apply not_elem_of_singleton_1 in H;
first [ exact H | clear dependent H]
| H: (not (elem_of ?x (union ?l ?r))) |- _ ⇒ (apply not_elem_of_union in H; destruct H)
end
);
fail
end.
Definition evar_fresh_dep {Σ : Signature} (S : EVarSet) : {x : evar & x ∉ S} :=
@existT evar (fun x ⇒ x ∉ S) (evar_fresh_s S) (set_evar_fresh_is_fresh' S).
Definition svar_fresh_dep {Σ : Signature} (S : SVarSet) : {X : svar & X ∉ S} :=
@existT svar (fun x ⇒ x ∉ S) (svar_fresh_s S) (set_svar_fresh_is_fresh' S).
Fixpoint evar_fresh_seq {Σ : Signature} (avoid : EVarSet) (n : nat) : list evar :=
match n with
| 0 ⇒ []
| S n' ⇒
let x := (evar_fresh_s avoid) in
x :: evar_fresh_seq ({[x]} ∪ avoid) (n')
end.
Fixpoint svar_fresh_seq {Σ : Signature} (avoid : SVarSet) (n : nat) : list svar :=
match n with
| 0 ⇒ []
| S n' ⇒
let X := (svar_fresh_s avoid) in
X :: svar_fresh_seq ({[X]} ∪ avoid) (n')
end.
Lemma evar_fresh_seq_disj {Σ : Signature} S n:
list_to_set (evar_fresh_seq S n) ## S.
Lemma svar_fresh_seq_disj {Σ : Signature} S n:
list_to_set (svar_fresh_seq S n) ## S.
Note: we cannot reuse NoDup, until the proof system is
formalised as `... -> Set`.
Fixpoint no_dups {A : Set} {eqdec : EqDecision A} (l : list A) :=
match l with
| [] ⇒ True
| x::xs ⇒ x ∉ xs ∧ no_dups xs
end.
Lemma no_dups_NoDup :
∀ {A : Set} {eqdec : EqDecision A} (l : list A), no_dups l ↔ NoDup l.
Class fresh_evars {Σ : Signature} (l : list evar) (s : EVarSet) :=
{
evar_duplicates : no_dups l;
all_evars_fresh : ∀ x, x ∈ l → x ∉ s;
}.
Lemma fresh_evars_bigger {Σ : Signature} {el s} s' :
fresh_evars el s → s' ⊆ s → fresh_evars el s'.
Lemma less_fresh_evars {Σ : Signature} {x el s} :
fresh_evars (x::el) s → fresh_evars el s.
Class fresh_svars {Σ : Signature} (l : list svar) (s : SVarSet) :=
{
svar_duplicates : no_dups l;
all_svars_fresh : ∀ X, X ∈ l → X ∉ s;
}.
Lemma fresh_svars_bigger {Σ : Signature} {sl s} s' :
fresh_svars sl s → s' ⊆ s → fresh_svars sl s'.
Lemma less_fresh_svars {Σ : Signature} {X sl s} :
fresh_evars (X::sl) s → fresh_evars sl s.
Ltac solve_fresh :=
(eapply not_elem_of_larger_impl_not_elem_of;
[|apply x_eq_fresh_impl_x_notin_free_evars; reflexivity];
simpl; clear; set_solver) +
by (unfold evar_is_fresh_in;
eapply evar_is_fresh_in_richer'; [|apply set_evar_fresh_is_fresh'];
clear; set_solver).
Ltac solve_sfresh :=
(eapply not_elem_of_larger_impl_not_elem_of;
[|apply X_eq_fresh_impl_X_notin_free_svars; reflexivity];
simpl; clear; set_solver) +
by (unfold svar_is_fresh_in;
eapply svar_is_fresh_in_richer'; [|apply set_svar_fresh_is_fresh'];
clear; set_solver).
match l with
| [] ⇒ True
| x::xs ⇒ x ∉ xs ∧ no_dups xs
end.
Lemma no_dups_NoDup :
∀ {A : Set} {eqdec : EqDecision A} (l : list A), no_dups l ↔ NoDup l.
Class fresh_evars {Σ : Signature} (l : list evar) (s : EVarSet) :=
{
evar_duplicates : no_dups l;
all_evars_fresh : ∀ x, x ∈ l → x ∉ s;
}.
Lemma fresh_evars_bigger {Σ : Signature} {el s} s' :
fresh_evars el s → s' ⊆ s → fresh_evars el s'.
Lemma less_fresh_evars {Σ : Signature} {x el s} :
fresh_evars (x::el) s → fresh_evars el s.
Class fresh_svars {Σ : Signature} (l : list svar) (s : SVarSet) :=
{
svar_duplicates : no_dups l;
all_svars_fresh : ∀ X, X ∈ l → X ∉ s;
}.
Lemma fresh_svars_bigger {Σ : Signature} {sl s} s' :
fresh_svars sl s → s' ⊆ s → fresh_svars sl s'.
Lemma less_fresh_svars {Σ : Signature} {X sl s} :
fresh_evars (X::sl) s → fresh_evars sl s.
Ltac solve_fresh :=
(eapply not_elem_of_larger_impl_not_elem_of;
[|apply x_eq_fresh_impl_x_notin_free_evars; reflexivity];
simpl; clear; set_solver) +
by (unfold evar_is_fresh_in;
eapply evar_is_fresh_in_richer'; [|apply set_evar_fresh_is_fresh'];
clear; set_solver).
Ltac solve_sfresh :=
(eapply not_elem_of_larger_impl_not_elem_of;
[|apply X_eq_fresh_impl_X_notin_free_svars; reflexivity];
simpl; clear; set_solver) +
by (unfold svar_is_fresh_in;
eapply svar_is_fresh_in_richer'; [|apply set_svar_fresh_is_fresh'];
clear; set_solver).
This page has been generated by coqdoc