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
c02e3a94
Commit
c02e3a94
authored
Jun 17, 2021
by
Andrew Hirsch
Browse files
Fixed a quick inconsistency in the RestrictedSemantics result.
parent
40b4a580
Changes
1
Hide whitespace changes
Inline
Side-by-side
RestrictedSemantics.v
View file @
c02e3a94
...
...
@@ -47,7 +47,7 @@ Module RestrictedSemantics (Import E : Expression) (Import TE : TypedExpression
RChorStep
(
RIfFF
l1
)
B
(
If
l1
ff
C1
C2
)
C2
|
DefLocalIStep
:
forall
R
l
C1
C1
'
C2
,
RChorStep
R
[]
C1
C1
'
->
RChorStep
R
[]
(
DefLocal
l
C1
C2
)
(
DefLocal
l
C1
'
C2
)
RChorStep
(
RArg
R
)
[]
(
DefLocal
l
C1
C2
)
(
DefLocal
l
C1
'
C2
)
|
DefLocalStep
:
forall
(
l
:
Loc
)
(
v
:
Expr
)
(
C2
:
Chor
),
ExprVal
v
->
RChorStep
(
RDefLocal
l
v
)
nil
(
DefLocal
l
(
Done
l
v
)
C2
)
(
C2
[
ce
|
ValueSubst
l
v
])
...
...
@@ -440,7 +440,7 @@ Module RestrictedSemantics (Import E : Expression) (Import TE : TypedExpression
intros
C1
C2
stdstep
;
induction
stdstep
.
all:
try
(
eexists
;
eexists
;
split
;
[
reflexivity
|
constructor
;
auto
];
fail
).
-
destruct
IHstdstep
as
[
R
[
C2
'
[
equiv
step
]]].
exists
R
;
exists
(
LetLocal
l
⟪
new
⟫
←
C2
'
fby
C2
);
split
;
auto
with
Chor
.
exists
(
RArg
R
)
;
exists
(
LetLocal
l
⟪
new
⟫
←
C2
'
fby
C2
);
split
;
auto
with
Chor
.
-
destruct
IHstdstep
as
[
R
[
C2
'
[
equiv
step
]]].
exists
(
RFun
R
);
exists
(
AppLocal
l
C2
'
e
);
split
;
auto
with
Chor
.
(
*
-
exists
(
RAppLocalE
l
e1
e2
);
exists
(
AppLocal
l
C
e2
);
split
;
auto
with
Chor
.
*
)
...
...
@@ -462,7 +462,7 @@ Module RestrictedSemantics (Import E : Expression) (Import TE : TypedExpression
|
IfTTOnTop
:
forall
p
C1
C2
,
RedexOnTop
(
RIfTT
p
)
(
If
p
tt
C1
C2
)
|
IfFFOnTop
:
forall
p
C1
C2
,
RedexOnTop
(
RIfFF
p
)
(
If
p
ff
C1
C2
)
|
SyncOnTop
:
forall
p
d
q
C
,
RedexOnTop
(
RSync
p
d
q
)
(
Sync
p
d
q
C
)
|
IDefLocalOntop
:
forall
l
C1
C2
R
,
RedexOnTop
R
C1
->
RedexOnTop
R
(
DefLocal
l
C1
C2
)
|
IDefLocalOntop
:
forall
l
C1
C2
R
,
RedexOnTop
R
C1
->
RedexOnTop
(
RArg
R
)
(
DefLocal
l
C1
C2
)
|
DefLocalOnTop
:
forall
l
e
C
,
RedexOnTop
(
RDefLocal
l
e
)
(
DefLocal
l
(
Done
l
e
)
C
)
|
AppLocalEOnTop
:
forall
l
e1
e2
C
,
RedexOnTop
(
RAppLocalE
l
e1
e2
)
(
AppLocal
l
C
e1
)
|
AppLocalOnTop
:
forall
l
C
e
,
RedexOnTop
(
RAppLocal
l
e
)
(
AppLocal
l
(
RecLocal
l
C
)
e
)
...
...
@@ -482,7 +482,6 @@ Module RestrictedSemantics (Import E : Expression) (Import TE : TypedExpression
assert
(
~
In
a
c
)
by
(
let
i
:=
fresh
in
intro
i
;
apply
H
;
right
;
exact
i
);
clear
H
end
.
Lemma
RStepOnTop
:
forall
(
R
:
Redex
)
(
B
:
list
Loc
)
(
C1
C2
:
Chor
),
RChorStep
R
B
C1
C2
->
...
...
@@ -601,6 +600,7 @@ Module RestrictedSemantics (Import E : Expression) (Import TE : TypedExpression
Theorem
LiftRestrictedChorStepToUnrestricted
:
forall
C1
C2
B
R
,
RChorStep
B
R
C1
C2
->
ChorStep
B
R
C1
C2
.
Proof
using
.
intros
C1
C2
B
R
step
;
induction
step
;
auto
with
Chor
.
Qed
.
Corollary
RestrictedRelativePreservation
:
...
...
Write
Preview
Supports
Markdown
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