Skip to content

GitLab

Commit fedfec2c authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

Meta.v scindé en deux (nouveau fichier Restrict.v)

parent 05190ea1
Hide whitespace changes
Inline Side-by-side
Makefile
View file @ fedfec2c
......@@ -4,7 +4,7 @@
## \VV/ # ##
## // # ##
###############################################################################
## GNUMakefile for Coq 8.8.2
## GNUMakefile for Coq 8.9.1
# For debugging purposes (must stay here, don't move below)
INITIAL_VARS := $(.VARIABLES)
......@@ -86,7 +86,6 @@ COQC ?= "$(COQBIN)coqc"
COQTOP ?= "$(COQBIN)coqtop"
COQCHK ?= "$(COQBIN)coqchk"
COQDEP ?= "$(COQBIN)coqdep"
GALLINA ?= "$(COQBIN)gallina"
COQDOC ?= "$(COQBIN)coqdoc"
COQMKFILE ?= "$(COQBIN)coq_makefile"
......@@ -148,7 +147,11 @@ TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line
# Flags #######################################################################
#
# We define a bunch of variables combining the parameters
# We define a bunch of variables combining the parameters.
# To add additional flags to coq, coqchk or coqdoc, set the
# {COQ,COQCHK,COQDOC}EXTRAFLAGS variable to whatever you want to add.
# To overwrite the default choice and set your own flags entirely, set the
# {COQ,COQCHK,COQDOC}FLAGS variable.
SHOW := $(if $(VERBOSE),@true "",@echo "")
HIDE := $(if $(VERBOSE),,@)
......@@ -168,15 +171,22 @@ DYNOBJ:=.cmxs
DYNLIB:=.cmxs
endif
COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS)
COQCHKFLAGS?=-silent -o $(COQLIBS)
COQDOCFLAGS?=-interpolate -utf8
# these variables are meant to be overriden if you want to add *extra* flags
COQEXTRAFLAGS?=
COQCHKEXTRAFLAGS?=
COQDOCEXTRAFLAGS?=
# these flags do NOT contain the libraries, to make them easier to overwrite
COQFLAGS?=-q $(OPT) $(OTHERFLAGS) $(COQEXTRAFLAGS)
COQCHKFLAGS?=-silent -o $(COQCHKEXTRAFLAGS)
COQDOCFLAGS?=-interpolate -utf8 $(COQDOCEXTRAFLAGS)
COQDOCLIBS?=$(COQLIBS_NOML)
# The version of Coq being run and the version of coq_makefile that
# generated this makefile
COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1)
COQMAKEFILE_VERSION:=8.8.2
COQMAKEFILE_VERSION:=8.9.1
COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)")
......@@ -245,7 +255,6 @@ VO = vo
VOFILES = $(VFILES:.v=.$(VO))
GLOBFILES = $(VFILES:.v=.glob)
GFILES = $(VFILES:.v=.g)
HTMLFILES = $(VFILES:.v=.html)
GHTMLFILES = $(VFILES:.v=.g.html)
BEAUTYFILES = $(addsuffix .beautified,$(VFILES))
......@@ -384,7 +393,7 @@ quick: $(VOFILES:.vo=.vio)
.PHONY: quick
vio2vo:
$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) \
$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \
-schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio)
.PHONY: vio2vo
......@@ -396,17 +405,17 @@ quick2vo:
done); \
echo "VIO2VO: $$VIOFILES"; \
if [ -n "$$VIOFILES" ]; then \
$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $$VIOFILES; \
$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -schedule-vio2vo $(J) $$VIOFILES; \
fi
.PHONY: quick2vo
checkproofs:
$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) \
$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \
-schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio)
.PHONY: checkproofs
validate: $(VOFILES)
$(TIMER) $(COQCHK) $(COQCHKFLAGS) $^
$(TIMER) $(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $^
.PHONY: validate
only: $(TGTS)
......@@ -431,8 +440,6 @@ all-mli.tex: $(MLIFILES:.mli=.cmi)
$(HIDE)$(CAMLDOC) -latex \
-o $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES)
gallina: $(GFILES)
all.ps: $(VFILES)
$(SHOW)'COQDOC -ps $(GAL)'
$(HIDE)$(COQDOC) \
......@@ -553,7 +560,6 @@ clean::
$(HIDE)find . -name .coq-native -type d -empty -delete
$(HIDE)rm -f $(VOFILES)
$(HIDE)rm -f $(VOFILES:.vo=.vio)
$(HIDE)rm -f $(GFILES)
$(HIDE)rm -f $(BEAUTYFILES) $(VFILES:=.old)
$(HIDE)rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob all-mli.tex
$(HIDE)rm -f $(VFILES:.v=.glob)
......@@ -654,15 +660,15 @@ endif
$(VOFILES): %.vo: %.v
$(SHOW)COQC $<
$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $< $(TIMING_EXTRA)
$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $< $(TIMING_EXTRA)
# FIXME ?merge with .vo / .vio ?
$(GLOBFILES): %.glob: %.v
$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $<
$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
$(VFILES:.v=.vio): %.vio: %.v
$(SHOW)COQC -quick $<
$(HIDE)$(TIMER) $(COQC) -quick $(COQDEBUG) $(COQFLAGS) $<
$(HIDE)$(TIMER) $(COQC) -quick $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
$(addsuffix .timing.diff,$(VFILES)): %.timing.diff : %.before-timing %.after-timing
$(SHOW)PYTHON TIMING-DIFF $<
......@@ -670,11 +676,7 @@ $(addsuffix .timing.diff,$(VFILES)): %.timing.diff : %.before-timing %.after-tim
$(BEAUTYFILES): %.v.beautified: %.v
$(SHOW)'BEAUTIFY $<'
$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $<
$(GFILES): %.g: %.v
$(SHOW)'GALLINA $<'
$(HIDE)$(GALLINA) $<
$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -beautify $<
$(TEXFILES): %.tex: %.v
$(SHOW)'COQDOC -latex $<'
......@@ -764,6 +766,7 @@ printenv::
@echo 'OCAMLFIND = $(OCAMLFIND)'
@echo 'PP = $(PP)'
@echo 'COQFLAGS = $(COQFLAGS)'
@echo 'COQLIB = $(COQLIBS)'
@echo 'COQLIBINSTALL = $(COQLIBINSTALL)'
@echo 'COQDOCINSTALL = $(COQDOCINSTALL)'
.PHONY: printenv
......
Makefile.conf
View file @ fedfec2c
......@@ -8,7 +8,7 @@
# #
###############################################################################
COQMF_VFILES = AsciiOrder.v StringOrder.v StringUtils.v Utils.v Defs.v Nam.v Mix.v NameProofs.v Subst.v Meta.v Equiv.v Equiv2.v AltSubst.v Countable.v Theories.v PreModels.v Models.v Peano.v ZF.v
COQMF_VFILES = AsciiOrder.v StringOrder.v StringUtils.v Utils.v Defs.v Nam.v Mix.v NameProofs.v Subst.v Restrict.v Meta.v Equiv.v Equiv2.v AltSubst.v Countable.v Theories.v PreModels.v Models.v Peano.v ZF.v
COQMF_MLIFILES =
COQMF_MLFILES =
COQMF_ML4FILES =
......@@ -34,17 +34,17 @@ COQMF_CMDLINE_COQLIBS =
# #
###############################################################################
COQMF_LOCAL=0
COQMF_COQLIB=/home/samuel/.opam/system/lib/coq/
COQMF_DOCDIR=/home/samuel/.opam/system/doc/
COQMF_OCAMLFIND=/home/samuel/.opam/system/bin/ocamlfind
COQMF_CAMLP5O=/home/samuel/.opam/system/bin/camlp5o
COQMF_CAMLP5BIN=/home/samuel/.opam/system/bin/
COQMF_CAMLP5LIB=/home/samuel/.opam/system/lib/camlp5
COQMF_LOCAL=1
COQMF_COQLIB=/home/letouzey/V8//
COQMF_DOCDIR=/home/letouzey/V8/doc/
COQMF_OCAMLFIND=/usr/bin/ocamlfind
COQMF_CAMLP5O=/usr/bin/camlp5o
COQMF_CAMLP5BIN=/usr/bin/
COQMF_CAMLP5LIB=/usr/lib/ocaml/camlp5
COQMF_CAMLP5OPTIONS=-loc loc
COQMF_CAMLFLAGS=-thread -rectypes -w +a-4-9-27-41-42-44-45-48-50-58-59 -safe-string
COQMF_CAMLFLAGS=-thread -rectypes -w +a-4-9-27-41-42-44-45-48-50-58-59 -safe-string -strict-sequence
COQMF_HASNATDYNLINK=true
COQMF_COQ_SRC_SUBDIRS=config dev lib clib kernel library engine pretyping interp parsing proofs tactics toplevel printing intf grammar ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/fourier plugins/funind plugins/ltac plugins/micromega plugins/nsatz plugins/omega plugins/quote plugins/romega plugins/rtauto plugins/setoid_ring plugins/ssr plugins/ssrmatching plugins/syntax plugins/xml
COQMF_COQ_SRC_SUBDIRS=config dev lib clib kernel library engine pretyping interp parsing proofs tactics toplevel printing grammar ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/funind plugins/ltac plugins/micromega plugins/nsatz plugins/omega plugins/quote plugins/romega plugins/rtauto plugins/setoid_ring plugins/ssr plugins/ssrmatching plugins/syntax plugins/xml
COQMF_WINDRIVE=
###############################################################################
......
Meta.v
View file @ fedfec2c
......@@ -1267,652 +1267,6 @@ Proof.
repeat (econstructor; eauto; unfold In; intuition).
Qed.
(** We could restrict a proof to use only some signature
(and only correctly). For that we replace unknown or incorrect
terms by a free variable, and unknown or incorrect predicates
by False. *)
Fixpoint restrict_term sign x t :=
match t with
| Fun f l =>
match sign.(funsymbs) f with
| None => FVar x
| Some ar =>
if length l =? ar then Fun f (map (restrict_term sign x) l)
else FVar x
end
| _ => t
end.
Fixpoint restrict sign x f :=
match f with
| True => True
| False => False
| Pred p l =>
match sign.(predsymbs) p with
| None => False
| Some ar =>
if length l =? ar then Pred p (map (restrict_term sign x) l)
else False
end
| Not f => Not (restrict sign x f)
| Op o f1 f2 => Op o (restrict sign x f1) (restrict sign x f2)
| Quant q f => Quant q (restrict sign x f)
end.
Definition restrict_ctx sign x c :=
map (restrict sign x) c.
Definition restrict_seq sign x '(c ⊢ f) :=
(restrict_ctx sign x c ⊢ restrict sign x f).
Definition restrict_rule sign x r :=
match r with
| All_e t => All_e (restrict_term sign x t)
| Ex_i t => Ex_i (restrict_term sign x t)
| _ => r
end.
Fixpoint restrict_deriv sign x d :=
let '(Rule r s l) := d in
Rule (restrict_rule sign x r)
(restrict_seq sign x s)
(map (restrict_deriv sign x) l).
Lemma claim_restrict sign x d :
claim (restrict_deriv sign x d) =
restrict_seq sign x (claim d).
Proof.
now destruct d.
Qed.
Lemma restrict_term_level sign x t :
level (restrict_term sign x t) <= level t.
Proof.
revert t.
fix IH 1. destruct t as [ | | f l]; cbn; auto with *.
destruct funsymbs; cbn; auto with *.
case eqbspec; cbn; auto with *.
intros _. clear f a.
revert l.
fix IH' 1. destruct l as [ |t l]; cbn; auto using Nat.max_le_compat with *.
Qed.
Lemma restrict_term_bclosed sign x t :
BClosed t -> BClosed (restrict_term sign x t).
Proof.
unfold BClosed. assert (H := restrict_term_level sign x t). auto with *.
Qed.
Lemma restrict_level sign x f :
level (restrict sign x f) <= level f.
Proof.
induction f; cbn; auto using Nat.max_le_compat with *.
destruct predsymbs; cbn; auto with *.
case eqbspec; cbn; auto with *.
intros _. clear p a.
induction l as [|t l IH]; cbn;
auto using Nat.max_le_compat, restrict_term_level.
Qed.
Lemma restrict_bclosed sign x f :
BClosed f -> BClosed (restrict sign x f).
Proof.
unfold BClosed. assert (H := restrict_level sign x f). auto with *.
Qed.
Lemma restrict_term_fvars sign x t :
Names.Subset (fvars (restrict_term sign x t))
(Names.add x (fvars t)).
Proof.
induction t as [ | | f l IH] using term_ind'; cbn; auto with *.
destruct funsymbs; cbn; auto with *.
case eqbspec; cbn; auto with *.
intros _. apply subset_unionmap_map'; auto.
Qed.
Lemma restrict_form_fvars sign x f :
Names.Subset (fvars (restrict sign x f))
(Names.add x (fvars f)).
Proof.
induction f; cbn; auto with *.
destruct predsymbs; cbn; auto with *.
case eqbspec; cbn; auto with *.
intros _. apply subset_unionmap_map'.
intros t _. apply restrict_term_fvars.
Qed.
Lemma restrict_ctx_fvars sign x c :
Names.Subset (fvars (restrict_ctx sign x c))
(Names.add x (fvars c)).
Proof.
unfold restrict_ctx.
apply subset_unionmap_map'.
intros f _. apply restrict_form_fvars.
Qed.
Lemma restrict_seq_fvars sign x s :
Names.Subset (fvars (restrict_seq sign x s))
(Names.add x (fvars s)).
Proof.
destruct s; cbn. rewrite restrict_ctx_fvars, restrict_form_fvars.
namedec.
Qed.
Lemma restrict_rule_fvars sign x r :
Names.Subset (fvars (restrict_rule sign x r))
(Names.add x (fvars r)).
Proof.
destruct r; cbn; rewrite ?restrict_term_fvars; auto with *.
Qed.
Lemma restrict_deriv_fvars sign x d :
Names.Subset (fvars (restrict_deriv sign x d))
(Names.add x (fvars d)).
Proof.
induction d as [r s ds IH] using derivation_ind'; cbn.
rewrite restrict_rule_fvars, restrict_seq_fvars.
rewrite Forall_forall in IH.
apply subset_unionmap_map' in IH. rewrite IH. namedec.
Qed.
Lemma restrict_term_bsubst sign x n (t u:term) :
restrict_term sign x (bsubst n u t) =
bsubst n (restrict_term sign x u) (restrict_term sign x t).
Proof.
induction t as [ | |f l IH] using term_ind'; cbn; auto.
- case eqbspec; auto.
- destruct funsymbs; cbn; auto with *.
rewrite map_length.
case eqbspec; cbn; auto.
intros _.
f_equal. rewrite !map_map. apply map_ext_iff; auto.
Qed.
Lemma restrict_lift sign x t :
restrict_term sign x (lift t) = lift (restrict_term sign x t).
Proof.
induction t as [ | |f l IH] using term_ind'; cbn; auto.
destruct funsymbs; cbn; auto with *.
rewrite map_length.
case eqbspec; cbn; auto.
intros _. f_equal. rewrite !map_map. apply map_ext_iff; auto.
Qed.
Lemma restrict_bsubst sign x n t f :
restrict sign x (bsubst n t f) =
bsubst n (restrict_term sign x t) (restrict sign x f).
Proof.
revert n t.
induction f; cbn; intros; f_equal; auto.
destruct predsymbs; cbn; auto with *.
rewrite map_length.
case eqbspec; cbn; auto.
intros _.
f_equal. rewrite !map_map.
apply map_ext_iff; auto using restrict_term_bsubst.
rewrite <- restrict_lift. auto.
Qed.
Ltac solver :=
try econstructor; auto;
try match goal with
| H : ~Names.In _ _ -> Valid _ ?d |- Valid _ ?d => apply H; namedec end;
try (unfold Claim; rewrite claim_restrict);
try match goal with
| H : claim ?d = _ |- context [claim ?d] => now rewrite H end.
Lemma restrict_valid logic sign x (d:derivation) :
~Names.In x (fvars d) ->
Valid logic d ->
Valid logic (restrict_deriv sign x d).
Proof.
induction 2; cbn - [Names.union] in *; try (solver; fail).
- constructor. now apply in_map.
- constructor.
+ cbn. rewrite restrict_ctx_fvars, restrict_form_fvars. namedec.
+ apply IHValid; namedec.
+ unfold Claim. rewrite claim_restrict. rewrite H2. simpl.
f_equal. apply restrict_bsubst.
- rewrite restrict_bsubst.
constructor.
+ apply IHValid; namedec.
+ unfold Claim. rewrite claim_restrict. now rewrite H1.
- constructor.
+ apply IHValid; namedec.
+ unfold Claim. rewrite claim_restrict. rewrite H1.
cbn. now rewrite restrict_bsubst.
- apply V_Ex_e with (restrict sign x A).
+ cbn. rewrite restrict_ctx_fvars, !restrict_form_fvars. namedec.
+ apply IHValid1; namedec.
+ apply IHValid2; namedec.
+ unfold Claim. rewrite claim_restrict. now rewrite H1.
+ unfold Claim. rewrite claim_restrict. rewrite H2.
cbn. f_equal. f_equal. apply restrict_bsubst.
Qed.
Lemma check_restrict_term_id sign x (t:term) :
check sign t = true -> restrict_term sign x t = t.
Proof.
induction t as [ | | f l IH] using term_ind'; cbn; auto.
destruct funsymbs; try easy.
rewrite lazy_andb_iff. intros (->,H). f_equal.
rewrite forallb_forall in H.
apply map_id_iff; auto.
Qed.
Lemma check_restrict_id sign x (f:formula) :
check sign f = true -> restrict sign x f = f.
Proof.
induction f; cbn; intros; f_equal; auto.
- destruct predsymbs; try easy.
rewrite lazy_andb_iff in H. destruct H as (->,H). f_equal.
rewrite forallb_forall in H.
apply map_id_iff; auto using check_restrict_term_id.
- rewrite ?lazy_andb_iff in H; intuition.
- rewrite ?lazy_andb_iff in H; intuition.
Qed.
Lemma check_restrict_ctx_id sign x (c:context) :
check sign c = true -> restrict_ctx sign x c = c.
Proof.
induction c as [|f c IH]; cbn; rewrite ?andb_true_iff; intros;
f_equal; auto.
- now apply check_restrict_id.
- now apply IH.
Qed.
Lemma restrict_term_check sign x (t:term) :
check sign (restrict_term sign x t) = true.
Proof.
induction t as [ | | f l IH] using term_ind'; cbn; auto.
destruct funsymbs eqn:E; try easy.
case eqbspec; cbn; auto.
intros <-.
rewrite E, map_length, eqb_refl, forallb_map, forallb_forall; auto.
Qed.
Lemma restrict_form_check sign x (f:formula) :
check sign (restrict sign x f) = true.
Proof.
induction f; cbn; auto.
- destruct predsymbs eqn:E; try easy.
case eqbspec; cbn; auto.
intros <-.
rewrite E, map_length, eqb_refl, forallb_map, forallb_forall;
auto using restrict_term_check.
- now rewrite IHf1, IHf2.
Qed.
Lemma restrict_ctx_check sign x (c:context) :
check sign (restrict_ctx sign x c) = true.
Proof.
induction c as [ |f c IH]; cbn; auto.
rewrite andb_true_iff; split; auto using restrict_form_check.
Qed.
Lemma restrict_seq_check sign x (s:sequent) :
check sign (restrict_seq sign x s) = true.
Proof.
destruct s. cbn.
now rewrite restrict_ctx_check, restrict_form_check.
Qed.
Lemma restrict_rule_check sign x (r:rule_kind) :
check sign (restrict_rule sign x r) = true.
Proof.
destruct r; cbn; auto using restrict_term_check.
Qed.
Lemma restrict_deriv_check sign x (d:derivation) :
check sign (restrict_deriv sign x d) = true.
Proof.
induction d as [r s ds IH] using derivation_ind'; cbn.
rewrite restrict_rule_check, restrict_seq_check.
rewrite forallb_map, forallb_forall, Forall_forall in *; auto.
Qed.
(** When a derivation has some bounded variables, we could
replace them by anything free. *)
Fixpoint forcelevel_term n x t :=
match t with
| FVar _ => t
| BVar m => if m <? n then t else FVar x
| Fun f l => Fun f (map (forcelevel_term n x) l)
end.
Fixpoint forcelevel n x f :=
match f with
| True => True
| False => False
| Pred p l => Pred p (map (forcelevel_term n x) l)
| Not f => Not (forcelevel n x f)
| Op o f1 f2 => Op o (forcelevel n x f1) (forcelevel n x f2)
| Quant q f => Quant q (forcelevel (S n) x f)
end.
Definition forcelevel_ctx x (c:context) :=
map (forcelevel 0 x) c.
Definition forcelevel_seq x '(c ⊢ f) :=
forcelevel_ctx x c ⊢ forcelevel 0 x f.
Definition forcelevel_rule x r :=
match r with
| All_e wit => All_e (forcelevel_term 0 x wit)
| Ex_i wit => Ex_i (forcelevel_term 0 x wit)
| _ => r
end.
Fixpoint forcelevel_deriv x d :=
let '(Rule r s ds) := d in
Rule (forcelevel_rule x r) (forcelevel_seq x s)
(map (forcelevel_deriv x) ds).
Lemma claim_forcelevel x d :
claim (forcelevel_deriv x d) = forcelevel_seq x (claim d).
Proof.
now destruct d.
Qed.
Lemma forcelevel_term_fvars n x t :
Names.Subset (fvars (forcelevel_term n x t)) (Names.add x (fvars t)).
Proof.
induction t as [ | | f l IH] using term_ind';
cbn - [Nat.ltb]; auto with *.
- case Nat.ltb_spec; cbn; auto with *.
- apply subset_unionmap_map'; auto.
Qed.
Lemma forcelevel_fvars n x f :
Names.Subset (fvars (forcelevel n x f)) (Names.add x (fvars f)).
Proof.
revert n.
induction f; cbn; intros; auto with *.
- apply subset_unionmap_map'.
intros t _. apply forcelevel_term_fvars.
- rewrite IHf1, IHf2. namedec.
Qed.
Lemma forcelevel_ctx_fvars x (c:context) :
Names.Subset (fvars (forcelevel_ctx x c)) (Names.add x (fvars c)).
Proof.
unfold forcelevel_ctx. unfold fvars, fvars_list.
apply subset_unionmap_map'.
intros f _. apply forcelevel_fvars.
Qed.
Lemma forcelevel_term_level n x t :
level (forcelevel_term n x t) <= n.
Proof.
induction t as [ | | f l IH] using term_ind';
cbn - [Nat.ltb]; auto with *.
- case Nat.ltb_spec; cbn; auto with *.
- rewrite map_map. apply list_max_map_le; auto.
Qed.
Lemma forcelevel_term_bclosed x t :
BClosed (forcelevel_term 0 x t).
Proof.
assert (H := forcelevel_term_level 0 x t). auto with *.
Qed.
Lemma forcelevel_level n x f :
level (forcelevel n x f) <= n.
Proof.
revert n.
induction f; cbn; intros; auto with *.
- rewrite map_map. apply list_max_map_le.
auto using forcelevel_term_level.
- apply max_le; auto.
- specialize (IHf (S n)). auto with *.
Qed.
Lemma forcelevel_bclosed x f :
BClosed (forcelevel 0 x f).
Proof.
assert (H := forcelevel_level 0 x f). auto with *.
Qed.
Lemma forcelevel_ctx_bclosed x c :
BClosed (forcelevel_ctx x c).
Proof.
induction c as [|f c IH]; cbn; auto.
unfold BClosed, level, level_list. cbn.
now rewrite forcelevel_bclosed, IH.
Qed.
Lemma forcelevel_seq_bclosed x s :
BClosed (forcelevel_seq x s).
Proof.
destruct s; cbn.
unfold BClosed, level, level_seq.
now rewrite forcelevel_bclosed, forcelevel_ctx_bclosed.
Qed.