Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Andrew Hirsch
Pirouette Coq Code
Commits
3e6274d4
Commit
3e6274d4
authored
Jun 18, 2021
by
Andrew Hirsch
Browse files
Local soundness for Tau steps.
parent
c02e3a94
Changes
1
Hide whitespace changes
Inline
Side-by-side
ChoreographyCompiler.v
View file @
3e6274d4
...
...
@@ -2079,287 +2079,274 @@ Module ChoreographyCompiler (Import E : Expression) (L : Locations) (LM : Locati
exists
El2
;
split
;
auto
.
Qed
.
(
*
Program
Definition
TauConExprRedexToRedex
(
R
:
ConExprRedex
)
(
pf
:
ConExprRedexToLabel
R
=
Tau
)
(
l
:
Loc
)
:
C
.
Redex
:=
*
)
(
*
match
R
with
*
)
(
*
|
RetE
e1
e2
=>
C
.
RDone
l
e1
e2
*
)
(
*
|
IfE
e1
e2
=>
C
.
RIfE
l
e1
e2
*
)
(
*
|
IfTT
=>
C
.
RIfTT
l
*
)
(
*
|
IfFF
=>
C
.
RIfFF
l
*
)
(
*
|
SendE
l
'
e1
e2
=>
C
.
RSendE
l
e1
e2
l
'
*
)
(
*
|
SendV
x
x0
=>
_
*
)
(
*
|
RecvV
x
x0
=>
_
*
)
(
*
|
ChooseRedex
x
x0
=>
_
*
)
(
*
|
AllowChoiceLRedex
x
=>
_
*
)
(
*
|
AllowChoiceRRedex
x
=>
_
*
)
(
*
|
LetRetRedex
x
=>
_
*
)
(
*
|
AppLocalE
e1
e2
=>
C
.
RAppLocalE
l
e1
e2
*
)
(
*
|
AppLocalRedex
x
=>
_
*
)
(
*
|
AppGlobalRedex
=>
_
*
)
(
*
end
.
*
)
Program
Fixpoint
TauConExprRedexToRedex
(
R
:
ConExprRedex
)
(
pf
:
ConExprRedexToLabel
R
=
Tau
)
(
l
:
Loc
)
:
C
.
Redex
:=
match
R
with
|
RetE
e1
e2
=>
C
.
RDone
l
e1
e2
|
IfE
e1
e2
=>
C
.
RIfE
l
e1
e2
|
IfTT
=>
C
.
RIfTT
l
|
IfFF
=>
C
.
RIfFF
l
|
SendE
l
'
e1
e2
=>
C
.
RSendE
l
e1
e2
l
'
|
SendV
x
x0
=>
_
|
RecvV
x
x0
=>
_
|
ChooseRedex
x
x0
=>
_
|
AllowChoiceLRedex
x
=>
_
|
AllowChoiceRRedex
x
=>
_
|
LetRetRedex
x
=>
_
|
AppLocalE
e1
e2
=>
C
.
RAppLocalE
l
e1
e2
|
AppLocalRedex
x
=>
_
|
AppGlobalRedex
=>
_
|
FunRedex
R
=>
C
.
RFun
(
TauConExprRedexToRedex
R
_
l
)
|
ArgRedex
R
=>
C
.
RArg
(
TauConExprRedexToRedex
R
_
l
)
end
.
(
*
Inductive
LocalCompleteAppliedIH
:
Loc
->
ConExpr
->
ConExprRedex
->
ConExpr
->
C
.
Chor
->
Prop
:=
*
)
(
*
|
LCAIH
:
forall
l
E1
R
E2
C
,
LocalCompleteAppliedIH
l
E1
R
E2
C
.
*
)
(
*
Ltac
ProjectChorDestructor
:=
*
)
(
*
repeat
match
goal
with
*
)
(
*
|
[
H
:
Some
_
=
Some
_
|-
_
]
=>
inversion
H
;
clear
H
;
subst
*
)
(
*
|
[
H
:
_
/
\
_
|-
_
]
=>
destruct
H
*
)
(
*
|
[
H
:
context
[
L
.
eq_dec
?
a
?
b
]
|-
_
]
=>
*
)
(
*
tryif
unify
a
b
*
)
(
*
then
let
n
:=
fresh
in
*
)
(
*
destruct
(
L
.
eq_dec
a
b
)
as
[
_
|
n
];
*
)
(
*
[
|
destruct
(
n
eq_refl
)]
*
)
(
*
else
lazymatch
goal
with
*
)
(
*
|
[
e
:
a
=
b
|-
_
]
=>
*
)
(
*
let
n
:=
fresh
in
*
)
(
*
destruct
(
L
.
eq_dec
a
b
)
as
[
_
|
n
];
*
)
(
*
[
|
destruct
(
n
e
)]
*
)
(
*
|
[
e
:
b
=
a
|-
_
]
=>
*
)
(
*
let
n
:=
fresh
in
*
)
(
*
destruct
(
L
.
eq_dec
a
b
)
as
[
_
|
n
];
*
)
(
*
[
|
destruct
(
n
(
eq_sym
e
))]
*
)
(
*
|
[
n
:
a
<>
b
|-
_
]
=>
*
)
(
*
let
e
:=
fresh
in
*
)
(
*
destruct
(
L
.
eq_dec
a
b
)
as
[
e
|
_
];
*
)
(
*
[
destruct
(
n
e
)
|
]
*
)
(
*
|
[
n
:
b
<>
a
|-
_
]
=>
*
)
(
*
let
e
:=
fresh
in
*
)
(
*
destruct
(
L
.
eq_dec
a
b
)
as
[
e
|
_
];
*
)
(
*
[
destruct
(
n
(
eq_sym
e
))
|
]
*
)
(
*
|
_
=>
let
eq
:=
fresh
"eq"
in
*
)
(
*
let
neq
:=
fresh
"neq"
in
*
)
(
*
destruct
(
L
.
eq_dec
a
b
)
as
[
eq
|
neq
];
subst
*
)
(
*
end
*
)
(
*
|
[
|-
context
[
L
.
eq_dec
?
a
?
b
]]
=>
*
)
(
*
tryif
unify
a
b
*
)
(
*
then
let
n
:=
fresh
in
*
)
(
*
destruct
(
L
.
eq_dec
a
b
)
as
[
_
|
n
];
*
)
(
*
[
|
destruct
(
n
eq_refl
)]
*
)
(
*
else
lazymatch
goal
with
*
)
(
*
|
[
e
:
a
=
b
|-
_
]
=>
*
)
(
*
let
n
:=
fresh
in
*
)
(
*
destruct
(
L
.
eq_dec
a
b
)
as
[
_
|
n
];
*
)
(
*
[
|
destruct
(
n
e
)]
*
)
(
*
|
[
e
:
b
=
a
|-
_
]
=>
*
)
(
*
let
n
:=
fresh
in
*
)
(
*
destruct
(
L
.
eq_dec
a
b
)
as
[
_
|
n
];
*
)
(
*
[
|
destruct
(
n
(
eq_sym
e
))]
*
)
(
*
|
[
n
:
a
<>
b
|-
_
]
=>
*
)
(
*
let
e
:=
fresh
in
*
)
(
*
destruct
(
L
.
eq_dec
a
b
)
as
[
e
|
_
];
*
)
(
*
[
destruct
(
n
e
)
|
]
*
)
(
*
|
[
n
:
b
<>
a
|-
_
]
=>
*
)
(
*
let
e
:=
fresh
in
*
)
(
*
destruct
(
L
.
eq_dec
a
b
)
as
[
e
|
_
];
*
)
(
*
[
destruct
(
n
(
eq_sym
e
))
|
]
*
)
(
*
|
_
=>
let
eq
:=
fresh
"eq"
in
*
)
(
*
let
neq
:=
fresh
"neq"
in
*
)
(
*
destruct
(
L
.
eq_dec
a
b
)
as
[
eq
|
neq
];
subst
*
)
(
*
end
*
)
(
*
|
[
H
:
context
[
ExprEqDec
?
a
?
b
]
|-
_
]
=>
*
)
(
*
tryif
unify
a
b
*
)
(
*
then
let
n
:=
fresh
in
*
)
(
*
destruct
(
ExprEqDec
a
b
)
as
[
_
|
n
];
*
)
(
*
[
|
destruct
(
n
eq_refl
)]
*
)
(
*
else
lazymatch
goal
with
*
)
(
*
|
[
e
:
a
=
b
|-
_
]
=>
*
)
(
*
let
n
:=
fresh
in
*
)
(
*
destruct
(
ExprEqDec
a
b
)
as
[
_
|
n
];
*
)
(
*
[
|
destruct
(
n
e
)]
*
)
(
*
|
[
e
:
b
=
a
|-
_
]
=>
*
)
(
*
let
n
:=
fresh
in
*
)
(
*
destruct
(
ExprEqDec
a
b
)
as
[
_
|
n
];
*
)
(
*
[
|
destruct
(
n
(
eq_sym
e
))]
*
)
(
*
|
[
n
:
a
<>
b
|-
_
]
=>
*
)
(
*
let
e
:=
fresh
in
*
)
(
*
destruct
(
ExprEqDec
a
b
)
as
[
e
|
_
];
*
)
(
*
[
destruct
(
n
e
)
|
]
*
)
(
*
|
[
n
:
b
<>
a
|-
_
]
=>
*
)
(
*
let
e
:=
fresh
in
*
)
(
*
destruct
(
ExprEqDec
a
b
)
as
[
e
|
_
];
*
)
(
*
[
destruct
(
n
(
eq_sym
e
))
|
]
*
)
(
*
|
_
=>
let
eq
:=
fresh
"eq"
in
*
)
(
*
let
neq
:=
fresh
"neq"
in
*
)
(
*
destruct
(
ExprEqDec
a
b
)
as
[
eq
|
neq
];
subst
*
)
(
*
end
*
)
(
*
|
[
|-
context
[
ExprEqDec
?
a
?
b
]]
=>
*
)
(
*
tryif
unify
a
b
*
)
(
*
then
let
n
:=
fresh
in
*
)
(
*
destruct
(
ExprEqDec
a
b
)
as
[
_
|
n
];
*
)
(
*
[
|
destruct
(
n
eq_refl
)]
*
)
(
*
else
lazymatch
goal
with
*
)
(
*
|
[
e
:
a
=
b
|-
_
]
=>
*
)
(
*
let
n
:=
fresh
in
*
)
(
*
destruct
(
ExprEqDec
a
b
)
as
[
_
|
n
];
*
)
(
*
[
|
destruct
(
n
e
)]
*
)
(
*
|
[
e
:
b
=
a
|-
_
]
=>
*
)
(
*
let
n
:=
fresh
in
*
)
(
*
destruct
(
ExprEqDec
a
b
)
as
[
_
|
n
];
*
)
(
*
[
|
destruct
(
n
(
eq_sym
e
))]
*
)
(
*
|
[
n
:
a
<>
b
|-
_
]
=>
*
)
(
*
let
e
:=
fresh
in
*
)
(
*
destruct
(
ExprEqDec
a
b
)
as
[
e
|
_
];
*
)
(
*
[
destruct
(
n
e
)
|
]
*
)
(
*
|
[
n
:
b
<>
a
|-
_
]
=>
*
)
(
*
let
e
:=
fresh
in
*
)
(
*
destruct
(
ExprEqDec
a
b
)
as
[
e
|
_
];
*
)
(
*
[
destruct
(
n
(
eq_sym
e
))
|
]
*
)
(
*
|
_
=>
let
eq
:=
fresh
"eq"
in
*
)
(
*
let
neq
:=
fresh
"neq"
in
*
)
(
*
destruct
(
ExprEqDec
a
b
)
as
[
eq
|
neq
];
subst
*
)
(
*
end
*
)
(
*
|
[
H
:
context
[
ProjectChor
?
C
?
l
]
|-
_
]
=>
*
)
(
*
lazymatch
type
of
H
with
*
)
(
*
|
ProjectChor
C
l
=
_
=>
fail
*
)
(
*
|
_
=>
*
)
(
*
lazymatch
goal
with
*
)
(
*
|
[
eq
:
ProjectChor
C
l
=
_
|-
_
]
=>
rewrite
eq
in
H
*
)
(
*
|
_
=>
let
eq
:=
fresh
"eq"
in
destruct
(
ProjectChor
C
l
)
eqn
:
eq
*
)
(
*
end
*
)
(
*
end
*
)
(
*
|
[
|-
context
[
ProjectChor
?
C
?
l
]
]
=>
*
)
(
*
lazymatch
goal
with
*
)
(
*
|
[
eq
:
ProjectChor
C
l
=
_
|-
_
]
=>
rewrite
eq
*
)
(
*
|
_
=>
let
eq
:=
fresh
"eq"
in
destruct
(
ProjectChor
C
l
)
eqn
:
eq
*
)
(
*
end
*
)
(
*
|
[
d
:
C
.
LRChoice
|-
_
]
=>
destruct
d
*
)
(
*
|
[
H
:
ConExprMergeRel
?
a
?
b
?
c
|-
context
[
ConExprMerge
?
a
?
b
]]
=>
*
)
(
*
rewrite
(
ConExprMergeRelSpec1
_
_
_
H
)
*
)
(
*
|
[
H
:
ConExprMergeRel
?
a
?
b
?
c
|-
context
[
ConExprMerge
?
b
?
a
]]
=>
*
)
(
*
rewrite
MergeComm
;
rewrite
(
ConExprMergeRelSpec1
_
_
_
H
)
*
)
Inductive
LocalCompleteAppliedIH
:
Loc
->
ConExpr
->
ConExprRedex
->
ConExpr
->
C
.
Chor
->
Prop
:=
|
LCAIH
:
forall
l
E1
R
E2
C
,
LocalCompleteAppliedIH
l
E1
R
E2
C
.
Ltac
ProjectChorDestructor
:=
repeat
match
goal
with
|
[
H
:
Some
_
=
Some
_
|-
_
]
=>
inversion
H
;
clear
H
;
subst
|
[
H
:
_
/
\
_
|-
_
]
=>
destruct
H
|
[
H
:
context
[
L
.
eq_dec
?
a
?
b
]
|-
_
]
=>
tryif
unify
a
b
then
let
n
:=
fresh
in
destruct
(
L
.
eq_dec
a
b
)
as
[
_
|
n
];
[
|
destruct
(
n
eq_refl
)]
else
lazymatch
goal
with
|
[
e
:
a
=
b
|-
_
]
=>
let
n
:=
fresh
in
destruct
(
L
.
eq_dec
a
b
)
as
[
_
|
n
];
[
|
destruct
(
n
e
)]
|
[
e
:
b
=
a
|-
_
]
=>
let
n
:=
fresh
in
destruct
(
L
.
eq_dec
a
b
)
as
[
_
|
n
];
[
|
destruct
(
n
(
eq_sym
e
))]
|
[
n
:
a
<>
b
|-
_
]
=>
let
e
:=
fresh
in
destruct
(
L
.
eq_dec
a
b
)
as
[
e
|
_
];
[
destruct
(
n
e
)
|
]
|
[
n
:
b
<>
a
|-
_
]
=>
let
e
:=
fresh
in
destruct
(
L
.
eq_dec
a
b
)
as
[
e
|
_
];
[
destruct
(
n
(
eq_sym
e
))
|
]
|
_
=>
let
eq
:=
fresh
"eq"
in
let
neq
:=
fresh
"neq"
in
destruct
(
L
.
eq_dec
a
b
)
as
[
eq
|
neq
];
subst
end
|
[
|-
context
[
L
.
eq_dec
?
a
?
b
]]
=>
tryif
unify
a
b
then
let
n
:=
fresh
in
destruct
(
L
.
eq_dec
a
b
)
as
[
_
|
n
];
[
|
destruct
(
n
eq_refl
)]
else
lazymatch
goal
with
|
[
e
:
a
=
b
|-
_
]
=>
let
n
:=
fresh
in
destruct
(
L
.
eq_dec
a
b
)
as
[
_
|
n
];
[
|
destruct
(
n
e
)]
|
[
e
:
b
=
a
|-
_
]
=>
let
n
:=
fresh
in
destruct
(
L
.
eq_dec
a
b
)
as
[
_
|
n
];
[
|
destruct
(
n
(
eq_sym
e
))]
|
[
n
:
a
<>
b
|-
_
]
=>
let
e
:=
fresh
in
destruct
(
L
.
eq_dec
a
b
)
as
[
e
|
_
];
[
destruct
(
n
e
)
|
]
|
[
n
:
b
<>
a
|-
_
]
=>
let
e
:=
fresh
in
destruct
(
L
.
eq_dec
a
b
)
as
[
e
|
_
];
[
destruct
(
n
(
eq_sym
e
))
|
]
|
_
=>
let
eq
:=
fresh
"eq"
in
let
neq
:=
fresh
"neq"
in
destruct
(
L
.
eq_dec
a
b
)
as
[
eq
|
neq
];
subst
end
|
[
H
:
context
[
ExprEqDec
?
a
?
b
]
|-
_
]
=>
tryif
unify
a
b
then
let
n
:=
fresh
in
destruct
(
ExprEqDec
a
b
)
as
[
_
|
n
];
[
|
destruct
(
n
eq_refl
)]
else
lazymatch
goal
with
|
[
e
:
a
=
b
|-
_
]
=>
let
n
:=
fresh
in
destruct
(
ExprEqDec
a
b
)
as
[
_
|
n
];
[
|
destruct
(
n
e
)]
|
[
e
:
b
=
a
|-
_
]
=>
let
n
:=
fresh
in
destruct
(
ExprEqDec
a
b
)
as
[
_
|
n
];
[
|
destruct
(
n
(
eq_sym
e
))]
|
[
n
:
a
<>
b
|-
_
]
=>
let
e
:=
fresh
in
destruct
(
ExprEqDec
a
b
)
as
[
e
|
_
];
[
destruct
(
n
e
)
|
]
|
[
n
:
b
<>
a
|-
_
]
=>
let
e
:=
fresh
in
destruct
(
ExprEqDec
a
b
)
as
[
e
|
_
];
[
destruct
(
n
(
eq_sym
e
))
|
]
|
_
=>
let
eq
:=
fresh
"eq"
in
let
neq
:=
fresh
"neq"
in
destruct
(
ExprEqDec
a
b
)
as
[
eq
|
neq
];
subst
end
|
[
|-
context
[
ExprEqDec
?
a
?
b
]]
=>
tryif
unify
a
b
then
let
n
:=
fresh
in
destruct
(
ExprEqDec
a
b
)
as
[
_
|
n
];
[
|
destruct
(
n
eq_refl
)]
else
lazymatch
goal
with
|
[
e
:
a
=
b
|-
_
]
=>
let
n
:=
fresh
in
destruct
(
ExprEqDec
a
b
)
as
[
_
|
n
];
[
|
destruct
(
n
e
)]
|
[
e
:
b
=
a
|-
_
]
=>
let
n
:=
fresh
in
destruct
(
ExprEqDec
a
b
)
as
[
_
|
n
];
[
|
destruct
(
n
(
eq_sym
e
))]
|
[
n
:
a
<>
b
|-
_
]
=>
let
e
:=
fresh
in
destruct
(
ExprEqDec
a
b
)
as
[
e
|
_
];
[
destruct
(
n
e
)
|
]
|
[
n
:
b
<>
a
|-
_
]
=>
let
e
:=
fresh
in
destruct
(
ExprEqDec
a
b
)
as
[
e
|
_
];
[
destruct
(
n
(
eq_sym
e
))
|
]
|
_
=>
let
eq
:=
fresh
"eq"
in
let
neq
:=
fresh
"neq"
in
destruct
(
ExprEqDec
a
b
)
as
[
eq
|
neq
];
subst
end
|
[
H
:
context
[
ProjectChor
?
C
?
l
]
|-
_
]
=>
lazymatch
type
of
H
with
|
ProjectChor
C
l
=
_
=>
fail
|
_
=>
lazymatch
goal
with
|
[
eq
:
ProjectChor
C
l
=
_
|-
_
]
=>
rewrite
eq
in
H
|
_
=>
let
eq
:=
fresh
"eq"
in
destruct
(
ProjectChor
C
l
)
eqn
:
eq
end
end
|
[
|-
context
[
ProjectChor
?
C
?
l
]
]
=>
lazymatch
goal
with
|
[
eq
:
ProjectChor
C
l
=
_
|-
_
]
=>
rewrite
eq
|
_
=>
let
eq
:=
fresh
"eq"
in
destruct
(
ProjectChor
C
l
)
eqn
:
eq
end
|
[
d
:
C
.
LRChoice
|-
_
]
=>
destruct
d
|
[
H
:
ConExprMergeRel
?
a
?
b
?
c
|-
context
[
ConExprMerge
?
a
?
b
]]
=>
rewrite
(
ConExprMergeRelSpec1
_
_
_
H
)
|
[
H
:
ConExprMergeRel
?
a
?
b
?
c
|-
context
[
ConExprMerge
?
b
?
a
]]
=>
rewrite
MergeComm
;
rewrite
(
ConExprMergeRelSpec1
_
_
_
H
)
(
*
end
.
*
)
end
.
(
*
Lemma
ProjectLetRetInversion
:
forall
C
l
E1
E2
,
ProjectChor
C
l
=
Some
(
LetRet
E1
E2
)
->
*
)
(
*
exists
C1
C2
,
ProjectChor
C1
l
=
Some
E1
/
\
*
)
(
*
ProjectChor
C2
l
=
Some
E2
.
*
)
(
*
Proof
using
.
*
)
(
*
intro
C
;
C
.
ChorInduction
C
;
intros
p
E1
E2
eq
;
cbn
in
eq
;
ProjectChorDestructor
;
*
)
(
*
try
discriminate
.
*
)
(
*
all
:
try
(
apply
IHC
;
auto
;
fail
).
*
)
(
*
-
apply
ConExprMergeRelSpec2
in
eq
;
inversion
eq
;
subst
.
*
)
(
*
apply
IHC1
in
eq0
.
apply
IHC2
in
eq1
.
*
)
(
*
destruct
eq0
as
[
C11
[
C12
[
proj11
proj12
]]];
destruct
eq1
as
[
C21
[
C22
[
proj21
proj22
]]].
*
)
(
*
apply
ConExprMergeRelSpec1
in
H3
;
apply
ConExprMergeRelSpec1
in
H4
.
*
)
(
*
exists
(
C
.
If
l
e
C11
C21
);
exists
(
C
.
If
l
e
C12
C22
);
split
;
cbn
;
ProjectChorDestructor
;
auto
.
*
)
(
*
-
exists
C1
;
exists
C2
;
split
;
auto
.
*
)
(
*
Qed
.
*
)
Lemma
ProjectLetRetInversion
:
forall
C
l
E1
E2
,
ProjectChor
C
l
=
Some
(
LetRet
E1
E2
)
->
exists
C1
C2
,
ProjectChor
C1
l
=
Some
E1
/
\
ProjectChor
C2
l
=
Some
E2
.
Proof
using
.
intro
C
;
C
.
ChorInduction
C
;
intros
p
E1
E2
eq
;
cbn
in
eq
;
ProjectChorDestructor
;
try
discriminate
.
all:
try
(
apply
IHC
;
auto
;
fail
).
-
apply
ConExprMergeRelSpec2
in
eq
;
inversion
eq
;
subst
.
apply
IHC1
in
eq0
.
apply
IHC2
in
eq1
.
destruct
eq0
as
[
C11
[
C12
[
proj11
proj12
]]];
destruct
eq1
as
[
C21
[
C22
[
proj21
proj22
]]].
apply
ConExprMergeRelSpec1
in
H3
;
apply
ConExprMergeRelSpec1
in
H4
.
exists
(
C
.
If
l
e
C11
C21
);
exists
(
C
.
If
l
e
C12
C22
);
split
;
cbn
;
ProjectChorDestructor
;
auto
.
-
exists
C1
;
exists
C2
;
split
;
auto
.
Qed
.
(
*
Lemma
LocalTauSoundness
'
:
forall
C1
p
E1
R
E2
(
pf
:
ConExprRedexToLabel
R
=
Tau
),
*
)
(
*
ConExprStep
'
E1
R
E2
->
*
)
(
*
ProjectChor
C1
p
=
Some
E1
->
*
)
(
*
C
.
InANF
C1
->
*
)
(
*
exists
C2
,
ProjectChor
C2
p
=
Some
E2
/
\
*
)
(
*
forall
B
,
~
In
p
B
->
C
.
ChorStep
(
TauConExprRedexToRedex
R
pf
p
)
B
C1
C2
.
*
)
(
*
Proof
using
.
*
)
(
*
intro
C1
;
C
.
ChorInduction
C1
;
cbn
;
intros
p
E1
R
E2
pf
step
eq
anf_C
;
*
)
(
*
destruct
R
;
cbn
in
pf
;
try
discriminate
;
cbn
;
clear
pf
.
*
)
(
*
all
:
ProjectChorDestructor
;
try
discriminate
;
inversion
step
;
subst
;
cbn
.
*
)
(
*
all
:
try
(
eexists
;
split
;
intros
;
eauto
with
Chor
;
cbn
;
*
)
(
*
ProjectChorDestructor
;
auto
;
fail
).
*
)
(
*
all
:
repeat
match
goal
with
*
)
(
*
|
[
eq
:
ConExprMerge
?
a
?
b
=
Some
?
c
|-
_
]
=>
*
)
(
*
tryif
let
H
:=
fresh
""
c
in
idtac
*
)
(
*
then
fail
*
)
(
*
else
lazymatch
goal
with
*
)
(
*
|
[
_
:
ConExprMergeRel
a
b
c
|-
_
]
=>
fail
*
)
(
*
|
_
=>
let
H
:=
fresh
"merge"
in
*
)
(
*
pose
proof
(
ConExprMergeRelSpec2
_
_
_
eq
)
as
H
;
*
)
(
*
inversion
H
;
subst
*
)
(
*
end
*
)
(
*
|
[
IH
:
forall
p
E1
R
E2
(
pf
:
ConExprRedexToLabel
R
=
Tau
),
*
)
(
*
ConExprStep
'
E1
R
E2
->
*
)
(
*
ProjectChor
?
C1
p
=
Some
E1
->
*
)
(
*
C
.
InANF
?
C1
->
*
)
(
*
exists
C2
,
ProjectChor
C2
p
=
Some
E2
/
\
*
)
(
*
(
forall
B
,
~
In
p
B
->
C
.
ChorStep
(
TauConExprRedexToRedex
R
pf
p
)
B
?
C1
C2
),
*
)
(
*
step
:
ConExprStep
'
?
E1
?
R
?
E2
,
*
)
(
*
eq
:
ProjectChor
?
C1
?
p
=
Some
?
E1
,
anf
:
C
.
InANF
?
C1
|-
_
]
=>
*
)
(
*
lazymatch
goal
with
*
)
(
*
|
[
_
:
LocalCompleteAppliedIH
p
E1
R
E2
C1
|-
_
]
=>
fail
*
)
(
*
|
_
=>
*
)
(
*
let
lcaih
:=
fresh
"lcaih"
in
*
)
(
*
let
C2
:=
fresh
"C"
in
*
)
(
*
let
step
'
:=
fresh
"step"
in
*
)
(
*
let
eq
'
:=
fresh
"eq"
in
*
)
(
*
pose
proof
(
LCAIH
p
E1
R
E2
C1
)
as
lcaih
;
*
)
(
*
destruct
(
IH
p
E1
R
E2
ltac
:
(
cbn
;
auto
)
step
eq
anf
)
as
[
C2
[
eq
'
step
'
]];
*
)
(
*
cbn
in
step
'
*
)
(
*
end
*
)
(
*
|
[
H
:
ConExprMergeRel
?
E1
?
E2
?
E3
,
*
)
(
*
H
'
:
ConExprStep
'
?
E3
?
R
?
E4
|-
_
]
=>
*
)
(
*
lazymatch
goal
with
*
)
(
*
|
[
_
:
ConExprStep
'
E1
_
_
|-
_
]
=>
fail
*
)
(
*
|
_
=>
*
)
(
*
let
E1
'
:=
fresh
"E"
in
*
)
(
*
let
E2
'
:=
fresh
"E"
in
*
)
(
*
let
merge
:=
fresh
"merge"
in
*
)
(
*
let
step1
:=
fresh
"step"
in
*
)
(
*
let
step2
:=
fresh
"step"
in
*
)
(
*
destruct
(
UnmergeRelTauStep
'
E1
E2
E3
_
E4
H
'
ltac
:
(
cbn
;
auto
)
H
)
*
)
(
*
as
[
E1
'
[
E2
'
[
merge
[
step1
step2
]]]]
*
)
(
*
end
*
)
(
*
end
.
*
)
(
*
all
:
try
(
eexists
;
split
;
[
|
intros
;
eauto
with
Chor
;
econstructor
;
eauto
with
Chor
;
*
)
(
*
repeat
match
goal
with
*
)
(
*
|
[
neq
:
?
p
<>
?
l
,
ni
:
~
In
?
p
?
B
|-
context
[
?
l
::
?
B
]]
=>
*
)
(
*
lazymatch
goal
with
*
)
(
*
|
[
_
:
~
In
p
(
l
::
B
)
|-
_
]
=>
fail
*
)
(
*
|
_
=>
*
)
(
*
let
i
:=
fresh
in
*
)
(
*
let
eq
:=
fresh
in
*
)
(
*
assert
(
~
In
p
(
l
::
B
))
*
)
(
*
by
(
intro
i
;
destruct
i
as
[
eq
|
i
];
*
)
(
*
[
destruct
(
neq
(
eq_sym
eq
))
|
destruct
(
ni
i
)])
*
)
(
*
end
*
)
(
*
|
[
step
:
forall
B
,
~
In
?
p
B
->
C
.
ChorStep
?
R
B
?
C1
?
C2
,
*
)
(
*
ni
:
~
In
?
p
?
B
|-
_
]
=>
*
)
(
*
lazymatch
goal
with
*
)
(
*
|
[
_
:
C
.
ChorStep
R
B
C1
C2
|-
_
]
=>
fail
*
)
(
*
|
_
=>
pose
proof
(
step
B
ni
)
*
)
(
*
end
*
)
(
*
end
;
auto
];
repeat
(
cbn
;
ProjectChorDestructor
;
eauto
);
fail
);
*
)
(
*
try
match
goal
with
*
)
(
*
|
[
H
:
ConExprStep
'
(
RecGlobal
_
)
_
_
|-
_
]
=>
inversion
H
*
)
(
*
|
[
H
:
ConExprStep
'
Unit
_
_
|-
_
]
=>
inversion
H
*
)
(
*
end
.
*
)
(
*
-
exists
(
C
.
AppLocal
p
C1
e1
);
split
;
cbn
;
ProjectChorDestructor
;
eauto
with
ConExpr
.
*
)
(
*
destruct
C1
;
cbn
in
*
;
ProjectChorDestructor
;
try
discriminate
;
*
)
(
*
try
match
goal
with
*
)
(
*
|
[
H
:
C
.
FunctionOK
?
C
|-
_
]
=>
inversion
H
;
fail
*
)
(
*
end
.
*
)
(
*
intros
B
ni
;
auto
with
Chor
.
*
)
(
*
-
exists
(
C
.
AppGlobal
C0
C
);
split
;
cbn
;
ProjectChorDestructor
;
eauto
with
ConExpr
.
*
)
(
*
destruct
C0
;
cbn
in
*
;
ProjectChorDestructor
;
try
discriminate
;
*
)
(
*
try
match
goal
with
*
)
(
*
|
[
H
:
C
.
FunctionOK
?
C
|-
_
]
=>
inversion
H
;
fail
*
)
(
*
end
.
*
)
(
*
admit
.
intros
B
ni
;
auto
with
Chor
.
*
)
(
*
-
admit
.
*
)
(
*
-
admit
.
*
)
(
*
-
admit
.
*
)
(
*
-
admit
.
*
)
(
*
-
admit
.
*
)
(
*
Admitted
.
*
)
(
*
Theorem
LocalTauSoundness
:
forall
C1
p
E1
E2
,
*
)
(
*
ProjectChor
C1
p
=
Some
E1
->
*
)
(
*
ConExprStep
E1
Tau
E2
->
*
)
(
*
exists
R
C2
,
ProjectRedex
R
p
=
Some
Tau
/
\
*
)
(
*
ProjectChor
C2
p
=
Some
E2
/
\
*
)
(
*
C
.
ChorStep
R
[]
C1
C2
.
*
)
(
*
Proof
using
.
*
)
(
*
intros
C1
p
E1
E2
H
H0
.
*
)
(
*
destruct
(
ConExprStepToPrime
H0
)
as
[
R
[
pf
step
]];
clear
H0
.
*
)
(
*
destruct
(
LocalTauSoundness
'
C1
p
E1
R
E2
pf
step
H
)
as
[
C2
[
eq2
step
'
]].
*
)
(
*
exists
(
TauConExprRedexToRedex
R
pf
p
);
exists
C2
;
split
;
[
|
split
];
auto
.
*
)
(
*
-
destruct
R
;
cbn
in
*
;
ProjectChorDestructor
;
auto
;
discriminate
.
*
)
(
*
Qed
.
*
)
Lemma
LocalTauSoundness
'
:
forall
C1
p
E1
R
E2
(
pf
:
ConExprRedexToLabel
R
=
Tau
),
ConExprStep
'
E1
R
E2
->
ProjectChor
C1
p
=
Some
E1
->
exists
C2
,
ProjectChor
C2
p
=
Some
E2
/
\
forall
B
,
~
In
p
B
->
C
.
ChorStep
(
TauConExprRedexToRedex
R
pf
p
)
B
C1
C2
.
Proof
using
.
intro
C1
;
C
.
ChorInduction
C1
;
cbn
;
intros
p
E1
R
E2
pf
step
eq
;
destruct
R
;
cbn
in
pf
;
try
discriminate
;
cbn
;
try
clear
pf
.
all:
ProjectChorDestructor
;
try
discriminate
;
inversion
step
;
subst
;
cbn
.
all:
try
(
eexists
;
split
;
intros
;
eauto
with
Chor
;
cbn
;
ProjectChorDestructor
;
auto
;
fail
).
all:
repeat
match
goal
with
|
[
eq
:
ConExprMerge
?
a
?
b
=
Some
?
c
|-
_
]
=>
tryif
let
H
:=
fresh
""
c
in
idtac
then
fail
else
lazymatch
goal
with
|
[
_
:
ConExprMergeRel
a
b
c
|-
_
]
=>
fail
|
_
=>
let
H
:=
fresh
"merge"
in
pose
proof
(
ConExprMergeRelSpec2
_
_
_
eq
)
as
H
;
inversion
H
;
subst
end
|
[
IH
:
forall
p
E1
R
E2
(
pf
:
ConExprRedexToLabel
R
=
Tau
),
ConExprStep
'
E1
R
E2
->
ProjectChor
?
C1
p
=
Some
E1
->
exists
C2
,
ProjectChor
C2
p
=
Some
E2
/
\
(
forall
B
,
~
In
p
B
->
C
.
ChorStep
(
TauConExprRedexToRedex
R
pf
p
)
B
?
C1
C2
),
step
:
ConExprStep
'
?
E1
?
R
?
E2
,
eq
:
ProjectChor
?
C1
?
p
=
Some
?
E1
|-
_
]
=>
lazymatch
goal
with
|
[
_
:
LocalCompleteAppliedIH
p
E1
R
E2
C1
|-
_
]
=>
fail
|
_
=>
let
lcaih
:=
fresh
"lcaih"
in
let
C2
:=
fresh
"C"
in
let
step
'
:=
fresh
"step"
in
let
eq
'
:=
fresh
"eq"
in
pose
proof
(
LCAIH
p
E1
R
E2
C1
)
as
lcaih
;
destruct
(
IH
p
E1
R
E2
ltac
:
(
cbn
;
auto
)
step
eq
)
as
[
C2
[
eq
'
step
'
]];
cbn
in
step
'
end
|
[
H
:
ConExprMergeRel
?
E1
?
E2
?
E3
,
H
'
:
ConExprStep
'
?
E3
?
R
?
E4
|-
_
]
=>
lazymatch
goal
with
|
[
_
:
ConExprStep
'
E1
_
_
|-
_
]
=>
fail
|
_
=>
let
E1
'
:=
fresh
"E"
in
let
E2
'
:=
fresh
"E"
in
let
merge
:=
fresh
"merge"
in
let
step1
:=
fresh
"step"
in
let
step2
:=
fresh
"step"
in
destruct
(
UnmergeRelTauStep
'
E1
E2
E3
_
E4
H
'
ltac
:
(
cbn
;
auto
)
H
)
as
[
E1
'
[
E2
'
[
merge
[
step1
step2
]]]]
end
end
.
all:
try
(
eexists
;
split
;
[
|
intros
;
eauto
with
Chor
;
econstructor
;
eauto
with
Chor
;
repeat
match
goal
with
|
[
neq
:
?
p
<>
?
l
,
ni
:
~
In
?
p
?
B
|-
context
[
?
l
::
?
B
]]
=>
lazymatch
goal
with
|
[
_
:
~
In
p
(
l
::
B
)
|-
_
]
=>
fail
|
_
=>
let
i
:=
fresh
in
let
eq
:=
fresh
in
assert
(
~
In
p
(
l
::
B
))
by
(
intro
i
;
destruct
i
as
[
eq
|
i
];
[
destruct
(
neq
(
eq_sym
eq
))
|
destruct
(
ni
i
)])
end
|
[
step
:
forall
B
,
~
In
?
p
B
->
C
.
ChorStep
?
R
B
?
C1
?
C2
,
ni
:
~
In
?
p
?
B
|-
_
]
=>
lazymatch
goal
with
|
[
_
:
C
.
ChorStep
R
B
C1
C2
|-
_
]
=>
fail
|
_
=>
pose
proof
(
step
B
ni
)
end
end
;
auto
];
repeat
(
cbn
;
ProjectChorDestructor
;
eauto
);
fail
);
try
match
goal
with
