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
Joshua Yanovski
iris-coq
Commits
466f1be9
Commit
466f1be9
authored
Jan 12, 2016
by
Robbert Krebbers
Browse files
Set Obligation Tactic := idtac globally.
parent
f30c0242
Changes
9
Hide whitespace changes
Inline
Side-by-side
channel/heap_lang.v
View file @
466f1be9
...
...
@@ -405,7 +405,6 @@ End Tests.
(
**
Instantiate
the
Iris
language
interface
.
This
closes
reduction
under
evaluation
contexts
.
We
could
potentially
make
this
a
generic
construction
.
*
)
Section
Language
.
Local
Obligation
Tactic
:=
idtac
.
Definition
ectx_step
e1
σ
1
e2
σ
2
(
ef
:
option
expr
)
:=
exists
K
e1
'
e2
'
,
e1
=
fill
K
e1
'
/
\
e2
=
fill
K
e2
'
/
\
prim_step
e1
'
σ
1
e2
'
σ
2
ef
.
...
...
modures/cofe.v
View file @
466f1be9
Require
Export
prelude
.
prelude
.
Obligation
Tactic
:=
idtac
.
(
**
Unbundeled
version
*
)
Class
Dist
A
:=
dist
:
nat
→
relation
A
.
...
...
modures/fin_maps.v
View file @
466f1be9
Require
Export
modures
.
cmra
prelude
.
gmap
.
Require
Import
modures
.
option
.
Local
Obligation
Tactic
:=
idtac
.
Section
map
.
Context
`
{
Countable
K
}
.
...
...
prelude/base.v
View file @
466f1be9
...
...
@@ -8,6 +8,7 @@ Global Generalizable All Variables.
Global
Set
Automatic
Coercions
Import
.
Global
Set
Asymmetric
Patterns
.
Require
Export
Morphisms
RelationClasses
List
Bool
Utf8
Program
Setoid
.
Obligation
Tactic
:=
idtac
.
(
**
*
General
*
)
(
**
Zipping
lists
.
*
)
...
...
prelude/countable.v
View file @
466f1be9
(
*
Copyright
(
c
)
2012
-
2015
,
Robbert
Krebbers
.
*
)
(
*
This
file
is
distributed
under
the
terms
of
the
BSD
license
.
*
)
Require
Export
prelude
.
list
.
Local
Obligation
Tactic
:=
idtac
.
Local
Open
Scope
positive
.
Class
Countable
A
`
{
∀
x
y
:
A
,
Decision
(
x
=
y
)
}
:=
{
...
...
prelude/fin_collections.v
View file @
466f1be9
...
...
@@ -93,15 +93,15 @@ Proof.
Defined
.
Global
Program
Instance
collection_subseteq_dec_slow
(
X
Y
:
C
)
:
Decision
(
X
⊆
Y
)
|
100
:=
match
decide_rel
(
=
)
(
size
(
X
∖
Y
))
0
with
|
left
E1
=>
left
_
|
right
E1
=>
right
_
match
decide_rel
(
=
)
(
size
(
X
∖
Y
))
0
return
_
with
|
left
_
=>
left
_
|
right
_
=>
right
_
end
.
Next
Obligation
.
intros
x
Ex
;
apply
dec_stable
;
intro
.
destruct
(
proj1
(
elem_of_empty
x
)).
intros
X
Y
E1
x
?
;
apply
dec_stable
;
intro
.
destruct
(
proj1
(
elem_of_empty
x
)).
apply
(
size_empty_inv
_
E1
).
by
rewrite
elem_of_difference
.
Qed
.
Next
Obligation
.
intros
E2
.
destruct
E1
.
apply
size_empty_iff
,
equiv_empty
.
intros
x
.
intros
X
Y
E1
E2
;
destruct
E1
.
apply
size_empty_iff
,
equiv_empty
.
intros
x
.
rewrite
elem_of_difference
.
intros
[
E3
?
].
by
apply
E2
in
E3
.
Qed
.
Lemma
size_union_alt
X
Y
:
size
(
X
∪
Y
)
=
size
X
+
size
(
Y
∖
X
).
...
...
prelude/finite.v
View file @
466f1be9
(
*
Copyright
(
c
)
2012
-
2015
,
Robbert
Krebbers
.
*
)
(
*
This
file
is
distributed
under
the
terms
of
the
BSD
license
.
*
)
Require
Export
prelude
.
countable
prelude
.
list
.
Obligation
Tactic
:=
idtac
.
Class
Finite
A
`
{
∀
x
y
:
A
,
Decision
(
x
=
y
)
}
:=
{
enum
:
list
A
;
...
...
prelude/hashset.v
View file @
466f1be9
...
...
@@ -25,14 +25,14 @@ Next Obligation. by intros n X; simpl_map. Qed.
Program
Instance
hashset_singleton
:
Singleton
A
(
hashset
hash
)
:=
λ
x
,
Hashset
{
[
hash
x
↦
[
x
]
]
}
_.
Next
Obligation
.
intros
n
l
.
rewrite
lookup_singleton_Some
.
intros
[
<-
<-
].
intros
x
n
l
[
<-
<-
]
%
lookup_singleton_Some
.
rewrite
Forall_singleton
;
auto
using
NoDup_singleton
.
Qed
.
Program
Instance
hashset_union
:
Union
(
hashset
hash
)
:=
λ
m1
m2
,
let
(
m1
,
Hm1
)
:=
m1
in
let
(
m2
,
Hm2
)
:=
m2
in
Hashset
(
union_with
(
λ
l
k
,
Some
(
list_union
l
k
))
m1
m2
)
_.
Next
Obligation
.
intros
n
l
'
.
rewrite
lookup_union_with_Some
.
intros
_
_
m1
Hm1
m2
Hm2
n
l
'
;
rewrite
lookup_union_with_Some
.
intros
[[
??
]
|
[[
??
]
|
(
l
&
k
&?&?&?
)]];
simplify_equality
'
;
auto
.
split
;
[
apply
Forall_list_union
|
apply
NoDup_list_union
];
first
[
by
eapply
Hm1
;
eauto
|
by
eapply
Hm2
;
eauto
].
...
...
@@ -42,7 +42,7 @@ Program Instance hashset_intersection: Intersection (hashset hash) := λ m1 m2,
Hashset
(
intersection_with
(
λ
l
k
,
let
l
'
:=
list_intersection
l
k
in
guard
(
l
'
≠
[]);
Some
l
'
)
m1
m2
)
_.
Next
Obligation
.
intros
n
l
'
.
rewrite
lookup_intersection_with_Some
.
intros
_
_
m1
Hm1
m2
Hm2
n
l
'
.
rewrite
lookup_intersection_with_Some
.
intros
(
?&?&?&?&?
);
simplify_option_equality
.
split
;
[
apply
Forall_list_intersection
|
apply
NoDup_list_intersection
];
first
[
by
eapply
Hm1
;
eauto
|
by
eapply
Hm2
;
eauto
].
...
...
@@ -52,7 +52,7 @@ Program Instance hashset_difference: Difference (hashset hash) := λ m1 m2,
Hashset
(
difference_with
(
λ
l
k
,
let
l
'
:=
list_difference
l
k
in
guard
(
l
'
≠
[]);
Some
l
'
)
m1
m2
)
_.
Next
Obligation
.
intros
n
l
'
.
rewrite
lookup_difference_with_Some
.
intros
_
_
m1
Hm1
m2
Hm2
n
l
'
.
rewrite
lookup_difference_with_Some
.
intros
[[
??
]
|
(
?&?&?&?&?
)];
simplify_option_equality
;
auto
.
split
;
[
apply
Forall_list_difference
|
apply
NoDup_list_difference
];
first
[
by
eapply
Hm1
;
eauto
|
by
eapply
Hm2
;
eauto
].
...
...
prelude/numbers.v
View file @
466f1be9
...
...
@@ -189,17 +189,11 @@ Proof. by injection 1. Qed.
Instance
N_eq_dec
:
∀
x
y
:
N
,
Decision
(
x
=
y
)
:=
N
.
eq_dec
.
Program
Instance
N_le_dec
(
x
y
:
N
)
:
Decision
(
x
≤
y
)
%
N
:=
match
Ncompare
x
y
with
|
Gt
=>
right
_
|
_
=>
left
_
end
.
Next
Obligation
.
congruence
.
Qed
.
match
Ncompare
x
y
with
Gt
=>
right
_
|
_
=>
left
_
end
.
Solve
Obligations
with
naive_solver
.
Program
Instance
N_lt_dec
(
x
y
:
N
)
:
Decision
(
x
<
y
)
%
N
:=
match
Ncompare
x
y
with
|
Lt
=>
left
_
|
_
=>
right
_
end
.
Next
Obligation
.
congruence
.
Qed
.
match
Ncompare
x
y
with
Lt
=>
left
_
|
_
=>
right
_
end
.
Solve
Obligations
with
naive_solver
.
Instance
N_inhabited
:
Inhabited
N
:=
populate
1
%
N
.
Instance:
PartialOrder
(
≤
)
%
N
.
Proof
.
...
...
@@ -340,10 +334,12 @@ Arguments Qred _ : simpl never.
Instance
Qc_eq_dec
:
∀
x
y
:
Qc
,
Decision
(
x
=
y
)
:=
Qc_eq_dec
.
Program
Instance
Qc_le_dec
(
x
y
:
Qc
)
:
Decision
(
x
≤
y
)
:=
if
Qclt_le_dec
y
x
then
right
_
else
left
_.
Next
Obligation
.
by
apply
Qclt_not_le
.
Qed
.
Next
Obligation
.
intros
x
y
;
apply
Qclt_not_le
.
Qed
.
Next
Obligation
.
done
.
Qed
.
Program
Instance
Qc_lt_dec
(
x
y
:
Qc
)
:
Decision
(
x
<
y
)
:=
if
Qclt_le_dec
x
y
then
left
_
else
right
_.
Next
Obligation
.
by
apply
Qcle_not_lt
.
Qed
.
Solve
Obligations
with
done
.
Next
Obligation
.
intros
x
y
;
apply
Qcle_not_lt
.
Qed
.
Instance:
PartialOrder
(
≤
).
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