Module RConstants
Section
RConstants
.
Require
Import
String
.
Require
Import
EquivDec
.
Require
Import
List
.
Require
Import
RUtil
RList
RSublist
RFresh
RBindings
RAssoc
.
Definition
CONST_PREFIX
:
string
:= "
CONST
$"%
string
.
Definition
mkConstantName
(
n
:
string
) :=
append
CONST_PREFIX
n
.
Definition
mkConstant
{
A
} (
b
:
string
*
A
)
:= (
mkConstantName
(
fst
b
),(
snd
b
)).
Definition
mkConstants
{
A
} (
l
:
list
(
string
*
A
))
:=
map
mkConstant
l
.
Section
ConstantsProp
.
Definition
filterConstants
{
A
} (
l
:
list
(
string
*
A
))
:=
filter
(
fun
xy
=>
prefix
CONST_PREFIX
(
fst
xy
))
l
.
Lemma
filterConstants_lookup_pre
{
A
} (
l
:
list
(
string
*
A
))
s
:
lookup
equiv_dec
(
filterConstants
l
) (
append
CONST_PREFIX
s
)
=
lookup
equiv_dec
l
(
append
CONST_PREFIX
s
).
Proof.
revert
s
.
induction
l
;
simpl
;
trivial
.
destruct
a
;
simpl
.
intros
.
match_case
;
intros
;
simpl
.
-
dest_eqdec
;
trivial
.
apply
IHl
.
-
specialize
(
IHl
s0
).
simpl
in
IHl
;
rewrite
IHl
.
dest_eqdec
.
+
simpl
in
*.
rewrite
prefix_nil
in
H
.
congruence
.
+
trivial
.
Qed.
Lemma
filter_rev
{
A
} (
f
:
A
->
bool
)
l
:
filter
f
(
rev
l
) =
rev
(
filter
f
l
).
Proof.
induction
l
;
simpl
;
trivial
.
rewrite
filter_app
,
IHl
.
simpl
.
match_destr
.
rewrite
app_nil_r
.
trivial
.
Qed.
Lemma
filterConstants_rev
{
A
} (
l
:
list
(
string
*
A
)) :
filterConstants
(
rev
l
) =
rev
(
filterConstants
l
).
Proof.
unfold
filterConstants
.
rewrite
filter_rev
.
trivial
.
Qed.
Lemma
mkConstants_rev
{
A
} (
l
:
list
(
string
*
A
)) :
mkConstants
(
rev
l
) =
rev
(
mkConstants
l
).
Proof.
unfold
mkConstants
.
rewrite
map_rev
.
trivial
.
Qed.
Lemma
filterConstants_assoc_lookupr_pre
{
A
} (
l
:
list
(
string
*
A
))
s
:
assoc_lookupr
equiv_dec
(
filterConstants
l
) (
append
CONST_PREFIX
s
)
=
assoc_lookupr
equiv_dec
l
(
append
CONST_PREFIX
s
).
Proof.
rewrite
(
assoc_lookupr_lookup
equiv_dec
_
(
filterConstants
l
)).
rewrite
(
assoc_lookupr_lookup
equiv_dec
_
l
).
rewrite
<-
filterConstants_rev
.
rewrite
filterConstants_lookup_pre
.
trivial
.
Qed.
Lemma
filterConstants_mkConstants
{
A
} (
l
:
list
(
string
*
A
)) :
filterConstants
(
mkConstants
l
) =
mkConstants
l
.
Proof.
induction
l
;
simpl
;
trivial
.
rewrite
IHl
.
rewrite
prefix_nil
.
trivial
.
Qed.
Lemma
mkConstants_NoDup
{
A
} (
l
:
list
(
string
*
A
)) :
NoDup
(
domain
l
) <->
NoDup
(
domain
(
mkConstants
l
)).
Proof.
Opaque
append
.
unfold
mkConstants
,
domain
.
rewrite
map_map
;
simpl
.
rewrite
<- (
map_map
(@
fst
_
A
) (
append
CONST_PREFIX
)).
split
;
intros
.
-
apply
map_inj_NoDup
;
trivial
.
intros
.
apply
append_eq_inv1
in
H0
;
trivial
.
-
apply
unmap_NoDup
in
H
.
trivial
.
Transparent
append
.
Qed.
Lemma
filterConstants_NoDup
{
A
} (
l
:
list
(
string
*
A
)) :
NoDup
(
domain
l
) ->
NoDup
(
domain
(
filterConstants
l
)).
Proof.
unfold
filterConstants
,
domain
.
apply
sublist_NoDup
.
apply
sublist_map
.
simpl
.
apply
filter_sublist
.
Qed.
Lemma
mkConstants_indom
{
A
} (
l
:
list
(
string
*
A
))
x
:
In
x
(
domain
(
mkConstants
l
)) ->
prefix
CONST_PREFIX
x
=
true
.
Proof.
intros
inn
.
unfold
domain
,
mkConstants
in
inn
.
rewrite
map_map
in
inn
;
simpl
in
inn
.
apply
in_map_iff
in
inn
.
destruct
inn
as
[? [? ?]];
subst
.
simpl
.
apply
prefix_nil
.
Qed.
Lemma
mkConstants_nindom
{
A
} (
l
:
list
(
string
*
A
))
x
:
prefix
CONST_PREFIX
x
=
false
->
~ (
In
x
(
domain
(
mkConstants
l
))).
Proof.
intros
pre
inn
.
apply
mkConstants_indom
in
inn
.
congruence
.
Qed.
Lemma
mkConstants_lookup_pre
{
A
}
l
x
(
y
:
A
) :
lookup
string_eqdec
(
mkConstants
l
)
x
=
Some
y
->
prefix
CONST_PREFIX
x
=
true
.
Proof.
intros
inn
.
apply
lookup_in
in
inn
.
apply
in_dom
in
inn
.
eapply
mkConstants_indom
;
eauto
.
Qed.
Lemma
mkConstants_lookup
{
A
} (
l
:
list
(
string
*
A
))
x
:
lookup
string_eqdec
(
mkConstants
l
) (
append
CONST_PREFIX
x
) =
lookup
string_eqdec
l
x
.
Proof.
Opaque
append
.
induction
l
;
simpl
;
trivial
.
unfold
mkConstantName
.
destruct
a
;
simpl
.
repeat
match_destr
;
unfold
Equivalence.equiv
in
* .
-
apply
append_eq_inv1
in
e
.
congruence
.
-
congruence
.
Transparent
append
.
Qed.
Lemma
mkConstants_assoc_lookupr
{
A
} (
l
:
list
(
string
*
A
))
x
:
assoc_lookupr
string_eqdec
(
mkConstants
l
) (
append
CONST_PREFIX
x
) =
assoc_lookupr
string_eqdec
l
x
.
Proof.
rewrite
(
assoc_lookupr_lookup
string_eqdec
_
(
mkConstants
l
)).
rewrite
(
assoc_lookupr_lookup
string_eqdec
_
l
).
rewrite
<-
mkConstants_rev
.
rewrite
mkConstants_lookup
.
trivial
.
Qed.
Lemma
rec_sort_mkConstants_comm
{
A
} (
l
:
list
(
string
*
A
)) :
rec_sort
(
mkConstants
l
) =
mkConstants
(
rec_sort
l
).
Proof.
unfold
mkConstants
.
rewrite
<-
map_rec_sort
.
reflexivity
.
intros
.
unfold
mkConstant
;
simpl
.
destruct
x
;
destruct
y
;
simpl
.
unfold
mkConstantName
.
split
;
intros
;
auto
.
Qed.
End
ConstantsProp
.
Section
World
.
Require
Import
RData
.
Require
Import
ForeignData
.
Context
{
fdata
:
foreign_data
}.
Definition
WORLD
:
string
:= "
WORLD
"%
string
.
Definition
mkWorld
(
world
:
list
data
) :
list
(
string
*
data
)
:= (
WORLD
,(
dcoll
world
))::
nil
.
End
World
.
Section
unConst
.
Require
Import
String
.
Definition
unConstVar
(
fv
:
string
) :
string
:=
if
(
prefix
"
CONST
$"
fv
)
then
substring
6 ((
length
fv
) - 6)
fv
else
fv
.
End
unConst
.
End
RConstants
.