Skip to content
GitLab
Commit 61fd1f69 authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

Toolbox.v : split Meta.v in half, all basic properties now in this new file

parent 35cb1ae6
Hide whitespace changes
Inline Side-by-side
AltSubst.v
View file @ 61fd1f69
......@@ -4,7 +4,7 @@
(** The NatDed development, Pierre Letouzey, 2019.
This file is released under the CC0 License, see the LICENSE file *)
Require Import Defs NameProofs Nam Subst Equiv Meta.
Require Import Defs NameProofs Nam Subst Equiv Toolbox.
Import ListNotations.
Import Nam.Form.
Local Open Scope bool_scope.
......
Equiv.v
View file @ 61fd1f69
......@@ -4,7 +4,7 @@
(** The NatDed development, Pierre Letouzey, 2019.
This file is released under the CC0 License, see the LICENSE file *)
Require Import Defs NameProofs Nam Subst Meta.
Require Import Defs NameProofs Nam Subst Toolbox.
Import ListNotations.
Import Nam.Form.
Local Open Scope bool_scope.
......@@ -315,7 +315,7 @@ Proof.
- case eqbspec.
+ intros ->.
unfold Mix.fsubst.
rewrite Meta.form_vmap_id; auto.
rewrite Toolbox.form_vmap_id; auto.
intros x. rewrite nam2mix_fvars. simpl.
unfold Mix.varsubst.
intros IN.
......@@ -345,7 +345,7 @@ Lemma nam2mix_subst_nop x stk f :
Proof.
intros NI.
rewrite nam2mix_subst_fsubst; auto.
- cbn. unfold Mix.fsubst. rewrite Meta.form_vmap_id; auto.
- cbn. unfold Mix.fsubst. rewrite Toolbox.form_vmap_id; auto.
intros v Hv. unfold Mix.varsubst. case eqbspec; auto. now intros ->.
- intros v Hv. cbn. nameiff. now intros ->.
Qed.
......@@ -374,7 +374,7 @@ Proof.
change (x::stk++[x]) with ((x::stk)++[x]).
rewrite nam2mix_shadowstack by (simpl; auto).
symmetry.
apply Meta.form_level_bsubst_id.
apply Toolbox.form_level_bsubst_id.
now rewrite nam2mix_level.
+ intros NE.
rewrite lift_nop.
......@@ -406,7 +406,7 @@ Proof.
intros Hz.
rewrite 2 nam2mix_subst_bsubst0. cbn.
split.
- intros H. apply Meta.bsubst_fresh_inj in H; auto.
- intros H. apply Toolbox.bsubst_fresh_inj in H; auto.
rewrite !nam2mix_fvars. cbn. namedec.
- now intros ->.
Qed.
......@@ -426,7 +426,7 @@ Proof.
rewrite nam2mix_subst_bsubst0. cbn.
rewrite <- (nam2mix_bsubst0_var x f').
split.
- apply Meta.bsubst_fresh_inj.
- apply Toolbox.bsubst_fresh_inj.
rewrite !nam2mix_fvars. cbn. namedec.
- now intros ->.
Qed.
......@@ -607,7 +607,7 @@ Proof.
apply nam2mix_canonical.
rewrite !nam2mix0_subst_fsubst.
rewrite nam2mix_term_subst by auto.
apply Meta.form_fsubst_fsubst; auto.
apply Toolbox.form_fsubst_fsubst; auto.
rewrite nam2mix_tvars. cbn. namedec.
Qed.
......
Makefile.conf
View file @ 61fd1f69
......@@ -8,7 +8,7 @@
# #
###############################################################################
COQMF_VFILES = AsciiOrder.v StringOrder.v StringUtils.v Utils.v Defs.v Nam.v Mix.v NameProofs.v Subst.v Restrict.v Meta.v ProofExamples.v Wellformed.v Equiv.v Equiv2.v AltSubst.v Countable.v Theories.v Nary.v PreModels.v Models.v Peano.v contribs/zfc/zfc.v ZF.v Skolem.v
COQMF_VFILES = AsciiOrder.v StringOrder.v StringUtils.v Utils.v Defs.v Nam.v Mix.v NameProofs.v Subst.v Restrict.v Toolbox.v Meta.v ProofExamples.v Wellformed.v Equiv.v Equiv2.v AltSubst.v Countable.v Theories.v Nary.v PreModels.v Models.v Peano.v contribs/zfc/zfc.v ZF.v Skolem.v
COQMF_MLIFILES =
COQMF_MLFILES =
COQMF_ML4FILES =
......
Meta.v
View file @ 61fd1f69
......@@ -4,7 +4,7 @@
(** The NatDed development, Pierre Letouzey, 2019.
This file is released under the CC0 License, see the LICENSE file *)
Require Import Defs NameProofs Mix.
Require Import Defs NameProofs Mix Toolbox.
Import ListNotations.
Local Open Scope bool_scope.
Local Open Scope lazy_bool_scope.
......@@ -13,641 +13,6 @@ Local Open Scope eqb_scope.
Implicit Type t u : term.
Implicit Type f : formula.
(** Properties of [lift] *)
Lemma level_lift k t : level (lift k t) <= S (level t).
Proof.
induction t as [ | | f l IH] using term_ind'; cbn; auto with arith.
- case Nat.leb_spec; auto.
- rewrite map_map.
apply list_max_map_le. intros a Ha. transitivity (S (level a)); auto.
rewrite <- Nat.succ_le_mono. now apply list_max_map_in.
Qed.
Lemma lift_nop_le k t : level t <= k -> lift k t = t.
Proof.
induction t as [ | | f l IH] using term_ind'; cbn; auto.
- case Nat.leb_spec; auto. omega.
- rewrite list_max_map_le. intros H. f_equal. apply map_id_iff; auto.
Qed.
Lemma lift_nop k t : BClosed t -> lift k t = t.
Proof.
unfold BClosed. intros H. apply lift_nop_le. rewrite H; omega.
Qed.
Lemma check_lift sign k t :
check sign (lift k t) = check sign t.
Proof.
induction t as [ | | f l IH] using term_ind'; cbn; auto.
- case Nat.leb_spec; auto.
- destruct funsymbs; auto.
rewrite map_length. case eqb; auto.
apply eq_true_iff_eq. rewrite forallb_map, !forallb_forall.
split; intros H x Hx. rewrite <- IH; auto. rewrite IH; auto.
Qed.
Lemma fvars_lift k t : fvars (lift k t) = fvars t.
Proof.
induction t as [ | | f l IH] using term_ind'; cbn; auto with *.
- case Nat.leb_spec; auto.
- induction l; simpl; auto.
rewrite IH, IHl; simpl; auto.
intros x Hx. apply IH. simpl; auto.
Qed.
Lemma level_lift_form k f : level (lift k f) <= S (level f).
Proof.
revert k. induction f; intro; cbn; auto with arith.
+ rewrite map_map.
rewrite list_max_map_le.
intros.
transitivity (S (level a)).
- apply level_lift.
- apply-> Nat.succ_le_mono.
apply list_max_map_in.
assumption.
+ specialize (IHf1 k).
specialize (IHf2 k).
omega with *.
+ specialize (IHf (S k)).
omega.
Qed.
Lemma check_lift_form sign f k :
check sign (lift k f) = check sign f.
Proof.
revert k. induction f; cbn; auto.
+ destruct (predsymbs sign p); auto.
intro. rewrite map_length. case eqb; auto.
apply eq_true_iff_eq. rewrite forallb_map, !forallb_forall.
split; intros.
- destruct H with (x := x); auto. rewrite check_lift. reflexivity.
- destruct H with (x := x); auto. rewrite check_lift. reflexivity.
+ intro. rewrite IHf1. rewrite IHf2. reflexivity.
Qed.
Lemma fvars_lift_form f k :
fvars (lift k f) = fvars f.
Proof.
revert k. induction f; intro; cbn; auto with *.
- induction l; simpl; auto.
rewrite fvars_lift, IHl; simpl; auto.
- rewrite IHf1. rewrite IHf2. auto.
Qed.
(** [bsubst] and [check] *)
Lemma check_bsubst_term sign n (u t:term) :
check sign u = true -> check sign t = true ->
check sign (bsubst n u t) = true.
Proof.
induction t as [ | | f l IH] using term_ind'; cbn; auto.
- case eqbspec; auto.
- destruct funsymbs; auto.
rewrite !lazy_andb_iff, map_length.
intros Hu (Hl,Hl'); split; auto.
rewrite forallb_map, forallb_forall in *. auto.
Qed.
Lemma check_bsubst sign n u (f:formula) :
check sign u = true -> check sign f = true ->
check sign (bsubst n u f) = true.
Proof.
revert n u.
induction f; cbn; intros n u Hu Hf; auto.
- destruct predsymbs; auto.
rewrite !lazy_andb_iff in *. rewrite map_length.
destruct Hf as (Hl,Hl'); split; auto.
rewrite forallb_map, forallb_forall in *.
auto using check_bsubst_term.
- rewrite !lazy_andb_iff in *; intuition.
- apply IHf; auto. now rewrite check_lift.
Qed.
(** [bsubst] and [level] *)
Lemma level_bsubst_term_max n (u t:term) :
level (bsubst n u t) <= Nat.max (level u) (level t).
Proof.
revert t. fix IH 1; destruct t; cbn -[Nat.max].
- auto with arith.
- case eqbspec; cbn -[Nat.max]; omega with *.
- revert l. fix IHl 1; destruct l; cbn -[Nat.max].
+ auto with arith.
+ specialize (IH t). specialize (IHl l). omega with *.
Qed.
Lemma level_bsubst_max n u (f:formula) :
level (bsubst n u f) <= Nat.max (level u) (level f).
Proof.
revert n u.
induction f; intros; cbn -[Nat.max]; auto with arith.
- apply (level_bsubst_term_max n u (Fun "" l)).
- specialize (IHf1 n u). specialize (IHf2 n u). omega with *.
- assert (H := level_lift 0 u).
specialize (IHf (S n) (lift 0 u)). omega with *.
Qed.
Lemma level_bsubst_term n (u t:term) :
level t <= S n -> level u <= n ->
level (bsubst n u t) <= n.
Proof.
induction t as [ | | f l IH] using term_ind'; cbn; auto with arith.
- case eqbspec; cbn; auto. intros; omega.
- intros Hl Hu. rewrite map_map. apply list_max_map_le.
rewrite list_max_map_le in Hl; auto.
Qed.
Lemma level_bsubst n u (f:formula) :
level f <= S n -> level u <= n ->
level (bsubst n u f) <= n.
Proof.
revert n u.
induction f; cbn; intros n u Hf Hu; auto with arith.
- apply (level_bsubst_term n u (Fun "" l)); auto.
- rewrite max_le in *; intuition.
- change n with (Nat.pred (S n)) at 2. apply Nat.pred_le_mono.
apply IHf. omega. transitivity (S (level u)). apply level_lift.
omega.
Qed.
Lemma level_bsubst_term' n (u t : term) :
level u <= S n -> level (bsubst n u t) <= level t.
Proof.
intro Hu. revert t. fix IH 1. destruct t; cbn; auto.
- case eqbspec; intros; subst; auto.
- revert l. fix IH' 1. destruct l; cbn; auto.
apply Nat.max_le_compat; auto.
Qed.
Lemma level_bsubst' n u (f:formula) :
level u <= S n -> level (bsubst n u f) <= level f.
Proof.
revert n u. induction f; cbn; intros n u Hu; auto with arith.
- now apply (level_bsubst_term' n u (Fun "" l)).
- apply Nat.max_le_compat; auto.
- apply Nat.pred_le_mono; auto with arith.
apply IHf. transitivity (S (level u)). apply level_lift. omega.
Qed.
(** [bsubst] and [fvars] : over-approximations *)
Lemma bsubst_term_fvars n (u t:term) :
Names.Subset (fvars (bsubst n u t)) (Names.union (fvars u) (fvars t)).
Proof.
induction t as [ | | f l IH] using term_ind'; cbn; auto with *.
apply subset_unionmap_map; auto.
Qed.
Lemma bsubst_fvars n u (f:formula) :
Names.Subset (fvars (bsubst n u f)) (Names.union (fvars u) (fvars f)).
Proof.
revert n u.
induction f; cbn; intros; auto with *.
- apply (bsubst_term_fvars n u (Fun "" l)).
- rewrite IHf1, IHf2. namedec.
- rewrite IHf. now rewrite fvars_lift.
Qed.
Lemma bsubst_ctx_fvars n u (c:context) :
Names.Subset (fvars (bsubst n u c)) (Names.union (fvars u) (fvars c)).
Proof.
induction c as [|f c IH]; cbn; auto with *.
rewrite bsubst_fvars, IH. namedec.
Qed.
(** [bsubst] and [fvars] : under-approximations *)
Lemma bsubst_term_fvars' n (u t : term) :
Names.Subset (fvars t) (fvars (bsubst n u t)).
Proof.
revert t. fix IH 1. destruct t; cbn; auto with set.
clear f.
revert l. fix IH' 1. destruct l; cbn; auto with set.
intro x. NamesF.set_iff. intros [IN|IN].
- left; now apply IH.
- right. now apply IH'.
Qed.
Lemma bsubst_fvars' n u (f:formula) :
Names.Subset (fvars f) (fvars (bsubst n u f)).
Proof.
revert n u; induction f; cbn; intros n u; auto with set.
- apply (bsubst_term_fvars' n u (Fun "" l)).
- intro x. NamesF.set_iff. intros [IN|IN].
left; now apply IHf1.
right; now apply IHf2.
Qed.
(** [bsubst] above the level does nothing *)
Lemma term_level_bsubst_id n u (t:term) :
level t <= n -> bsubst n u t = t.
Proof.
induction t as [ | |f l IH] using term_ind'; cbn; try easy.
- case eqbspec; auto. intros ->. omega.
- intros LE.
rewrite list_max_map_le in LE. f_equal. apply map_id_iff. intuition.
Qed.
Lemma form_level_bsubst_id n u (f:formula) :
level f <= n -> bsubst n u f = f.
Proof.
revert n u.
induction f; cbn; intros n u LE; f_equal; auto.
- injection (term_level_bsubst_id n u (Fun "" l)); cbn; auto.
- apply IHf1. omega with *.
- apply IHf2. omega with *.
- apply IHf. omega with *.
Qed.
Lemma bclosed_bsubst_id n u (t:term) :
BClosed t -> bsubst n u t = t.
Proof.
unfold BClosed. intros. apply term_level_bsubst_id. auto with *.
Qed.
(** [bsubst] to a fresh variable is injective *)
Lemma term_bsubst_fresh_inj n z (t t':term):
~ Names.In z (Names.union (fvars t) (fvars t')) ->
bsubst n (FVar z) t = bsubst n (FVar z) t' ->
t = t'.
Proof.
revert t t'.
fix IH 1; destruct t, t'; cbn; intros NI; try discriminate.
- intro E. exact E.
- clear IH. case eqbspec; auto. intros -> [= ->]. namedec.
- clear IH. case eqbspec; auto. intros -> [= ->]. namedec.
- clear IH. do 2 case eqbspec; intros; subst; easy.
- clear IH. case eqbspec; easy.
- clear IH. case eqbspec; easy.
- intros [= <- E]; f_equal.
revert l l0 NI E.
fix IH' 1; destruct l, l0; cbn; trivial; try discriminate.
intros NI. intros [= E E']. f_equal. apply IH; auto. namedec.
apply IH'; auto. namedec.
Qed.
Lemma bsubst_fresh_inj n z (f f':formula):
~ Names.In z (Names.union (fvars f) (fvars f')) ->
Mix.bsubst n (Mix.FVar z) f = Mix.bsubst n (Mix.FVar z) f' ->
f = f'.
Proof.
revert f' n.
induction f; destruct f'; cbn; intros n NI; try easy.
- intros[= <- E]. f_equal.
injection (term_bsubst_fresh_inj n z (Mix.Fun "" l) (Mix.Fun "" l0));
cbn; auto. now f_equal.
- intros [= E]. f_equal; eauto.
- intros [= <- E1 E2]. f_equal. eapply IHf1; eauto. namedec.
eapply IHf2; eauto. namedec.
- intros [= <- E]. f_equal. eapply IHf; eauto.
Qed.
(** Properties of [fclosed] *)
Lemma term_fclosed_spec t : fclosed t = true <-> FClosed t.
Proof.
unfold FClosed.
induction t using term_ind'; cbn.
- rewrite <- Names.is_empty_spec. namedec.
- rewrite <- Names.is_empty_spec. reflexivity.
- rewrite forallb_forall. unfold Names.Empty.
setoid_rewrite unionmap_in. split.
+ intros F a (t & IN & IN').
specialize (F t IN'). rewrite H in F; auto. now apply (F a).
+ intros G x Hx. rewrite H; auto. intros a Ha. apply (G a).
now exists x.
Qed.
Lemma form_fclosed_spec f : fclosed f = true <-> FClosed f.
Proof.
unfold FClosed.
induction f; cbn; auto.
- rewrite <- Names.is_empty_spec. namedec.
- rewrite <- Names.is_empty_spec. namedec.
- apply (term_fclosed_spec (Fun "" l)).
- rewrite lazy_andb_iff, IHf1, IHf2.
intuition.
Qed.
Lemma fclosed_bsubst n t f :
fclosed t = true -> fclosed (bsubst n t f) = fclosed f.
Proof.
intros E. apply eq_true_iff_eq. rewrite !form_fclosed_spec.
rewrite term_fclosed_spec in E. unfold FClosed in *.
assert (Names.Equal (fvars (bsubst n t f)) (fvars f)).
{ intros a. split. rewrite bsubst_fvars. namedec.
apply bsubst_fvars'. }
now rewrite H.
Qed.
Lemma fclosed_lift n f : fclosed (lift n f) = fclosed f.
Proof.
apply eq_true_iff_eq. rewrite !form_fclosed_spec.
unfold FClosed. now rewrite fvars_lift_form.
Qed.
(** [vmap] basic results : extensionality, identity, composition *)
Lemma term_vmap_ext h h' (t:term) :
(forall v:variable, Names.In v (fvars t) -> h v = h' v) ->
vmap h t = vmap h' t.
Proof.
induction t as [ | |f l IH] using term_ind'; cbn; auto with set.
intros H. f_equal. apply map_ext_in; eauto with set.
Qed.
Lemma form_vmap_ext h h' (f:formula) :
(forall v:variable, Names.In v (fvars f) -> h v = h' v) ->
vmap h f = vmap h' f.
Proof.
induction f; cbn; intro; f_equal; auto with set.
now injection (term_vmap_ext h h' (Fun "" l)).
Qed.
Lemma ctx_vmap_ext h h' (c:context) :
(forall v:variable, Names.In v (fvars c) -> h v = h' v) ->
vmap h c = vmap h' c.
Proof.
induction c; cbn; intros; f_equal;
auto using form_vmap_ext with set.
Qed.
Lemma seq_vmap_ext h h' (s:sequent) :
(forall v:variable, Names.In v (fvars s) -> h v = h' v) ->
vmap h s = vmap h' s.
Proof.
destruct s; intros. cbn in *. f_equal.
apply ctx_vmap_ext; auto with set.
apply form_vmap_ext; auto with set.
Qed.
Lemma term_vmap_id h (t:term) :
(forall v:variable, Names.In v (fvars t) -> h v = FVar v) ->
vmap h t = t.
Proof.
induction t as [ | |f l IH] using term_ind'; cbn; auto with set.
intros H. f_equal. apply map_id_iff; eauto with set.
Qed.
Lemma form_vmap_id h (f:formula) :
(forall v:variable, Names.In v (fvars f) -> h v = FVar v) ->
vmap h f = f.
Proof.
induction f; cbn; intro; f_equal; auto with set.
now injection (term_vmap_id h (Fun "" l)).
Qed.
Lemma ctx_vmap_id h (c:context) :
(forall v:variable, Names.In v (fvars c) -> h v = FVar v) ->
vmap h c = c.
Proof.
induction c; cbn; intros; f_equal;
auto using form_vmap_id with set.
Qed.
Lemma term_vmap_vmap h h' (t:term) :
vmap h (vmap h' t) = vmap (fun v => vmap h (h' v)) t.
Proof.
induction t as [ | |f l IH] using term_ind'; cbn; trivial.
f_equal. rewrite map_map. apply map_ext_in; auto.
Qed.
Lemma form_vmap_vmap h h' (f:formula) :
vmap h (vmap h' f) = vmap (fun v => vmap h (h' v)) f.
Proof.
induction f; cbn; f_equal; auto.
now injection (term_vmap_vmap h h' (Fun "" l)).
Qed.
Lemma ctx_vmap_vmap h h' (c:context) :
vmap h (vmap h' c) = vmap (fun v => vmap h (h' v)) c.
Proof.
induction c; cbn; f_equal; auto using form_vmap_vmap with set.
Qed.
(** Estimating free variables of a substitution *)
Lemma term_fvars_vmap h (t:term) :
Names.Subset
(fvars (vmap h t))
(Names.flatmap (fun v => fvars (h v)) (fvars t)).
Proof.
induction t as [ | |f l IH] using term_ind'; cbn.
- unfold Names.singleton. cbn. namedec.
- namedec.
- intros v. rewrite unionmap_map_in. intros (a & Hv & Ha).
generalize (IH a Ha v Hv). apply flatmap_subset; auto.
intro. eauto with set.
Qed.
Lemma form_fvars_vmap h (f:formula) :
Names.Subset
(fvars (vmap h f))
(Names.flatmap (fun v => fvars (h v)) (fvars f)).
Proof.
induction f; simpl; try namedec.
- apply (term_fvars_vmap h (Fun "" l)).
- cbn. rewrite flatmap_union. namedec.
Qed.
Lemma ctx_fvars_vmap h (c:context) :
Names.Subset
(fvars (vmap h c))
(Names.flatmap (fun v => fvars (h v)) (fvars c)).
Proof.
induction c as [|f c IH]; cbn.
- namedec.
- generalize (form_fvars_vmap h f).
rewrite flatmap_union. namedec.
Qed.
Lemma seq_fvars_vmap h (s:sequent) :
Names.Subset
(fvars (vmap h s))
(Names.flatmap (fun v => fvars (h v)) (fvars s)).
Proof.
destruct s. cbn.
rewrite flatmap_union.
generalize (form_fvars_vmap h f) (ctx_fvars_vmap h c). namedec.
Qed.
(** [fsubst] commutes *)
Lemma term_fsubst_fsubst x y (u v t:term) :
x<>y -> ~Names.In x (fvars v) ->
fsubst y v (fsubst x u t) =
fsubst x (fsubst y v u) (fsubst y v t).
Proof.
induction t as [ | |f l IH] using term_ind'; cbn;
intros NE NI; auto.
- do 2 (unfold varsubst; case eqbspec; cbn); intros; subst.
+ easy.
+ unfold varsubst. now rewrite eqb_refl.
+ unfold fsubst. symmetry. apply term_vmap_id.
intros z Hz. unfold varsubst.
case eqbspec; auto. namedec.
+ unfold varsubst. now case eqbspec.
- f_equal. rewrite !map_map.
apply map_ext_iff. intros a Ha.
apply IH; auto.
Qed.
Lemma form_fsubst_fsubst x y (u v:term)(f:formula) :
x<>y -> ~Names.In x (fvars v) ->
fsubst y v (fsubst x u f) =
fsubst x (fsubst y v u) (fsubst y v f).
Proof.
induction f; cbn; intros NE NI; f_equal; auto.
injection (term_fsubst_fsubst x y u v (Fun "" l)); auto.
Qed.
(** Alternating [vmap] and [bsubst] *)
Definition BClosed_sub (h:variable->term) :=
forall v, BClosed (h v).
Lemma lift_vmap (h:variable->term) k t :
lift k (vmap h t) = vmap (fun v => lift k (h v)) (lift k t).
Proof.
induction t as [ | | f l IH] using term_ind'; cbn; auto.
- case Nat.leb_spec; auto.
- f_equal. rewrite !map_map. apply map_ext_iff; auto.
Qed.