Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
FP
Stacked Borrows Coq
Commits
63dfd1ef
Commit
63dfd1ef
authored
Jul 07, 2019
by
Ralf Jung
Browse files
ex1: better names
parent
40ee246b
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/opt/ex1.v
View file @
63dfd1ef
...
...
@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
(
**
Moving
read
of
mutable
reference
up
across
code
not
using
that
ref
.
*
)
(
*
Assuming
x
:
&
mut
i32
*
)
Definition
ex1
:
function
:=
Definition
ex1
_unopt
:
function
:=
fun:
[
"i"
],
let:
"x"
:=
new_place
(
&
mut
int
)
"i"
in
(
*
put
argument
into
place
*
)
Retag
"x"
Default
;;
...
...
@@ -28,7 +28,7 @@ Definition ex1_opt : function :=
Lemma
ex1_sim_body
fs
ft
:
sim_local_funs_lookup
fs
ft
→
⊨ᶠ
{
fs
,
ft
}
ex1
≥
ex1_opt
.
⊨ᶠ
{
fs
,
ft
}
ex1
_unopt
≥
ex1_opt
.
Proof
.
intros
Hfst
.
apply
(
sim_fun_simple1
10
)
=>
// rarg es css et cs args argt AREL ??.
...
...
@@ -59,10 +59,10 @@ Proof.
Admitted
.
Lemma
ex1
_sim
(
prog
:
fn_env
)
:
Lemma
ex1
(
prog
:
fn_env
)
:
stuck_decidable
→
has_main
prog
→
let
prog_src
:=
<
[
"ex1"
:=
ex1
]
>
prog
in
let
prog_src
:=
<
[
"ex1"
:=
ex1
_unopt
]
>
prog
in
let
prog_tgt
:=
<
[
"ex1"
:=
ex1_opt
]
>
prog
in
behave_prog
prog_tgt
<
1
=
behave_prog
prog_src
.
Proof
.
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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