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
Janno
iris-coq
Commits
2f1ae293
Commit
2f1ae293
authored
Jun 20, 2018
by
Ralf Jung
Browse files
use lia instead of omega
parent
700677ca
Changes
9
Hide whitespace changes
Inline
Side-by-side
theories/algebra/cofe_solver.v
View file @
2f1ae293
...
...
@@ -93,7 +93,7 @@ Proof using Fcontr. intros. by rewrite -(fg (X (S (S k)))) -(g_tower X). Qed.
Lemma
ff_tower
k
i
(
X
:
tower
)
:
ff
i
(
X
(
S
k
))
≡
{
k
}
≡
X
(
i
+
S
k
).
Proof
using
Fcontr
.
intros
;
induction
i
as
[|
i
IH
]
;
simpl
;
[
done
|].
by
rewrite
IH
Nat
.
add_succ_r
(
dist_le
_
_
_
_
(
f_tower
_
X
))
;
last
omeg
a
.
by
rewrite
IH
Nat
.
add_succ_r
(
dist_le
_
_
_
_
(
f_tower
_
X
))
;
last
li
a
.
Qed
.
Lemma
gg_tower
k
i
(
X
:
tower
)
:
gg
i
(
X
(
i
+
k
))
≡
X
k
.
Proof
.
by
induction
i
as
[|
i
IH
]
;
simpl
;
[
done
|
rewrite
g_tower
IH
].
Qed
.
...
...
theories/algebra/gmultiset.v
View file @
2f1ae293
...
...
@@ -74,7 +74,7 @@ Section gmultiset.
rewrite
local_update_unital_discrete
=>
Z'
_
/
leibniz_equiv_iff
->.
split
.
done
.
rewrite
!
gmultiset_op_union
=>
x
.
repeat
(
rewrite
multiplicity_difference
||
rewrite
multiplicity_union
).
omeg
a
.
li
a
.
Qed
.
End
gmultiset
.
...
...
theories/algebra/list.v
View file @
2f1ae293
...
...
@@ -68,11 +68,11 @@ Global Program Instance list_cofe `{Cofe A} : Cofe listC :=
Next
Obligation
.
intros
?
n
c
;
rewrite
/
compl
/
list_compl
.
destruct
(
c
0
)
as
[|
x
l
]
eqn
:
Hc0
at
1
.
{
by
destruct
(
chain_cauchy
c
0
n
)
;
auto
with
omeg
a
.
}
rewrite
-(
λ
H
,
length_ne
_
_
_
(
chain_cauchy
c
0
n
H
))
;
last
omeg
a
.
{
by
destruct
(
chain_cauchy
c
0
n
)
;
auto
with
li
a
.
}
rewrite
-(
λ
H
,
length_ne
_
_
_
(
chain_cauchy
c
0
n
H
))
;
last
li
a
.
apply
Forall2_lookup
=>
i
.
rewrite
-
dist_option_Forall2
list_lookup_fmap
.
destruct
(
decide
(
i
<
length
(
c
n
)))
;
last
first
.
{
rewrite
lookup_seq_ge
?lookup_ge_None_2
;
auto
with
omeg
a
.
}
{
rewrite
lookup_seq_ge
?lookup_ge_None_2
;
auto
with
li
a
.
}
rewrite
lookup_seq
//=
(
conv_compl
n
(
list_chain
c
_
_
))
/=.
destruct
(
lookup_lt_is_Some_2
(
c
n
)
i
)
as
[?
Hcn
]
;
first
done
.
by
rewrite
Hcn
.
...
...
@@ -310,7 +310,7 @@ Section properties.
Lemma
list_lookup_singletonM_ne
i
j
x
:
i
≠
j
→
({[
i
:
=
x
]}
:
list
A
)
!!
j
=
None
∨
({[
i
:
=
x
]}
:
list
A
)
!!
j
=
Some
ε
.
Proof
.
revert
j
;
induction
i
;
intros
[|
j
]
;
naive_solver
auto
with
omeg
a
.
Qed
.
Proof
.
revert
j
;
induction
i
;
intros
[|
j
]
;
naive_solver
auto
with
li
a
.
Qed
.
Lemma
list_singletonM_validN
n
i
x
:
✓
{
n
}
({[
i
:
=
x
]}
:
list
A
)
↔
✓
{
n
}
x
.
Proof
.
rewrite
list_lookup_validN
.
split
.
...
...
theories/algebra/local_updates.v
View file @
2f1ae293
...
...
@@ -179,7 +179,7 @@ Proof.
move
=>
Hex
.
apply
local_update_unital
=>
n
z
/=
Hy
Heq
.
split
;
first
done
.
destruct
z
as
[
z
|]
;
last
done
.
exfalso
.
move
:
Hy
.
rewrite
Heq
/=
-
Some_op
=>
Hy
.
eapply
Hex
.
eapply
cmra_validN_le
.
eapply
Hy
.
omeg
a
.
eapply
cmra_validN_le
.
eapply
Hy
.
li
a
.
Qed
.
(** * Natural numbers *)
...
...
theories/algebra/ofe.v
View file @
2f1ae293
...
...
@@ -178,7 +178,7 @@ Section ofe.
Lemma
conv_compl'
`
{
Cofe
A
}
n
(
c
:
chain
A
)
:
compl
c
≡
{
n
}
≡
c
(
S
n
).
Proof
.
transitivity
(
c
n
)
;
first
by
apply
conv_compl
.
symmetry
.
apply
chain_cauchy
.
omeg
a
.
apply
chain_cauchy
.
li
a
.
Qed
.
Lemma
discrete_iff
n
(
x
:
A
)
`
{!
Discrete
x
}
y
:
x
≡
y
↔
x
≡
{
n
}
≡
y
.
...
...
@@ -292,9 +292,9 @@ Program Definition fixpoint_chain {A : ofeT} `{Inhabited A} (f : A → A)
`
{!
Contractive
f
}
:
chain
A
:
=
{|
chain_car
i
:
=
Nat
.
iter
(
S
i
)
f
inhabitant
|}.
Next
Obligation
.
intros
A
?
f
?
n
.
induction
n
as
[|
n
IH
]=>
-[|
i
]
//=
?
;
try
omeg
a
.
induction
n
as
[|
n
IH
]=>
-[|
i
]
//=
?
;
try
li
a
.
-
apply
(
contractive_0
f
).
-
apply
(
contractive_S
f
),
IH
;
auto
with
omeg
a
.
-
apply
(
contractive_S
f
),
IH
;
auto
with
li
a
.
Qed
.
Program
Definition
fixpoint_def
`
{
Cofe
A
,
Inhabited
A
}
(
f
:
A
→
A
)
...
...
@@ -341,7 +341,7 @@ Section fixpoint.
intros
?
[
x
Hx
]
Hincr
Hlim
.
set
(
chcar
i
:
=
Nat
.
iter
(
S
i
)
f
x
).
assert
(
Hcauch
:
∀
n
i
:
nat
,
n
≤
i
→
chcar
i
≡
{
n
}
≡
chcar
n
).
{
intros
n
.
rewrite
/
chcar
.
induction
n
as
[|
n
IH
]=>
-[|
i
]
//=
;
eauto
using
contractive_0
,
contractive_S
with
omeg
a
.
}
eauto
using
contractive_0
,
contractive_S
with
li
a
.
}
set
(
fp2
:
=
compl
{|
chain_cauchy
:
=
Hcauch
|}).
assert
(
f
fp2
≡
fp2
).
{
apply
equiv_dist
=>
n
.
rewrite
/
fp2
(
conv_compl
n
)
/=
/
chcar
.
...
...
@@ -856,7 +856,7 @@ Section discrete_ofe.
{
compl
c
:
=
c
0
}.
Next
Obligation
.
intros
n
c
.
rewrite
/
compl
/=
;
symmetry
;
apply
(
chain_cauchy
c
0
n
).
omeg
a
.
symmetry
;
apply
(
chain_cauchy
c
0
n
).
li
a
.
Qed
.
End
discrete_ofe
.
...
...
theories/base_logic/double_negation.v
View file @
2f1ae293
...
...
@@ -90,7 +90,7 @@ Proof.
*
rewrite
comm
-
assoc
.
done
.
*
rewrite
comm
-
assoc
.
done
.
*
exists
y'
.
split
=>//.
by
exists
x'
.
-
intros
;
assert
(
n'
<
a
).
omeg
a
.
-
intros
;
assert
(
n'
<
a
).
li
a
.
move
:
laterN_small
.
uPred
.
unseal
.
naive_solver
.
Qed
.
...
...
@@ -178,22 +178,22 @@ Lemma nnupd_nnupd_k_dist k P: (|=n=> P)%I ≡{k}≡ (|=n=>_k P)%I.
case
(
decide
(
k'
<
n
)).
**
move
:
laterN_small
;
uPred
.
unseal
;
naive_solver
.
**
intros
.
exfalso
.
eapply
HnnP
;
eauto
.
assert
(
n
≤
k'
).
omeg
a
.
assert
(
n
≤
k'
).
li
a
.
intros
n''
x''
???.
specialize
(
HPF
n''
x''
).
exfalso
.
eapply
laterN_big
;
last
(
unseal
;
eauto
).
eauto
.
omeg
a
.
eauto
.
li
a
.
*
inversion
Hle
;
simpl
;
subst
.
**
unseal
.
intros
(
HnnP
&
HnnP_IH
)
n
k'
x'
??
HPF
.
case
(
decide
(
k'
<
n
)).
***
move
:
laterN_small
;
uPred
.
unseal
;
naive_solver
.
***
intros
.
exfalso
.
assert
(
n
≤
k'
).
omeg
a
.
assert
(
n
=
S
k
∨
n
<
S
k
)
as
[->|]
by
omeg
a
.
***
intros
.
exfalso
.
assert
(
n
≤
k'
).
li
a
.
assert
(
n
=
S
k
∨
n
<
S
k
)
as
[->|]
by
li
a
.
****
eapply
laterN_big
;
eauto
;
unseal
.
eapply
HnnP
;
eauto
.
move
:
HPF
;
by
unseal
.
****
move
:
nnupd_k_elim
.
unseal
.
intros
Hnnupdk
.
eapply
laterN_big
;
eauto
.
unseal
.
eapply
(
Hnnupdk
n
k
)
;
first
omeg
a
;
eauto
.
eapply
(
Hnnupdk
n
k
)
;
first
li
a
;
eauto
.
exists
x
,
x'
.
split_and
!
;
eauto
.
eapply
uPred_mono
;
eauto
.
**
intros
HP
.
eapply
IHk
;
auto
.
move
:
HP
.
unseal
.
intros
(?&?)
;
naive_solver
.
...
...
@@ -265,7 +265,7 @@ Proof.
exfalso
.
eapply
laterN_big
;
last
(
uPred
.
unseal
;
eapply
(
Hwand
n'
x'
))
;
eauto
.
*
rewrite
comm
.
done
.
*
rewrite
comm
.
done
.
-
intros
;
assert
(
n'
<
a
).
omeg
a
.
-
intros
;
assert
(
n'
<
a
).
li
a
.
move
:
laterN_small
.
uPred
.
unseal
.
naive_solver
.
Qed
.
...
...
@@ -286,7 +286,7 @@ Proof using Type*.
red
;
rewrite
//=
=>
n'
x'
???.
case
(
decide
(
n'
=
k
))
;
intros
.
-
subst
.
exfalso
.
eapply
Hfal
.
rewrite
(
comm
op
)
;
eauto
.
-
assert
(
n'
<
k
).
omeg
a
.
-
assert
(
n'
<
k
).
li
a
.
move
:
laterN_small
.
uPred
.
unseal
.
naive_solver
.
Qed
.
End
classical
.
...
...
@@ -306,7 +306,7 @@ Proof.
split
.
unseal
.
intros
n'
??
Hupd
.
case
(
decide
(
n'
<
n
)).
-
intros
.
move
:
laterN_small
.
unseal
.
naive_solver
.
-
intros
.
assert
(
n
≤
n'
).
omeg
a
.
-
intros
.
assert
(
n
≤
n'
).
li
a
.
exfalso
.
specialize
(
Hupd
n'
ε
).
eapply
Hdne
.
intros
Hfal
.
eapply
laterN_big
;
eauto
.
...
...
@@ -326,14 +326,14 @@ Proof.
specialize
(
Hf3
(
S
k
)
(
S
k
)
ε
).
rewrite
right_id
in
Hf3
*.
unseal
.
intros
Hf3
.
eapply
Hf3
;
eauto
.
intros
???
Hx'
.
rewrite
left_id
in
Hx'
*=>
Hx'
.
assert
(
n'
<
S
k
∨
n'
=
S
k
)
as
[|]
by
omeg
a
.
assert
(
n'
<
S
k
∨
n'
=
S
k
)
as
[|]
by
li
a
.
*
intros
.
move
:
(
laterN_small
n'
(
S
k
)
x'
False
).
rewrite
//=.
unseal
.
intros
Hsmall
.
eapply
Hsmall
;
eauto
.
*
subst
.
intros
.
exfalso
.
eapply
Hf2
.
exists
x'
.
split
;
eauto
using
cmra_validN_S
.
-
intros
k
P
x
Hx
.
rewrite
?Nat_iter_S_r
.
replace
(
S
(
S
n
)
+
k
)
with
(
S
n
+
(
S
k
))
by
omeg
a
.
replace
(
S
n
+
k
)
with
(
n
+
(
S
k
))
by
omeg
a
.
intros
.
eapply
IHn
.
replace
(
S
n
+
S
k
)
with
(
S
(
S
n
)
+
k
)
by
omeg
a
.
eauto
.
replace
(
S
(
S
n
)
+
k
)
with
(
S
n
+
(
S
k
))
by
li
a
.
replace
(
S
n
+
k
)
with
(
n
+
(
S
k
))
by
li
a
.
intros
.
eapply
IHn
.
replace
(
S
n
+
S
k
)
with
(
S
(
S
n
)
+
k
)
by
li
a
.
eauto
.
rewrite
?Nat_iter_S_r
.
eauto
.
Qed
.
...
...
@@ -356,7 +356,7 @@ Proof.
destruct
n
.
-
rewrite
//=
;
unseal
;
auto
.
-
intros
???
Hfal
.
eapply
(
adequacy_helper2
_
n
1
)
;
(
replace
(
S
n
+
1
)
with
(
S
(
S
n
))
by
omeg
a
)
;
eauto
.
eapply
(
adequacy_helper2
_
n
1
)
;
(
replace
(
S
n
+
1
)
with
(
S
(
S
n
))
by
li
a
)
;
eauto
.
unseal
.
intros
(
x'
&?&
Hphi
).
simpl
in
*.
eapply
Hfal
.
auto
.
Qed
.
...
...
theories/base_logic/upred.v
View file @
2f1ae293
...
...
@@ -5,7 +5,7 @@ From Coq.Init Require Import Nat.
Set
Default
Proof
Using
"Type"
.
Local
Hint
Extern
1
(
_
≼
_
)
=>
etrans
;
[
eassumption
|].
Local
Hint
Extern
1
(
_
≼
_
)
=>
etrans
;
[|
eassumption
].
Local
Hint
Extern
10
(
_
≤
_
)
=>
omeg
a
.
Local
Hint
Extern
10
(
_
≤
_
)
=>
li
a
.
(** The basic definition of the uPred type, its metric and functor laws.
You probably do not want to import this file. Instead, import
...
...
@@ -466,7 +466,7 @@ Qed.
Lemma
later_contractive
:
Contractive
(@
uPred_later
M
).
Proof
.
unseal
;
intros
[|
n
]
P
Q
HPQ
;
split
=>
-[|
n'
]
x
??
//=
;
try
omeg
a
.
unseal
;
intros
[|
n
]
P
Q
HPQ
;
split
=>
-[|
n'
]
x
??
//=
;
try
li
a
.
apply
HPQ
;
eauto
using
cmra_validN_S
.
Qed
.
...
...
theories/heap_lang/lib/counter.v
View file @
2f1ae293
...
...
@@ -130,7 +130,7 @@ Section contrib_spec.
wp_bind
(
CAS
_
_
_
).
iInv
N
as
(
c'
)
">[Hγ Hl]"
.
destruct
(
decide
(
c'
=
c
))
as
[->|].
-
iMod
(
own_update_2
with
"Hγ Hγf"
)
as
"[Hγ Hγf]"
.
{
apply
frac_auth_update
,
(
nat_local_update
_
_
(
S
c
)
(
S
n
))
;
omeg
a
.
}
{
apply
frac_auth_update
,
(
nat_local_update
_
_
(
S
c
)
(
S
n
))
;
li
a
.
}
wp_cas_suc
.
iModIntro
.
iSplitL
"Hl Hγ"
.
{
iNext
.
iExists
(
S
c
).
rewrite
Nat2Z
.
inj_succ
Z
.
add_1_l
.
by
iFrame
.
}
wp_if
.
by
iApply
"HΦ"
.
...
...
theories/program_logic/weakestpre.v
View file @
2f1ae293
...
...
@@ -58,7 +58,7 @@ Proof.
(* FIXME: reflexivity, as being called many times by f_equiv and f_contractive
is very slow here *)
do
18
(
f_contractive
||
f_equiv
).
apply
IH
;
first
lia
.
intros
v
.
eapply
dist_le
;
eauto
with
omeg
a
.
intros
v
.
eapply
dist_le
;
eauto
with
li
a
.
Qed
.
Global
Instance
wp_proper
s
E
e
:
Proper
(
pointwise_relation
_
(
≡
)
==>
(
≡
))
(
wp
(
PROP
:
=
iProp
Σ
)
s
E
e
).
...
...
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