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

Restrict reworked, a forceWF function for forcelevel + restrict

parent ea4f820a
Require Import Defs NameProofs Mix.
Require Import Defs NameProofs Mix Wellformed.
Import ListNotations.
Local Open Scope bool_scope.
Local Open Scope lazy_bool_scope.
......@@ -234,37 +234,6 @@ Proof.
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.
......@@ -315,6 +284,44 @@ Proof.
rewrite forallb_map, forallb_forall, Forall_forall in *; auto.
Qed.
Lemma 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 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 restrict_term_id.
- rewrite ?lazy_andb_iff in H; intuition.
- rewrite ?lazy_andb_iff in H; intuition.
Qed.
Lemma 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 restrict_id.
- now apply IH.
Qed.
Lemma restrict_seq_id sign x (s:sequent) :
check sign s = true -> restrict_seq sign x s = s.
Proof.
destruct s as (c,f). cbn. rewrite lazy_andb_iff. intros (Hc,Hf).
f_equal. now apply restrict_ctx_id. now apply restrict_id.
Qed.
(** When a derivation has some bounded variables, we could
replace them by anything free. *)
......@@ -592,6 +599,8 @@ Proof.
f_equal. apply forcelevel_bsubst; auto.
Qed.
(** [restrict] and [forcelevel] commute *)
Lemma restrict_forcelevel_term sign x n y t :
restrict_term sign x (forcelevel_term n y t) =
forcelevel_term n y (restrict_term sign x t).
......@@ -654,3 +663,45 @@ Proof.
- rewrite !map_map. apply map_ext_iff.
rewrite Forall_forall in IH; auto.
Qed.
(** Combining [restrict] and [forcelevel] on a derivation *)
Definition forceWF sign (d:derivation) :=
let vars := fvars d in
let x := fresh vars in
let y := fresh (Names.add x vars) in
forcelevel_deriv y (restrict_deriv sign x d).
Lemma forceWF_WF sign d : WF sign (forceWF sign d).
Proof.
unfold forceWF. split.
- rewrite <- restrict_forcelevel_deriv.
apply restrict_deriv_check.
- apply forcelevel_deriv_bclosed.
Qed.
Lemma forceWF_Valid lg sign d :
Valid lg d -> Valid lg (forceWF sign d).
Proof.
intros V.
unfold forceWF.
set (vars := fvars d) in *.
set (x := fresh vars).
set (y := fresh _).
apply forcelevel_deriv_valid.
- rewrite restrict_deriv_fvars. apply fresh_ok.
- apply restrict_valid; auto. apply fresh_ok.
Qed.
Lemma forceWF_claim sign d :
WF sign (claim d) -> claim (forceWF sign d) = claim d.
Proof.
intros W.
unfold forceWF.
set (vars := fvars d) in *.
set (x := fresh vars).
set (y := fresh _).
rewrite claim_forcelevel, claim_restrict.
destruct d. cbn. cbn in W. rewrite restrict_seq_id by apply W.
apply forcelevel_seq_id. apply W.
Qed.
......@@ -103,38 +103,16 @@ Lemma thm_alt th T :
IsTheorem th T <-> IsTheoremStrict th T.
Proof.
split.
- intros (WF & axs & F & PR).
split; auto. rewrite Provable_alt in PR.
destruct PR as (d & V & C).
destruct (exist_fresh (fvars d)) as (x,Hx).
destruct (exist_fresh (Names.add x (fvars d))) as (y,Hy).
exists (forcelevel_deriv y (restrict_deriv th x d)).
exists axs; repeat split; auto.
+ rewrite <- restrict_forcelevel_deriv.
apply restrict_deriv_check.
+ apply forcelevel_deriv_bclosed.
+ apply forcelevel_deriv_valid.
* rewrite restrict_deriv_fvars.
namedec.
* apply restrict_valid; auto.
+ rewrite Forall_forall in F.
unfold Claim.
rewrite claim_forcelevel, claim_restrict, C.
cbn. f_equal.
* assert (check th axs = true).
{ unfold check, check_list.
apply forallb_forall.
intros A HA. apply WCAxiom; auto. }
rewrite check_restrict_ctx_id by auto.
apply forcelevel_ctx_id.
unfold BClosed, level, level_list.
apply list_max_map_0.
intros A HA. apply (WCAxiom th A); auto.
* rewrite check_restrict_id by apply WF.
apply forcelevel_id.
assert (level T = 0) by apply WF.
auto with *.
- intros (CL & d & axs & V & F & C).
- intros (W & axs & F & P).
split; auto. rewrite Provable_alt in P.
destruct P as (d & V & C).
exists (forceWF th d).
exists axs; split; split; auto using forceWF_WF, forceWF_Valid.
unfold Claim in *. rewrite <- C. apply forceWF_claim.
rewrite C, seq_WF. split; try apply W.
rewrite ctx_WF. rewrite Forall_forall in *. intros x Hx.
apply WCAxiom; auto.
- intros (W & d & axs & V & F & C).
split; auto.
exists axs; split; auto.
rewrite Provable_alt.
......@@ -441,17 +419,17 @@ Proof.
apply (restrict_valid logic th x) in V; auto with set.
assert (C' := claim_restrict th x d).
rewrite C in C'. cbn in C'.
rewrite (check_restrict_id th x T) in C'; auto.
rewrite (restrict_id th x T) in C'; auto.
assert (map (restrict th x) axs' = axs').
{ apply map_id_iff. intros a Ha.
apply check_restrict_id.
apply restrict_id.
apply WCAxiom. rewrite Forall_forall in F'; auto. }
rewrite H0 in C'; clear H0.
assert (restrict th x newAx = bsubst 0 (FVar x) A).
{ unfold newAx.
rewrite restrict_bsubst. f_equal.
- cbn. now rewrite E.
- apply check_restrict_id. apply CLA. }
- apply restrict_id. apply CLA. }
rewrite H0 in C'; clear H0.
apply Valid_Pr in V. rewrite C' in V.
apply (R_Ex_e logic x _ A).
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment