blob: 8588836eeb1d4263974577abf2461c1b427dc331 (
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
|
Require Import Coq.ZArith.ZArith.
Require Import Crypto.LegacyArithmetic.Interface.
Require Import Crypto.LegacyArithmetic.Double.Core.
Require Import Crypto.LegacyArithmetic.Double.Proofs.Decode.
Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
Require Import Crypto.Util.ZUtil.LandLorShiftBounds.
Require Import Crypto.Util.Tactics.BreakMatch.
Local Open Scope Z_scope.
Section bitwise_or.
Context {n W}
{decode : decoder n W}
{is_decode : is_decode decode}
{or : bitwise_or W}
{is_or : is_bitwise_or or}.
Global Instance is_bitwise_or_double
: is_bitwise_or or_double.
Proof using Type*.
constructor; intros x y.
destruct n as [|p|].
{ rewrite !(tuple_decoder_n_O (W:=W) 2); easy. }
{ assert (0 <= Z.lor (decode (fst x)) (decode (fst y)) < 2^Z.pos p) by auto with zarith.
rewrite (tuple_decoder_2 x), (tuple_decoder_2 y), (tuple_decoder_2 (or_double x y))
by apply Zle_0_pos.
push_decode.
apply Z.bits_inj'; intros; autorewrite with Ztestbit.
break_match; Z.ltb_to_lt; autorewrite with Ztestbit; reflexivity. }
{ rewrite !(tuple_decoder_n_neg (W:=W) 2); easy. }
Qed.
End bitwise_or.
|
