Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Pierre Letouzey
natded
Commits
afd28b66
Commit
afd28b66
authored
Aug 02, 2020
by
Pierre Letouzey
Browse files
Restrict reworked, a forceWF function for forcelevel + restrict
parent
ea4f820a
Changes
2
Hide whitespace changes
Inline
Sidebyside
Restrict.v
View file @
afd28b66
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
.
Theories.v
View file @
afd28b66
...
...
@@ 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
).
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment