diff options
| author |  Jade Philipoom <jadep@google.com> | 2018-05-31 15:28:52 +0200 |
|---|---|---|
| committer | Jade Philipoom <jadep@google.com> | 2018-05-31 15:28:52 +0200 |
| commit | bca2349afb867fcd4b1d01099457d0945acaca16 (patch) | |
| tree | 9091da39009b063c76f8482e8c89ddca54ab92fe /src/Experiments/SimplyTypedArithmetic.v | |
| parent | 040719849e7e20402a99bf9540a0dd2810b06e09 (diff) | |
move around some Lets so that 8.8 doesn't error
Diffstat (limited to 'src/Experiments/SimplyTypedArithmetic.v')
| -rw-r--r-- | src/Experiments/SimplyTypedArithmetic.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v index 970c4223b..d8c16258d 100644 --- a/src/Experiments/SimplyTypedArithmetic.v +++ b/src/Experiments/SimplyTypedArithmetic.v @@ -8547,12 +8547,8 @@ Module PreFancy. Section with_wordmax. Context (log2wordmax : Z) (log2wordmax_pos : 1 < log2wordmax) (log2wordmax_even : log2wordmax mod 2 = 0). Let wordmax := 2 ^ log2wordmax. - Let half_bits := log2wordmax / 2. - Let wordmax_half_bits := 2 ^ half_bits. - Lemma wordmax_gt_2 : 2 < wordmax. Proof. - clear - wordmax log2wordmax log2wordmax_pos. subst wordmax. apply Z.le_lt_trans with (m:=2 ^ 1); [ reflexivity | ]. apply Z.pow_lt_mono_r; omega. Qed. @@ -8563,12 +8559,16 @@ Module PreFancy. subst wordmax. apply Z.mod_same_pow; omega. Qed. - Lemma wordmax_half_bits_pos : 0 < wordmax_half_bits. - Proof. subst wordmax_half_bits half_bits. Z.zero_bounds. Qed. - + Let half_bits := log2wordmax / 2. + Lemma half_bits_nonneg : 0 <= half_bits. Proof. subst half_bits; Z.zero_bounds. Qed. + Let wordmax_half_bits := 2 ^ half_bits. + + Lemma wordmax_half_bits_pos : 0 < wordmax_half_bits. + Proof. subst wordmax_half_bits half_bits. Z.zero_bounds. Qed. + Lemma half_bits_squared : (wordmax_half_bits - 1) * (wordmax_half_bits - 1) <= wordmax - 1. Proof. pose proof wordmax_half_bits_pos. |