Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Pierre Letouzey
natded
Commits
5e0e5897
Commit
5e0e5897
authored
Apr 16, 2019
by
Pierre Letouzey
Browse files
nettoyage : Vars --> Names
parent
b3196214
Changes
16
Expand all
Hide whitespace changes
Inline
Side-by-side
Alpha.v
View file @
5e0e5897
This diff is collapsed.
Click to expand it.
Alpha2.v
View file @
5e0e5897
This diff is collapsed.
Click to expand it.
Countable.v
View file @
5e0e5897
Require
Import
Ascii
Defs
Mix
Proofs
Meta
Omega
Setoid
Morphisms
NArith
.
Require
Import
Ascii
NArith
Omega
Setoid
Morphisms
.
Require
Import
Defs
Mix
NameProofs
Meta
.
Import
ListNotations
.
Local
Open
Scope
bool_scope
.
Local
Open
Scope
lazy_bool_scope
.
...
...
Defs.v
View file @
5e0e5897
...
...
@@ -7,12 +7,33 @@ Local Open Scope lazy_bool_scope.
Local
Open
Scope
string_scope
.
Local
Open
Scope
eqb_scope
.
(
**
Names
*
)
(
**
Names
are
coded
as
string
.
They
will
be
used
both
for
variables
and
function
symbols
and
predicate
symbols
.
During
proofs
,
these
strings
may
be
arbitrary
.
In
case
of
formula
parsing
,
we
'
ll
use
the
usual
syntactic
conventions
for
identifiers
:
a
letter
first
,
then
letters
or
digits
or
"_"
.
Some
symbols
will
also
be
accepted
as
function
or
predicate
symbols
,
such
as
"+"
"*"
"="
"∈"
.
In
fact
,
pretty
much
anything
that
doesn
'
t
contain
the
parenthesis
characters
or
the
comma
.
*
)
Definition
name
:=
string
.
Bind
Scope
string_scope
with
name
.
(
**
Variables
*
)
Definition
variable
:=
name
.
Bind
Scope
string_scope
with
name
.
(
**
Signatures
*
)
(
**
Just
in
case
,
a
signature
that
could
be
infinite
*
)
Definition
function_symbol
:=
string
.
Definition
predicate_symbol
:=
string
.
Definition
function_symbol
:=
name
.
Definition
predicate_symbol
:=
name
.
Definition
arity
:=
nat
.
Bind
Scope
string_scope
with
function_symbol
.
...
...
@@ -39,11 +60,6 @@ Definition to_infinite sign :=
End
Finite
.
(
**
In
pratice
,
the
symbols
could
be
special
characters
as
"+"
,
or
names
.
In
fact
,
pretty
much
anything
that
doesn
'
t
contain
the
parenthesis
characters
or
the
comma
.
*
)
Definition
peano_sign
:=
{|
Finite
.
funsymbs
:=
[(
"O"
,
0
);(
"S"
,
1
);(
"+"
,
2
);(
"*"
,
2
)];
Finite
.
predsymbs
:=
[(
"="
,
2
)]
|}
.
...
...
@@ -53,60 +69,55 @@ Definition zf_sign :=
Finite
.
predsymbs
:=
[(
"="
,
2
);(
"∈"
,
2
)]
|}
.
(
**
Variables
*
)
(
**
Sets
of
names
*
)
Module
Names
.
Include
MSetRBT
.
Make
(
StringOT
).
Definition
of_list
:
list
name
->
t
:=
fold_right
add
empty
.
(
**
Variables
are
coded
as
string
,
and
will
follow
the
usual
syntactic
conventions
for
identifiers
:
a
letter
first
,
then
letters
or
digits
or
"_"
.
*
)
Fixpoint
unions
(
l
:
list
t
)
:=
match
l
with
|
[]
=>
empty
|
vs
::
l
=>
union
vs
(
unions
l
)
end
.
Definition
variable
:=
string
.
Definition
unionmap
{
A
}
(
f
:
A
->
t
)
:=
fix
unionmap
(
l
:
list
A
)
:=
match
l
with
|
[]
=>
empty
|
a
::
l
=>
union
(
f
a
)
(
unionmap
l
)
end
.
Bind
Scope
string_scope
with
variable
.
Definition
map
(
f
:
name
->
name
)
(
s
:
t
)
:=
fold
(
fun
v
=>
add
(
f
v
))
s
empty
.
Module
Vars
:=
MSetRBT
.
Make
(
StringOT
).
Definition
flatmap
(
f
:
name
->
t
)
(
s
:
t
)
:=
fold
(
fun
v
=>
union
(
f
v
))
s
empty
.
End
Names
.
(
*
Prevent
incomplete
reductions
*
)
Arguments
Vars
.
singleton
!
_.
Arguments
Vars
.
add
!
_
!
_.
Arguments
Vars
.
remove
!
_
!
_.
Arguments
Vars
.
union
!
_
!
_.
Arguments
Vars
.
inter
!
_
!
_.
Arguments
Vars
.
diff
!
_
!
_.
Definition
vars_of_list
:
list
variable
->
Vars
.
t
:=
fold_right
Vars
.
add
Vars
.
empty
.
Fixpoint
vars_unions
(
l
:
list
Vars
.
t
)
:=
match
l
with
|
[]
=>
Vars
.
empty
|
vs
::
l
=>
Vars
.
union
vs
(
vars_unions
l
)
end
.
Definition
vars_unionmap
{
A
}
(
f
:
A
->
Vars
.
t
)
:=
fix
flatmap
(
l
:
list
A
)
:=
match
l
with
|
[]
=>
Vars
.
empty
|
a
::
l
=>
Vars
.
union
(
f
a
)
(
flatmap
l
)
end
.
Definition
vars_map
(
f
:
string
->
string
)
(
vs
:
Vars
.
t
)
:=
Vars
.
fold
(
fun
v
=>
Vars
.
add
(
f
v
))
vs
Vars
.
empty
.
Definition
vars_flatmap
(
f
:
string
->
Vars
.
t
)
(
vs
:
Vars
.
t
)
:=
Vars
.
fold
(
fun
v
=>
Vars
.
union
(
f
v
))
vs
Vars
.
empty
.
(
**
[
fresh_var
vars
]
:
gives
a
new
variable
not
in
the
set
[
vars
].
*
)
Fixpoint
fresh_var_loop
(
vars
:
Vars
.
t
)
(
id
:
string
)
n
:
variable
:=
Arguments
Names
.
singleton
!
_.
Arguments
Names
.
add
!
_
!
_.
Arguments
Names
.
remove
!
_
!
_.
Arguments
Names
.
union
!
_
!
_.
Arguments
Names
.
inter
!
_
!
_.
Arguments
Names
.
diff
!
_
!
_.
(
**
[
fresh
names
]
:
gives
a
new
name
not
in
the
set
[
names
].
*
)
Fixpoint
fresh_loop
(
names
:
Names
.
t
)
(
id
:
string
)
n
:
variable
:=
match
n
with
|
O
=>
id
|
S
n
=>
if
negb
(
Var
s
.
mem
id
var
s
)
then
id
else
fresh_
var_
loop
var
s
(
id
++
"x"
)
n
|
S
n
=>
if
negb
(
Name
s
.
mem
id
name
s
)
then
id
else
fresh_loop
name
s
(
id
++
"x"
)
n
end
.
Definition
fresh
_var
var
s
:=
fresh_
var_
loop
var
s
"x"
(
Var
s
.
cardinal
var
s
).
Definition
fresh
name
s
:=
fresh_loop
name
s
"x"
(
Name
s
.
cardinal
name
s
).
(
*
Compute
fresh
_var
(
Var
s
.
add
"x"
(
Var
s
.
add
"y"
(
Var
s
.
singleton
"xx"
))).
*
)
(
*
Compute
fresh
(
Name
s
.
add
"x"
(
Name
s
.
add
"y"
(
Name
s
.
singleton
"xx"
))).
*
)
(
**
Misc
types
:
operators
,
quantificators
*
)
...
...
Equiv.v
View file @
5e0e5897
(
**
Conversion
from
Named
formulas
to
Locally
Nameless
formulas
*
)
Require
Import
RelationClasses
Arith
Omega
Defs
Proofs
.
Require
Import
RelationClasses
Arith
Omega
Defs
Name
Proofs
.
Require
Nam
Mix
.
Import
ListNotations
.
Import
Nam
Nam
.
Form
.
...
...
@@ -49,7 +49,7 @@ Fixpoint mix2nam stack f :=
|
Mix
.
Op
o
f1
f2
=>
Op
o
(
mix2nam
stack
f1
)
(
mix2nam
stack
f2
)
|
Mix
.
Pred
p
args
=>
Pred
p
(
List
.
map
(
mix2nam_term
stack
)
args
)
|
Mix
.
Quant
q
f
=>
let
v
:=
fresh
_var
(
Var
s
.
union
(
vars_
of_list
stack
)
(
Mix
.
fvars
f
))
in
let
v
:=
fresh
(
Name
s
.
union
(
Names
.
of_list
stack
)
(
Mix
.
fvars
f
))
in
Nam
.
Quant
q
v
(
mix2nam
(
v
::
stack
)
f
)
end
.
...
...
@@ -60,13 +60,13 @@ Fixpoint mix2nam stack f :=
Module
Nam2Mix
.
Inductive
Inv
(
vars
:
Var
s
.
t
)
:
Subst
.
t
->
Subst
.
t
->
Prop
:=
Inductive
Inv
(
vars
:
Name
s
.
t
)
:
Subst
.
t
->
Subst
.
t
->
Prop
:=
|
InvNil
:
Inv
vars
[]
[]
|
InvCons
v
v
'
z
sub
sub
'
:
Inv
vars
sub
sub
'
->
~
Var
s
.
In
z
vars
->
~
Var
s
.
In
z
(
Nam
.
Subst
.
vars
sub
)
->
~
Var
s
.
In
z
(
Nam
.
Subst
.
vars
sub
'
)
->
~
Name
s
.
In
z
vars
->
~
Name
s
.
In
z
(
Nam
.
Subst
.
vars
sub
)
->
~
Name
s
.
In
z
(
Nam
.
Subst
.
vars
sub
'
)
->
Inv
vars
((
v
,
Var
z
)
::
sub
)
((
v
'
,
Var
z
)
::
sub
'
).
End
Nam2Mix
.
...
...
@@ -82,13 +82,13 @@ Qed.
Lemma
Inv_notIn
sub
sub
'
vars
v
:
Inv
vars
sub
sub
'
->
~
(
Var
s
.
In
v
vars
/
\
Var
s
.
In
v
(
Subst
.
outvars
sub
)).
~
(
Name
s
.
In
v
vars
/
\
Name
s
.
In
v
(
Subst
.
outvars
sub
)).
Proof
.
induction
1
;
unfold
Subst
.
vars
in
*
;
simpl
;
vars
dec
.
induction
1
;
unfold
Subst
.
vars
in
*
;
simpl
;
name
dec
.
Qed
.
Lemma
Inv_weak
sub
sub
'
vars
vars
'
:
Var
s
.
Subset
vars
'
vars
->
Inv
vars
sub
sub
'
->
Inv
vars
'
sub
sub
'
.
Name
s
.
Subset
vars
'
vars
->
Inv
vars
sub
sub
'
->
Inv
vars
'
sub
sub
'
.
Proof
.
induction
2
;
auto
.
Qed
.
...
...
@@ -105,13 +105,13 @@ Proof.
Qed
.
Lemma
list_assoc_some_in
v
sub
z
:
list_assoc
v
sub
=
Some
(
Var
z
)
->
Var
s
.
In
z
(
Subst
.
outvars
sub
).
list_assoc
v
sub
=
Some
(
Var
z
)
->
Name
s
.
In
z
(
Subst
.
outvars
sub
).
Proof
.
induction
sub
as
[
|
(
v
'
,
t
)
sub
IH
];
try
easy
.
simpl
.
case
eqbspec
.
-
intros
<-
[
=
->
].
simpl
.
vars
dec
.
-
intros
_
E
.
apply
IH
in
E
.
simpl
.
vars
dec
.
-
intros
<-
[
=
->
].
simpl
.
name
dec
.
-
intros
_
E
.
apply
IH
in
E
.
simpl
.
name
dec
.
Qed
.
Lemma
list_assoc_index
vars
v
v
'
sub
sub
'
z
:
...
...
@@ -127,9 +127,9 @@ Proof.
do
2
case
eqbspec
.
-
intros
.
now
exists
0.
-
intros
NE
<-
[
=
<-
]
E
.
apply
list_assoc_some_in
in
E
.
unfold
Nam
.
Subst
.
vars
in
*
.
vars
dec
.
unfold
Nam
.
Subst
.
vars
in
*
.
name
dec
.
-
intros
<-
NE
E
[
=
<-
].
apply
list_assoc_some_in
in
E
.
unfold
Nam
.
Subst
.
vars
in
*
.
vars
dec
.
unfold
Nam
.
Subst
.
vars
in
*
.
name
dec
.
-
intros
_
_
E
E
'
.
destruct
(
IHInv
E
E
'
)
as
(
k
&
Hk
&
Hk
'
).
exists
(
S
k
).
simpl
in
*
.
now
rewrite
Hk
,
Hk
'
.
Qed
.
...
...
@@ -161,7 +161,7 @@ Proof.
Qed
.
Lemma
nam2mix_term_ok
sub
sub
'
t
t
'
:
Inv
(
Var
s
.
union
(
Term
.
vars
t
)
(
Term
.
vars
t
'
))
sub
sub
'
->
Inv
(
Name
s
.
union
(
Term
.
vars
t
)
(
Term
.
vars
t
'
))
sub
sub
'
->
Term
.
substs
sub
t
=
Term
.
substs
sub
'
t
'
<->
nam2mix_term
(
map
fst
sub
)
t
=
nam2mix_term
(
map
fst
sub
'
)
t
'
.
Proof
.
...
...
@@ -177,11 +177,11 @@ Proof.
now
rewrite
Hk
,
Hk
'
.
*
intros
->
.
apply
list_assoc_some_in
in
E
.
destruct
(
Inv_notIn
_
_
_
v
'
inv
).
vars
dec
.
destruct
(
Inv_notIn
_
_
_
v
'
inv
).
name
dec
.
*
intros
<-
.
apply
list_assoc_some_in
in
E
'
.
apply
Inv_sym
in
inv
.
destruct
(
Inv_notIn
_
_
_
v
inv
).
vars
dec
.
destruct
(
Inv_notIn
_
_
_
v
inv
).
name
dec
.
*
intros
[
=
<-
].
rewrite
list_assoc_index_none
in
E
,
E
'
.
simpl
in
*
.
now
rewrite
E
,
E
'
.
...
...
@@ -207,16 +207,16 @@ Proof.
fix
IH
'
1.
destruct
a
as
[
|
t
a
],
a
'
as
[
|
t
'
a
'
];
try
easy
.
simpl
.
intros
[
=
E
E
'
]
inv
.
f_equal
.
*
apply
IH
;
auto
.
eapply
Inv_weak
;
eauto
.
vars
dec
.
*
apply
IH
'
;
auto
.
eapply
Inv_weak
;
eauto
.
vars
dec
.
*
apply
IH
;
auto
.
eapply
Inv_weak
;
eauto
.
name
dec
.
*
apply
IH
'
;
auto
.
eapply
Inv_weak
;
eauto
.
name
dec
.
+
intros
[
=
<-
E
].
f_equal
.
simpl
in
inv
.
clear
f
.
revert
a
a
'
E
inv
.
fix
IH
'
1.
destruct
a
as
[
|
t
a
],
a
'
as
[
|
t
'
a
'
];
try
easy
.
simpl
.
intros
[
=
E
E
'
]
inv
.
f_equal
.
*
apply
IH
;
auto
.
eapply
Inv_weak
;
eauto
.
vars
dec
.
*
apply
IH
'
;
auto
.
eapply
Inv_weak
;
eauto
.
vars
dec
.
*
apply
IH
;
auto
.
eapply
Inv_weak
;
eauto
.
name
dec
.
*
apply
IH
'
;
auto
.
eapply
Inv_weak
;
eauto
.
name
dec
.
Qed
.
Lemma
term_substs_nil
t
:
...
...
@@ -229,7 +229,7 @@ Qed.
Lemma
substs_nil
f
:
substs
[]
f
=
f
.
Proof
.
induction
f
;
cbn
-
[
fresh
_var
];
f_equal
;
auto
.
induction
f
;
cbn
-
[
fresh
];
f_equal
;
auto
.
apply
map_id_iff
.
intros
a
_.
apply
term_substs_nil
.
Qed
.
...
...
@@ -241,7 +241,7 @@ Proof.
Qed
.
Lemma
nam2mix_canonical_gen
sub
sub
'
f
f
'
:
Inv
(
Var
s
.
union
(
allvars
f
)
(
allvars
f
'
))
sub
sub
'
->
Inv
(
Name
s
.
union
(
allvars
f
)
(
allvars
f
'
))
sub
sub
'
->
α
eq_gen
sub
f
sub
'
f
'
=
true
<->
nam2mix
(
List
.
map
fst
sub
)
f
=
nam2mix
(
List
.
map
fst
sub
'
)
f
'
.
Proof
.
...
...
@@ -256,13 +256,13 @@ Proof.
-
rewrite
IHf
by
auto
.
split
;
[
intros
<-
|
intros
[
=
]];
easy
.
-
rewrite
!
lazy_andb_iff
,
!
eqb_eq
.
rewrite
IHf1
,
IHf2
by
(
eapply
Inv_weak
;
eauto
;
vars
dec
).
rewrite
IHf1
,
IHf2
by
(
eapply
Inv_weak
;
eauto
;
name
dec
).
split
;
[
intros
((
<-
,
<-
),
<-
)
|
intros
[
=
<-
<-
<-
]];
easy
.
-
rewrite
lazy_andb_iff
,
!
eqb_eq
.
set
(
vars
:=
Var
s
.
union
_
_
).
assert
(
Hz
:=
fresh_
var_
ok
vars
).
set
(
z
:=
fresh
_var
vars
)
in
*
.
rewrite
IHf
by
(
constructor
;
try
(
eapply
Inv_weak
;
eauto
);
vars
dec
).
set
(
vars
:=
Name
s
.
union
_
_
).
assert
(
Hz
:=
fresh_ok
vars
).
set
(
z
:=
fresh
vars
)
in
*
.
rewrite
IHf
by
(
constructor
;
try
(
eapply
Inv_weak
;
eauto
);
name
dec
).
simpl
.
split
;
[
intros
(
<-
,
<-
)
|
intros
[
=
]];
easy
.
Qed
.
...
...
@@ -278,7 +278,7 @@ Qed.
Lemma
mix_nam_mix_term_gen
stack
t
:
NoDup
stack
->
Mix
.
level
t
<=
List
.
length
stack
->
(
forall
v
,
In
v
stack
->
~
Var
s
.
In
v
(
Mix
.
fvars
t
))
->
(
forall
v
,
In
v
stack
->
~
Name
s
.
In
v
(
Mix
.
fvars
t
))
->
nam2mix_term
stack
(
mix2nam_term
stack
t
)
=
t
.
Proof
.
intros
ND
.
...
...
@@ -286,7 +286,7 @@ Proof.
-
destruct
(
list_index
v
stack
)
eqn
:
E
;
auto
.
assert
(
IN
:
In
v
stack
).
{
apply
list_index_in
.
now
rewrite
E
.
}
apply
FR
in
IN
.
vars
dec
.
apply
FR
in
IN
.
name
dec
.
-
rewrite
list_index_nth
;
auto
.
-
f_equal
.
clear
f
.
revert
l
LE
FR
.
...
...
@@ -294,15 +294,15 @@ Proof.
intros
LE
FR
.
f_equal
.
+
apply
IH
;
auto
.
omega
with
*
.
intros
v
IN
.
apply
FR
in
IN
.
vars
dec
.
intros
v
IN
.
apply
FR
in
IN
.
name
dec
.
+
apply
IHl
;
auto
.
omega
with
*
.
intros
v
IN
.
apply
FR
in
IN
.
vars
dec
.
intros
v
IN
.
apply
FR
in
IN
.
name
dec
.
Qed
.
Lemma
mix_nam_mix_gen
stack
f
:
NoDup
stack
->
Mix
.
level
f
<=
List
.
length
stack
->
(
forall
v
,
In
v
stack
->
~
Var
s
.
In
v
(
Mix
.
fvars
f
))
->
(
forall
v
,
In
v
stack
->
~
Name
s
.
In
v
(
Mix
.
fvars
f
))
->
nam2mix
stack
(
mix2nam
stack
f
)
=
f
.
Proof
.
revert
stack
.
...
...
@@ -312,23 +312,23 @@ Proof.
-
f_equal
.
auto
.
-
cbn
in
*
.
f_equal
.
+
apply
IHf1
;
auto
.
omega
with
*
.
intros
v
IN
.
apply
FR
in
IN
.
vars
dec
.
intros
v
IN
.
apply
FR
in
IN
.
name
dec
.
+
apply
IHf2
;
auto
.
omega
with
*
.
intros
v
IN
.
apply
FR
in
IN
.
vars
dec
.
intros
v
IN
.
apply
FR
in
IN
.
name
dec
.
-
cbn
in
*
.
f_equal
.
apply
IHf
;
auto
.
+
constructor
;
auto
.
set
(
vars
:=
Var
s
.
union
(
vars_
of_list
stack
)
(
Mix
.
fvars
f
)).
assert
(
FR
'
:=
fresh_
var_
ok
vars
).
set
(
vars
:=
Name
s
.
union
(
Names
.
of_list
stack
)
(
Mix
.
fvars
f
)).
assert
(
FR
'
:=
fresh_ok
vars
).
contradict
FR
'
.
unfold
vars
at
2.
VarsF
.
set_
iff
.
left
.
now
apply
var
s_of_list_in
.
unfold
vars
at
2.
name
iff
.
left
.
now
apply
name
s_of_list_in
.
+
simpl
.
omega
with
*
.
+
simpl
.
intros
v
[
<-|
IN
].
*
set
(
vars
:=
Var
s
.
union
(
vars_
of_list
stack
)
(
Mix
.
fvars
f
)).
generalize
(
fresh_
var_
ok
vars
).
vars
dec
.
*
apply
FR
in
IN
.
vars
dec
.
*
set
(
vars
:=
Name
s
.
union
(
Names
.
of_list
stack
)
(
Mix
.
fvars
f
)).
generalize
(
fresh_ok
vars
).
name
dec
.
*
apply
FR
in
IN
.
name
dec
.
Qed
.
Lemma
mix_nam_mix_term
t
:
...
...
Equiv2.v
View file @
5e0e5897
(
**
Conversion
from
Named
derivations
to
Locally
Nameless
derivations
*
)
Require
Import
RelationClasses
Arith
Omega
Defs
Proofs
Equiv
Alpha
Alpha2
Meta
.
Require
Import
RelationClasses
Arith
Omega
.
Require
Import
Defs
NameProofs
Equiv
Alpha
Alpha2
Meta
.
Require
Nam
Mix
.
Import
ListNotations
.
Import
Nam
Nam
.
Form
.
...
...
@@ -26,11 +27,11 @@ Proof.
Qed
.
Lemma
nam2mix_ctx_fvars
(
c
:
Nam
.
context
)
:
Var
s
.
Equal
(
Mix
.
fvars
(
nam2mix_ctx
c
))
(
Ctx
.
freevars
c
).
Name
s
.
Equal
(
Mix
.
fvars
(
nam2mix_ctx
c
))
(
Ctx
.
freevars
c
).
Proof
.
induction
c
as
[
|
f
c
IH
];
cbn
;
auto
.
-
vars
dec
.
-
rewrite
nam2mix_fvars
,
IH
.
simpl
.
vars
dec
.
-
name
dec
.
-
rewrite
nam2mix_fvars
,
IH
.
simpl
.
name
dec
.
Qed
.
(
**
Sequents
*
)
...
...
@@ -145,20 +146,20 @@ Proof.
apply
eq_true_iff_eq
.
rewrite
!
andb_true_iff
.
rewrite
!
negb_true_iff
,
<-
!
not_true_iff_false
.
rewrite
!
Var
s
.
mem_spec
.
rewrite
!
Name
s
.
mem_spec
.
rewrite
!
eqb_eq
.
split
;
intros
((
U
,
V
),
W
);
split
;
try
split
;
auto
.
+
change
(
Mix
.
FVar
x
)
with
(
nam2mix_term
[]
(
Var
x
))
in
V
.
rewrite
<-
nam2mix_altsubst_bsubst0
in
V
.
apply
nam2mix_rename_iff3
;
auto
.
rewrite
nam2mix_fvars
in
W
.
simpl
in
W
.
vars
dec
.
+
rewrite
<-
nam2mix_ctx_fvars
.
rewrite
<-
U
.
vars
dec
.
rewrite
nam2mix_fvars
in
W
.
simpl
in
W
.
name
dec
.
+
rewrite
<-
nam2mix_ctx_fvars
.
rewrite
<-
U
.
name
dec
.
+
rewrite
V
.
change
(
Mix
.
FVar
x
)
with
(
nam2mix_term
[]
(
Nam
.
Var
x
)).
rewrite
<-
nam2mix_altsubst_bsubst0
.
symmetry
.
apply
nam2mix_altsubst_nop
.
+
rewrite
U
,
V
,
nam2mix_ctx_fvars
.
rewrite
nam2mix_fvars
.
simpl
.
vars
dec
.
rewrite
nam2mix_fvars
.
simpl
.
name
dec
.
-
rewrite
nam2mix_subst_alt
,
nam2mix_altsubst_bsubst0
.
rewrite
nam2mix_term_bclosed
,
eqb_refl
.
apply
andb_true_r
.
...
...
@@ -169,7 +170,7 @@ Proof.
apply
eq_true_iff_eq
.
rewrite
!
andb_true_iff
.
rewrite
!
negb_true_iff
,
<-
!
not_true_iff_false
.
rewrite
!
Var
s
.
mem_spec
.
rewrite
!
Name
s
.
mem_spec
.
rewrite
!
eqb_eq
.
split
.
+
intros
(((
U
,
V
),
W
),
X
);
repeat
split
;
auto
.
...
...
@@ -177,10 +178,10 @@ Proof.
*
change
(
Mix
.
FVar
x
)
with
(
nam2mix_term
[]
(
Var
x
))
in
W
.
rewrite
<-
nam2mix_altsubst_bsubst0
in
W
.
apply
nam2mix_rename_iff3
;
auto
.
rewrite
nam2mix_fvars
in
X
.
simpl
in
X
.
vars
dec
.
rewrite
nam2mix_fvars
in
X
.
simpl
in
X
.
name
dec
.
*
revert
X
.
destruct
s
.
cbn
in
*
.
injection
U
as
<-
<-
.
rewrite
<-!
nam2mix_ctx_fvars
,
!
nam2mix_fvars
.
simpl
.
clear
.
vars
dec
.
clear
.
name
dec
.
+
intros
((
U
,(
V
,
W
)),
Z
);
repeat
split
;
auto
.
*
rewrite
U
.
f_equal
;
auto
.
*
rewrite
W
.
...
...
@@ -190,7 +191,7 @@ Proof.
*
revert
Z
.
destruct
s
.
cbn
in
*
.
rewrite
V
,
W
.
injection
U
as
<-
<-
.
rewrite
<-!
nam2mix_ctx_fvars
,
!
nam2mix_fvars
.
simpl
.
clear
.
vars
dec
.
simpl
.
clear
.
name
dec
.
Qed
.
Lemma
nam2mix_valid_deriv
logic
(
d
:
Nam
.
derivation
)
:
...
...
Makefile.conf
View file @
5e0e5897
...
...
@@ -8,7 +8,7 @@
# #
###############################################################################
COQMF_VFILES
=
AsciiOrder
.
v
StringOrder
.
v
StringUtils
.
v
Utils
.
v
Defs
.
v
Nam
.
v
Mix
.
v
Proofs
.
v
Alpha
.
v
Equiv
.
v
Alpha2
.
v
Equiv2
.
v
Meta
.
v
Countable
.
v
Theories
.
v
PreModels
.
v
Models
.
v
COQMF_VFILES
=
AsciiOrder
.
v
StringOrder
.
v
StringUtils
.
v
Utils
.
v
Defs
.
v
Nam
.
v
Mix
.
v
Name
Proofs
.
v
Alpha
.
v
Equiv
.
v
Alpha2
.
v
Equiv2
.
v
Meta
.
v
Countable
.
v
Theories
.
v
PreModels
.
v
Models
.
v
COQMF_MLIFILES
=
COQMF_MLFILES
=
COQMF_ML4FILES
=
...
...
Meta.v
View file @
5e0e5897
This diff is collapsed.
Click to expand it.
Mix.v
View file @
5e0e5897
...
...
@@ -97,7 +97,7 @@ Class Level (A : Type) := level : A -> nat.
Arguments
level
{
_
}
{
_
}
!
_.
(
**
Compute
the
set
of
free
variables
*
)
Class
FVars
(
A
:
Type
)
:=
fvars
:
A
->
Var
s
.
t
.
Class
FVars
(
A
:
Type
)
:=
fvars
:
A
->
Name
s
.
t
.
Arguments
fvars
{
_
}
{
_
}
!
_.
(
**
General
replacement
of
free
variables
*
)
...
...
@@ -108,7 +108,7 @@ Arguments vmap {_} {_} _ !_.
Definition
BClosed
{
A
}
`
{
Level
A
}
(
a
:
A
)
:=
level
a
=
0.
Definition
FClosed
{
A
}
`
{
FVars
A
}
(
a
:
A
)
:=
Var
s
.
Empty
(
fvars
a
).
Definition
FClosed
{
A
}
`
{
FVars
A
}
(
a
:
A
)
:=
Name
s
.
Empty
(
fvars
a
).
Hint
Unfold
BClosed
FClosed
.
...
...
@@ -132,7 +132,7 @@ Instance level_list {A}`{Level A} : Level (list A) :=
fun
l
=>
list_max
(
List
.
map
level
l
).
Instance
fvars_list
{
A
}
`
{
FVars
A
}
:
FVars
(
list
A
)
:=
vars_
unionmap
fvars
.
Names
.
unionmap
fvars
.
Instance
vmap_list
{
A
}
`
{
VMap
A
}
:
VMap
(
list
A
)
:=
fun
h
=>
List
.
map
(
vmap
h
).
...
...
@@ -147,7 +147,7 @@ Instance level_pair {A B}`{Level A}`{Level B} : Level (A*B) :=
fun
'
(
a
,
b
)
=>
Nat
.
max
(
level
a
)
(
level
b
).
Instance
fvars_pair
{
A
B
}
`
{
FVars
A
}
`
{
FVars
B
}
:
FVars
(
A
*
B
)
:=
fun
'
(
a
,
b
)
=>
Var
s
.
union
(
fvars
a
)
(
fvars
b
).
fun
'
(
a
,
b
)
=>
Name
s
.
union
(
fvars
a
)
(
fvars
b
).
Instance
vmap_pair
{
A
B
}
`
{
VMap
A
}
`
{
VMap
B
}
:
VMap
(
A
*
B
)
:=
fun
h
'
(
a
,
b
)
=>
(
vmap
h
a
,
vmap
h
b
).
...
...
@@ -175,9 +175,9 @@ Compute check (Finite.to_infinite peano_sign) peano_term_example.
Instance
term_fvars
:
FVars
term
:=
fix
term_fvars
t
:=
match
t
with
|
BVar
_
=>
Var
s
.
empty
|
FVar
v
=>
Var
s
.
singleton
v
|
Fun
_
args
=>
vars_
unionmap
term_fvars
args
|
BVar
_
=>
Name
s
.
empty
|
FVar
v
=>
Name
s
.
singleton
v
|
Fun
_
args
=>
Names
.
unionmap
term_fvars
args
end
.
Instance
term_level
:
Level
term
:=
...
...
@@ -337,11 +337,11 @@ Instance form_bsubst : BSubst formula :=
Instance form_fvars : FVars formula :=
fix form_fvars f :=
match f with
| True | False =>
Var
s.empty
| True | False =>
Name
s.empty
| Not f => form_fvars f
| Op _ f f' =>
Var
s.union (form_fvars f) (form_fvars f')
| Op _ f f' =>
Name
s.union (form_fvars f) (form_fvars f')
| Quant _ f => form_fvars f
| Pred _ args =>
vars_
unionmap fvars args
| Pred _ args =>
Names.
unionmap fvars args
end.
Instance form_vmap : VMap formula :=
...
...
@@ -406,7 +406,7 @@ Instance level_seq : Level sequent :=
fun '(Γ ⊢ A) => Nat.max (level Γ) (level A).
Instance seq_fvars : FVars sequent :=
fun '(Γ ⊢ A) =>
Var
s.union (fvars Γ) (fvars A).
fun '(Γ ⊢ A) =>
Name
s.union (fvars Γ) (fvars A).
Instance seq_vmap : VMap sequent :=
fun h '(Γ ⊢ A) => (vmap h Γ ⊢ vmap h A).
...
...
@@ -469,15 +469,15 @@ Instance check_derivation : Check derivation :=
Instance fvars_rule : FVars rule_kind :=
fun r =>
match r with
| All_i x | Ex_e x =>
Var
s.singleton x
| All_i x | Ex_e x =>
Name
s.singleton x
| All_e wit | Ex_i wit => fvars wit
| _ =>
Var
s.empty
| _ =>
Name
s.empty
end.
Instance fvars_derivation : FVars derivation :=
fix fvars_derivation d :=
let '(Rule r s ds) := d in
vars_
unions [fvars r; fvars s;
vars_
unionmap fvars_derivation ds].
Names.
unions [fvars r; fvars s;
Names.
unionmap fvars_derivation ds].
Instance bsubst_rule : BSubst rule_kind :=
fun n u r =>
...
...
@@ -545,7 +545,7 @@ Definition valid_deriv_step logic '(Rule r s ld) :=
(s =? (Γ ⊢ B)) &&& (s2 =? (Γ ⊢ A))
| All_i x, (Γ⊢∀A), [Γ' ⊢ A'] =>
(Γ =? Γ') &&& (A' =? bsubst 0 (FVar x) A)
&&& negb (
Var
s.mem x (fvars (Γ⊢A)))
&&& negb (
Name
s.mem x (fvars (Γ⊢A)))
| All_e t, (Γ ⊢ B), [Γ'⊢ ∀A] =>
(Γ =? Γ') &&& (B =? bsubst 0 t A) &&& (level t =? 0)
| Ex_i t, (Γ ⊢ ∃A), [Γ'⊢B] =>
...
...
@@ -553,7 +553,7 @@ Definition valid_deriv_step logic '(Rule r s ld) :=
| Ex_e x, s, [Γ⊢∃A; A'::Γ'⊢B] =>
(s =? (Γ ⊢ B)) &&& (Γ' =? Γ)
&&& (A' =? bsubst 0 (FVar x) A)
&&& negb (
Var
s.mem x (fvars (A::Γ⊢B)))
&&& negb (
Name
s.mem x (fvars (A::Γ⊢B)))
| Absu, s, [Not A::Γ ⊢ False] =>
(logic =? Classic) &&& (s =? (Γ ⊢ A))
| _,_,_ => false
...
...
@@ -753,7 +753,7 @@ Inductive Valid (l:logic) : derivation -> Prop :=
Claim d1 (Γ ⊢ A->B) -> Claim d2 (Γ ⊢ A) ->
Valid l (Rule Imp_e (Γ ⊢ B) [d1;d2])
| V_All_i x d Γ A :
~
Var
s.In x (fvars (Γ ⊢ A)) ->
~
Name
s.In x (fvars (Γ ⊢ A)) ->
Valid l d -> Claim d (Γ ⊢ bsubst 0 (FVar x) A) ->
Valid l (Rule (All_i x) (Γ ⊢ ∀A) [d])
| V_All_e t d Γ A :
...
...
@@ -763,7 +763,7 @@ Inductive Valid (l:logic) : derivation -> Prop :=
BClosed t -> Valid l d -> Claim d (Γ ⊢ bsubst 0 t A) ->
Valid l (Rule (Ex_i t) (Γ ⊢ ∃A) [d])
| V_Ex_e x d1 d2 Γ A B :
~
Var
s.In x (fvars (A::Γ⊢B)) ->
~
Name
s.In x (fvars (A::Γ⊢B)) ->
Valid l d1 -> Valid l d2 ->
Claim d1 (Γ ⊢ ∃A) -> Claim d2 ((bsubst 0 (FVar x) A)::Γ ⊢ B) ->
Valid l (Rule (Ex_e x) (Γ ⊢ B) [d1;d2])
...
...
@@ -815,13 +815,13 @@ Proof.
mytac; subst; eauto.
+ now apply V_Ax, list_mem_in.
+ apply V_All_i; auto.
rewrite <-
Var
s.mem_spec. cbn. intros EQ. now rewrite EQ in *.
rewrite <-
Name
s.mem_spec. cbn. intros EQ. now rewrite EQ in *.
+ apply V_Ex_e with f; auto.
rewrite <-
Var
s.mem_spec. cbn. intros EQ. now rewrite EQ in *.
rewrite <-
Name
s.mem_spec. cbn. intros EQ. now rewrite EQ in *.
- induction 1; simpl; rewr; auto.
+ apply list_mem_in in H. now rewrite H.
+ rewrite <-
Var
s.mem_spec in H. destruct
Var
s.mem; auto.