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
Jonas Kastberg
iris
Commits
1c9e8581
Commit
1c9e8581
authored
Dec 19, 2016
by
Ralf Jung
Browse files
add decide_left, decide_right
parent
2e3a9be0
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/prelude/decidable.v
View file @
1c9e8581
...
...
@@ -36,6 +36,11 @@ Lemma decide_iff {A} P Q `{Decision P, Decision Q} (x y : A) :
(
P
↔
Q
)
→
(
if
decide
P
then
x
else
y
)
=
(
if
decide
Q
then
x
else
y
).
Proof
.
intros
[??].
destruct
(
decide
P
),
(
decide
Q
)
;
tauto
.
Qed
.
Lemma
decide_left
`
{
Decision
P
,
!
ProofIrrel
P
}
(
HP
:
P
)
:
decide
P
=
left
HP
.
Proof
.
destruct
(
decide
P
)
as
[?|?]
;
[|
contradiction
].
f_equal
.
apply
proof_irrel
.
Qed
.
Lemma
decide_right
`
{
Decision
P
}
`
{!
ProofIrrel
(
¬
P
)}
(
HP
:
¬
P
)
:
decide
P
=
right
HP
.
Proof
.
destruct
(
decide
P
)
as
[?|?]
;
[
contradiction
|].
f_equal
.
apply
proof_irrel
.
Qed
.
(** The tactic [destruct_decide] destructs a sumbool [dec]. If one of the
components is double negated, it will try to remove the double negation. *)
Tactic
Notation
"destruct_decide"
constr
(
dec
)
"as"
ident
(
H
)
:
=
...
...
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