blob: 0f29e837ec77a7ad1321a924ef4b1783ab284a41 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
|
Require Import Coqlib.
Require Import Integers.
Require Import Values.
Require Import Floats.
Definition bitwise_select_int b vtrue vfalse :=
Val.or (Val.and (Val.neg b) vtrue)
(Val.and (Val.sub b Vone) vfalse).
Lemma bitwise_select_int_true :
forall vtrue vfalse,
bitwise_select_int (Val.of_optbool (Some true)) (Vint vtrue) (Vint vfalse)
= Vint vtrue.
Proof.
intros. cbn. f_equal.
change (Int.neg Int.one) with Int.mone.
rewrite Int.and_commut.
rewrite Int.and_mone.
rewrite Int.sub_idem.
rewrite Int.and_commut.
rewrite Int.and_zero.
apply Int.or_zero.
Qed.
Lemma bitwise_select_int_false :
forall vtrue vfalse,
bitwise_select_int (Val.of_optbool (Some false)) (Vint vtrue) (Vint vfalse)
= Vint vfalse.
Proof.
intros. cbn. f_equal.
rewrite Int.neg_zero.
rewrite Int.and_commut.
rewrite Int.and_zero.
rewrite Int.sub_zero_r.
change (Int.neg Int.one) with Int.mone.
rewrite Int.and_commut.
rewrite Int.and_mone.
rewrite Int.or_commut.
apply Int.or_zero.
Qed.
|
