Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
AVA
FloVer
Commits
2ba31c82
Commit
2ba31c82
authored
Oct 26, 2017
by
Heiko Becker
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Start working on speeding up computations by simplifying typeMap computation
parent
35989490
Changes
4
Hide whitespace changes
Inline
Side-by-side
Showing
4 changed files
with
584 additions
and
13 deletions
+584
-13
coq/Expressions.v
coq/Expressions.v
+453
-1
coq/Infra/Ltacs.v
coq/Infra/Ltacs.v
+8
-2
coq/Infra/MachineType.v
coq/Infra/MachineType.v
+36
-5
coq/Typing.v
coq/Typing.v
+87
-5
No files found.
coq/Expressions.v
View file @
2ba31c82
...
...
@@ -2,7 +2,7 @@
Formalization
of
the
base
expression
language
for
the
daisy
framework
**
)
Require
Import
Coq
.
Reals
.
Reals
Coq
.
micromega
.
Psatz
Coq
.
QArith
.
QArith
Coq
.
QArith
.
Qreals
.
Coq
.
QArith
.
Qreals
Coq
.
Structures
.
Orders
Coq
.
Structures
.
OrdersFacts
.
Require
Import
Daisy
.
Infra
.
RealRationalProps
Daisy
.
Infra
.
RationalSimps
Daisy
.
Infra
.
Ltacs
.
Require
Export
Daisy
.
Infra
.
Abbrevs
Daisy
.
Infra
.
RealSimps
Daisy
.
Infra
.
NatSet
...
...
@@ -75,6 +75,12 @@ Proof.
case
b
;
auto
.
Qed
.
Lemma
unopEq_sym
u1
u2
:
unopEq
u1
u2
=
unopEq
u2
u1
.
Proof
.
destruct
u1
,
u2
;
compute
;
auto
.
Qed
.
Lemma
unopEq_compat_eq
b1
b2
:
unopEq
b1
b2
=
true
<->
b1
=
b2
.
Proof
.
...
...
@@ -187,6 +193,452 @@ Proof.
eapply
IHe
;
eauto
.
Qed
.
Module
ExpOrderedType
(
V_ordered
:
OrderedType
)
<:
OrderedType
.
Module
V_orderedFacts
:=
OrderedTypeFacts
(
V_ordered
).
Definition
V
:=
V_ordered
.
t
.
Fixpoint
expCompare
(
e1
:
exp
V
)
(
e2
:
exp
V
)
:=
match
e1
,
e2
with
|
Var
_
n1
,
Var
_
n2
=>
Nat
.
compare
n1
n2
|
Var
_
n1
,
_
=>
Lt
|
Const
m1
v1
,
Const
m2
v2
=>
if
mTypeEq
m1
m2
then
V_ordered
.
compare
v1
v2
else
(
if
morePrecise
m1
m2
then
Lt
else
Gt
)
|
Const
_
_
,
Var
_
_
=>
Gt
|
Const
_
_
,
_
=>
Lt
|
Unop
u1
e1
,
Unop
u2
e2
=>
if
unopEq
u1
u2
then
expCompare
e1
e2
else
(
if
unopEq
u1
Neg
then
Lt
else
Gt
)
|
Unop
_
_
,
Binop
_
_
_
=>
Lt
|
Unop
_
_
,
Downcast
_
_
=>
Lt
|
Unop
_
_
,
_
=>
Gt
|
Downcast
m1
e1
,
Downcast
m2
e2
=>
if
mTypeEq
m1
m2
then
expCompare
e1
e2
else
(
if
morePrecise
m1
m2
then
Lt
else
Gt
)
|
Downcast
_
_
,
Binop
_
_
_
=>
Lt
|
Downcast
_
_
,
_
=>
Gt
|
Binop
b1
e11
e12
,
Binop
b2
e21
e22
=>
let
res
:=
match
b1
,
b2
with
|
Plus
,
Plus
=>
Eq
|
Plus
,
_
=>
Lt
|
Sub
,
Sub
=>
Eq
|
Sub
,
Plus
=>
Gt
|
Sub
,
_
=>
Lt
|
Mult
,
Mult
=>
Eq
|
Mult
,
Div
=>
Lt
|
Mult
,
_
=>
Gt
|
Div
,
Div
=>
Eq
|
Div
,
_
=>
Gt
end
in
match
res
with
|
Eq
=>
match
expCompare
e11
e21
with
|
Eq
=>
expCompare
e12
e22
|
Lt
=>
Lt
|
Gt
=>
Gt
end
|
_
=>
res
end
|
_
,
_
=>
Gt
end
.
Lemma
expCompare_refl
e
:
expCompare
e
e
=
Eq
.
Proof
.
induction
e
;
simpl
.
-
apply
Nat
.
compare_refl
.
-
rewrite
mTypeEq_refl
.
apply
V_orderedFacts
.
compare_refl
.
-
rewrite
unopEq_refl
;
auto
.
-
rewrite
IHe1
,
IHe2
.
destruct
b
;
auto
.
-
rewrite
mTypeEq_refl
;
auto
.
Qed
.
(
*
Lemma
expCompare_eq_compat_eq
e1
:
*
)
(
*
forall
e2
,
*
)
(
*
expCompare
e1
e2
=
Eq
<->
*
)
(
*
eq
e1
e2
.
*
)
(
*
Proof
.
*
)
(
*
induction
e1
;
destruct
e2
;
split
;
intros
*
cmp_res
;
simpl
in
*
;
*
)
(
*
subst
;
try
congruence
.
*
)
(
*
-
rewrite
Nat
.
compare_eq_iff
in
cmp_res
;
subst
;
auto
.
*
)
(
*
-
inversion
cmp_res
;
subst
;
simpl
.
apply
Nat
.
compare_refl
.
*
)
(
*
-
destruct
(
mTypeEq
m
m0
*
)
(
*
apply
V_orderedFacts
.
compare_eq
in
cmp_res
.
*
)
(
*
f_equal
.
*
)
(
*
hnf
in
cmp_res
.
*
)
Lemma
expCompare_eq_trans
e1
:
forall
e2
e3
,
expCompare
e1
e2
=
Eq
->
expCompare
e2
e3
=
Eq
->
expCompare
e1
e3
=
Eq
.
Proof
.
induction
e1
;
intros
*
eq12
eq23
;
destruct
e2
;
destruct
e3
;
simpl
in
*
;
try
congruence
.
-
rewrite
Nat
.
compare_eq_iff
in
*
;
subst
;
auto
.
-
destruct
(
mTypeEq
m
m0
)
eqn
:?
;
[
destruct
(
mTypeEq
m0
m1
)
eqn
:?
|
destruct
(
morePrecise
m
m0
)
eqn
:?
;
congruence
];
[
|
destruct
(
morePrecise
m0
m1
)
eqn
:?
;
congruence
].
type_conv
.
rewrite
mTypeEq_refl
.
rewrite
V_orderedFacts
.
compare_eq_iff
in
*
;
eapply
V_orderedFacts
.
eq_trans
;
eauto
.
-
destruct
(
unopEq
u
u0
)
eqn
:?
;
destruct
(
unopEq
u0
u1
)
eqn
:?
;
try
rewrite
unopEq_compat_eq
in
*
;
subst
;
try
rewrite
unopEq_refl
;
try
congruence
.
+
eapply
IHe1
;
eauto
.
+
destruct
(
unopEq
u0
Neg
);
congruence
.
+
destruct
(
unopEq
u
Neg
);
congruence
.
+
destruct
(
unopEq
u
Neg
);
congruence
.
-
destruct
b
;
destruct
b0
;
try
congruence
;
destruct
b1
;
try
congruence
;
destruct
(
expCompare
e1_1
e2_1
)
eqn
:?
;
destruct
(
expCompare
e2_1
e3_1
)
eqn
:?
;
try
congruence
;
try
erewrite
IHe1_1
;
eauto
.
-
destruct
(
mTypeEq
m
m0
)
eqn
:?
;
destruct
(
mTypeEq
m0
m1
)
eqn
:?
;
type_conv
;
try
rewrite
mTypeEq_refl
.
+
eapply
IHe1
;
eauto
.
+
destruct
(
morePrecise
m0
m1
);
congruence
.
+
destruct
(
morePrecise
m
m1
);
congruence
.
+
destruct
(
morePrecise
m
m0
);
congruence
.
Qed
.
Lemma
expCompare_antisym
e1
:
forall
e2
,
expCompare
e1
e2
=
CompOpp
(
expCompare
e2
e1
).
Proof
.
induction
e1
;
destruct
e2
;
simpl
;
try
auto
.
-
apply
Nat
.
compare_antisym
.
-
rewrite
mTypeEq_sym
.
destruct
(
mTypeEq
m0
m
)
eqn
:?
;
type_conv
;
try
congruence
;
try
rewrite
mTypeEq_refl
.
+
apply
V_orderedFacts
.
compare_antisym
.
+
destruct
(
morePrecise
m
m0
)
eqn
:?
;
destruct
(
morePrecise
m0
m
)
eqn
:?
;
try
(
split
;
auto
;
fail
).
*
pose
proof
(
morePrecise_antisym
_
_
Heqb0
Heqb1
);
type_conv
;
congruence
.
*
destruct
m
,
m0
;
unfold
morePrecise
in
*
;
cbv
;
congruence
.
-
rewrite
unopEq_sym
.
destruct
(
unopEq
u0
u
)
eqn
:?
;
try
rewrite
unopEq_compat_eq
in
*
;
subst
;
try
rewrite
unopEq_refl
,
IHe1
;
try
(
apply
IHe1
).
destruct
(
unopEq
u
Neg
)
eqn
:?
;
try
rewrite
unopEq_compat_eq
in
*
;
destruct
(
unopEq
u0
Neg
)
eqn
:?
;
try
rewrite
unopEq_compat_eq
in
*
;
subst
;
simpl
in
*
;
try
congruence
.
destruct
u
,
u0
;
simpl
in
*
;
congruence
.
-
destruct
b
,
b0
;
simpl
;
try
(
split
;
auto
;
fail
);
destruct
(
expCompare
e1_1
e2_1
)
eqn
:
first_comp
;
rewrite
IHe1_1
in
*
;
simpl
in
*
;
rewrite
CompOpp_iff
in
first_comp
;
rewrite
first_comp
;
simpl
;
try
auto
.
-
rewrite
mTypeEq_sym
.
destruct
(
mTypeEq
m0
m
)
eqn
:?
;
type_conv
;
try
auto
.
+
destruct
(
morePrecise
m
m0
)
eqn
:?
;
destruct
(
morePrecise
m0
m
)
eqn
:?
;
try
(
split
;
auto
;
fail
).
*
pose
proof
(
morePrecise_antisym
_
_
Heqb0
Heqb1
);
type_conv
;
congruence
.
*
destruct
m
,
m0
;
unfold
morePrecise
in
*
;
cbv
;
congruence
.
Qed
.
Lemma
expCompare_lt_eq_is_lt
e1
:
forall
e2
e3
,
expCompare
e1
e2
=
Lt
->
expCompare
e2
e3
=
Eq
->
expCompare
e1
e3
=
Lt
.
Proof
.
induction
e1
;
intros
*
compare_lt
compare_eq
;
destruct
e2
;
simpl
in
*
;
destruct
e3
;
try
congruence
.
-
rewrite
Nat
.
compare_eq_iff
in
compare_eq
;
subst
;
auto
.
-
destruct
(
mTypeEq
m
m0
)
eqn
:?
;
destruct
(
mTypeEq
m0
m1
)
eqn
:?
.
+
pose
proof
(
V_orderedFacts
.
compare_compat
).
unfold
Proper
in
H
.
apply
V_orderedFacts
.
compare_eq_iff
in
compare_eq
.
specialize
(
H
v
v
(
V_orderedFacts
.
eq_refl
v
)
v0
v1
compare_eq
).
type_conv
;
rewrite
mTypeEq_refl
,
<-
H
;
auto
.
+
rewrite
mTypeEq_compat_eq
in
Heqb
;
subst
.
rewrite
Heqb0
.
destruct
(
morePrecise
m0
m1
)
eqn
:?
;
congruence
.
+
rewrite
mTypeEq_compat_eq
in
Heqb0
;
subst
.
rewrite
Heqb
;
destruct
(
morePrecise
m
m1
)
eqn
:?
;
congruence
.
+
destruct
(
morePrecise
m0
m1
);
congruence
.
-
destruct
(
unopEq
u
u0
)
eqn
:?
;
destruct
(
unopEq
u0
u1
)
eqn
:?
;
try
rewrite
unopEq_compat_eq
in
*
;
subst
;
try
rewrite
unopEq_refl
;
try
auto
;
try
congruence
.
+
eapply
IHe1
;
eauto
.
+
destruct
(
unopEq
u0
Neg
);
congruence
.
+
destruct
(
unopEq
u
Neg
);
try
congruence
.
destruct
(
unopEq
u
u1
);
congruence
.
+
destruct
(
unopEq
u0
Neg
);
congruence
.
-
destruct
b
;
destruct
b0
;
try
congruence
;
destruct
b1
;
try
congruence
;
destruct
(
expCompare
e1_1
e2_1
)
eqn
:?
;
destruct
(
expCompare
e2_1
e3_1
)
eqn
:?
;
try
congruence
;
try
(
erewrite
IHe1_1
;
eauto
;
fail
""
);
try
erewrite
expCompare_eq_trans
;
eauto
.
-
destruct
(
mTypeEq
m
m0
)
eqn
:?
;
destruct
(
mTypeEq
m0
m1
)
eqn
:?
.
+
type_conv
;
subst
.
rewrite
mTypeEq_refl
.
eapply
IHe1
;
eauto
.
+
destruct
(
morePrecise
m0
m1
);
congruence
.
+
rewrite
mTypeEq_compat_eq
in
Heqb0
;
subst
.
rewrite
Heqb
.
destruct
(
morePrecise
m
m1
)
eqn
:?
;
congruence
.
+
destruct
(
morePrecise
m0
m1
);
congruence
.
Qed
.
Lemma
expCompare_eq_lt_is_lt
e1
:
forall
e2
e3
,
expCompare
e1
e2
=
Eq
->
expCompare
e2
e3
=
Lt
->
expCompare
e1
e3
=
Lt
.
Proof
.
induction
e1
;
intros
*
compare_eq
compare_lt
;
destruct
e2
;
simpl
in
*
;
destruct
e3
;
try
congruence
.
-
rewrite
Nat
.
compare_eq_iff
in
compare_eq
;
subst
;
auto
.
-
destruct
(
mTypeEq
m
m0
)
eqn
:?
;
destruct
(
mTypeEq
m0
m1
)
eqn
:?
.
+
pose
proof
(
V_orderedFacts
.
compare_compat
).
unfold
Proper
in
H
.
apply
V_orderedFacts
.
compare_eq_iff
in
compare_eq
.
specialize
(
H
v
v0
compare_eq
v1
v1
(
V_orderedFacts
.
eq_refl
v1
)).
type_conv
;
rewrite
mTypeEq_refl
,
H
;
auto
.
+
rewrite
mTypeEq_compat_eq
in
Heqb
;
subst
.
rewrite
Heqb0
.
destruct
(
morePrecise
m0
m1
)
eqn
:?
;
congruence
.
+
rewrite
mTypeEq_compat_eq
in
Heqb0
;
subst
.
rewrite
Heqb
;
destruct
(
morePrecise
m
m1
)
eqn
:?
;
congruence
.
+
destruct
(
morePrecise
m
m0
);
congruence
.
-
destruct
(
unopEq
u
u0
)
eqn
:?
;
destruct
(
unopEq
u0
u1
)
eqn
:?
;
try
rewrite
unopEq_compat_eq
in
*
;
subst
;
try
rewrite
unopEq_refl
;
try
auto
;
try
congruence
.
+
eapply
IHe1
;
eauto
.
+
rewrite
Heqb0
.
destruct
(
unopEq
u0
Neg
);
congruence
.
+
destruct
(
unopEq
u
Neg
);
congruence
.
+
destruct
(
unopEq
u
Neg
);
congruence
.
-
destruct
b
;
destruct
b0
;
destruct
b1
;
try
congruence
;
destruct
(
expCompare
e1_1
e2_1
)
eqn
:?
;
destruct
(
expCompare
e2_1
e3_1
)
eqn
:?
;
try
congruence
;
try
(
erewrite
IHe1_1
;
eauto
;
fail
""
);
try
erewrite
expCompare_eq_trans
;
eauto
.
-
destruct
(
mTypeEq
m
m0
)
eqn
:?
;
destruct
(
mTypeEq
m0
m1
)
eqn
:?
.
+
type_conv
;
subst
.
rewrite
mTypeEq_refl
.
eapply
IHe1
;
eauto
.
+
rewrite
mTypeEq_compat_eq
in
Heqb
;
subst
.
rewrite
Heqb0
.
destruct
(
morePrecise
m0
m1
);
congruence
.
+
rewrite
mTypeEq_compat_eq
in
Heqb0
;
subst
.
rewrite
Heqb
.
destruct
(
morePrecise
m
m1
)
eqn
:?
;
congruence
.
+
destruct
(
morePrecise
m
m0
);
congruence
.
Qed
.
Definition
eq
e1
e2
:=
expCompare
e1
e2
=
Eq
.
Definition
lt
(
e1
:
exp
V
)
(
e2
:
exp
V
)
:=
expCompare
e1
e2
=
Lt
.
Instance
lt_strorder
:
StrictOrder
lt
.
Proof
.
split
.
-
unfold
Irreflexive
.
unfold
Reflexive
.
intros
x
;
unfold
complement
.
intros
lt_x
.
induction
x
;
unfold
lt
in
*
;
simpl
in
lt_x
.
+
rewrite
PeanoNat
.
Nat
.
compare_refl
in
lt_x
.
congruence
.
+
rewrite
mTypeEq_refl
,
V_orderedFacts
.
compare_refl
in
*
;
congruence
.
+
rewrite
unopEq_refl
in
*
;
simpl
in
*
.
apply
IHx
;
auto
.
+
destruct
b
;
destruct
(
expCompare
x1
x1
)
eqn
:?
;
try
congruence
.
+
rewrite
mTypeEq_refl
in
lt_x
.
apply
IHx
;
auto
.
-
unfold
Transitive
.
intros
e1
.
unfold
lt
.
induction
e1
;
intros
*
lt_e1_e2
lt_e2_e3
;
simpl
in
*
;
destruct
y
;
destruct
z
;
simpl
in
*
;
try
auto
;
try
congruence
.
+
rewrite
<-
nat_compare_lt
in
*
.
omega
.
+
destruct
(
mTypeEq
m
m0
)
eqn
:?
;
destruct
(
mTypeEq
m0
m1
)
eqn
:?
.
*
type_conv
;
rewrite
mTypeEq_refl
,
V_orderedFacts
.
compare_lt_iff
in
*
;
eapply
V_orderedFacts
.
lt_trans
;
eauto
.
*
rewrite
mTypeEq_compat_eq
in
Heqb
;
subst
.
rewrite
Heqb0
.
assumption
.
*
rewrite
mTypeEq_compat_eq
in
Heqb0
;
subst
.
rewrite
Heqb
;
assumption
.
*
destruct
(
mTypeEq
m
m1
)
eqn
:?
.
{
rewrite
mTypeEq_compat_eq
in
Heqb1
;
subst
.
destruct
(
morePrecise
m0
m1
)
eqn
:?
;
destruct
(
morePrecise
m1
m0
)
eqn
:?
;
try
congruence
.
pose
proof
(
morePrecise_antisym
_
_
Heqb1
Heqb2
).
type_conv
;
congruence
.
}
{
destruct
(
morePrecise
m
m0
)
eqn
:?
;
destruct
(
morePrecise
m0
m1
)
eqn
:?
;
try
congruence
.
erewrite
morePrecise_trans
;
eauto
.
}
+
destruct
(
unopEq
u
u0
)
eqn
:?
;
destruct
(
unopEq
u0
u1
)
eqn
:?
;
try
rewrite
unopEq_compat_eq
in
*
;
subst
;
[
destruct
(
expCompare
e1
y
)
eqn
:?
;
try
congruence
;
rewrite
unopEq_refl
;
eapply
IHe1
;
eauto
|
destruct
(
unopEq
u0
Neg
)
eqn
:?
;
try
congruence
;
rewrite
unopEq_compat_eq
in
*
;
subst
|
|
].
*
rewrite
Heqb0
;
auto
.
*
destruct
(
unopEq
u
Neg
)
eqn
:?
;
try
congruence
;
rewrite
unopEq_compat_eq
in
*
;
subst
.
rewrite
Heqb
;
auto
.
*
destruct
(
unopEq
u
u1
)
eqn
:?
;
try
congruence
.
rewrite
unopEq_compat_eq
in
Heqb1
;
subst
.
destruct
(
unopEq
u1
Neg
)
eqn
:?
;
try
congruence
;
destruct
(
unopEq
u0
Neg
)
eqn
:?
;
try
congruence
;
rewrite
unopEq_compat_eq
in
*
;
subst
.
simpl
in
*
;
congruence
.
+
destruct
b
;
destruct
b0
;
destruct
b1
;
try
congruence
;
destruct
(
expCompare
e1_1
y1
)
eqn
:?
;
try
congruence
;
destruct
(
expCompare
y1
z1
)
eqn
:?
;
try
congruence
;
try
(
erewrite
expCompare_eq_trans
;
eauto
;
fail
);
try
(
erewrite
expCompare_eq_lt_is_lt
;
eauto
;
fail
);
try
(
erewrite
expCompare_lt_eq_is_lt
;
eauto
;
fail
);
try
(
erewrite
IHe1_1
;
eauto
).
+
destruct
(
mTypeEq
m
m0
)
eqn
:?
;
destruct
(
mTypeEq
m0
m1
)
eqn
:?
;
[
type_conv
;
subst
;
rewrite
mTypeEq_refl
|
|
|
].
*
eapply
IHe1
;
eauto
.
*
rewrite
mTypeEq_compat_eq
in
Heqb
;
subst
.
rewrite
Heqb0
;
destruct
(
morePrecise
m0
m1
);
congruence
.
*
rewrite
mTypeEq_compat_eq
in
Heqb0
;
subst
.
rewrite
Heqb
.
destruct
(
morePrecise
m
m1
);
congruence
.
*
destruct
(
mTypeEq
m
m1
)
eqn
:?
.
{
rewrite
mTypeEq_compat_eq
in
Heqb1
;
subst
.
destruct
(
morePrecise
m1
m0
)
eqn
:?
;
try
congruence
.
destruct
(
morePrecise
m0
m1
)
eqn
:?
;
try
congruence
.
pose
proof
(
morePrecise_antisym
_
_
Heqb1
Heqb2
).
type_conv
;
subst
.
congruence
.
}
{
destruct
(
morePrecise
m
m0
)
eqn
:?
;
try
congruence
.
destruct
(
morePrecise
m0
m1
)
eqn
:?
;
try
congruence
.
pose
proof
(
morePrecise_trans
_
_
_
Heqb2
Heqb3
).
rewrite
H
;
auto
.
}
Defined
.
Lemma
eq_compat
:
Proper
(
eq
==>
eq
==>
iff
)
eq
.
Proof
.
unfold
Proper
;
hnf
.
intros
e1
;
induction
e1
;
intros
e2
e1_eq_e2
;
hnf
;
intros
e3
e4
e3_eq_e4
;
unfold
lt
,
eq
in
*
;
destruct
e2
,
e3
,
e4
;
simpl
in
*
;
try
congruence
;
try
(
split
;
auto
;
fail
).
-
repeat
rewrite
Nat
.
compare_eq_iff
in
*
;
subst
.
split
;
try
auto
.
-
destruct
(
mTypeEq
m
m0
)
eqn
:?
;
destruct
(
mTypeEq
m1
m2
)
eqn
:?
;
[
type_conv
|
|
|
].
+
rewrite
V_orderedFacts
.
compare_eq_iff
in
*
.
rewrite
(
V_orderedFacts
.
compare_compat
e1_eq_e2
e3_eq_e4
).
split
;
auto
.
+
destruct
(
morePrecise
m1
m2
);
congruence
.
+
destruct
(
morePrecise
m
m0
);
congruence
.
+
destruct
(
morePrecise
m
m0
);
congruence
.
-
destruct
(
unopEq
u
u0
)
eqn
:?
;
destruct
(
unopEq
u1
u2
)
eqn
:?
;
try
rewrite
unopEq_compat_eq
in
*
;
subst
;
try
(
destruct
(
unopEq
u
Neg
);
congruence
);
try
(
destruct
(
unopEq
u1
Neg
);
congruence
).
specialize
(
IHe1
e2
e1_eq_e2
e3
e4
e3_eq_e4
).
simpl
in
*
.
destruct
(
unopEq
u0
u2
);
try
rewrite
IHe1
;
split
;
auto
.
-
destruct
b
;
destruct
b0
;
destruct
b1
;
destruct
b2
;
try
congruence
;
try
(
split
;
auto
;
fail
);
destruct
(
expCompare
e1_1
e2_1
)
eqn
:?
;
destruct
(
expCompare
e3_1
e4_1
)
eqn
:?
;
try
congruence
;
destruct
(
expCompare
e1_1
e3_1
)
eqn
:?
;
destruct
(
expCompare
e2_1
e4_1
)
eqn
:?
;
try
(
split
;
congruence
);
try
(
specialize
(
IHe1_2
_
e1_eq_e2
_
_
e3_eq_e4
);
simpl
in
*
;
rewrite
IHe1_2
in
*
;
split
;
auto
;
fail
);
try
(
split
;
try
congruence
;
intros
);
try
(
specialize
(
IHe1_1
_
Heqc
_
_
Heqc0
);
simpl
in
*
;
rewrite
IHe1_1
in
*
;
congruence
);
try
(
specialize
(
IHe1_1
_
Heqc
_
_
Heqc0
);
simpl
in
*
;
rewrite
<-
IHe1_1
in
*
;
congruence
).
-
destruct
(
mTypeEq
m
m0
)
eqn
:?
;
destruct
(
mTypeEq
m1
m2
)
eqn
:?
;
[
type_conv
|
|
|
].
+
specialize
(
IHe1
_
e1_eq_e2
_
_
e3_eq_e4
);
simpl
in
*
.
destruct
(
mTypeEq
m0
m2
);
try
congruence
.
split
;
auto
.
+
destruct
(
morePrecise
m1
m2
);
congruence
.
+
destruct
(
morePrecise
m
m0
);
congruence
.
+
destruct
(
morePrecise
m
m0
);
congruence
.
Qed
.
Instance
lt_compat
:
Proper
(
eq
==>
eq
==>
iff
)
lt
.
Proof
.
unfold
Proper
;
hnf
.
intros
e1
;
induction
e1
;
intros
e2
e1_eq_e2
;
hnf
;
intros
e3
e4
e3_eq_e4
;
unfold
lt
,
eq
in
*
;
destruct
e2
,
e3
,
e4
;
simpl
in
*
;
try
congruence
;
try
(
split
;
auto
;
fail
).
-
rewrite
Nat
.
compare_eq_iff
in
*
;
subst
.
split
;
try
auto
.
-
destruct
(
mTypeEq
m
m0
)
eqn
:?
;
destruct
(
mTypeEq
m1
m2
)
eqn
:?
;
[
type_conv
|
|
|
].
+
rewrite
V_orderedFacts
.
compare_eq_iff
in
*
.
rewrite
(
V_orderedFacts
.
compare_compat
e1_eq_e2
e3_eq_e4
).
split
;
auto
.
+
destruct
(
morePrecise
m1
m2
);
congruence
.
+
destruct
(
morePrecise
m
m0
);
congruence
.
+
destruct
(
morePrecise
m
m0
);
congruence
.
-
destruct
(
unopEq
u
u0
)
eqn
:?
;
destruct
(
unopEq
u1
u2
)
eqn
:?
;
try
rewrite
unopEq_compat_eq
in
*
;
subst
;
try
(
destruct
(
unopEq
u
Neg
);
congruence
);
try
(
destruct
(
unopEq
u1
Neg
);
congruence
).
specialize
(
IHe1
e2
e1_eq_e2
e3
e4
e3_eq_e4
).
simpl
in
*
.
destruct
(
unopEq
u0
u2
);
try
rewrite
IHe1
;
split
;
auto
.
-
pose
proof
eq_compat
as
eq_comp
.
unfold
Proper
,
eq
in
eq_comp
.
destruct
b
,
b0
,
b1
,
b2
;
try
congruence
;
try
(
split
;
auto
;
fail
);
destruct
(
expCompare
e1_1
e2_1
)
eqn
:?
;
destruct
(
expCompare
e3_1
e4_1
)
eqn
:?
;
try
congruence
;
destruct
(
expCompare
e1_1
e3_1
)
eqn
:?
;
destruct
(
expCompare
e2_1
e4_1
)
eqn
:?
;
try
(
split
;
congruence
);
try
(
specialize
(
IHe1_2
_
e1_eq_e2
_
_
e3_eq_e4
);
simpl
in
*
;
rewrite
IHe1_2
in
*
;
split
;
auto
;
fail
);
try
(
split
;
try
congruence
;
intros
);
try
(
specialize
(
IHe1_1
_
Heqc
_
_
Heqc0
);
simpl
in
*
;
rewrite
IHe1_1
in
*
;
congruence
);
try
(
specialize
(
IHe1_1
_
Heqc
_
_
Heqc0
);
simpl
in
*
;
rewrite
<-
IHe1_1
in
*
;
congruence
);
try
(
rewrite
(
eq_comp
_
_
Heqc
_
_
Heqc0
)
in
*
;
congruence
);
try
(
rewrite
<-
(
eq_comp
_
_
Heqc
_
_
Heqc0
)
in
*
;
congruence
).
-
destruct
(
mTypeEq
m
m0
)
eqn
:?
;
destruct
(
mTypeEq
m1
m2
)
eqn
:?
;
[
type_conv
|
|
|
].
+
specialize
(
IHe1
_
e1_eq_e2
_
_
e3_eq_e4
);
simpl
in
*
.
destruct
(
mTypeEq
m0
m2
);
try
congruence
.
split
;
auto
.
+
destruct
(
morePrecise
m1
m2
);
congruence
.
+
destruct
(
morePrecise
m
m0
);
congruence
.
+
destruct
(
morePrecise
m
m0
);
congruence
.
Defined
.
Lemma
compare_spec
:
forall
x
y
,
CompSpec
eq
lt
x
y
(
expCompare
x
y
).
Proof
.
intros
e1
e2
.
destruct
(
expCompare
e1
e2
)
eqn
:?
.
-
apply
CompEq
.
unfold
eq
;
auto
.
-
apply
CompLt
.
unfold
lt
;
auto
.
-
apply
CompGt
.
unfold
lt
.
rewrite
expCompare_antisym
in
Heqc
.
rewrite
CompOpp_iff
in
Heqc
.
simpl
in
*
;
auto
.
Qed
.
End
ExpOrderedType
.
(
*
MARKER
*
)
Fixpoint
toRExp
(
e
:
exp
Q
)
:=
match
e
with
|
Var
_
v
=>
Var
R
v
...
...
coq/Infra/Ltacs.v
View file @
2ba31c82
...
...
@@ -72,13 +72,19 @@ Ltac match_simpl :=
Ltac
destruct_if
:=
match
goal
with
|
[
H
:
(
if
?
c
then
?
a
else
?
b
)
=
_
|-
_
]
=>
|
[
H
:
if
?
c
then
?
a
else
?
b
=
_
|-
_
]
=>
case_eq
?
c
;
let
name
:=
fresh
"cond"
in
intros
name
;
rewrite
name
in
*
;
try
congruence
end
.
|
[
H
:
_
|-
if
?
c
then
?
a
else
?
b
=
_
]
=>
case_eq
?
c
;
let
name
:=
fresh
"cond"
in
intros
name
;
rewrite
name
in
*
;
try
congruence
end
.
(
*
HOL4
Style
patter
matching
tactics
*
)
Tactic
Notation
"lift "
tactic
(
t
)
:=
...
...
coq/Infra/MachineType.v
View file @
2ba31c82
...
...
@@ -92,12 +92,10 @@ Ltac type_conv :=
end
).
Lemma
mTypeEq_sym
(
m1
:
mType
)
(
m2
:
mType
)
:
forall
b
,
mTypeEq
m1
m2
=
b
->
mTypeEq
m2
m1
=
b
.
mTypeEq
m1
m2
=
mTypeEq
m2
m1
.
Proof
.
intros
.
destruct
b
;
[
rewrite
mTypeEq_compat_eq
in
*
|
rewrite
mTypeEq_compat_eq_false
in
*
];
auto
.
destruct
m1
,
m2
;
compute
;
auto
.
Qed
.
(
**
...
...
@@ -109,6 +107,39 @@ Qed.
Definition
isMorePrecise
(
m1
:
mType
)
(
m2
:
mType
)
:=
Qle_bool
(
mTypeToQ
m1
)
(
mTypeToQ
m2
).
Definition
morePrecise
(
m1
:
mType
)
(
m2
:
mType
)
:=
match
m1
,
m2
with
|
M0
,
_
=>
true
|
M16
,
M16
=>
true
|
M32
,
M32
=>
true
|
M32
,
M16
=>
true
|
M64
,
M0
=>
false
|
M64
,
_
=>
true
|
_
,
_
=>
false
end
.
Lemma
morePrecise_antisym
m1
m2
:
morePrecise
m1
m2
=
true
->
morePrecise
m2
m1
=
true
->
mTypeEq
m1
m2
=
true
.
Proof
.
destruct
m1
;
destruct
m2
;
cbv
;
auto
.
Qed
.
Lemma
morePrecise_trans
m1
m2
m3
:
morePrecise
m1
m2
=
true
->
morePrecise
m2
m3
=
true
->
morePrecise
m1
m3
=
true
.
Proof
.
destruct
m1
;
destruct
m2
;
destruct
m3
;
cbv
;
auto
.
Qed
.
Lemma
isMorePrecise_morePrecise
m1
m2
:
isMorePrecise
m1
m2
=
morePrecise
m1
m2
.
Proof
.
destruct
m1
eqn
:?
,
m2
eqn
:?
;
compute
;
auto
.
Qed
.
Lemma
isMorePrecise_refl
(
m
:
mType
)
:
isMorePrecise
m
m
=
true
.
Proof
.
...
...
@@ -136,7 +167,7 @@ Qed.
has
to
happen
in
64
bits
**
)
Definition
join
(
m1
:
mType
)
(
m2
:
mType
)
:=
if
(
isM
orePrecise
m1
m2
)
then
m1
else
m2
.
if
(
m
orePrecise
m1
m2
)
then
m1
else
m2
.
(
*
Lemma
M0_join_is_M0
m1
m2
:
*
)
(
*
join
m1
m2
=
M0
->
m1
=
M0
/
\
m2
=
M0
.
*
)
...
...
coq/Typing.v
View file @
2ba31c82
...
...
@@ -21,7 +21,7 @@ Fixpoint typeExpression (V:Type) (Gamma:nat -> option mType) (e:exp V) : option
|
_
=>
None
end
end
.
(
*
Fixpoint
typeMap
(
Gamma
:
nat
->
option
mType
)
(
e
:
exp
Q
)
(
e
'
:
exp
Q
)
:
option
mType
:=
match
e
with
|
Var
_
v
=>
if
expEq
e
e
'
then
Gamma
v
else
None
...
...
@@ -36,6 +36,46 @@ Fixpoint typeMap (Gamma:nat -> option mType) (e:exp Q) (e': exp Q) : option mTyp
|
None
,
None
=>
None
end
|
Downcast
m
e1
=>
if
expEq
e
e
'
then
typeExpression
Gamma
(
Downcast
m
e1
)
else
typeMap
Gamma
e1
e
'
end
.
*
)
Fixpoint
typeMap
(
Gamma
:
nat
->
option
mType
)
(
e
:
exp
Q
)
:
exp
Q
->
option
mType
:=
match
e
with
|
Var
_
v
=>
(
fun
e
'
=>
if
expEq
e
e
'
then
Gamma
v
else
None
)
|
Const
m
n
=>
(
fun
e
'
=>
if
expEq
e
e
'
then
Some
m
else
None
)
|
Unop
u
e1
=>
let
tMap
:=
typeMap
Gamma
e1
in
(
fun
e
'
=>
if
expEq
e
e
'
then
tMap
e1
else
tMap
e
'
)
|
Binop
b
e1
e2
=>
let
tMap1
:=
typeMap
Gamma
e1
in
let
tMap2
:=
typeMap
Gamma
e2
in
let
m1
:=
tMap1
e1
in
let
m2
:=
tMap2
e2
in
(
fun
e
'
=>
if
expEq
e
e
'
then